Editing CTRex (section)

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