[Haskell-cafe] Type equality proof
Yandex
miguelimo38 at yandex.ru
Tue Mar 17 06:49:14 EDT 2009
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
>
More information about the Haskell-Cafe
mailing list