CTRex

Introduction

This page will describe the design, usage and motivation for CTRex.

CTRex is a library for Haskell which implements extensible records using closed type families and type literals. It does not use overlapping instances.

Features:

• Row-polymorphism

• Support for scoped labels (i.e. duplicate labels) and non-scoped labels (i.e. the lacks predicate on rows).

• The value level interface and the type level interface correspond to each other.

• The order of labels (except for duplicate labels) does not matter. I.e. {x = 0, y = 0} and {y = 0, x = 0} have the same type.

• Syntactic sugar on the value level as well as type level.

• If all values in a record satisfy a constraint such as Show, then we are able to do operations on all fields in a record, if that operation only requires that the constraint is satisfied. In this way we can create instances such as Forall r Show => Show (Rec r). This is available to the application programmer as well.

• Fast extend, lookup and restriction (all O(log n)) using HashMaps.

The haddock documentation is available here.

Programmer interface

Labels

Labels (such as x,y and z) in CTRex are type level symbols (i.e. type level strings). We can point to a label by using the label type:

data Label (s :: Symbol) = Label

For example, we can declare shorthands for pointing at the type level symbol "x", "y" and "z" as follows.

x = Label :: Label "x" 
y = Label :: Label "y" 
z = Label :: Label "z"

Of course it would be much nicer to just write `x instead of Label :: Label "x" but this is currently not available. This may change in the future.

Rows and records

A type-level record, i.e. the mapping of labels to types is called a row. A record has the following type: Rec (r :: Row *), where r is the row.

The constructors of Rec as well as the constructors of the datakind Row are not exported.

Hence we can only manipulate records and rows by the value and type level operations given in the CTRex module.

Operations

For all operations available on records, the value level interface and the type level interface correspond to each other.

For example, the value level operation for extending a record (adding a field) has type

 extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)

whereas the type level operation for adding a field has type

 Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row *

In this way each value level operation (that changes the type) has a corresponding type level operation with a similar name. If the value level operation is not infix the type level operation is named the same, but starting with a capitol. And if the value level operation is an operator, is starts with a '.' and the type level operation starts with a ':'.

The following operations are available:

• Extension:

Value level:

extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r) <haskell>
Type level: <haskell>  Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row *

• Selection:

Value level:

 (.!) :: KnownSymbol l => Rec r -> Label l -> r :! l <haskell>
Type level: <haskell> type family (r :: Row *) :! (t :: Symbol) :: *

• Restriction:

Value level:

(.-) :: KnownSymbol l =>  Rec r -> Label l -> Rec (r :- l)<haskell>
Type level: <haskell> type family (r :: Row *) :- (s :: Symbol)  :: Row *

• Record merge :

Type level:

 type family (l :: Row *) :++  (r :: Row *)  :: Row *

Value level:

(.++) :: Rec l -> Rec r -> Rec (l :++ r)<haskell>
* Rename (This operation can also be expressed using restriction, selection and selection, but this looks nicer):
Value level: <haskell>rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r) <haskell>
Type level: <haskell>type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row *

Syntactic sugar

 
p :<-| z .| y :<- 'b' .| z :!= False .| x := 2 .| y := 'a' .| empty

instead of

 
 rename z p $ update y 'b' $ extendUnique z False $ extend x 2 $ extend y 'a' empty