Home

Extensible Records With Scoped Labels

Extensible Records With Scoped Labels
Daan Leijen
Records provide a safe and flexible way to construct data structures. We describe a natural approach to typing polymorphic and extensible records that is simple, easy to use in practice, and straightforward to implement. A novel aspect of this work is that records can contain duplicate labels, effectively introducing a form of scoping over the labels. Furthermore, it is a fully orthogonal extension to existing type systems and programming languages...
Last time one of Daan's papers was mentioned, there was a very positive response (after Frank reminded us a couple of times). This is equally good: clever, elegant, and clearly presented.

(Between this and the Sheard paper, it's a good week for practical type systems...)

By Matt Hellige at 2005-11-15 16:29 | Implementation | Type Theory | other blogs | 16298 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Is this similiar to private row types in ML?

I certainly don't fully understand either, but there seams to be some overlap between the two.

By CoreyOConnor at Tue, 2005-11-15 19:00 | login or register to post comments

I like it

From the description, Daan's record system looks like it would be very pleasant to use.

I wish the paper had done some comparision to HList. I have the impression that HList is more flexible (for example, record labels are first-class), but it uses some high-octane extensions to Haskell's type class system (functional dependencies and overlapping instances) and possibly can't be as efficiently implemented. (I don't think HList can do constant-time field access without extensive compiler support.)

By Dave Menendez at Tue, 2005-11-15 20:03 | login or register to post comments

Morrow is great

In the earlier paper it explains how Morrow allows first-class row labels, used for both records and tagged unions, with efficient compilation. I didn't read this paper yet, but from the abstract it's built on top of Morrow.

By Daniel Yokomizo at Wed, 2005-11-16 21:01 | login or register to post comments

Yes, but...

I do wish this paper was a bit more clear about the exact relationship to the previous paper. There's a lot of discussion of "Related Designs" and "Related Work", but there's not even a single mention (or citation) of his own previous paper, which would appear to be most relevant indeed. I think the new contribution here is the "scoped labels" bit, but I've been meaning to go through both papers together and check. I don't think that should really be necessary...

That said, Morrow is really neat. I noticed that he removed the interpreter from his site, but it should be coming back.

Daan has posted here before... Maybe we can coax him out again. ;)

By Matt Hellige at Wed, 2005-11-16 22:07 | login or register to post comments

Telescoped names

From records with scoped labels it's not far to telescopes.

Both impose some partial order on labels/names, but telescopes do so explicitly by using previously defined names in types.

By Andris Birkmanis at Tue, 2005-11-15 20:28 | login or register to post comments

Qualified Types for MLF

Below that paper on the page of Daan is a paper on qualified types for MLF which is nice too, maybe a bit impractical though.

I don't get the constant complexity of selection using vectors in the records paper?

By marco at Tue, 2005-11-15 22:04 | login or register to post comments

This might help...

I don't get the constant complexity of selection using vectors in the records paper?

This paper has a pretty clear presentation, I think. The basic idea is that the compiler adds extension predicates to the type of the basic record operations and then translates those predicates to additional run-time parameters, which can be hidden from the programmer and propagated as necessary. So, at run-time we end up passing around integers that we'll use to index the vectors in constant time.

If you think about how Haskell's type classes can be implemented by passing dictionaries at run-time, you'll probably get the basic idea. But I don't feel like I'm explaining this very well. You might want to check out section 2.2 of the paper I linked to above...

By Matt Hellige at Wed, 2005-11-16 22:21 | login or register to post comments

Hmmm.....

Reading the paper. I get it ! I don't get it ? ... I don't get it? ... I get it! .... At least I think so?

Great, run-time offset calculation it is then. Can't oversee the implications though, ... whatever. Thanks for the reference.

And on a personal note: Jesus! Be kind on my eyes and wear a T-shirt. Or anything for that matter! *enormously wide grin*

By marco at Thu, 2005-11-17 23:50 | login or register to post comments

Re: extensible records, GADTs, & Piccola, in no particular order

Between this and the Sheard paper, it's a good week for practical type systems

Is it possible to add these extensible records to Sheard's type system? Is there a reason you can't or shouldn't or needn't combine them?

Also, the Piccola language has extensible records, and IIRC, the papers I read said they were looking for a type system. Is this type system appropriate?

By James McCartney at Sun, 2005-11-20 01:24 | login or register to post comments