[Haskell-cafe] Type equality proof

[Yandex]

data (a :=: a') where
  Refl :: a :=: a
  Comm :: (a :=: a') -> (a' :=: a)
  Trans :: (a :=: a') -> (a' :=: a'') -> (a :=: a'')
 

Martijn van Steenbergen 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
>