[Haskell-cafe] Re: Eta-expansion and existentials (or: types destroy my laziness)

[Dan Doel]

On Tuesday 19 October 2010 6:16:16 am Max Bolingbroke wrote:

> Thanks - your definitions are similar to Roman's suggestion.
> Unfortunately my criteria 3) is not quite what I actually wanted - I
> really wanted something "GHC-optimisable" - (so non-recursive
> definitions are a necessary but not sufficient condition).
>
> ...
>
> I hadn't seen this - thanks! It is certainly a neat trick. I can't
> quite see how to use it to eliminate the existential I'm actually
> interested eta-expanding without causing work duplication, but I'll
> keep thinking about it.

I doubt it's possible, aside from your unsafeCoerce version.

The nub of the problem seems to me to be the lack of irrefutable match on the 
existential---irrefutable match should be equivalent to eta expanding values, 
so it's been intentionally disallowed. One could argue that this corresponds 
to their weak elimination:

  elim :: (forall a. P a -> r) -> (exists a. P a) -> r

However, this argument is a bit circular, since that eliminator could be 
defined to behave similarly to an irrefutable match. One might expect it to be 
strict, but it isn't necessary (although it might be difficult to specify how 
such a lazy reduction would work formally, without resorting to other, 
stronger elimination principles).

Presumably, GHC requires strictness because of constraints that can be bundled 
in an existential. For one, with local equality constraints, it'd be unsound 
in the same way that irrefutable matches on a type equality GADT are. However, 
I also seem to recall that GHC expects all dictionaries to be strictly 
evaluated (for optimization purposes), while irrefutable matching on a 
constrained existential would introduce lazy dictionaries. Or, put another 
way, eta expansion of a dictionary-holding existential would result in a value 
holding a bottom dictionary, whereas that's otherwise impossible, I think.

However, your stream type has no constraints, so there's nothing that would 
make an irrefutable match unreasonable (unless I'm missing something). I don't 
expect GHC to start to support this, because, "you can only use irrefutable 
matches on existentials without constraints," is a complicated rule. But I 
believe that is the core of your troubles, and it doesn't have any necessary 
connection to type safety in this case.

Cheers,
-- Dan