+ in front of Naturals is not at all natural

[Profpatsch]

I nearly stumbled over the very first exercise because it was not at all clear to me that I need to annotate even naturals with +.

And the error message thrown is simply:

Error: Expression doesn't match annotation

./tmp/config : { age : Natural, name : Text }

I’m sure the explicit + has some deeper reasons, but do we need it for naturals? If yes, the tutorial should be very clear of this upfront.

[Gabriella439]

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

[Gabriella439]

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

[echatav]

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 ❰Natural❱s

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?

[Gabriella439]

@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