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 :<: M => m :<: N
Usage.
------
The record {N1 = x1, ... Nn = xn} should be constructed as (extend N1
x1 $ ... $ extend Nn xn) Empty.
Extension, projection, deletion and union are all as polymorphic as
you could want, and you can even use field names as ordinary values.
For example, you can define update by:
> update :: Contains n r, Lacks n (Delete n r) => Constructor n -> a
-> r -> Extend n a (Delete n r)
> update n y t = extend n y (delete n t)
Problems.
---------
1. Pattern matching.
Pattern matching on complete records is possible (though you must
get the fields in the right order!) but there is no equivalent to the
trex .. notation for 'any other fields'.
2. Maintaining the :<: order.
Within one module this could be generated with a template, but
between modules this is more of a problem. Of course, we could use a
built-in class based on alphabetical order, but this would need
compiler support.
3. Controlling the use of constructors.
If you use N to construct records and types directly, instead of
Extend N and extend N, you get fields in the wrong order and
everything breaks. The type system can't stop you doing this.
4. Testing.
I don't actually know if this works, because phrac won't compile
it. We really need the second-order polymorphism of field
constructors, and phrac doesn't have forall. (There is also the
trivial point of the order of arguments to Extend).
Barney.
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
