[Haskell-cafe] Re: topEq for types
oleg at pobox.com
oleg at pobox.com
Tue Nov 21 02:42:02 EST 2006
Nicolas Frisby described the problem and the solution of the type
equality comparison that takes into account the top-most type
constructor only. Thus `Maybe Bool' should be considered equal to
`Maybe Char' because both types have the same top constructor Maybe.
The following complete code shows another solution. The code includes
several tests, test1 through test6, along with the expected answers.
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}
-- type equality for the top-level type constructor
-- That is, decide two types to be equal if the top-most type constructor
-- matches. Thus `Maybe Bool' should be considered equal to `Maybe Char'
module TEQ where
-- Our approach is simple. Given a type, we normalize it:
-- replace all arguments of the type constructor with unit.
-- After that, we use the regular HList's TypeEq.
class Normalize t r | t -> r
instance TypeCast (c ()) r => Normalize (c x) r
instance TypeCast (c () ()) r => Normalize (c x y) r
instance TypeCast (c () () ()) r => Normalize (c x y z) r
-- add instances for type constructors of higher arities
instance TypeCast y x => Normalize x y
top_eq :: (Normalize a a', Normalize b b', TypeEq a' b' r) =>
a -> b -> r
top_eq = undefined
test1 = top_eq (undefined::Int) (undefined::Char)
-- :t test1
-- test1 :: HFalse
test2 = top_eq (undefined::Bool) (undefined::Bool)
-- test2 :: HTrue
test3 = top_eq (undefined::Maybe Bool) (undefined::Maybe Char)
-- test3 :: HTrue
test4 = top_eq (undefined::Maybe Bool) (undefined::[Char])
-- test4 :: HFalse
test5 = top_eq (undefined::Either Int Char) (undefined::Either Char Int)
-- test5 :: HTrue
test6 = top_eq (undefined::Either Int Char) (undefined::[Char])
-- test6 :: HFalse
-- The following is borrowed from HList and included here for completeness
data HTrue
data HFalse
class TypeCast a b | a -> b, b->a where typeCast :: a -> b
class TypeCast' t a b | t a -> b, t b -> a where typeCast' :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast' () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x = x
class TypeEq x y b | x y -> b
instance TypeEq x x HTrue
instance TypeCast HFalse b => TypeEq x y b
More information about the Haskell-Cafe
mailing list