Editing CTRex (section)

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