[Haskell-cafe] A Question of Restriction

[wren ng thornton]

Brian Troutwine wrote:
> Hello Wouter.
> 
> I've had a go at the paper linked and perused other references found
> with Google. Unfortunately, such sophisticated use of the type system
> is pretty far out of my normal problem domain and I can't see how to
> apply the techniques presented to my motivating example. Would you be
> so kind as to elaborate?

     data Foo = One | Two | Three | Four
     data Odd = One | Three
     data Even = Two | Four

     ==>

     {-
     data Fix f = Fix { unFix :: f (Fix f) }
     data (:+:) f g x = Inl (f x) | Inr (g x)
     ...
     -}

     data One   r = One
     data Two   r = Two
     data Three r = Three
     data Four  r = Four

     instance Functor One   where fmap _ One   = One
     instance Functor Two   where fmap _ Two   = Two
     instance Functor Three where fmap _ Three = Three
     instance Functor Four  where fmap _ Four  = Four

     type Foo  = Fix (One :+: Two :+: Three :+: Four)
     type Odd  = Fix (One :+: Three)
     type Even = Fix (Two :+: Four)


If your original types were actually recursive, then the unfixed 
functors should use their r parameter in place of the recursive call, e.g.

     data List a = Nil | Cons a (List a)
     ==>
     data List a r = Nil | Cons a r

Also, if you know a certain collection of component types must always 
occur together, then you can flatten parts of the coproduct and use 
normal unions as well. E.g.

     data Odd  r = One | Three
     data Two  r = Two
     data Four r = Four
     type Foo    = Fix (Odd :+: Two :+: Four)

-- 
Live well,
~wren