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