[Haskell-cafe] Type equality proof

[Ryan Ingram]

On Tue, Mar 17, 2009 at 10:30 AM, Brent Yorgey <byorgey at seas.upenn.edu> wrote:
> 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