[Haskell] extensible records using associated types

[Barney Hilken]

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

[Barney Hilken]

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

[Barney Hilken]

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

[Manuel M T Chakravarty]

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

[Barney Hilken]

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

[Barney Hilken]

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