# Difference between revisions of "CTRex"

(→Labels) |
(→Row polymorphism) |
||

(20 intermediate revisions by the same user not shown) | |||

Line 33: | Line 33: | ||

− | Extensible records are records where we can add values (with corresponding label) to existing records. Suppose we have a record <hask> | + | Extensible records are records where we can add values (with corresponding label) to existing records. Suppose we have a record <hask>r = { x = 0, y = 0 }</hask>. If we have an extensible record system we can then add a value to this record: |

− | <haskell> extend z "Bla" | + | <haskell> extend z "Bla" r </haskell> |

Which gives <hask>{x = 0, y = 0 , z = "Bla"} </hask> | Which gives <hask>{x = 0, y = 0 , z = "Bla"} </hask> | ||

Line 44: | Line 44: | ||

Such extension is not possible with the <hask>Rec</hask> type above, the fields of the record are fixed. In the non-extensible record system in Haskell currently, the records are typed '''nominally''', which means that we see if two record types are the same by checking the '''names ''' of the records. For example, to check if the type <hask>HRec</hask> is the same as <hask>HRec2</hask>, we check if their names (HRec and HRec2) are equal. n | Such extension is not possible with the <hask>Rec</hask> type above, the fields of the record are fixed. In the non-extensible record system in Haskell currently, the records are typed '''nominally''', which means that we see if two record types are the same by checking the '''names ''' of the records. For example, to check if the type <hask>HRec</hask> is the same as <hask>HRec2</hask>, we check if their names (HRec and HRec2) are equal. n | ||

− | In an extensible record system the record type are '''structural'': two records have the same type if they carry the same fields with the same types, i.e. if they have the same row. This also means we do not have to declare the type of the record before using it. For example (in CTRex): | + | In an extensible record system the record type are '''structural''': two records have the same type if they carry the same fields with the same types, i.e. if they have the same row. This also means we do not have to declare the type of the record before using it. For example (in CTRex): |

Line 94: | Line 94: | ||

For this we need row polymorphism: we want to make the function <hask>f</hask> '''polymorphic''' in the rest of the row as follows: | For this we need row polymorphism: we want to make the function <hask>f</hask> '''polymorphic''' in the rest of the row as follows: | ||

<haskell> | <haskell> | ||

− | f :: | + | f :: ((r :! "x") ~ Double, (r :! "y") ~ Double) => |

− | -> Rec (" | + | Rec r -> Rec ("norm" ::= Double :| r) |

f r = norm := dist ((r.!x * r.!x) + (r.!y * r.!y)) .| r | f r = norm := dist ((r.!x * r.!x) + (r.!y * r.!y)) .| r | ||

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

− | + | Now the type <hask> f </hask> reads as follows: Given some record with row <hask>r</hask>where x and y have type Double, return a record in which x,y and dist have type Double and there are also some other fields described by row <hask>r</hask>. The type that GHC infers is even more general : | |

− | + | <haskell> | |

− | + | f :: (Floating t, (r :! "y") ~ t, (r :! "x") ~ t) => | |

+ | Rec r -> Rec (Extend "norm" (r :! "x") r) | ||

+ | </haskell> | ||

== Difference between Heterogenous maps and extensible records == | == Difference between Heterogenous maps and extensible records == | ||

Line 144: | Line 146: | ||

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

− | Hence we can only manipulate records and rows by the value and type level operations given in the CTRex module. | + | Hence, we can only manipulate records and rows by the value and type level operations given in the CTRex module. |

== Operations == | == Operations == | ||

Line 158: | Line 160: | ||

Here we use regular type syntax to denote the kinds of the closed type family <hask>Extend</hask> | Here we use regular type syntax to denote the kinds of the closed type family <hask>Extend</hask> | ||

− | 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 capital. | + | 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 capital. 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: | The following operations are available: | ||

+ | * Empty Record: | ||

+ | ** Value level: <hask>empty :: Rec Empty </hask> | ||

+ | ** Type level: <hask> Empty :: Row *</hask> | ||

* Extension: | * Extension: | ||

** Value level: <hask>extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r) </hask> | ** Value level: <hask>extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r) </hask> | ||

Line 176: | Line 181: | ||

** Type level: <hask> (:++) :: Row * -> Row * -> Row *</hask> | ** Type level: <hask> (:++) :: Row * -> Row * -> Row *</hask> | ||

− | * Rename (This operation can also be expressed using | + | * Rename (This operation can also be expressed using the above operations, but this looks nicer): |

** 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>Rename :: Symbol -> Symbol -> Row * -> Row * </hask> | ** Type level: <hask>Rename :: Symbol -> Symbol -> Row * -> Row * </hask> | ||

Line 262: | Line 267: | ||

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

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

− | (c,r'') = | + | (c,r'') = (r'.!x, r' .- x) |

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

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

Line 274: | Line 279: | ||

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

+ | |||

+ | As another use case for duplicate labels: consider implementing an interpreter for some embedded DSL, and you want to carry the | ||

+ | state of the variables in the an extensible record. Declaring a new variable in the embedded language then | ||

+ | causes us to extend the record. Since the embedded language allows shadowing (as most languages do), we can simply | ||

+ | extend the record, we do not have to jump through hoops to make sure there are no duplicate labels. Once the variable | ||

+ | goes out of scope, we restrict the record with the label to bring the old "variable" into scope. | ||

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

Line 282: | Line 293: | ||

The same thing for renaming: | The same thing for renaming: | ||

− | <haskell> | + | <haskell> |

+ | renameUnique :: (KnownSymbol l, KnownSymbol l', r :\ l') => | ||

+ | Label l -> Label l' -> Rec r -> Rec (Rename l l' 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: | 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> | + | <haskell> .+ :: Disjoint l r => Rec l -> Rec r -> Rec (l :++ r) </haskell> |

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

Line 301: | Line 314: | ||

− | Here <hask> CWit </hask> is a datatype that serves as a '''witness'' of a constraint. It's definition is as follows: | + | Here <hask> CWit </hask> is a datatype that serves as a '''witness''' of a constraint. It's definition is as follows: |

<haskell> data CWit (c :: * -> Constraint) = CWit </haskell> | <haskell> data CWit (c :: * -> Constraint) = CWit </haskell> | ||

− | We can use this to specify the constraint which should hold on the row, since this may be ambiguous. We can use this to implement, for example, some standard type classes on records: | + | We can use this to specify the constraint which should hold on the row, since this may be ambiguous. We can use this type class to implement, for example, some standard type classes on records: |

Line 451: | Line 464: | ||

Here we see that a record is actually just a map from string to the sequence of values. Notice that it is a sequence of values and not a single value, because the record may contain duplicate labels. | Here we see that a record is actually just a map from string to the sequence of values. Notice that it is a sequence of values and not a single value, because the record may contain duplicate labels. | ||

− | Extension is then rather simple, it simply prepends the value to the | + | Extension is then rather simple, it simply prepends the value to the sequence of values associated with the label: |

<haskell> | <haskell> | ||

Line 472: | Line 485: | ||

The use of <hask>unsafeCoerce</hask> here cannot go wrong because of the invariant. | The use of <hask>unsafeCoerce</hask> here cannot go wrong because of the invariant. | ||

+ | |||

+ | |||

+ | One might wonder why we use a Sequence here instead of a list, since we only query the head and prepend. This is implement record merge (.+) more efficiently since we can then use <hask>(><)</hask> (O(1)) instead of <hask>(++)</hask> (O(n)), as follows: | ||

+ | |||

+ | <haskell> | ||

+ | (.++) :: Rec l -> Rec r -> Rec (l :++ r) | ||

+ | (OR l) .++ (OR r) = OR $ M.unionWith (><) l r | ||

+ | </haskell> | ||

= Comparison with other approaches = | = Comparison with other approaches = | ||

Line 479: | Line 500: | ||

== HList records == | == HList records == | ||

− | The [http://hackage.haskell.org/package/HList HList package] provides [http://hackage.haskell.org/package/HList-0.3.0.1/docs/Data-HList-Record.html extensible] | + | The [http://hackage.haskell.org/package/HList HList package] provides [http://hackage.haskell.org/package/HList-0.3.0.1/docs/Data-HList-Record.html extensible records] build on heterogeneous lists. The differences with are as follows: |

* Rows are not sorted. This has the following downsides: | * Rows are not sorted. This has the following downsides: | ||

Line 513: | Line 534: | ||

* Record merge not available (?) | * Record merge not available (?) | ||

* Can pattern match on records(?) | * Can pattern match on records(?) | ||

− | * | + | * Nicer syntax |

* More (?) | * More (?) | ||

## Latest revision as of 08:53, 9 December 2013

## Contents

# Introduction

This page describes the design, usage and motivation for CTRex.

CTRex is a library for Haskell which implements extensible records using closed type families, datakinds 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.

# What the hell are extensible records?

## Basic extensible records

Records are values that contain other values, which are indexed by name (label). Examples of records are structs in c. In Haskell, we can currently declare record types as follows:

```
data HRec = HRec { x :: Int, y :: Bool, z :: String }
```

```
data HRec2 = HRec2 { p :: Bool, q :: Char }
```

Extensible records are records where we can add values (with corresponding label) to existing records. Suppose we have a record `r = { x = 0, y = 0 }`

. If we have an extensible record system we can then add a value to this record:

```
extend z "Bla" r
```

Which gives `{x = 0, y = 0 , z = "Bla"}`

A type-level record, i.e. the mapping of labels to types, such as `{x = Int, y = Bool, z = String }`

, is called a **row**.

Such extension is not possible with the `Rec`

type above, the fields of the record are fixed. In the non-extensible record system in Haskell currently, the records are typed **nominally**, which means that we see if two record types are the same by checking the **names ** of the records. For example, to check if the type `HRec`

is the same as `HRec2`

, we check if their names (HRec and HRec2) are equal. n

In an extensible record system the record type are **structural**: two records have the same type if they carry the same fields with the same types, i.e. if they have the same row. This also means we do not have to declare the type of the record before using it. For example (in CTRex):

```
x := 0 .| y := False .| empty
```

Constructs `{ x = 0, y = 0 }`

with type :

```
Rec ("x" ::= Int :| y ::= Bool .| Empty)
```

which means `{x = Int, y = Bool }`

This structural typing has the advantage that we can go from `{x = Int, y = Bool }`

to `{x = Int, y = Bool, z = String }`

by simply adding the field, we do not have to write a specific function to convert the two types (which would have been necessary with nominal record typing).

Because the associated type for a label is in the row of the record, labels can be used in different records for different types. This is currently not possible with standard records :

```
data X = X { x :: Int, y :: Bool }
data Y = Y { x :: Bool }
```

Will give a Multiple declarations of `x' error.

To summarize, extensible records have the following advantages:

- Labels can be used in different records for different types
- Records do not have to be declared before use.
- Structural typing eliminates the need for explicit conversion functions.

## Row polymorphism

Some extensible record systems, such as CTRex, support **row polymorphism**. This concept is best explained by an example, consider the following function (in CTRex):

```
f :: Rec ("x" ::= Double .| "y" ::= Double .| Empty)
-> Rec ("x" ::= Double .| "y" ::= Double .| "dist" ::= Double .| Empty)
f r = norm := dist ((r.!x * r.!x) + (r.!y * r.!y)) .| r
```

Where `(.!)`

is the function to get a value from a record. This function takes a record with row `{ x = Double, y = Double }`

and add returns the same record with a label `dist`

added, which carries the distance of the point `(x,y)`

from `(0,0)`

.

Now suppose we want to call this function with record `{ name = "PointA", x = 10, y = 10 }`

. This is not possible, because the row `{ name = String, x = Double, y = Double }`

and `{ x = Double, y = Double }`

are not the same.

For this we need row polymorphism: we want to make the function `f`

**polymorphic** in the rest of the row as follows:

```
f :: ((r :! "x") ~ Double, (r :! "y") ~ Double) =>
Rec r -> Rec ("norm" ::= Double :| r)
f r = norm := dist ((r.!x * r.!x) + (r.!y * r.!y)) .| r
```

Now the type `f`

reads as follows: Given some record with row `r`

where x and y have type Double, return a record in which x,y and dist have type Double and there are also some other fields described by row `r`

. The type that GHC infers is even more general :

```
f :: (Floating t, (r :! "y") ~ t, (r :! "x") ~ t) =>
Rec r -> Rec (Extend "norm" (r :! "x") r)
```

## Difference between Heterogenous maps and extensible records

A question that may arise after the previous section is: What is the difference between extensible records and heterogenous maps? A hetrogenous map is a map that can store values of different types, see for example the HMap package (blatant plug, my package ).

In heterogenous maps the type associated with a key is present **in the type of the key**. For example, in HMap a key has type `Key x a`

where a is the type of the things we can store at this key, for example `Int`

.

In extensible records, the type associated with a key (now called label) is stored **in the type of the record**, i.e. in its row. The row states, for example, that `x`

is associated with `Int`

, The label itself does not hold any information on the associated type. In fact, the associated type may differ between records.

This means that if a record has `x ::= Int`

in its row, then we are **sure** that this record has a value of type `Int`

for `x`

. In a hetrogenous map, we can never be sure if a key is present in a map, i.e. `lookup x m`

may return `Maybe`

.

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

In the remainder of this wiki page we write `x`

instead of `Label :: Label "x"`

, assuming we have already declared `x = Label :: Label "x"`

## Rows and records

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 :: Symbol -> * -> Row * -> Row *
```

Here we use regular type syntax to denote the kinds of the closed type family `Extend`

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 capital. 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:

- Empty Record:
- Value level:
`empty :: Rec Empty`

- Type level:
`Empty :: Row *`

- Value level:
- Extension:
- Value level:
`extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)`

- Type level:
`Extend :: Symbol -> * -> Row * -> Row *`

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

- Type level:
`(:!) :: Row * -> Symbol -> *`

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

- Type level:
`(:-) Row * -> Symbol -> Row *`

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

- Type level:
`(:++) :: Row * -> Row * -> Row *`

- Value level:

- Rename (This operation can also be expressed using the above operations, but this looks nicer):
- Value level:
`rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)`

- Type level:
`Rename :: Symbol -> Symbol -> 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:

```
(:|) :: RowOp * -> 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.

Also notice that this means that this sugar is also available when writing types:

```
Rec ("p" ::<-| "z" :| RUp :| "z" ::= Bool :| "x" ::= Double :| "y" ::= Char :| Empty)
```

is the type exactly corresponding to:

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

and equivalent to

```
Rename "p" "z" (Extend "z" Bool (Extend x Double (Extend "x" Int Empty)))
```

and of course equivalent to:

```
"p" ::= Bool :| "x" ::= Double :| "y" ::= Int :| Empty
```

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

```
f :: Rec ("x" ::= Int :| r) -> (Rec ("x" ::= Bool .| r)
```

and we want to write the following function:

```
g :: Rec r -> Rec ("p" ::= String .| r)
g r = let r' = f (x := 10 .| r)
(c,r'') = (r'.!x, 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.

As another use case for duplicate labels: consider implementing an interpreter for some embedded DSL, and you want to carry the state of the variables in the an extensible record. Declaring a new variable in the embedded language then causes us to extend the record. Since the embedded language allows shadowing (as most languages do), we can simply extend the record, we do not have to jump through hoops to make sure there are no duplicate labels. Once the variable goes out of scope, we restrict the record with the label to bring the old "variable" into scope.

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 function 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:

```
renameUnique :: (KnownSymbol l, KnownSymbol l', r :\ l') =>
Label l -> Label l' -> Rec r -> Rec (Rename l l' 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.

## Constrained record operations

If some constraint c holds for all types in the row of a record, then the methods in the following type class are available:

```
class Forall (r :: Row *) (c :: * -> Constraint) where
rinit :: CWit c -> (forall a. c a => a) -> Rec r
erase :: CWit c -> (forall a. c a => a -> b) -> Rec r -> [(String,b)]
eraseZip :: CWit c -> (forall a. c a => a -> a -> b) -> Rec r -> Rec r -> [(String,b)]
```

Here `CWit`

is a datatype that serves as a **witness** of a constraint. It's definition is as follows:

```
data CWit (c :: * -> Constraint) = CWit
```

We can use this to specify the constraint which should hold on the row, since this may be ambiguous. We can use this type class to implement, for example, some standard type classes on records:

```
instance (Forall r Show) => Show (Rec r) where
show r = "{ " ++ meat ++ " }"
where meat = intercalate ", " binds
binds = map (\(x,y) -> x ++ "=" ++ y) vs
vs = erase (CWit :: CWit Show) show r
instance (Forall r Eq) => Eq (Rec r) where
r == r' = and $ map snd $ eraseZip (CWit :: CWit Eq) (==) r r'
instance (Forall r Bounded) => Bounded (Rec r) where
minBound = rinit (CWit :: CWit Bounded) minBound
maxBound = rinit (CWit :: CWit Bounded) maxBound
```

We could make an interface to do even more general stuff on (pairs of) constrained records, but I have yet to find a use case for this.

## Type errors

Here we list which type errors are reported when using CTRex:

- Record does not have field

```
typerr1 = (x := 1 .| empty) .! y + 1
```

```
No instance for (Num (Records.NoSuchField "y"))
arising from a use of ‛+’
In the expression: (x := 1 .| empty) .! y + 1
```

Somewhat unsatisfactory, the expression:

```
typerr1 = (x := 1 .| empty) .! y
```

does not immediatly give a type error. Instead its type is:

```
typerr1 :: Records.NoSuchField "y"
```

- Record does not lack field

```
x :!= 1 .| x := 1 .| empty
```

Gives the error

```
Error:
Couldn't match type ‛'Records.LabelNotUnique "x"’
with ‛'Records.LabelUnique "x"’
In the first argument of ‛(.|)’, namely ‛x :!= 1’
```

- Records not disjoint

```
notdisjoint = let p = x := 2 .| empty
q = x := 2 .| empty
in p .+ q
```

Gives the error:

```
Couldn't match type ‛'Records.Duplicate "x"’
with ‛'Records.IsDisjoint’
Expected type: 'Records.IsDisjoint
Actual type: Records.DisjointR
('Records.R '["x" 'Records.:-> a4])
('Records.R '["x" 'Records.:-> a])
In the expression: p .+ q
```

# Implementation

The basis of the implementation is a label-type pair, which is represented by the following (unexported) datakind:

```
data LT a = Symbol :-> a
```

## Rows

A row is then simply a list of such label-type pairs:

```
newtype Row a = R [LT a] -- constructor not exported
```

Notice that the constructor is not exported, so if we ask for the type of

```
origin2 = y := 0 .| x := 0 .| empty
```

we get:

```
origin2
:: Rec ('Records.R '["x" 'Records.:-> Double, "y" 'Records.:-> Double])
```

Here the implementation of Row leaks a bit. The user cannot write down this type, since Records.R is not exported, and neither is :->.

Instead the user should not worry about the implementation and write the type in terms of operations (or let the type be inferred), i.e. :

```
origin2 :: Rec ("x" ::= Double :| "y" ::= Double :| Empty)
```

Operations on rows are implemented using closed type families. The list of label-type pairs in the row are always sorted. Each operation defined on Rows maintains this invariant. We are sure that no operations which violate this invariant can be created by the user, since the constructor is not exported.

To keep the list of label-type pairs sorted, we use the built-in closed type family :

```
<.=? :: Symbol -> Symbol -> Bool
```

Which compares two symbols at compile time and gives a Bool datakind telling us wether the left is <= than the right.

For instance, row extension is implemented as follows:

```
type family Extend :: Symbol -> * -> Row * -> Row * where
Extend l a (R x) = R (Inject (l :-> a) x)
type family Inject :: LT * -> [LT *] -> [LT *] where
Inject (l :-> t) '[] = (l :-> t ': '[])
Inject (l :-> t) (l' :-> t' ': x) =
Ifte (l <=.? l')
(l :-> t ': l' :-> t' ': x)
(l' :-> t' ': Inject (l :-> t) x)
```

## Records

To implement the records we introduce the following datatype which can contain anything:

```
data HideType where
HideType :: a -> HideType
```

A record is then defined as follows:

```
-- | A record with row r.
data Rec (r :: Row *) where
OR :: HashMap String (Seq HideType) -> Rec r
```

Here we see that a record is actually just a map from string to the sequence of values. Notice that it is a sequence of values and not a single value, because the record may contain duplicate labels.

Extension is then rather simple, it simply prepends the value to the sequence of values associated with the label:

```
extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)
extend (show -> l) a (OR m) = OR $ M.insert l v m
where v = HideType a <| M.lookupDefault S.empty l m
```

To safely convert back from Hidetype, we maintain the following invariant: The i-th value in the sequence associated with "x" has the i-th type associated with "x" in the row. This invariant is maintained by all operations on rows and records. Since the constructors of record and row are not exported, we know that it is impossible to declare new operations on records and rows that violate this invariant. A same kind of trick is used HMap.

Since we know that the actual type of the value in Hidetype is given in the row, we can safely convert it back:

```
(.!) :: KnownSymbol l => Rec r -> Label l -> r :! l
(OR m) .! (show -> a) = x'
where x S.:< t = S.viewl $ m M.! a
-- notice that this is safe because of invariant
x' = case x of HideType p -> unsafeCoerce p
```

The use of `unsafeCoerce`

here cannot go wrong because of the invariant.

One might wonder why we use a Sequence here instead of a list, since we only query the head and prepend. This is implement record merge (.+) more efficiently since we can then use `(><)`

(O(1)) instead of `(++)`

(O(n)), as follows:

```
(.++) :: Rec l -> Rec r -> Rec (l :++ r)
(OR l) .++ (OR r) = OR $ M.unionWith (><) l r
```

# Comparison with other approaches

Here we compare with other approaches.

## HList records

The HList package provides extensible records build on heterogeneous lists. The differences with are as follows:

- Rows are not sorted. This has the following downsides:
- Compile time operations, such as reordering the labels and checking for duplicate labels is costly (at compile time) link
`{x = 0, y = 0 }`

and`{ y = 0, x = 0 }`

do not have the same type. Hence, is we give a type declaration for the first and want to put in the latter, we need to call a manual conversion function.

- Constrained row operations are less convenient, since
- the Record newtype needs to be unwrapped, and
- there is no definition provided to create instances of applyAB that work on
`LVPair l a`

from instances that work on just`a`

- however there similarities between the two

CTRex function | HList function(s) |
---|---|

rinit | hReplicate |

erase | hMapOut |

eraseZip | hZip with hMapOut |

- Currently, the run time complexity of extend, restriction and lookup is O(n), versus O(log n) for CTRex. Proposals have been done to make this faster paper.
- Duplicate labels are disallowed in HList.
- HList has nicer support for writing labels

## Trex (Hugs)

The Haskell interpreter hugs supports a type system extension that allows extensible records. The differences are as follows:

- Constrained row operations are not available(?)
- Duplicate labels are disallowed
- Record merge not available (?)
- Can pattern match on records(?)
- Nicer syntax
- More (?)

## More

More to come! Please add stuff!

# Wishlist

- Nicer syntax for Label :: Label "x"
- Nice syntax for records, i.e. { x = 0, y = 0 }.
- Type level Show thing, so that we can pretty-print types, and the implementation of things such as row does not leak.
- The ability to pattern match on records.
- Type level
`error`

so that we can generate clearer error messages earlier.