[Haskell-cafe] Type equality proof
conor at strictlypositive.org
Wed Mar 18 11:21:01 EDT 2009
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
This one will run and run...
More information about the Haskell-Cafe