Extensible records for Haskell
------------------------------
A proposal for extensible records which is compatible with type
classes and constructor classes, and has a type inference algorithm.
Based on ideas of Sean Bechhofer and implemented within Mark Jones'
'Qualified Types'.
Barney Hilken and Giuliano Procida
This is a proposal for an expressive record language. Records are
first class values and can be manipulated by the extraction, addition
and deletion of named fields. Polymorphism is allowed over the types
of fields and over all fields not explicitly mentioned.
This record system is not based on subtyping. Instead, the necessary
constraints on polymorphism are expressed as predicates on types. This
means that Mark Jones' type inference algorithm extends to record
types.
In what follows we present one possible syntax for the record values,
types and predicates. The importance of our proposal is not the
particular syntax, but the logical structure of the type system, and
the way it integrates with type classes.
-- Labels --
Records are collections of named fields. Because of the limits of
namespace, it is necessary to declare which identifiers are to be
considered field names. The declaration
> label A1, ..., An
introduces field names or `labels' A1, ..., An. This also helps in
finding common errors such as typos.
-- Fixed records --
Fixed records are just ML records; their types include complete
information about the types of the fields. The expression
(A1 is v1, ..., An is vn)
denotes a record with fields labelled A1, ..., An containing values
v1, ..., vn respectively. The order of fields is not significant.
This expression has type
(A1 is t1, ..., An is tn)
where v1 :: t1, ..., vn :: tn, following the Haskell convention that
types have the same form as their values. The same expression can be
used as a pattern:
> f (A1 is x1, ..., an is xn) = rhs
where rhs can refer to variables x1, ..., xn.
-- Predicates --
Extensible records use the `predicates' of the type class mechanism to
allow record polymorphism. For each collection of labels A1, ..., An
there is a predicate
Lacks A1, ..., An r
which says that r is a record type with no `Ai' fields (r must be a
constructor variable of kind *). It satisfies
Lacks A1, ..., An r => Lacks B1, ...,Bm r
for any the subset Bi of the Ai. Note that
Lacks A1 r ... Lacks An r => Lacks A1, ..., An r
also holds. For aesthetic reasons, the abbreviation
Rec r
is used when n=0. It says simply that r is a record type.
-- Indeterminate record types --
For each label A there are type constructors
() ::: *
add A ::: * -> * -> *
del A ::: * -> *
satisfying
Lacks A ()
Lacks A r => Rec (add A t r)
Rec r => Rec (del A r)
Given a type t and a record type r with no A field, add A t r
constructs the type of records with all the fields of r, and
additionally, an A field of type t. When applied to an appropriate
fixed record type:
add A1 t1 (A2 is t2, ..., An is tn) = (A1 is t1, A2 is t2, ..., An is tn)
In this way fixed record types may be considered as successive
applications of add constructors to the null record type.
Given any record type r, del A r constructs the type of records which
do not have an A field, but are otherwise like r. If r does not have
an A field, then del A r = r.
If r is an indeterminate record type (possibly a simple type variable)
then add A t r is also an indeterminate record type, likewise del A
r. There may be many different ways of expressing the same record
type.
-- Polymorphic record operations --
For each label A there are three functions
A :: Lacks A r => add A t r -> t
add A :: Lacks A r => t -> r -> add A t r
del A :: Rec r => r -> del A r
of extraction, extension and deletion:
Aj (A1 is v1, ..., An is vn) = vj
add A1 v1 (A2 is v2, ..., An is vn) = (A1 is v1, A2 is v2, ..., An is vn)
del A1 (A1 is v1, ..., An is vn) = (A2 is v2, ..., An is vn)
del B (A1 is v1, ..., An is vn) = (A1 is v1, ..., An is vn)
The type system protects against failure and name-clash by insisting
that a field exists before it is extracted, and is absent before it is
added. Deletion does not require the existence of the field as this is
more expressive.
Partial pattern matching is also possible:
> f (A1 is x1, ..., An is xn | y) = rhs
If xj has type tj, y has type u and rhs has type v then
f :: Lacks A1, ..., An u => add A1 t1 (... add An tn u) -> v
-- Copatterns --
Pattern matching can be duallized in a useful way for record
definition. The equations
> A1 x = rhs1
.
.
.
> An x = rhsn
(where rhsj has type tj) define record
x :: (A1 is t1, ..., An is tn)
with field Aj given by rhsj. This can be generalised to function
definition and nested copatterns.
-- Implementation --
We have implemented almost all of this proposal in a parser and type
checker for an extension of Gofer. This has been written up as a
Diploma dissertation. We will make the appropriate parts of this
available to those interested in the details in the near future.
