Optional field types

[jneem]

This was an attempt at #2050

• makes fields optional in record types
• adds a unification rule for optional record fields
• adds automatic UniTerm -> Type conversions for records with "simple enough" contract annotations

I think the last one was a mistake, though. It's not backwards compatible (e.g. it breaks one test), and it leads to some weird special cases. I'm going to try doing the contract -> type conversion later (like maybe just in the typechecker itself) and see if that's better.

I also didn't figure out how to trigger subtype checking. I tried some variants of the existing subtype tests but I only ever hit the unification code.

[yannham]

I haven't looked at it yet, but my first reaction is maybe that a PR is a bit premature. A type system (especially with type inference) is a complicated and intricate system and each addition or changes must be principled and if possible backed by existing literature, IMHO. Sometimes seemingly harmless additions might interact unexpectedly with other parts of the system (often with polymorphism).

I currently don't know a lot about optional fields in structural typing, maybe it's a rather simple extension. I don't know yet if this requires an RFC, but I would advocate for at the very least an issue proposal where we can debate the design, the syntax, the motivations, and the interaction with the existing components - in particular how does it behave with respect to (row) polymorphism, to subtyping, to unification, to inference, to contracts, etc.

[jneem]

Oh, a PR is definitely premature 😅 I mostly just uploaded this to record the not-too-successful experiment. I'll open an issue for further discussion.

[yannham]

Ah, my bad! A draft PR for experimenting is rarely too premature indeed 🙂 I just wanted to avoid putting too much effort into this before careful design.