oleg@pobox.com wrote:
I have come to realize that irrefutable pattern matching of existentials may indeed be problematic. Let us consider the following existential data type
data FE = forall a. Typeable a => Foo a | forall a. Typeable a => Bar a
The following tests type and run (the latter raising the expected exception).
test1 = case (Foo ()) of Foo x -> show $ typeOf x test2 = case (Bar True) of Foo x -> show $ typeOf x
Let us suppose that irrefutable pattern matching of existentials is allowed. What would be the value of the expression
case (Bar True) of ~(Foo x) -> show $ typeOf x then?
Interesting, interesting. Without those "unsafe" Typeables and further simplified, we can say class Foo a where foo :: a -> Int instance Foo () where foo = const 1 instance Foo Bool where foo = const 2 data Bar = forall a . Foo a => Bar a culprit :: Bar -> Int culprit ~(Bar x) = foo x Now, hugs -98 gives > culprit (Bar (undefined :: ())) 1 > culprit (Bar (undefined :: Bool)) 2 The interesting part, however is > culprit undefined Program error: Prelude.undefined > culprit (Bar undefined) ERROR - Unresolved overloading *** Type : Foo a => Int *** Expression : culprit (Bar undefined) But both should be the same, shouldn't they? In the first case, the implementation gets an undefined dictionary. But in the second case, the type system complains. If we used explicit dictionaries as in data Bar = forall a . Bar (a->Int, a) the second case would yield _|_, too,
One may claim that the existential pattern match also binds an implicit dictionary argument, which is demanded above. That explanation is quite unsatisfactory, because it breaks the abstraction of type classes.
Indeed, the above shows the subtle difference: with type classes, one may not pass an undefined dictionary as this is an unresolved overloading. Irrefutable patterns for existential types somehow disturb things. Regards, apfelmus