[Haskell] extensible records using associated types
I'm sorry if this example has already been posted, but I couldn't find it by searching the archives. If it's new (and works properly), it provides more evidence that ATs are a good thing. You can use associated type synonyms to implement polymorphic extensible records. - We will represent records as values of the form N1 x1 (N2 x2 ... (Nn xn Empty)...) with corresponding type N1 a1 (N2 a2 ... (Nn an Empty)...) where the field name N is defined by the declaration data N a r = N a r For convenience, we define the type of field name constructors: >type Constructor n = forall a. forall r. a -> r -> n a r so that N :: Constructor N for each field name N. Next we define a class (:<:) whose purpose is to tell the compiler in which order to store fields: >class (m :: * -> * -> *) :<: (n :: * -> * -> *) The idea is that if N and M are distinct field names which might appear the same record, then there must be an instance of exactly one of N :<: M and M :<: N. The class Contains n r asserts that r is a record type with a field labelled n: >class Contains n r where >type Project n r >type Delete n r >project :: Constructor n -> r -> Project n r >delete :: Constructor n -> r -> Delete n r There are two associated types: Project n r is the type of the n field, and Delete n r is the type of the rest of the record. The functions project and delete give the corresponding values. The class Lacks n r asserts that r is a record type without a field labelled n: >class Lacks n r where >type Extend n a r >extend :: Constructor n -> a -> r -> Extend n a r There is one associated type: Extend n a r is the type of the record obtained by adding a field of type a labelled n. Note that according to the AT paper, the parameter a should come last, but this order is much more convenient. The function extend adds the new field to the record. The class Disjoint r s asserts that r and s are record types with no fields in common: >class Disjoint r s where >type Union r s >union :: r -> s -> Union r s There is one associated type: Union r s is the type of the merged record, and union is the merge function. Next we define the empty record: >data Empty = Empty It has no fields, so has no instances of Contains, but lots of instances of Lacks: >instance Lacks n Empty where >type Extend n a Empty = n a Empty >extend nn x Empty = nn x Empty It is also disjoint from everything: >instance Disjoint Empty r where >type Union Empty r = r >union Empty t = t Each field name must be defined as a data type together with instances of the classes Contains, Lacks and Disjoint as follows: >data N a r = N a r The type N a r certainly contains a field named N: >instance Contains N (N a r) where >type Project N (N a r) = a >type Delete N (N a r) = r >project N (N x t) = x >delete N (N x t) = t It also Contains all the fields of r, though you only need to check names which are below N: >instance m :<: N, Contains m r => Contains m (N a r) where >type Project m (N a r) = Project m r >type Delete m (N a r) = N a (Delete m r) >project mm (N x t) = project mm t >delete mm (N x t) = N x (delete mm t) Similarly, it Lacks all the fields which r Lacks, except for N itself. This is where we really need the ordering :<: to ensure that m is not equal to N. There are two cases, m :<: N: >instance m :<: N, Lacks m r => Lacks m (N a r) where >type Extend m b (N a r) = N a (Extend m b r) >extend mm y (N x t) = N x (extend mm y t) and N :<: m: >instance N :<: m => Lacks m (N a r) where >type Extend m b (N a r) = m b (N a r) >extend mm y (N x t) = mm y (N x t) To ensure that N a r is disjoint from s, it is enough that r is disjoint from s and N is not in their union: > instance Disjoint r s, Lacks N (Union r s) => Disjoint (N a r) s where >type Union (N a r) s = Extend N a (Union r s) >union (N x t) u = extend N x (union t u) Finally, we must maintain the ordering :<:. It has to be a global linear order, so if we know the last field name was M, we can define: >instance M :<: N >instance m :<:
Re: [Haskell] extensible records using associated types
Of course, under Usage, I should have written: The record {N1 = x1, ... Nn = xn} should be constructed as (extend N1 x1 $ ... $ extend Nn xn $ Empty). Sorry about any confusion! Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] extensible records using associated types
The implementation of records using types data N a r = N a r might well be inefficient, and I don't know enough about the workings of the compiler to see whether it could be improved by unboxing and strictness. But the real point of my post was the classes Contains, Lacks and Disjoint which give you extensibility. To give another example, if Haskell had non-extensible records {N1 = x1, ..., Nn = xn} of type {N1 :: a1, ..., Nn :: an} we could use the same technique to make them extensible. Assume we can represent the field names N somehow as values (N :: Constructor N). Then we can define instances of the form instance Contains Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} where type Project Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} = aj type Delete Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} = {N1 :: a1, ..., Nn :: an} project Nj {N1 = x1, ..., Nj = xj, ..., Nn = xn} = xj delete Nj {N1 = x1, ..., Nj = xj, ..., Nn = xn} = {N1 = x1, ..., Nn = xn} instance Lacks M {N1 :: a1, ..., Nn :: an} where type Extend M a {N1 :: a1, ..., Nn :: an} = {M :: a, N1 :: a1, ..., Nn :: an} type extend M x {N1 = x1, ..., Nn = xn} = {M = x, N1 = x1, ..., Nn = xn} instance Disjoint {N1 :: a1, ..., Nn :: an} {M1 :: b1, ..., Mm :: bm} where type Union {N1 :: a1, ..., Nn :: an} {M1 :: b1, ..., Mm :: bm} = {N1 :: a1, ..., Nn :: an, M1 :: b1, ..., Mm :: bm} union {N1 = x1, ..., Nn = xn} {M1 = y1, ..., Mm = ym} = {N1 = x1, ..., Nn = xn, M1 = y1, ..., Mm = ym} Of course, there are a lot of these (exponential in the number of field names!) so you don't really want to generate them all. But exactly the same classes (modulo the definition of Constructor, which should be hidden anyway) give you extensibility, so any code you write will work with either implementation. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] extensible records using associated types
Barney Hilken: > Similarly, it Lacks all the fields which r Lacks, except for N > itself. This is where we really need the ordering :<: to ensure that > m is not equal to N. There are two cases, m :<: N: > > >instance m :<: N, Lacks m r => Lacks m (N a r) where > >type Extend m b (N a r) = N a (Extend m b r) > >extend mm y (N x t) = N x (extend mm y t) > > and N :<: m: > > >instance N :<: m => Lacks m (N a r) where > >type Extend m b (N a r) = m b (N a r) > >extend mm y (N x t) = mm y (N x t) This is problematic as the instance heads are distinguished only by the context; ie, both instances are for `Lacks m (N a r)'. Haskell's instance selection mechanism (with or without associated types) selects instances purely by looking at the arguments of the class; hence, you cannot use instance context as a kind of guard to guide instance selection. Manuel ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] extensible records using associated types
Manuel M T Chakravarty: This is problematic as the instance heads are distinguished only by the context; ie, both instances are for `Lacks m (N a r)'. Haskell's instance selection mechanism (with or without associated types) selects instances purely by looking at the arguments of the class; hence, you cannot use instance context as a kind of guard to guide instance selection. A pity. Would resolving instance declarations as Horn clauses be useful to deal with any other examples of overlapping instances? If you don't mind the code for each new label being linear in the number of previous labels (so the total code is quadratic in the global number of labels) the idea can be rescued. Get rid of (:<:), and keep the same definitions of Constructor, Contains, Lacks, Disjoint and Empty, and the same instances of 'Lacks n Empty' and 'Disjoint Empty r'. For each label 'N', define: >data N a r = N a r > >instance Contains N (N a r) where >type Project N (N a r) = a >type Delete N (N a r) = r >project N (N x t) = x >delete N (N x t) = t > > instance Disjoint r s, Lacks N (Union r s) => Disjoint (N a r) s where >type Union (N a r) s = Extend N a (Union r s) >union (N x t) u = extend N x (union t u) and for each previous label 'M', define: >instance Contains M r => Contains M (N a r) where >type Project M (N a r) = Project M r >type Delete M (N a r) = N a (Delete M r) >project M (N x t) = project M t >delete M (N x t) = N x (delete M t) > >instance Lacks M r => Lacks M (N a r) where >type Extend M b (N a r) = N a (Extend M b r) >extend M y (N x t) = N x (extend M y t) > >instance Lacks N (M a r) where >type Extend N b (M a r) = N b (M a r) >extend N y (M x t) = N y (M x t) This saves the bother of fiddling with (:<:) but means that every time you import a module which declares labels you would have to generate code for the interactions between each new label and each existing one. At least it's not exponential! Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] extensible records using associated types
Sorry if people are really bored with this thread, but I thought of another advantage of this approach. Trex (and similar systems) have a limitation that stops you using them to define functions with default values. In systems like R (the stats package) most functions have a huge number of named parameters which usually take default values, but can be changed if necessary. In order to define such functions, what you want is an operation 'update r s' which takes the value of the record 's' (the non-default values) for each field which 's' has, and the value of 'r' (the default values) for all other fields. The type of 's' should be such that it can only have fields which 'r' has, and each such field must have the same type, but it doesn't need all the fields of 'r'. The type of the result is the same as the type of 'r'. This can't be typed in Hugs because you can only update particular fields, but we can easily add it to (at least the quadratic version of) AT-records. Introduce a class 'subRecord r s' which means that every field of 's' is a field of 'r' with the same type: >class subRecord r s where >update :: r -> s -> r The type 'Empty' is a subRecord of everything, and updating by it changes nothing: >instance subRecord r Empty where >update t Empty = t For each label 'N' define: >instance subRecord r s => subRecord (N a r) (N a s) where >update (N x t) (N y u) = N y (update t u) For each previous label 'M' define: >instance subRecord r (M b s) => subRecord (N a r) (M b s) where >update (N x t) (M y u) = N x (update t (M y u)) There are probably other useful additions to the records system which could be coded up in a similar way. In fact, the class 'Disjoint' of my original proposal already goes beyond hugs. Until it is clear what is useful and what is not, a system like this which requires little compiler support has the great advantage that it is easy to change. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell