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: ====> http://www.haskell.org/haskellwiki/CTRex <====== 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.
=====================================================
Adam Vogt:
Could you check whether the comparison with HList records is accurate?
Check
http://www.haskell.org/haskellwiki/CTRex#Comparison_with_other_approaches .
Thanks!
=============================================
AntC:
You seem to have strong opinions on why allowing duplicate labels is a bad
thing. Currently, my design supports both extension with scoping and the
lacks predicate (see
http://www.haskell.org/haskellwiki/CTRex#Duplicate_labels.2C_and_lacks). I
think duplicate labels are nice in some situations and bad in other
situations.
2013/12/3 AntC
John Lato
writes: On Mon, Dec 2, 2013 at 9:17 PM, AntC wrote:
... Importing an overlapping instance is trapped immediately; no risk of incoherence.
How can this possibly work with open type families? What happens in this case?
module A where type instance F a b c | b /~ c = Int module B where type instance F a b c | a /~ c = Bool
During compilation, neither A nor B is aware of the other. What happens in a module that imports both?
Thanks John, a good use case!
The trapping is needed with imports for any approach to open instances (not just type families). Suppose I have NoOverlappingInstances everywhere:
module A where instance C a b c where ... module B where instance C a b c where ... module D where instance C Int Bool Char where ...
And a module that imports all three. Any importer has to validate all instances sometime or other.
(Currently ghc sticks its head in the sand, and hopes there won't be a usage that trips over the ambiguity.)
All we're talking about is _when_ we validate. I'd rather know at the point of declaring the instance, or of importing the instance.
AntC
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe