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

[Tyson Whitehead]

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

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
-------------- 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/2595c35d/attachment.pgp>