[Haskell-cafe] Equality constraints in type families

[Hugo Pacheco]

That's simple Tom.
Imagine the factorial function for Int written as a paramorphism:

type instance F Int = Either One

instance (Mu Int) where
    inn (Left _) = 0
    inn (Right n) = succ n
    out 0 = Left ()
    out n = Right (pred n)

instance Functor (F Int) where
    fmap _ (Left ()) = Left ()
    fmap f (Right n) = Right (f n)

fact :: Int -> Int
fact = para (const 1 \/ (uncurry (*)) . (id >< succ))

If we consider that the paramorphism is implemented as an hylomorphism, then
an intermediate virtual type (d in the hylo definition) [Int]

If you test the constraints for d = [Int], a = Int and c = Int

F d c ~ F a (c,a)

F d a = F [Int] Int = Either One (Int,Int)
F a (c,a) = F Int (Int,Int) = Either One (Int,Int)

F d a ~ F a (a,a)

F d a = F a (a,a) -- pure substitution of the above case

Hope this helps.
Thanks again for you patience,
hugo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080311/ab244775/attachment.htm