Problematic irrefutable pattern matching of existentials
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? Hopefully not "Bool". One might say that the expression ought to bottom out. However, what reason one may give for that outcome? The only binding in the above expression is of 'x', whose value is never demanded. Indeed, "show $ typeOf (undefined :: ())" yields the non-bottom value "()". 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. The dictionary passing is merely an _implementation technique_ for type classes. Furthermore, it is not the only implementation technique: JHC and Chameleon, for example, use intensional type analysis to implement typeclasses. On a different note, Conor McBride wrote:
It isn't necessary to perform constructor discrimination when it's statically known that exactly one constructor is possible, so those patterns can always be made irrefutable, with matching replaced by projection.
that is, in essence, the idea behind `Tagless Staged Interpreters for Typed Languages' Pasalic, Taha, Sheard: ICFP02 It is well-written paper, with an excellent introduction and motivation. Incidentally, one can write their tagless staged interpreter in Haskell as it is. No dependent types are necessary.
On Sun, Oct 01, 2006 at 08:05:15PM -0700, 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?
Hopefully not "Bool". One might say that the expression ought to bottom out. However, what reason one may give for that outcome? The only binding in the above expression is of 'x', whose value is never demanded. Indeed, "show $ typeOf (undefined :: ())" yields the non-bottom value "()".
There is also the implicit dictionary argument of typeOf, and this is demanded, so the value should be _|_.
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
participants (3)
-
apfelmus＠quantentunnel.de -
oleg＠pobox.com -
Ross Paterson