[Haskell-cafe] Equality constraints in type families
Hugo Pacheco
hpacheco at gmail.com
Tue Mar 11 13:21:43 EDT 2008
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
More information about the Haskell-Cafe
mailing list