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.