[Haskell-cafe] Type equality proof

[Conor McBride]

Hi

On 18 Mar 2009, at 15:00, Conal Elliott wrote:

> I use these defs:
>
> -- | Lift proof through a unary type constructor
> liftEq :: a :=: a' -> f a :=: f a'
> liftEq Refl = Refl
>
> -- | Lift proof through a binary type constructor (including '(,)')
> liftEq2 :: a :=: a' -> b :=: b' -> f a b :=: f a' b'
> liftEq2 Refl Refl = Refl
>
> -- | Lift proof through a ternary type constructor (including '(,,)')
> liftEq3 :: a :=: a' -> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c'
> liftEq3 Refl Refl Refl = Refl

Makes you want kind polymorphism, doesn't it?
Then we could just have

   (=$=) :: f :=: g -> a :=: b -> f a :=: g b

Maybe the liftEq_n's are the way to go (although
we called them "resp_n" when I was young), but
they don't work for higher kinds.

An alternative ghastly hack might be

 > data PackT2T (f :: * -> *)

 > (=$=) :: (PackT2T f :=: PackT2T g) ->
 >          (a :=: b) -> (f a :=: g b)
 > Refl =$= Refl = Refl

But now you need a packer and an application for
each higher kind. Or some bonkers type-level
programming.

This one will run and run...

Cheers

Conor