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 etc. On Tue, Mar 17, 2009 at 3:39 AM, Martijn van Steenbergen < mart...@van.steenbergen.nl> wrote: > Olá café, > > With the recent generic programming work and influences from type-dependent > languages such as Agda, the following data type seems to come up often: > > data (a :=: a') where >> Refl :: a :=: a >> > > Everyone who needs it writes their own version; I'd like to compile a > package with this data type and related utilities, if such a package doesn't > exist already (I couldn't find one). Below is what I have so far; I'd much > appreciate it if you added your ideas of what else the package should > contain. > > {-# LANGUAGE GADTs #-} >> {-# LANGUAGE TypeOperators #-} >> >> module Eq where >> >> data (a :=: a') where >> Refl :: a :=: a >> >> class Eq1 f where >> eq1 :: f a -> f a' -> Maybe (a :=: a') >> >> class Eq2 f where >> eq2 :: f a b -> f a' b' -> Maybe (a :=: a', b :=: b') >> >> class Eq3 f where >> eq3 :: f a b c -> f a' b' c' -> Maybe (a :=: a', b :=: b', c :=: c') >> > > Thank you, > > Martijn. > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe