# Difference between revisions of "CTRex"

Line 44: | Line 44: | ||

A type-level record, i.e. the mapping of labels to types is called a '''row'''. | A type-level record, i.e. the mapping of labels to types is called a '''row'''. | ||

− | A record has the following type: <hask> Rec (r :: Row *) </hask>, where r is the row. | + | A record has the following type: <hask> Rec (r :: Row *) </hask>, where r is the row. |

The constructors of <hask>Rec</hask> as well as the constructors of the datakind <hask>Row</hask> are not exported. | The constructors of <hask>Rec</hask> as well as the constructors of the datakind <hask>Row</hask> are not exported. | ||

Line 80: | Line 80: | ||

** Value level: <hask>rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r) </hask> | ** Value level: <hask>rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r) </hask> | ||

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

− | |||

== Syntactic sugar == | == Syntactic sugar == | ||

− | + | We provide some handy declarations which allow us to chain operations with nicer syntax. For example we can write: | |

<haskell> | <haskell> | ||

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

Line 94: | Line 93: | ||

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

</haskell> | </haskell> | ||

+ | |||

+ | For this we have a GADT datatype RecOp which takes two arguments: | ||

+ | |||

+ | * c, the type of the constaint that should hold on the input row. | ||

+ | * rop, the row operation (see below). with the following constructors: | ||

+ | |||

+ | This datatype has the following constructors, all of which are sugar for record operations. | ||

+ | |||

+ | * <hask>(:<-) :: Label -> a -> RecOp (HasType l a) RUp</hask> Record update. Sugar for update. | ||

+ | * <hask>(:=) :: KnownSymbol l => Label l -> a -> RecOp NoConstr (l ::= a)</hask> Record extension. Sugar for extend. | ||

+ | * <hask>(:!=) :: KnownSymbol l => Label l -> a -> RecOp (Lacks l) (l ::= a)</hask> Record extension, without shadowing. Sugar for extendUnique. See the section on duplicate labels. | ||

+ | * <hask>(:<-|) :: (KnownSymbol l, KnownSymbol l') => Label l' -> Label l -> RecOp NoConstr (l' ::<-| l)</hask> Record label renaming. Sugar for rename. | ||

+ | * <hask>(:<-!) :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l' -> Label l -> RecOp (Lacks l') (l' ::<-| l)</hask> Record label renaming. Sugar for renameUnique. See the section on duplicate labels. | ||

+ | |||

+ | |||

+ | On the type level the same pattern again arises, we have a datakind (RowOp *) with the following constructors: | ||

+ | |||

+ | * <hask>RUp :: RowOp * </hask> Row operation for<hask>(:<-)</hask>. Identitity row operation. | ||

+ | * <hask>(::=) :: Symbol -> * -> RowOp * </hask> Row extension operation. Sugar for Extend. Type level operation for <hask>(:=)</hask> and <hask>(:!=)</hask> | ||

+ | * <hask>::<-|</hask> Row renaming. Sugar for Rename. Type level operation for <hask>(:<-|)</hask> and <hask>(:<-!)</hask> | ||

+ | |||

+ | We then have a type level operation to perform a row operation: | ||

+ | |||

+ | <haskell> type family (x :: RowOp *) :| (r :: Row *) :: Row * </haskell> | ||

+ | |||

+ | And a value level operation to perform a record operation: | ||

+ | |||

+ | <haskell> (.|) :: c r => RecOp c ro -> Rec r -> Rec (ro :| r) </haskell> | ||

+ | |||

+ | Notice that the constraint from the record operation is placed on the input row. | ||

+ | |||

+ | |||

+ | == Duplicate labels, and lacks == | ||

+ | |||

+ | Rows and records can contain duplicate labels as described in the paper [http://legacy.cs.uu.nl/daan/download/papers/scopedlabels.pdf Extensible records with scoped labels] by Daan Leijen. | ||

+ | |||

+ | Hence we can write: | ||

+ | |||

+ | <haskell> z = x := 10 .| x := "bla" .| Empty :: Rec ("x" ::= Int :| "x" ::= String :| Empty) | ||

+ | </haskell> | ||

+ | |||

+ | We can recover the information on the second instance of x by removing x: | ||

+ | <haskell> z .- x :: Rec ("x" ::= String :| Empty) | ||

+ | |||

+ | |||

+ | The motivation for this is as follows: Suppose we have a function <hask> f :: Rec ("x" ::= Int :| r) -> (Rec ("x" ::= Bool .| r)</hask> and we want to write the following function: | ||

+ | |||

+ | <haskell> | ||

+ | g :: Rec r -> Rec ("p" ::= String .| r) | ||

+ | g r = let r' = f (x := 10 .| r) | ||

+ | (c,r'') = decomp r x | ||

+ | v = if c then "Yes" else "Nope" | ||

+ | in p := v .| r'' | ||

+ | </haskell> | ||

+ | |||

+ | If it was not possible for records and rows to contain duplicate label the type of g would be: | ||

+ | |||

+ | <haskell> | ||

+ | g :: r :\ "x" => Rec r -> Rec ("p" ::= String .| r) | ||

+ | </haskell> | ||

+ | |||

+ | The constraint <hask> r :\ "x" </hask> reads as r lacks "x". The constraint leaks the implementation of g. We only use "x" internally in g , There is no reason for this constraint to hold in the rest of the program. | ||

+ | |||

+ | However, in other situations, duplicate labels may be undesired, for instance because we want to be sure that we do not hide previous information. For this reason we also provide the already introduced `lacks` constraint. | ||

+ | |||

+ | We also provide a handy record extension that has this constraint, so that you do not have to add types yourself: | ||

+ | |||

+ | <haskell> extendUnique :: (KnownSymbol l, l :\ r) => Label l -> a -> Rec r -> Rec (Extend l a r) </haskell> | ||

+ | |||

+ | The same thing for renaming: | ||

+ | <haskell> extendUnique :: (KnownSymbol l, r :\ l) => Label l -> a -> Rec r -> Rec (Extend l a r) </haskell> | ||

+ | |||

+ | We also provide a constraint to test that two Rows are '''disjoint'''. Corresponding to this we also provide a function to merge with this constraint: | ||

+ | |||

+ | <haskell> .+ :: Disjoint l r => Rec l -> Rec r -> Rec (l :+ r) </haskell> | ||

+ | |||

+ | Notice that .+ is commutative, while .++ is not. |

## Revision as of 18:03, 4 December 2013

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

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

- Value level:
- 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)`

- Type 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:
`type family Rename (l :: Symbol) (l' :: Symbol) (r :: Row *) :: Row *`

- Value level:

## Syntactic sugar

We provide some handy declarations which allow us to chain operations with nicer syntax. For example we can 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
```

For this we have a GADT datatype RecOp which takes two arguments:

- c, the type of the constaint that should hold on the input row.
- rop, the row operation (see below). with the following constructors:

This datatype has the following constructors, all of which are sugar for record operations.

`(:<-) :: Label -> a -> RecOp (HasType l a) RUp`

Record update. Sugar for update.`(:=) :: KnownSymbol l => Label l -> a -> RecOp NoConstr (l ::= a)`

Record extension. Sugar for extend.`(:!=) :: KnownSymbol l => Label l -> a -> RecOp (Lacks l) (l ::= a)`

Record extension, without shadowing. Sugar for extendUnique. See the section on duplicate labels.`(:<-|) :: (KnownSymbol l, KnownSymbol l') => Label l' -> Label l -> RecOp NoConstr (l' ::<-| l)`

Record label renaming. Sugar for rename.`(:<-!) :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l' -> Label l -> RecOp (Lacks l') (l' ::<-| l)`

Record label renaming. Sugar for renameUnique. See the section on duplicate labels.

On the type level the same pattern again arises, we have a datakind (RowOp *) with the following constructors:

`RUp :: RowOp *`

Row operation for`(:<-)`

. Identitity row operation.`(::=) :: Symbol -> * -> RowOp *`

Row extension operation. Sugar for Extend. Type level operation for`(:=)`

and`(:!=)`

`::<-|`

Row renaming. Sugar for Rename. Type level operation for`(:<-|)`

and`(:<-!)`

We then have a type level operation to perform a row operation:

```
type family (x :: RowOp *) :| (r :: Row *) :: Row *
```

And a value level operation to perform a record operation:

```
(.|) :: c r => RecOp c ro -> Rec r -> Rec (ro :| r)
```

Notice that the constraint from the record operation is placed on the input row.

## Duplicate labels, and lacks

Rows and records can contain duplicate labels as described in the paper Extensible records with scoped labels by Daan Leijen.

Hence we can write:

```
z = x := 10 .| x := "bla" .| Empty :: Rec ("x" ::= Int :| "x" ::= String :| Empty)
```

We can recover the information on the second instance of x by removing x:

```
z .- x :: Rec ("x" ::= String :| Empty)
The motivation for this is as follows: Suppose we have a function <hask> f :: Rec ("x" ::= Int :| r) -> (Rec ("x" ::= Bool .| r)</hask> and we want to write the following function:
<haskell>
g :: Rec r -> Rec ("p" ::= String .| r)
g r = let r' = f (x := 10 .| r)
(c,r'') = decomp r x
v = if c then "Yes" else "Nope"
in p := v .| r''
```

If it was not possible for records and rows to contain duplicate label the type of g would be:

```
g :: r :\ "x" => Rec r -> Rec ("p" ::= String .| r)
```

The constraint `r :\ "x"`

reads as r lacks "x". The constraint leaks the implementation of g. We only use "x" internally in g , There is no reason for this constraint to hold in the rest of the program.

However, in other situations, duplicate labels may be undesired, for instance because we want to be sure that we do not hide previous information. For this reason we also provide the already introduced `lacks` constraint.

We also provide a handy record extension that has this constraint, so that you do not have to add types yourself:

```
extendUnique :: (KnownSymbol l, l :\ r) => Label l -> a -> Rec r -> Rec (Extend l a r)
```

The same thing for renaming:

```
extendUnique :: (KnownSymbol l, r :\ l) => Label l -> a -> Rec r -> Rec (Extend l a r)
```

We also provide a constraint to test that two Rows are **disjoint**. Corresponding to this we also provide a function to merge with this constraint:

```
.+ :: Disjoint l r => Rec l -> Rec r -> Rec (l :+ r)
```

Notice that .+ is commutative, while .++ is not.