Records in Haskell

[AntC]

Ryan Newton <rrnewton <at> gmail.com> writes:

> 
> I admit I'm a big fan of polymorphic extension.  But I don't love it enough 
for it to impede progress!  
> 
> Regarding extension:  In trying to read through all this material I don't 
see a lot of love for "lacks" constraints a la TRex.
> Cheers,
>   -Ryan

Hi Ryan, I think the "lacks" constraint is sadly misunderstood, and in fact 
something like it will be needed eventually.

[A further thousand apologies for the multi-multiposts! somewhere in pipermail
 half my posts are going missing: I was only just warming up this far. Try 
again ... again ... third time ... last time]

(If anybody who knows the internals of Hugs/TRex is listening, it would be 
great to get confirmation of the following.)

As you say, it relates to whatever might happen for polymorphic records, so is 
outside the scope of what SPJ is trying to address in this thread.

On the other hand, let's try to avoid developing an approach for 'Records in 
Haskell' that has to be undone when/if we get more polymorphic.

All the suggestions in the current thread lead to an approach with a Has class 
with methods get and set. It would be sweet if in future the same Has class 
could be extended to extended(!) records, anonymous records, renamed labels, 
projections on records, merged records (as you'd get from a relational join), 
etc. Specifically:
      Has r l t => ...             really must mean 
         there's exactly one field labelled l in record r, at type t
         (which is a constraint on whatever merged/extended term r is)
compare TRex's
      (r\l) => ... Rec {| l : t | r |} ...   which really means
         there's exactly one field labelled l in the Rec, at type t

In hindsight, I think it was unfortunate that the original TRex paper [1] used 
the word "lacks" in context of its notation for constraining the record 
structure. (I'm looking especially at section 2.1 'Basic Operations'.) In all 
the operations, the types always include a Rec term with _both_ l and r. They 
don't all have a term of a 'bare':
      Rec {| r |}
TRex is trying to avoid a positional specification of the record fields (which 
is 'implementation determined'/hidden from the programmer). But I think 
of 'bare' r as representing a record with a 'hole' at whatever position l is 
in the full record. (So the constraint (r\l) means: you're going to find a Rec 
with exactly one l in it; if you also find a Rec with 'bare' r, that means the 
same Rec, but with a 'hole'.)

The HList guys picked up the word "lacks", and adapted it (successfully in 
context of what they were doing) to build 'Type Indexed Hlist's -- that is, 
record-like structures with exactly one field labelled l.

Perhaps TRex should have used a notation something like:
       (rr :> l @ t) => Rec {| rr |} ...       -- HasUnique rr l t
                   ... Rec {| rr \ l |} ...    -- rr with a hole in place of l


You say:
>  As one anecdote, I've been very pleased using Daan Leijen's scoped labels 
approach.
My anecdote: the new approaches and extensions to type inference in GHCi have 
been frustratingly slow in arriving and maturing. But we now have working 
superclass constraints, including type equality (~), and some heavy-weight 
type inference. I've built a toy (and somewhat limited) polymorphic record 
system (with Has/get/set), which:
    treats Data types as records; and
    treats tuples as anonymous (type-indexed) records; and
    implements project, extend and merge.
It relies on overlapping instances (so I don't mention it in polite company -- 
at least it doesn't use FunDeps to boot!). I achieve the effect of 'HasUnique' 
through instance resolution: if there's more than one occurence of label l in 
the record term, GHC bitches. (This is fragile: I can't use 
IncoherentInstances, and sometimes UndecidableInstances gives trouble.)


[1] A Polymorphic Type System for Extensible Records and Variants, Gaster/Mark 
P. Jones, 1996.