On Tue, Mar 17, 2009 at 10:30 AM, Brent Yorgey
I don't understand your classes Eq1, Eq2, and Eq3. How would you make an instance of Eq1 for, say, [] ?
You don't.
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.
Not necessarily. Consider this example: data U a where UInt :: U Integer UBool :: U Bool instance Eq1 U where eq1 UInt UInt = Just Refl eq1 UBool UBool = Just Refl eq1 _ _ = Nothing data Expr a where EPrim :: U a -> a -> Expr a EIf :: Expr Bool -> Expr a -> Expr a -> Expr a EPlus :: Expr Integer -> Expr Integer -> Expr Integer ELess :: Expr Integer -> Expr Integer -> Expr Bool typeOf :: Expr a -> U a typeOf (EPrim u _) = u typeOf (EIf _ t _) = typeOf t typeOf (EPlus _ _) = UInt typeOf (ELess _ _) = UBool instance Eq1 Expr where eq1 lhs rhs = eq1 (typeOf lhs) (typeOf rhs) These types are very useful for construction of type-safe interpreters and compilers. -- ryan