Difference between revisions of "CTRex"
(→Duplicate labels, and lacks) 
(→Duplicate labels, and lacks) 

Line 277:  Line 277:  
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 remove the label again 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. 
Revision as of 10:02, 6 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:
 Rowpolymorphism
 Support for scoped labels (i.e. duplicate labels) and nonscoped 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 asForall 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 x = { x = 0, y = 0 }
. If we have an extensible record system we can then add a value to this record:
extend z "Bla" x
Which gives {x = 0, y = 0 , z = "Bla"}
A typelevel 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 nonextensible 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 :: Rec ("x" ::= Double . "y" ::= Double . r)
> Rec ("x" ::= Double . "y" ::= Double . "dist" ::= Double . r)
f r = norm := dist ((r.!x * r.!x) + (r.!y * r.!y)) . r
Notice that in CTRex, the only difference with the previous version is that we replaced Empty
with r
in the type. Now the type f
reads as follows: Given some record where x and y have type Double and there are some other fields with types described by row r
, return a record in which x,y and dist have type Double and there are also some other fields described by row r
.
Of course, since f
cannot know anything about the the rest of the row, it can do nothing else than just leave it alone or replace it with undefined
.
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 remove the label again 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 labeltype pair, which is represented by the following (unexported) datakind:
data LT a = Symbol :> a
Rows
A row is then simply a list of such labeltype 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 labeltype 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 labeltype pairs sorted, we use the builtin 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 list 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 ith value in the sequence associated with "x" has the ith 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.
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 justa
 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(?)
 Nice 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 prettyprint 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.