[Haskell-cafe] Type equality proof
Ryan Ingram
ryani.spam at gmail.com
Tue Mar 17 14:40:19 EDT 2009
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
More information about the Haskell-Cafe
mailing list