[Haskell-cafe] Re: Problematic irrefutable pattern matching of existentials

[apfelmus at quantentunnel.de]

oleg at 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