seq/parametricity properties/free theorems and a proposal/question
twhitehead at gmail.com
Fri Mar 18 17:23:42 CET 2011
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).
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Size: 490 bytes
Desc: This is a digitally signed message part.
More information about the Libraries