[Haskell-cafe] Type equality proof

[Conal Elliott]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090318/896eb4a7/attachment.htm