[Haskell-cafe] Return of the revenge of the revisit of the extensible records, reiterated

[Atze van der Ploeg]

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 <anthony_clayden at clear.net.nz>

> > John Lato <jwlato <at> gmail.com> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131205/cb3a73be/attachment.html>