Proxy, new Typeable, and type-level equality
Twan van Laarhoven
twanvl at gmail.com
Thu Apr 4 11:38:29 CEST 2013
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
(the name `lift` is subject to bikeshedding of course.)
More information about the Libraries