seq/parametricity properties/free theorems and a proposal/question

[Dan Doel]

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