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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe