Data.OpenRecords

This module implements extensible records using closed type famillies.

See the examples.

Lists of (label,type) pairs are kept sorted thereby ensuring that { x = 0, y = 0 } and { y = 0, x = 0 } have the same type.

In this way we can implement standard type classes such as Show, Eq, Ord and Bounded for open records, given that all the elements of the open record satify the constraint.

Types and constraints

data Label s

A label

Constructors

Label

Instances

KnownSymbol s => Show (Label s)

class KnownSymbol n

This class gives the integer associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: 4.7.0.0

Minimal complete definition

symbolSing

data Rec r

A record with row r.

Instances

Forall r Bounded => Bounded (Rec r)

Forall r Eq => Eq (Rec r)

(Eq (Rec r), Forall r Ord) => Ord (Rec r)

(Labels r, Forall r Show) => Show (Rec r)

data Row a

The kind of rows. This type is only used as a datakind. A row is a typelevel entity telling us which symbols are associated with which types.

Construction

empty :: Rec Empty

The empty record

type family Empty :: Row *

Type level variant of empty

Equations

Empty = R []

Extension

extend :: KnownSymbol l => Label l -> a -> Rec r -> Rec (Extend l a r)

Record extension. The row may already contain the label, in which case the origin value can be obtained after restriction (.-) with the label.

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

Record extension without shadowing. The row may not already contain label l.

type family Extend l a r :: Row *

Type level operations of extend and extendUnique

Equations

Extend l a (R x) = R (Inject (l :-> a) x)

Renaming

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

Rename a label. The row may already contain the new label , in which case the origin value can be obtained after restriction (.-) with the new label.

renameUnique :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l -> Label l' -> Rec r -> Rec (Rename l l' r)

Rename a label. The row may not already contain the new label.

type family Rename l l' r :: Row *

Type level operation of rename and renameUnique

Equations

Rename l l' r = Extend l' (r :! l) (r :- l)

Restriction

(.-) :: KnownSymbol l => Rec r -> Label l -> Rec (r :- l) infix 8

Record restriction. Delete the label l from the record.

type family r :- s :: Row *

Type level operation of .-

Equations

(R r) :- l = R (Remove l r)

Update

update :: KnownSymbol l => Label l -> (r :! l) -> Rec r -> Rec r

Update the value associated with the label.

Query

(.!) :: KnownSymbol l => Rec r -> Label l -> r :! l

Record selection

type family r :! t :: * infixl 6

Type level operation of .!

Equations

(R r) :! l = Get l r

Combine

Union

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

Record union (not commutative)

type family l :++ r :: Row *

Type level operation of .++

Equations

(R l) :++ (R r) = R (Merge l r)

Disjoint union

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

Record disjoint union (commutative)

type family l :+ r :: Row *

Type level operation of .+

Equations

(R l) :+ (R r) = R (Merge l r)

Row constraints

type (:\) r l = LacksP l r ~ LabelUnique l

Does the row lack (i.e. it has not) the specified label?

type Disjoint l r = DisjointR l r ~ IsDisjoint

Are the two rows disjoint? (i.e. their sets of labels are disjoint)

class Labels r where

Methods

labels :: Rec r -> [String]

class Forall r c where

If the constaint c holds for all elements in the row r, then the methods in this class are available.

Methods

rinit :: CWit c -> (forall a. c a => a) -> Rec r

Given a default value a, wherea can be instantiated to each type in the row, create a new record in which all elements carry this default value.

erase :: CWit c -> (forall a. c a => a -> b) -> Rec r -> [b]

Given a function (a -> b) where a can be instantiated to each type in the row, apply the function to each element in the record and collect the result in a list.

eraseZip :: CWit c -> (forall a. c a => a -> a -> b) -> Rec r -> Rec r -> [b]

Given a function (a -> a -> b) where a can be instantiated to each type of the row, apply the function to each pair of values that can be obtained by indexing the two records with the same label and collect the result in a list.

data CWit c

A witness of a constraint. For use like this rinit (CWit :: CWit Bounded) minBound

data FWit f

Row only operations

Syntactic sugar

data RecOp c rowOp where

Here we provide a datatype for denoting record operations. Use .| to actually apply the operations.

This allows us to chain operations with nicer syntax. For example we can write:

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

Which results in:

{ p=False, x=2, y='b' }

Without this sugar, we would have written it like this:

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

:<-

Record update. Sugar for update.

:=

Record extension. Sugar for extend.

:!=

Record extension, without shadowing. Sugar for extendUnique.

:<-|

Record label renaming. Sugar for rename.

:<-!

Record label renaming. Sugar for renameUnique.

Constructors

(:<-) :: KnownSymbol l => Label l -> a -> RecOp (HasType l a) RUp infix 5

(:=) :: KnownSymbol l => Label l -> a -> RecOp NoConstr (l ::= a) infix 5

(:!=) :: KnownSymbol l => Label l -> a -> RecOp (Lacks l) (l ::= a) infix 5

(:<-|) :: (KnownSymbol l, KnownSymbol l') => Label l' -> Label l -> RecOp NoConstr (l' ::<-| l)

(:<-!) :: (KnownSymbol l, KnownSymbol l', r :\ l') => Label l' -> Label l -> RecOp (Lacks l') (l' ::<-| l)

data RowOp a where

Type level datakind corresponding to RecOp. Here we provide a datatype for denoting row operations. Use :| to actually apply the type level operation.

This allows us to chain type level operations with nicer syntax. For example we can write:

"p" ::<-| "z" :| RUp :| "z" ::= Bool :| "x" ::= Double :| "y" ::= Char :| Empty

As the type of the expression:

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

Without this sugar, we would have written it like this:

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

Of course, we can also just write:

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

instead, doing the computation ourselves, or even let the type infer.

RUp

Type level equivalent of :<-. Is the identity Row Operation.

::=

Type level equivalent of :=. Row extension. Sugar for Extend.

::<-|

Type level equivalent of :<-|. Row label renaming. Sugar for Rename.

Constructors

RUp :: RowOp a

(::=) :: Symbol -> a -> RowOp a infix 5

(::<-|) :: Symbol -> Symbol -> RowOp a infix 5

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

Apply an operation to a record.

type family x :| r :: Row * infixr 4

Apply a (typelevel) operation to a row. Type level operation of .|

Equations

RUp :| r = r

(l ::= a) :| r = Extend l a r

(l' ::<-| l) :| r = Rename l l' r