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

[Simon Marlow]

On 18/03/2011 15:12, Max Bolingbroke wrote:
> On 18 March 2011 14:54, Tyson Whitehead<twhitehead at gmail.com>  wrote:
>>   map f . map g = map (f . g)
>>
>> should be derivable from the type of map "(a ->  b) ->  [a] ->  [b]"
>
> I don't think this is true as stated. Consider:
>
> map f [] = []
> map f [x] = [f x]
> map f (x:y:zs) = f x : map zs
>
> Your proposed property is violated though we have the appropriate
> type. IIRC I think what is true is that
>
> map f . map' g = map' (f . g)
>
> For any map' :: (a ->  b) ->  [a] ->  [b]
>
>>   class Seq a where
>>     seq :: a ->  b ->  b
>
> 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
>
> So there are eminently practical reasons for polymorphic seq.

I agree with you, but there are also eminently practical reasons to 
*not* have a polymorphic seq.  If _|_ == \x._|_, the compiler is free to 
eta-expand much more often, and eta-expansion is a key optimisation. 
(though I think GHC violates the rules and eta-expands anyway, at least 
sometimes).  This is one of those times when there's no good answer, or 
at least, we haven't found one yet.

Cheers,
	Simon