On Sat, Sep 30, 2006 at 01:38:28AM -0700, oleg@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⑈