# CTRex

## Contents

# 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)`

- Value level:

Type level: `Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row *`

- Selection:
- Value level:
`(.!) :: KnownSymbol l => Rec r -> Label l -> r :! l`

- Type level:
`type family (r :: Row *) :! (t :: Symbol) :: *`

- Value level:

- Restriction:

- Value level:
`(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r :- l)`

- Type level:
`type family (r :: Row *) :- (s :: Symbol) :: Row *`

- Value level:

- Record merge :

`**Type level: ``type family (l :: Row *) :++ (r :: Row *) :: Row *`

- Value level:
`(.++) :: Rec l -> Rec r -> Rec (l :++ r)`

- Value level:
- Rename (This operation can also be expressed using restriction, selection and selection, but this looks nicer):

Value level: `rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)`

Type level: <hask>type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row *</haskell>

## 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
```