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

On March 18, 2011 11:12:44 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]

You are correct. You don't actually get the "map f . map g = map (f . g)" relationship without looking at the definition of map (which, as you point out, could be otherwise doing things like dropping elements). Ignoring my bad example though, the key, though still is that without seq, the only operations that polymorphic functions can invoke that peer inside their universally quantified arguments are those passed to them. This guarantee gives compilers more freedom in manipulating expressions (through free theorems and, as Simon pointed out, more eta-expansion). Cheers! -Tyson