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