# Difference between revisions of "CTRex"

(→Introduction) |
(→Introduction) |
||

Line 5: | Line 5: | ||

CTRex is a library for Haskell which implements extensible records using closed type families and type literals. It does '''not''' use overlapping instances. |
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? == |
||

+ | Features: |
||

− | A record is just a collection of label-value pairs. For example: |
||

+ | * Row-polymorphism |
||

− | <code> { x = 0 , y = "bla", z = False } </code> |
||

+ | * 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. For example, the value level operation for extending a record (adding a field) has type <hask> extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r) </hask> wheras the type level operation for adding a field has type <hask> Extend (l :: Symbol) (a :: *) (r :: Row *) :: Row *</hask>. 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). |
||

+ | * 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 to write |
||

+ | <haskell> |
||

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

+ | </haskell> |
||

+ | |||

+ | instead of |
||

+ | |||

+ | <haskell> |
||

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

+ | </haskell> |
||

+ | |||

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

+ | |||

+ | == 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: |
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: |

## Revision as of 16:37, 4 December 2013

# 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. 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). - 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 to write

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

- 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 satifies. In this way we can create instanstances such as`Forall r Show => Show (Rec r)`

. This is available to the application programmer as well.

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

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