Support analysis mode typing for record literals?

[crusso]

~/dfinity/motoko $ echo '{ foo = 5 * 5 } : { foo : Nat64 };' | moc 
Motoko compiler (revision 0.5.3-12-g84d34b505)
> stdin:1.1-1.16: type error, expression of type
  {foo : Nat}
cannot produce expected type
  {foo : Nat64}
>

Rossberg writes:

This is an artefact of treating these as sugar for let blocks. With our recent semantic change, we could in principle change that, by having dedicated typing rules for the short form.

[crusso]

@rossberg so I'd like to fix this.

My plan is to introduce a dedicated syntax.ml expressions node, RecE, for record literals,

exp = 
...
| RecE of rec_field list

rec_field  = 
| Field of id * exp
| VarField of id * exp 

that takes the (possibly mutable) fields and type checks and desugars them directly. No visibility/stability modifiers or patterns required.

The parser (including the deprecated productions) would no longer desugar record literals to blocks yielding objects (freshening field names to avoid recursion) but parse directly to RecE, simplifying lots of the productions and removing some desugaring from the parser.

Sound like a plan or did you have something else in mind?

[rossberg]

Sounds good to me!

[matthewhammer]

(Yay! Another step closer to being able to program in "real CBPV" within "core Motoko expressions"; we lacked the form that you are adding, among some others still missing.)

[crusso]

(Yay! Another step closer to being able to program in "real CBPV" within "core Motoko expressions"; we lacked the form that you are adding, among some others still missing.)

Not sure what CBPV has to do with it, but what's missing? Enquiring minds want to know!

[matthewhammer]

Not sure what CBPV has to do with it, but what's missing? Enquiring minds want to know!

Oh, I'm so glad that you asked!

CBPV is, in my view, a "sweet spot" for the following design goals that PL people often find themselves with:

1. A simple core calculus that resembles core ML
2. Something even more constrained than CBV, like ANF tends to be, so that typing rules that consider effects are simpler.
3. Something with nice mathematical/algebraic properties*, with connections to all the stuff that math folks like (categories, etc)

The key departures from the usual CBV core calc that most people would choose:

• Like in ANF, in CBPV, the forms that permit arbitrary expressions are limited; it's possible to speak of a value that cannot be an expression, but also, function applications always apply functions to values (not expressions), and so forth.
• Unlike CBV (and more like "four address code" style), function are computations, not values; closures (thunks) are values, and they have explicit syntax. More generally, the placement of computation versus value is totally explicit in syntax. (and this property is related to this PR, but looking at just the record type case).
• (*) Unlike ANF, CBPV is closed under substitution. I think that fact has huge implications for its category theory and other math, but I wouldn't know personally. In terms of the inductive meta theory proofs I tend to do (forall-exists some lang properties, inducting over evaluation), it makes them easier. ANF is totally broken in this regard, and is why compilers that use it can be painful to reason about with the usual tools we use in meta theory. Now that we have this record form, we have a value form (for records) that was missing in Motoko. That's the cryptic fact that I was noticing, I guess. It's important for lots and lots of subtle reasons, in the way that PL design tends to be very complex in its subtitles.

[crusso]

Thanks! I think here the issue was not having an introduction form for record since birectional checking seems to pivot on those. It was the same thing that made me uncomfortable with the suggestion to extend '? exp' to allow '!' escapes since it would no longer be an intro form. The fact that CBPV is closed under substitution should indeed make it good for optimization in a similar way that Kennedy argued continuations were better than ANF.