seq/parametricity properties/free theorems and a proposal/question
Dan Doel
dan.doel at gmail.com
Fri Mar 18 21:53:20 CET 2011
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
More information about the Libraries
mailing list