[Haskell-cafe] Type equality proof
Brent Yorgey
byorgey at seas.upenn.edu
Tue Mar 17 13:30:01 EDT 2009
On Tue, Mar 17, 2009 at 11:39:05AM +0100, Martijn van Steenbergen wrote:
>
>> {-# 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')
>
I don't understand your classes Eq1, Eq2, and Eq3. How would you make
an instance of Eq1 for, say, [] ?
instance Eq1 [] where
eq1 xs ys = ???
It seems you are confusing _value_ equality with _type_ equality? A
value of type a :=: a' is a proof that a and a' are the same type.
But given values of type f a and f a', there is no way to decide
whether a and a' are the same type (no matter what f is), since types
are erased at runtime.
Maybe you mean for eq1 to have a type like
eq1 :: (f a :=: f a') -> (a :=: a') ?
But actually, you don't need a type class for that either;
eq1 :: (f a :=: f a') -> (a :=: a')
eq1 Refl = Refl
type checks just fine.
-Brent
More information about the Haskell-Cafe
mailing list