[Haskell-cafe] irrefutable patterns for existential types / GADTs

[John Meacham]

On Sat, Sep 30, 2006 at 01:38:28AM -0700, oleg at pobox.com wrote:
> 
> It seems that irrefutable pattern match with existentials is safe. The
> fact that irrefutable pattern match with GADT is unsafe has been
> demonstrated back in September 2004.

it is safe in that you can't express coerce, but irrefutable pattern
matching on existentials has other practical issues for an
implementation. namely, even though you may not ever evaluate the
irrefutable pattern, its type is probably used in the underlying
translation somewhere like. if you happen to use any polymorphic
functions. for instance

> data Foo = exists a . Foo a
> f ~(Foo x) = const 4 (id x)

now, you would think that f _|_ would evaluate to 4, but (depending on
your translation) it might evaluate to _|_.

the reason being that id translates internally to 

> id = /\a . \x::a . x 

since you cannot pull out an appropriate type to pass to id without
evaluating the 'irrefutable' pattern, you end up with _|_ instead of 4.

basically, allowing irrefutable matching on existentials would expose
whether the underlying implementation performs type-erasure. even if an
implementation does type erasure like ghc. suddenly odd things occur,
like adding an unusned class constraint to a type signature might change
the behavior of a program. (since it will suddenly have to pull out a
dictionary)

All in all, even though type-safety is not broken, irrefutable patterns
should not be allowed for existentials.

        John

-- 
John Meacham - ⑆repetae.net⑆john⑈