From HaskellWiki
Revision as of 16:41, 4 December 2013 by Atzeus (talk | contribs) (Introduction)

Jump to: navigation, search


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.


  • 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.


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.

Once we have declared some (pointers to) labels. We can write { x = 0 , y = "bla", z = False } as follows:

 x := 0 .| y .= "bla" .| z := False .| empty

(again it would be nicer to just write { x = 0 , y = "bla", z = False } , but currently not possible).


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) wheras 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 the same name (but starting with a capitol).

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