New Some/None constructors for Optional values

[Gabriella439]

... as discussed in #113 (comment)

This adds new Some/None constructors that will (eventually) displace the
List-like syntax for Optional values.

The key new feature is that Some does not require you to supply the element
type. In other words, you can now write Some 1 instead of [ 1 ] : Optional Integer.

The second benefit is that the new constructors are just shorter in general.

This proposes that Some/None are the new normal forms for optional literals
and that the legacy List-like syntax β-normalizes to Some/None. The
reason why is that converting in the opposite direction from Some t to
[ t ] : Optional T would require performing type inference during
β-normalization (which would complicate β-normalization). In contrast,
converting from [ t ] : Optional T is straightforward and only requires
dropping the type.

Eventually the legacy List-like syntax will be dropped after a suitably
long migration period.

[quasicomputational]

The decoding judgement will need to learn about the null here.

[Gabriella439]

Oh, whoops, yes. I also forgot to bump the protocol version string to "1.1" and other related changes

[vmchale]

This sounds wonderful! It would simplify the parser as well :)

[Gabriella439]

Here's the matching pull request for the Haskell implementation: dhall-lang/dhall-haskell#559

[f-f]

@Gabriel439 this is cool 👏 👏

About your concerns in #113 (comment):

• Present/Absent: I agree with your analysis but I think it presents more compelling reasons to go with Some/None rather than with Present/Absent:
  1. shorter to type - I type them a lot and the reason why the current syntax is bothersome to me is mostly because it's a lot of chars
  2. they are already used in other langs (Rust, Scala, probably others), so more familiar to their userbase (which I think massively overlaps with our most-likely-to-be userbase)
• Some/None vs some/none: I'd classify them as "constructors" instead of "keyword"; now, in Dhall we don't have prior cases of "constructors" that we can refer to (as there is just special syntax to construct all other built-in values), but constructors are usually capitalized (in any language I can think of), so Some/None feels right

Then I have a couple of questions on the PR itself:

• Having to do a massive replacing for the protocol version string every time we add an AST constructor is a lot of work. Would it be possible to call the encoding function just encode and then say "we specify encode for the latest version X.Y", and then specify a version only when specifying the encoding for cases in any other version than the latest?
• If we normalize to the new Some/None (which is good) would this mean that when caching hash-protected imports the old [ .. ] : Optional .. form will not be present anymore? (since IIRC we beta-normalize imports before writing them to the cache)

[ocharles]

I'd point out that Present is also a verb (to present) which could be confusing if someone thought it was a method call.

…

On Sat, 1 Sep 2018, 8:08 pm Fabrizio Ferrai, ***@***.***> wrote: @Gabriel439 <https://github.com/Gabriel439> this is cool 👏 👏 About your concerns in #113 (comment) <#113 (comment)> : - Present/Absent: I agree with your analysis but I think it presents more compelling reasons to go with Some/None rather than with Present/Absent: 1. shorter to type - I type them a lot and the reason why the current syntax is bothersome to me is mostly because it's a lot of chars 2. they are already used in other langs (Rust, Scala, probably others), so more familiar to their userbase (which I think massively overlaps with our most-likely-to-be userbase) - Some/None vs some/none: I'd classify them as "constructors" instead of "keyword"; now, in Dhall we don't have prior cases of "constructors" that we can refer to (as there is just special syntax to construct all other built-in values), but constructors are usually capitalized (in any language I can think of), so Some/None feels right Then I have a couple of questions on the PR itself: - Having to do a massive replacing for the protocol version string every time we add an AST constructor is a lot of work. Would it be possible to call the encoding function just encode and then say "we specify encode for the latest version X.Y", and then specify a version only when specifying the encoding for cases in any other version than the latest? - If we normalize to the new Some/None (which is good) would this mean that when caching hash-protected imports the old [ .. ] : Optional .. form will not be present anymore? (since IIRC we beta-normalize imports before writing them to the cache) — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#227 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AABRjs_-zIeIUU9WC-bPXj93WKhSNnfQks5uWtszgaJpZM4WWFp-> .

[Gabriella439]

@f-f: Yeah, I'm warming up to Some/None myself, so I think I'll stick with them

Having to do a massive replacing for the protocol version string every time we add an AST constructor is a lot of work. Would it be possible to call the encoding function just encode and then say "we specify encode for the latest version X.Y", and then specify a version only when specifying the encoding for cases in any other version than the latest?

Sure, I will just use encode for the latest version

If we normalize to the new Some/None (which is good) would this mean that when caching hash-protected imports the old [ .. ] : Optional .. form will not be present anymore? (since IIRC we beta-normalize imports before writing them to the cache)

Yes. New cached values will now store Some/None for Optional literals. However, the binary protocol still has to specify how to serialize values that aren't in normal form (such as the legacy syntax for Optional literals) because binary serialization can be used for purposes other than caching (like transmitting Dhall expressions over the wire).

[istathar]

Much as I'm not thrilled about Just (although Nothing is terrific!) for the optional type, the other FP convention of Some seems worse. In English, anyway, you don't have "some apple" or "none [apple]"; the word some goes with a quantity more than one.

Too bad There'sASingle and EmptinessOfTheVoid doesn't have the brevity and pizzazz we are looking for.

AfC