Difference between revisions of "CTRex"
(71 intermediate revisions by 2 users not shown) | |||
Line 3: | Line 3: | ||
This page describes the design, usage and motivation for [https://github.com/atzeus/CTRex CTRex]. |
This page describes the design, usage and motivation for [https://github.com/atzeus/CTRex CTRex]. |
||
− | CTRex is a library for Haskell which implements extensible records using closed type families and type literals. It does '''not''' use overlapping instances. |
+ | 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: |
Features: |
||
Line 23: | Line 23: | ||
The haddock documentation is available [http://homepages.cwi.nl/~ploeg/openrecdocs/Records.html here]. |
The haddock documentation is available [http://homepages.cwi.nl/~ploeg/openrecdocs/Records.html here]. |
||
− | + | = What the hell are extensible records? = |
|
− | + | == Basic extensible records == |
|
− | Records are values that contain other values, which are indexed by name. Examples of records are structs in c. In Haskell, we can currently declare |
+ | 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: |
<haskell> data HRec = HRec { x :: Int, y :: Bool, z :: String } </haskell> |
<haskell> data HRec = HRec { x :: Int, y :: Bool, z :: String } </haskell> |
||
<haskell> data HRec2 = HRec2 { p :: Bool, q :: Char } </haskell> |
<haskell> data HRec2 = HRec2 { p :: Bool, q :: Char } </haskell> |
||
− | Extensible records are records where we can add values (with corresponding label) to existing records. Suppose we have a record <hask>x = { x = 0, y = 0 }</hask>. If we have an extensible record system we can then add a value to this record: |
||
+ | 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" x </haskell> |
||
+ | |||
+ | <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> |
||
+ | A type-level record, i.e. the mapping of labels to types, such as <hask> {x = Int, y = Bool, z = String } </hask>, is called a '''row'''. |
||
− | This 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, not if they have the same fields with the same types. |
||
+ | |||
+ | |||
+ | 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. This also means we do not have to declare the type of the record before using it. For example (in CTRex). |
||
<haskell> x := 0 .| y := False .| empty </haskell> |
<haskell> x := 0 .| y := False .| empty </haskell> |
||
+ | |||
Constructs <hask> { x = 0, y = 0 } </hask> with type : |
Constructs <hask> { x = 0, y = 0 } </hask> with type : |
||
+ | |||
<haskell> Rec ("x" ::= Int :| y ::= Bool .| Empty) </haskell> |
<haskell> Rec ("x" ::= Int :| y ::= Bool .| Empty) </haskell> |
||
+ | |||
which means <hask> {x = Int, y = Bool } </hask> |
which means <hask> {x = Int, y = Bool } </hask> |
||
− | Such a system has several advantages: |
||
+ | This structural typing has the advantage that we can go from <hask> {x = Int, y = Bool } </hask> to <hask> {x = Int, y = Bool, z = String } </hask> 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). |
||
− | * Labels can be used in different records for different types. This is currently not possible with standard records : |
||
+ | |||
+ | 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 : |
||
<haskell> |
<haskell> |
||
Line 58: | Line 67: | ||
data Y = Y { x :: Bool } |
data Y = Y { x :: Bool } |
||
</haskell> |
</haskell> |
||
+ | |||
Will give a Multiple declarations of `x' error. |
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. |
* Records do not have to be declared before use. |
||
+ | * Structural typing eliminates the need for explicit conversion functions. |
||
+ | == Row polymorphism == |
||
− | * Record typing is structural, meaning that we can go from <hask> {x = Int, y = Bool } </hask> to <hask> {x = Int, y = Bool, z = String } </hask> 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). |
||
+ | |||
+ | Some extensible record systems, such as CTRex, support '''row polymorphism'''. This concept is best explained by an example, consider the following function (in CTRex): |
||
+ | |||
+ | <haskell> |
||
+ | 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 |
||
+ | </haskell> |
||
+ | |||
+ | Where <hask>(.!)</hask> is the function to get a value from a record. This function takes a record with row <hask>{ x = Double, y = Double }</hask> and add returns the same record with a label <hask>dist</hask> added, which carries the distance of the point <hask>(x,y)</hask> from <hask>(0,0)</hask>. |
||
+ | |||
+ | |||
+ | Now suppose we want to call this function with record <hask>{ name = "PointA", x = 10, y = 10 }</hask>. This is not possible, because the row <hask>{ name = String, x = Double, y = Double }</hask> and <hask>{ x = Double, y = Double }</hask> are not the same. |
||
+ | |||
+ | |||
+ | 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> |
||
+ | 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 |
||
+ | </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 == |
||
+ | |||
+ | 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 [http://hackage.haskell.org/package/HMap 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 [http://hackage.haskell.org/package/HMap HMap] a key has type <hask>Key x a</hask> where a is the type of the things we can store at this key, for example <hask>Int</hask>. |
||
+ | |||
+ | |||
+ | 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 <hask>x</hask> is associated with <hask>Int</hask>, The label itself does not hold any information on the associated type. In fact, the associated type may differ between records. |
||
− | === 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 map (a map that can store values of different types, see for example the [http://hackage.haskell.org/package/HMap HMap package] (blatant plug, my package )). |
||
+ | This means that if a record has <hask>x ::= Int </hask> in its row, then we are '''sure''' that this record has a value of type <hask>Int</hask> for <hask>x</hask>. In a hetrogenous map, we can never be sure if a key is present in a map, i.e. <hask>lookup x m</hask> may return <hask>Maybe</hask>. |
||
− | === Row polymorphism === |
||
= Programmer interface = |
= Programmer interface = |
||
Line 87: | Line 135: | ||
Of course it would be much nicer to just write <hask>`x</hask> instead of <hask> Label :: Label "x"</hask> but this is currently not available. This may change in the future. |
Of course it would be much nicer to just write <hask>`x</hask> instead of <hask> Label :: Label "x"</hask> but this is currently not available. This may change in the future. |
||
+ | |||
+ | |||
+ | In the remainder of this wiki page we write <hask>x</hask> instead of <hask>Label :: Label "x"</hask>, assuming we have already declared <hask>x = Label :: Label "x"</hask> |
||
== Rows and records == |
== 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: <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. |
||
− | 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 109: | 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 127: | 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 213: | 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 220: | Line 274: | ||
If it was not possible for records and rows to contain duplicate label the type of g would be: |
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. |
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 233: | Line 293: | ||
The same thing for renaming: |
The same thing for renaming: |
||
+ | <haskell> |
||
− | <haskell> extendUnique :: (KnownSymbol l, r :\ l) => Label l -> a -> Rec r -> Rec (Extend l a r) </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. |
||
+ | |||
+ | == 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: |
||
+ | <haskell> |
||
+ | 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)] |
||
+ | </haskell> |
||
+ | |||
+ | |||
+ | 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> |
||
+ | |||
+ | 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: |
||
+ | |||
+ | |||
+ | <haskell> |
||
+ | 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 |
||
+ | </haskell> |
||
+ | |||
+ | |||
+ | 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 |
||
+ | |||
+ | <haskell> typerr1 = (x := 1 .| empty) .! y + 1 </haskell> |
||
+ | |||
+ | <haskell> |
||
+ | No instance for (Num (Records.NoSuchField "y")) |
||
+ | arising from a use of ‛+’ |
||
+ | In the expression: (x := 1 .| empty) .! y + 1 |
||
+ | </haskell> |
||
+ | |||
+ | Somewhat unsatisfactory, the expression: |
||
+ | |||
+ | <haskell> typerr1 = (x := 1 .| empty) .! y </haskell> |
||
+ | |||
+ | does not immediatly give a type error. Instead its type is: |
||
+ | |||
+ | <haskell> typerr1 :: Records.NoSuchField "y" </haskell> |
||
+ | |||
+ | * Record does not lack field |
||
+ | |||
+ | <haskell> x :!= 1 .| x := 1 .| empty </haskell> |
||
+ | |||
+ | Gives the error |
||
+ | |||
+ | <haskell> |
||
+ | Error: |
||
+ | Couldn't match type ‛'Records.LabelNotUnique "x"’ |
||
+ | with ‛'Records.LabelUnique "x"’ |
||
+ | In the first argument of ‛(.|)’, namely ‛x :!= 1’ |
||
+ | </haskell> |
||
+ | |||
+ | * Records not disjoint |
||
+ | |||
+ | <haskell> |
||
+ | notdisjoint = let p = x := 2 .| empty |
||
+ | q = x := 2 .| empty |
||
+ | in p .+ q |
||
+ | </haskell> |
||
+ | |||
+ | Gives the error: |
||
+ | |||
+ | <haskell> |
||
+ | 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 |
||
+ | </haskell> |
||
+ | |||
+ | = Implementation = |
||
+ | |||
+ | The basis of the implementation is a label-type pair, which is represented by the following (unexported) datakind: |
||
+ | |||
+ | <haskell> data LT a = Symbol :-> a </haskell> |
||
+ | |||
+ | == Rows == |
||
+ | |||
+ | A row is then simply a list of such label-type pairs: |
||
+ | <haskell> newtype Row a = R [LT a] -- constructor not exported </haskell> |
||
+ | |||
+ | Notice that the constructor is not exported, so if we ask for the type of |
||
+ | |||
+ | <haskell> |
||
+ | origin2 = y := 0 .| x := 0 .| empty |
||
+ | </haskell> |
||
+ | |||
+ | we get: |
||
+ | <haskell> |
||
+ | origin2 |
||
+ | :: Rec ('Records.R '["x" 'Records.:-> Double, "y" 'Records.:-> Double]) |
||
+ | </haskell> |
||
+ | |||
+ | 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. : |
||
+ | |||
+ | <haskell> |
||
+ | origin2 :: Rec ("x" ::= Double :| "y" ::= Double :| Empty) |
||
+ | </haskell> |
||
+ | |||
+ | 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 : |
||
+ | <haskell> <.=? :: Symbol -> Symbol -> Bool </haskell> |
||
+ | 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: |
||
+ | |||
+ | <haskell> |
||
+ | 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) |
||
+ | </haskell> |
||
+ | |||
+ | == Records == |
||
+ | |||
+ | To implement the records we introduce the following datatype which can contain anything: |
||
+ | |||
+ | <haskell> |
||
+ | data HideType where |
||
+ | HideType :: a -> HideType |
||
+ | </haskell> |
||
+ | |||
+ | A record is then defined as follows: |
||
+ | |||
+ | <haskell> |
||
+ | -- | A record with row r. |
||
+ | data Rec (r :: Row *) where |
||
+ | OR :: HashMap String (Seq HideType) -> Rec r |
||
+ | </haskell> |
||
+ | |||
+ | 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: |
||
+ | |||
+ | <haskell> |
||
+ | 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 |
||
+ | </haskell> |
||
+ | |||
+ | 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 [http://hackage.haskell.org/package/HMap HMap]. |
||
+ | |||
+ | Since we know that the actual type of the value in Hidetype is given in the row, we can safely convert it back: |
||
+ | <haskell> |
||
+ | (.!) :: 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 |
||
+ | </haskell> |
||
+ | |||
+ | 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 = |
||
+ | |||
+ | Here we compare with other approaches. |
||
+ | |||
+ | == 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 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) [http://code.haskell.org/~aavogt/HList-benchmark/a.html link] |
||
+ | ** <hask>{x = 0, y = 0 }</hask> and <hask>{ y = 0, x = 0 } </hask> 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 [http://hackage.haskell.org/package/HList-0.3.0.1/docs/Data-HList-FakePrelude.html#t:ApplyAB applyAB] that work on <hask>LVPair l a</hask> from instances that work on just <hask>a</hask> |
||
+ | ** however there similarities between the two |
||
+ | {| |
||
+ | ! CTRex function |
||
+ | ! HList function(s) |
||
+ | |- |
||
+ | | rinit |
||
+ | | [http://hackage.haskell.org/package/HList-0.3.0.1/docs/Data-HList-HList.html#g:15 hReplicate] |
||
+ | |- |
||
+ | | erase |
||
+ | | [http://hackage.haskell.org/package/HList-0.3.0.1/docs/Data-HList-HList.html#t:HMapOut hMapOut] |
||
+ | |- |
||
+ | | eraseZip |
||
+ | | [http://hackage.haskell.org/package/HList-0.3.0.1/docs/Data-HList-HZip.html 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 [http://www.fing.edu.uy/~mviera/papers/pepm13.pdf paper]. |
||
+ | * Duplicate labels are disallowed in HList. |
||
+ | * HList has nicer support for [http://hackage.haskell.org/package/HList-0.3.0.1/docs/Data-HList-MakeLabels.html 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 <hask>error</hask> so that we can generate clearer error messages earlier. |
Latest revision as of 08:53, 9 December 2013
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 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 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 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(?)
- 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.