On Tue, 11 Mar 2008, Hugo Pacheco wrote:
Yes, I have tried both implementations at the start and solved it by choosing for the following: type family F a :: * -> * type FList a x = Either () (a,x) type instance F [a] = FList a
instance (Functor (F [a])) where fmap _ (Left _) = Left () fmap f (Right (a,x)) = Right (a,f x)
For this implementation we do have that F [a] b ~ F [c] d <=> F [a] ~ F [c] /\ b ~ d Right? So for this instance, your para via hylo wouldn't work anyway. I'd like to see some type instances and types such that the equation F d a ~ F a (a,a) holds. With your example above, it's not possible to make the equation hold, .e.g. F [t] [s] ~ F [s] ([s],[s]) <=> Either () (t,[s]) ~ Either ()(s,([s],[s])) is not true for any (finite) types t and s. Do you have such an example? You should have one, if you want to be able to call para. Tom
I have my suspicions about your mentioning of both Functor (F d) and Functor (F a) in the signature. Which implementation of fmap do you want? Or should they be both the same (i.e. F d ~ F a)?
This is an hard question to which the answer is both.
In the definition of an hylomorphism I want the fmap from (F d):
hylo :: (Functor (F d)) => d -> (F d c -> c) -> (a -> F d a) -> a -> c hylo d g h = g . fmap (hylo d g h) . h
However, those constraints I have asked about would allow me to encode a paramorphism as an hylomorphism:
class Mu a where inn :: F a a -> a out :: a -> F a a
para :: (Mu a, Functor (F a),Mu d, Functor (F d),F d a ~ F a (a,a), F d c ~ F a (c,a)) => d -> (F a (c,a) -> c) -> a -> c para d f = hylo d f (fmap (id /\ id) . out)
In para, I would want the fmap from (F a) but that would be implicitly forced by the usage of out :: a -> F a a
Sorry for all the details, ignore them if they are too confusing. Do you think there might be a definition that would satisfy me both Functor instances and equality?
Thanks for your pacience, hugo
-- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/