seq/parametricity properties/free theorems and a proposal/question
Simon Marlow
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.
Cheers,
Simon
More information about the Libraries
mailing list