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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
