[Haskell-cafe] Problematic irrefutable pattern matching of
oleg at pobox.com
oleg at pobox.com
Sun Oct 1 23:05:15 EDT 2006
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
> 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
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
Incidentally, one can write their tagless staged interpreter in Haskell
as it is. No dependent types are necessary.
More information about the Haskell-Cafe