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

Max Bolingbroke batterseapower at hotmail.com
Fri Mar 18 16:12:44 CET 2011


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]

>  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.

Cheers,
Max



More information about the Libraries mailing list