Editing CTRex (section)

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