Editing CTRex (section)

== Duplicate labels, and lacks ==

Rows and records can contain duplicate labels as described in the paper [http://legacy.cs.uu.nl/daan/download/papers/scopedlabels.pdf Extensible records with scoped labels] by Daan Leijen. 

Hence we can write:

<haskell> z =  x := 10 .| x := "bla" .| Empty :: Rec ("x" ::= Int :| "x" ::= String :| Empty)
</haskell>

We can recover the information on the second instance of x by removing x:
<haskell> z .- x :: Rec ("x" ::= String :| Empty) </haskell>

The motivation for this is as follows: Suppose we have a function 
<haskell> f :: Rec ("x" ::= Int :| r) -> (Rec ("x" ::= Bool .| r) </haskell>

and we want to write the following function:

<haskell>
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''
</haskell>

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.

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:

<haskell> extendUnique :: (KnownSymbol l, l :\ r) => Label l -> a -> Rec r -> Rec (Extend l a r)  </haskell>

The same thing for renaming:
<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:

<haskell> .+ :: Disjoint l r => Rec l -> Rec r -> Rec (l :++ r) </haskell>

Notice that .+ is commutative, while .++ is not.