
On Friday 18 March 2011 2:19:19 PM Tyson Whitehead wrote:
Am I correct in figuring the only issue with giving a compiler supplied "Seq (a -> b)" instance in order to allow forcing the choice between "\x -> x-1" and "\x -> x+1" (and thus freeing the memory) is it invalidates the eta expansion "f = \x -> f x" because "seq _|_ y = _|_" while "seq (\x -> _|_ x) y = y"?
(the f's in this email are limited to those with out free x's)
The problem with having an (a -> b) instance is that it invalidates some of the goals of having the class in the first place: ensuring free theorems. Consider: f :: (a -> b) -> T for some concrete T. The free theorem is: h1 . g1 = g2 . h2 => f g1 = f g2 We can satisfy the precondition with h1 = g2 = const 5, g1 = _|_, and h2 = whatever. Then we have: f _|_ = f (const 5) But, since we have an instance Seq (a -> b), we can write: f :: (a -> b) -> T f g = g `seq` C and this f fails the above free theorem. It doesn't need a constraint because we know which instance we're using, the one for functions. f, of course, also distinguishes functions that would otherwise be extensionally equal, due to the eta thing. Anyhow, the free theorems you get for functions actually depend on the idea that you can't observe them in the way that seq does. -- Dan