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

[apfelmus at quantentunnel.de]

John Meacham wrote:

> 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)

So you mean that

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

is /strict/ in its first argument, i.e. in the /type/ a. So to speak,
type erasure is equivalent to strictness in all and every type argument.
For an irrefutable existential pattern, the type argument should be
lazy, of course. This allows you to "pull out an appropriate type", only
that it's pulled out only when needed. The point is that

    const c = /\a . \x :: a . c

has no problems of being lazy in its type argument.


Strictness in type arguments is of course a consequence of the fact that
there is no _|_ type. A systematic way to add irrefutable pattern
matches to existentials (or even GADTs) would therefore be the
introduction of lazy type arguments (alas introduction of a type _|_).
Type erasure then becomes a form of /strictness analysis/. I remember
that Wadler's projection based strictness analysis can discover unused
values and that's what happens very often with types as they are
seldomly calculated with at runtime. So you can erase them by virtue of
your strictness analyzer.

Thinking further, this would even allow to free type classes from the
dictionary approach: an overloaded function like

   (+) = /\a . \x :: a . \y :: a . x+y

performs a case analysis on its type argument and selects the right
specialized function. In case where this type is known at compile time,
the /inliner/ will select the right specialization. This type based
dispatch is more natural for type classes than dictionaries because the
latter would in principle allow to supply different dictionaries for one
and the same type.



Regards,
apfelmus