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.

What are extensible records?

A record is just a collection of label-value pairs. For example: { x = 0 , y = "bla", z = False }

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