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 <martijn@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