Dynamic row type for open records

[yannham]

Currently, the builtin contracts for row types are not implemented yet (#157), but hopefully they will be soon.

Questions about the expressivity of such contracts have been discussed in #45. This is to be understood in the context of a function taking a record as an argument, where contracts act on two dual aspects:

• shape (the burden is on the context, or the caller): if my function has the contract { a: Num } -> Num, the caller is responsible to provide me a record with a field a. The record contract can be open or closed: in the previous example, it is closed, as the argument must not have extra fields other than a. In a function forall a. {foo: Num | a} -> Num, it is open, since the argument must have at least foo, but can also have other extra fields.
• usage (the burden is on the function, or the callee): if I use a polymorphic type in my arguments, I must assure that I treat this polymorphic type as a black box. For example, a function with contract forall a. {foo: Num | a} -> {foo: Num} should not try to access any other field than foo on its argument. A function could have open usage, with a specification meaning "I need at least field foo, but I may access dynamically other field as well". This can't be expressed in the current type system.

Reusing the table of @teofr, we can already fill part of it with the current type system:

record contracts	closed fields	open fields
closed usage	closed record type: { a: Num } -> ..	polymorphism: forall a. {foo: Num | a} -> ..
open usage	N/A (absurd)	?

Filling the blank

One option to fill the blank would be to add a dynamic row type, as presented for example in this paper.

Currently, the tail of a row can either be the empty row, or a type variable to indicate an open row. But a type variable must be quantified somewhere and must obey to parametric polymorphism: as it is already the case for an arrow type like forall a. a -> a, contracts should enforce that the values of type a can never be inspected, just passed around. In particular, that makes the record closed in usage. This, for example, must not be allowed:

// Deserve a blame !
let f  = Assume(forall a. {foo: Num | a} -> Str, fun rec => rec.bar) {foo = 1; bar = "blah"}

Using the dynamic row type would allow a new value for the tail of a row, which is the dynamic type. This would mean that the tail of a record becomes subject to inspection:

// Ok
let f = Assume({foo: Num | Dyn} -> Str, fun rec => rec.bar) {foo = 1; bar = "blah"}

Which corresponds exactly to the missing case in the table. This has implications for the type static system, since it would probably fails in the current state with an "Illformed type" error if trying to unify a row type with a Dyn tail somewhere (even if not consistently). But it should be possible to accommodate: a complete type system with the dynamic row type, gradual types and polymorphism is precisely described in the aforementioned paper.

[aspiwack]

I think that you convinced me that dynamic rows make sense. They are rather in line with the rest of the design: if we can do type refinement by type-casing or what not, then we ought to be able to do the same for record fields (basically giving hasField some influence on the type flow).