*First-class labels for extensible rows. (draft)*

Daan Leijen.

Submitted to POPL'05. (PDF, BibTeX)

**Abstract**:
This paper describes a type system for extensible records and variants with first-class labels; labels are polymorphic and can be passed as arguments. This increases the expressiveness of conventional record calculi significantly, and we show how we can encode intersection types, closed-world overloading, type case, label selective calculi, and first-class messages. We formally motivate the need for row equality predicates to express type constraints in the presence of polymorphic labels. This naturally leads to an orthogonal treatment of unrestricted row polymorphism that can be used to express first-class patterns. Based on the theory of qualified types, we present an effective type inference algorithm and efficient compilation method. The type inference algorithm, including the discussed extensions, is fully implemented in the experimental Morrow compiler.

Always trust Daan to come up with something both elegant and practical...! However the examples involving bottom (undefined) labels left me skeptical.

## Recent comments

18 hours 53 min ago

19 hours 9 min ago

20 hours 2 min ago

20 hours 49 min ago

21 hours 16 min ago

21 hours 39 min ago

21 hours 56 min ago

22 hours 39 min ago

23 hours 1 min ago

23 hours 17 min ago