Editing CTRex (section)

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