seq/parametricity properties/free theorems and a proposal/question
marlowsd at gmail.com
Fri Mar 18 16:26:59 CET 2011
On 18/03/2011 15:12, 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]
>> 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.
I agree with you, but there are also eminently practical reasons to
*not* have a polymorphic seq. If _|_ == \x._|_, the compiler is free to
eta-expand much more often, and eta-expansion is a key optimisation.
(though I think GHC violates the rules and eta-expands anyway, at least
sometimes). This is one of those times when there's no good answer, or
at least, we haven't found one yet.
More information about the Libraries