Are extensible records first class patterns?

If you have a language with extensible records (like those of Gaster and Jones), and you view functions like a -> Maybe { r } for some row r as patterns, are there practical obstacles that prevent you from extending the environment of a case alternative with the row of the result type of its controlling pattern?

I would appreciate pointers to anywhere that this is discussed in the literature, or an explanation of why it is a bad idea. Google hasn't been especially helpful.

-- concrete syntax for records is entirely made-up

wildcard_pattern = const Just {}

-- without first class labels, the compiler would have to make a whole family
-- of declarations like this, one for each variable bound by a pattern
variable_pattern_x val = Just { x := val }

-- same comment applies
as_pattern_x pat val = case pat val of
                         Just rec -> { x := val, rec }
                         Nothing -> Nothing

-- I'm not 100% sure that this handles laziness correctly, but you get the idea
-- declarations like this would be automatically generated from the datatype declarations
cons_pattern pat_head pat_tail [] = Nothing
cons_pattern pat_head pat_tail (x:xs) = case pat_head x of
                                          Just rec_head -> case pat_tail xs of
                                                             Just rec_tail -> record_join rec_head rec_tail
                                                             Nothing -> Nothing
                                          Nothing -> Nothing

nil_pattern [] = Just {}
nil_pattern _ = Nothing

Extensible programming with first-class cases

Here's a related idea:
Extensible programming with first-class cases that relies on the dual of extensible records.

One part of your proposal that looks tricky is the record_join operator. Mixing polymorphic record concatenation with type inference is non-trivial.

By Sam Lindley at Sat, 2009-06-06 11:13 | login or register to post comments

Developing intuition about why

I've heard that too (that type inference for polymorphic record concatenation is problematic), and read a number of papers addressing parts of it, but I can't really wrap my head around why this should be. Could anyone point me to a concise explanation of why this is the case?

I guess the reason I am confused is because it seems like you should be able to collect constraints for the definition of something like join, and at any polymorphic use sites simply propagate those constraints, and when you ultimately get to the (necessarily monomorphic?) top-level use site(s) check the constraints in a relatively straightforward fashion. Is the problem that this process will lead you to tentatively accept--if never allow usage of--polymorphic functions with non-sensical types, and that avoiding this requires satisfiability checking everywhere?

This is likely to be an extremely uninformed question, but I've done my homework and I can't quite get my head around it.

By Douglas McClean at Mon, 2009-06-08 00:52 | login or register to post comments

Polymorphic record

Polymorphic record concatenation is tough, because of the need to propagate information ensuring that record labels are unique. So you can't type concatenation as:

    - Here row is the kind of sequences name:type, ... 
    - {r} means construct a record type from the the row r
    - r1 @ r2 means construct a row that's the concatenation of r1 and r2

    val concat : forall r1, r2:row. {r1} -> {r2} -> {r1 @ r2}

This is no good, because what if r1 and r2 share fields? So we need something like:

    val concat : forall r1, r2:row, disjoint(r1, r2) -> {r1} -> {r2} -> {r1 @ r2}

So we need a predicate disjoint(r, r') which tells us two rows are disjoint from one another. (Similarly, you could add predicates that certain fields are absent. There are lots of ways to skin this cat.) Ideally, we want to infer this disjointness information, too, which can make life quite complicated.

One alternative that Daan Leijen has suggested is to permit replicated field names, and to simply resolve conflicts by a scoping rule -- the first label in the type "wins". This means that you can get away without using disjointness or absence predicates, which can simplify the complexity of the type system. (Extensible Records with Scoped Labels)

By neelk at Mon, 2009-06-08 02:07 | login or register to post comments

disjointness

Hmm .. aren't there rather a lot of alternatives here? First, records can be concatenated into a pair. The pair can then be flattened into a set of fields with a label and a value: the value is a tuple of all the values of the label. Then one could replace singleton tuples with their values leaving non-singletons alone. Alternatively one could add colours to the labels: this form is similar to a discriminated union using constructors to distinguish each case .. and is identical to the first construction (just a plain pair of records).

The real question is: exactly WHY are you trying to concatenate two records? None of the above constructions handles this simple case: (trxno, date, amount), (trxno, date, description) where you really want (trxno, date, amount, description) or Error if trxno and date aren't equal.

Perhaps we should look to actual practice here, namely real world database management.

By skaller at Mon, 2011-11-07 03:15 | login or register to post comments

I agree, it's exactly that

I agree, it's exactly that record join operation, which compares the records for equality on their common attributes and returns the concatenation result or nothing, that is needed to make this work. Exactly as its done in relational databases but in the Maybe monad instead of the Set monad.

I'm working on predicates for qualified types that would encode all this.

By Douglas McClean at Mon, 2011-11-07 03:49 | login or register to post comments

Lambda the Ultimate

User login

Navigation