[Haskell-cafe] Re: Eta-expansion and existentials (or: types
destroy my laziness)
dan.doel at gmail.com
Tue Oct 19 14:01:34 EDT 2010
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.
More information about the Haskell-Cafe