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

[wren ng thornton]

On 3/18/11 10:54 AM, Tyson Whitehead wrote:
> However, this last bit about passing them to similarly constrained functions
> is not true thanks seq.  There is no guarantee map, or some other polymorphic
> function it invokes has not used seq to look inside the universally quantified
> types and potentially expose _|_.  For example, consider
>
>    map' f [] = []
>    map' f (x:xs) = x `seq` f x : map f xs
>
> Now "map' f . map' g = map' (f . g)" is not true for all arguments.

Though I'm not sure we should expect it to be. Category theoretically 
speaking, in general we should not expect the two composition functions 
to be the same. And indeed we do still get the following functor law:

     map' f . map' g == map' (f .! g)

where

     (f .! g) x = f $! g x

is the composition of the strict subcategory of Haskell.

-- 
Live well,
~wren