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

On 18/03/2011 15:12, Max Bolingbroke wrote:

On 18 March 2011 14:54, Tyson Whitehead 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