Giter Site home page Giter Site logo

Comments (4)

Gabriella439 avatar Gabriella439 commented on August 12, 2024

Good point. I should pick a different type for the first exercise until the tutorial explains Natural numbers

from dhall-haskell.

Gabriella439 avatar Gabriella439 commented on August 12, 2024

Also, to answer your question: yes you do need the + prefix for Natural numbers. They are a distinct type from Integers. See: https://hackage.haskell.org/package/dhall-1.0.1/docs/Dhall-Tutorial.html#g:14

from dhall-haskell.

echatav avatar echatav commented on August 12, 2024

It does lead to some confusing errors for newbies.

#:global-project hephaestus$ echo "1 + 1" | dhall

Use "dhall --explain" for detailed errors

Error: ❰+❱ only works on Naturals

1 + 1

(stdin):1:1

#:global-project hephaestus$ echo "1+1" | dhall

Use "dhall --explain" for detailed errors

Error: Not a function

1+1

(stdin):1:1

#:global-project hephaestus$ echo "+1++1" | dhall

Use "dhall --explain" for detailed errors

Error: ❰++❱ only works on Text

+1++1

(stdin):1:1
#:global-project hephaestus$ echo "+1+ +1" | dhall
Natural

+2

Not sure what would be better. I'd say to require + or - for Integers instead of Naturals but what do you do with 0?

from dhall-haskell.

Gabriella439 avatar Gabriella439 commented on August 12, 2024

@echatav: So in the first case, the --explain flag would go into detail about how you can't add Integers:

$ dhall --explain
1 + 1
<Ctrl-D>

Error: ❰+❱ only works on ❰Natural❱s

Explanation: The ❰+❱ operator expects two arguments that have type ❰Natural❱

For example, this is a valid use of ❰+❱: 


    ┌─────────┐
    │ +3 + +5 │
    └─────────┘


You provided this argument:

↳ 1

... which does not have type ❰Natural❱ but instead has type:

↳ Integer

Some common reasons why you might get this error:

● You might have tried to use an ❰Integer❱, which is not allowed:


    ┌─────────────────────────────────────────┐
    │ λ(x : Integer) → λ(y : Integer) → x + y │  Not valid
    └─────────────────────────────────────────┘


  You can only use ❰Natural❱ numbers


● You might have mistakenly used an ❰Integer❱ literal, which is not allowed:


    ┌───────┐
    │ 2 + 2 │  Not valid
    └───────┘


  You need to prefix each literal with a ❰+❱ to transform them into ❰Natural❱
  literals, like this:


    ┌─────────┐
    │ +2 + +2 │  Valid
    └─────────┘

────────────────────────────────────────────────────────────────────────────────

1 + 1

(stdin):1:1

The contract for error messages is that --explain should provide enough information.

I can improve the error message for the second case by special-casing the error to notice if the function is an Integer or a Natural and the argument is a Natural and provide a hint that the user might want to put spaces around the +

For the third case, I think the error message is clear even without --explain: the compiler is obviously parsing the ++ as the Text append operator. It might be disconcerting but I don't think it's confusing

from dhall-haskell.

Related Issues (20)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.