This is really fascinating work, Jon. This has introduced me to a number of new features I didn’t know existed.
Are you concerned that such “duck typing” on records w.r.t. their field names might lead to loss of the very safety Haskell works so hard to guarantee? One can imagine two record types which from separate frameworks, one of which has the fields “name” and “size,” (maybe a key for a cache table of encoded data) and the other of which has those names plus “color” (referring to, say, a shape entity in a drawing application). The former is technically a subtype of the latter, as you’ve defined subtyping, but those fields are semantically distinct, and the type intersection is actually pretty meaningless.
Thanks, Andy, that’s a really good question. This seems to be one of the primary weaknesses of structural typing… One thing that could be done to get around it would be to generalize Field to be polymorphic over the kind of its key; that way, when desiring guarantees that your spurious relations to not arise between your records and those of other modules, you could use your own universe of keys, like so:
data (:::) :: k -> * -> * where
Field :: s ::: t
data LocallyAvailableFields = Name | Age
name = Field :: Name ::: String
age = Field :: Age ::: Int
man = (name, "jon") :& (age, 20) :& RNil
Another thing that might be done would be to abstract out even the field representation itself; this would make the implementation a bit more complicated, but it would allow easy declaration of local “field universes”:
data MyFields :: * -> * where
Name :: MyFields String
Age :: MyFields Int
man = (Name, "jon") :& (Age, 20) :& RNil
I sort of like this approach, but I haven’t yet thought through its implications on the rest of the system; currently a lot depends on the structure of the field representation, but it may be possible to abstract that away and allow something like what I have proposed above.