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

[Tyson Whitehead]

On March 18, 2011 11:12:44 Max Bolingbroke wrote:
> AFAIK Haskell used to have this but it was removed because a
> polymorphic seq is just so damn convenient! Furthermore, this solution
> would not help unless you did not have a Seq (a -> b) instance, but
> such an instance could be necessary to avoid some space leaks, since
> you can write stuff like:
> 
> case holds_on_to_lots_of_memory of
>   True -> \x -> x-1
>   False -> \x -> x+1

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)

That is, it doesn't affect the parenthetic guarantees (to apply it you have to 
know the underling constructor is ->)?  Would it be possible to resolve this 
by having a compiler supplied "Seq (a -> b)" that performs eta contraction?  
That is, recursively recognize and expand thunks of the sort "\x -> f x"?

(perhaps it is possible that the compiler can know all places it can generates 
them and all code that can generate them and arranges for them to be tagged)

Cheers!  -Tyson
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: This is a digitally signed message part.
URL: <http://www.haskell.org/pipermail/libraries/attachments/20110318/93421039/attachment-0001.pgp>