Difference between revisions of "CTRex"

From HaskellWiki
Jump to navigation Jump to search
Line 9: Line 9:
 
* Row-polymorphism
 
* Row-polymorphism
 
* Support for scoped labels (i.e. duplicate labels) '''and''' non-scoped labels (i.e. the lacks predicate on rows).
 
* 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 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'''.
 
* 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
+
* Syntactic sugar on the value level as well as type level.
<haskell>
 
p :<-| z .| y :<- 'b' .| z :!= False .| x := 2 .| 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 satified. 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.
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 ==
Line 45: Line 36:
 
<haskell> x := 0 .| y .= "bla" .| z := False .| empty </haskell>
 
<haskell> x := 0 .| y .= "bla" .| z := False .| empty </haskell>
 
(again it would be nicer to just write <code> { x = 0 , y = "bla", z = False } </code>, but currently not possible).
 
(again it would be nicer to just write <code> { x = 0 , y = "bla", z = False } </code>, but currently not possible).
  +
  +
== Extension ==
  +
 
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).
  +
  +
  +
== Syntactic sugar ==
  +
 
<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>

Revision as of 16:40, 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.
  • 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 satified. 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).

Extension

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


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