Dear all,
I have written a document describing the design, usage and motivation for these extensible records (now called CTRex, a nod to Trex).
It is available at:
Improvements, comments and questions welcome!
Below are some long overdue responses to comments in this post.
Cheers!
Atze
==================================================
Oleg:
You said:
> This is all very true. However, if we wish to pass the function f
> above the record {y=0, x=0} (with permuted fields), we most likely
> wish to pass that function a record {x=0, y=0, z='a'} with more> fields. Most of the time when we deal with extensible records, we
> really wish to explore their extensibility. Keeping fields sorted> does not help at all in the latter problem -- we must manually insert
> the call to the subtyping coercion function. Once we do that, the> problem with the order of the fields disappears.
In my design such coercion calls are unnecessary, or am I missing something here?
> I also would like to point out that there are two sorts of
> record types. One sort is
> Rec [x: Int, y:Bool]
> in the imagine syntax. Current HList types are uglier versions of the
> above. But there is another sort:
> (HasField r x Int, HasField r y Bool) => r
> It represents an extensible record type. Extensibility is build in,
> and the order of the fields is immaterial. Quite a few functions on
> records can be given the above type. Furthermore, the second sort can
> be used not only with structural subtyping but also with nominal
> subtyping.
I agree. There is a difference between systems with records and row polymorphic records (if I understand you correctly).
My system supports both, the former is written as:
Rec ("x" ::= Int .| "y" ::= Bool .| Empty)
the latter is written as
Rec ("x" ::= Int .| "y" ::= Bool .| r)
where r is the rest of the row, not the whole row as you write it.
Notice that .| is a type level *function* (not a constructor!) that inserts a label-type value into the row.
Hence Rec ("x" ::= Int .| "y" ::= Bool .| Empty) ~ Rec ("y" ::= Bool .| "x" ::= Int .| Empty)
I do not understand you point about nominal subtyping, how can we nominally subtype r? It has no name? I can only imagine structural subtyping on records.
=====================================================
=============================================
AntC: