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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe