Proxy, new Typeable, and type-level equality

[Twan van Laarhoven]

On 03/04/13 18:08, Richard Eisenberg wrote:
> Hi all,
>
>> sym :: (a :~: b) -> (b :~: a)
>> trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
>> coerce :: (a :~: b) -> a -> b
>> liftEq :: (a :~: b) -> (f a :~: f b)
>> liftEq2 :: (a :~: a') -> (b :~: b') -> (f a b :~: f a' b')
>> liftEq3 :: ...
>> liftEq4 :: ...

Why do you need all these lift functions? Wouldn't a single kind polymorphic one do?

     lift :: (f :~: g) -> (a :~: b) -> (f a :~: g b)

Then you can define

     liftEq ab = refl `lift` ab
     liftEq2 ab cd = (refl `lift` ab) `lift` cd
     -- etc.

(the name `lift` is subject to bikeshedding of course.)


Twan