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

[apfelmus at quantentunnel.de]

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

You mean f.i. by specializing a polymorphic type via type signature? So that

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

would behave different for (const :: a -> Int) and (const :: (a,a) ->
Int)? At least the latter does not even typecheck. I suspect that all
possible program behavior changes are already catched at the
type/implementation level: when all types are strict, there just cannot
be irrefutable patterns for existentials :)

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

True. But you don't have different optimizations for types and values,
do you?

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

In Haskell, only irrefutable patterns for existentials and perhaps GADTs
come to mind. But it would be for the good health of our poor computer
programs ("whaa, My mind just exploded.") :)


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

Mh, type classes are in essence polymorphic variants on the type level.
As types and values do not really differ, you could gain something from
existing polymorphic variant implementations like in some ML dialects. A
quick google revealed

http://caml.inria.fr/pub/papers/garrigue-polymorphic_variants-ml98.pdf

but I don't know if it helps. Polymorphic recursion makes things difficult.

As a side effect, once you got type classes separately compiled, you get
some form of polymorphic variants on the value level for free! Then,
it's only a step backward to support open data types proposed by Löh and
Hinze

http://www.informatik.uni-bonn.de/~ralf/publications/OpenDatatypes.pdf

Regards,
apfelmus