Simon suggests that:
| type classes can model extensible records.
Indeed, they can, and in several different ways, depending on the kind
of extensible records that you want to give the programmer. The particular
system that Simon outlined is pretty close to a proposal for `structures in
Haskell' that John Peterson has been working on here at Yale.
However, there are some complications with this approach that Simon didn't
mention. It's true that there is a simple translation for records in which
all fields have fixed ground types:
| record Person = { Age : Int; Weight : Int }
|
| class Person a where
| setAge :: a -> Int -> a
| getAge :: a -> Int
| ...similarly for Weight...
But now consider examples like:
record Pair a b = { Fst : a, Snd : b }
What types should be used for setFst and getFst here? There seem to be two
possibilities; either you don't allow records with variable type fields, or
you extend the type system with parametric type classes (Chen, Hudak and
Odersky, LFP '92) and take:
setFst :: (p :: Pair a b) => p -> a -> p
getFst :: (p :: Pair a b) => p -> a
Another approach to extensible records using classes/predicates was outlined
in my thesis a couple of years ago, motivated in turn by some work done by
Harper and Pierce in about 1990. A similar type system was developed
independently by Ohori (POPL '92) although the connection with type classes
is less apparent in his work.
The basic idea in this case is to have, in effect, a class for every label L
whose instances are precisely those record types that don't have an L field.
Let's write t\L to indicate that type t is an instance of the class for L
(in the past, I've written this as t lacks L ... for a more conventional
Haskell syntax, we could just write LacksL t). Now you can describe (and
implement) standard operators on extensible records by families of functions
(indexed by labels L):
selection: (_ . L) :: (r\L) => (r | L::t) -> t
extension: (_ | L=_ ) :: (r\L) => r -> t -> (r | L::t)
delete: (_ \ L) :: (r\L) => (r | L::t) -> r
override: (_ | L:=_) :: (r\L) => (r | L::t) -> t' -> (r | L::t')
This doesn't require parametric type classes to deal with examples like the
one above; instead, it requires a special syntax for record types. The idea
here is that (r | L::t) is the type of records with type r, extended with a
single field L of type t. This type expression is only well-formed if r\L
and we can use this to simplify the way that the types above are presented to
the programmer. For example, selection can be treated as having the type:
(r | L::t) -> t
Simple record types, like Person above, can be thought of as abbreviations for
extensions of the empty record, ():
type Person = (Age::Int, Weight::Int) -- ((()| Age::Int) | Weight::Int)
Ordering of fields is, as you might hope, not significant.
I hope that these examples give some idea of the range of systems that can be
described:
- grouping according to individual fields, or groups of fields?
- can field names be used in distinct record types?
- do we allow variable type fields in a particular record?
- do we allow polymorphic values as record fields?
- is a new syntax for record types required?
There are also several other examples that won't have been brought out in the
examples above. For example, there are good reasons for extending the
monomorphism restriction or defaulting mechanism with some proposals for
extensible records.
All the best,
Mark
