[Haskell-cafe] Equality constraints in type families

[Tom Schrijvers]

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 at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/