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

[John Meacham]

On Tue, Oct 03, 2006 at 12:10:52PM +0200, apfelmus at quantentunnel.de wrote:
> 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.

yeah, that is what I mean. however, since we don't have explicit type
passing in haskell, reasoning about the lazyness of types would be quite
tricky, leading to odd things like changing type signatures (without
changing the underlying types) can change the behavior of a program.

not to mention the optimizations that would be excluded by having to
preserve the strictness in types behavior... worrying about it in values
is tricky enough. :)

It would actually not be difficult to add lazy types to jhc at all. I
just don't see any use for them when dealing with haskell source. but
another front end.. (omega or cayenne perhaps?) certainly might make use
of them.

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

this is actually exactly what jhc does. it is based on the lambda cube
and makes no distinction between types and values, so there is no
particular type erasure pass, but a lot of the types happen to be erased
by run-time due to standard program transformations.

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

again, this is precicely how jhc implements type classes. There are
numerous benefits, in particular a single scrutinization of a type will
determine concrete methods for _every_ class used on that type, in
effect you get run-time specialization for free. The huge disadvantage
is that it does not play well nice at all with separate compilation,
this is an active area of research for me in jhc.


        John


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