On 18 March 2011 14:54, Tyson Whitehead 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

Others have commented on the whys and the wherefores of the removal of the Eval, so I won't belabor that here, but the History of Haskell paper goes into a bit more depth, IIRC, talking about how this happened during the refactoring of a large Haskell project. You may want to read Johann and Voightlander's "Free theorems in the presence of seq" and "The impact of seq on free theorems". http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.4936 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.71.1777 They have done a lot of work on making more rigorous the strictness side conditions that exist on many free theorems, and show how with a bit of unrolling and sideways thinking you can still reason about code equationally using free theorems, even in a world with fully polymorphic seq. -Edward On Fri, Mar 18, 2011 at 10:54 AM, Tyson Whitehead wrote:

The haskell (2010) report says:

"The function seq is defined by the equations:

seq _|_ b = _|_ seq a b = b, if a /= _|_

seq is usually introduced to improve performance by avoiding unneeded laziness. Strict datatypes (see Section 4.2.1) are defined in terms of the $! operator. However, the provision of seq has important semantic consequences, because it is available at every type. As a consequence, _|_ is not the same as \x -> _|_ since seq can be used to distinguish them. For the same reason, the existence of seq weakens Haskell’s parametricity properties."

As has been noted in the literature (and presumably the mailing lists), this has important consequences for free theorems. For example, the property

map f . map g = map (f . g)

should be derivable from the type of map "(a -> b) -> [a] -> [b]" (i.e., as map works on all a's and b's, it can't actually do anything other than move the a's around, wrap them with the given function to get the b's, or pass them along to other functions which should be similarly constrained).

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.

map' (const 0) . map' (const undefined :: Int -> Int) $ [1..10] = [undefined] map' (const 0 . undefined :: Int -> Int) $ [1..10] = [0,0,0,0,0,0,0,0,0,0]

My proposal (although I'm sure someone must have brought this up before, so it's more of a question) is why not take the magic away from seq by making it a class function like deepSeq

class Seq a where seq :: a -> b -> b

It is easily implemented in haskell by simply forces the constructor for the underlying data type (something also easily derivable by the compiler)

instance Seq Int where seq' 0 y = y seq' _ y = y

Now, unless I'm missing something, we have restore the strength of Haskell's parametricity properties

map :: (a -> b) -> [a] -> [b] map f [] = [] map f (x:xs) = f x : map f xs

map' :: Seq a => (a -> b) -> [a] -> [b] map' f [] = [] map' f (x:xs) = x `seq'` f x : map f xs

as the full range of operations that can be performed on universally quantified types (in addition to moving them around) is reflected in any explicitly and implicitly (through the dictionaries) passed functions over those types.

Thanks! -Tyson

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

Thank you all for all the feedback on this. I very much enjoyed the insights. I finished up Launchbury and Pateron's "Parametricity and Unboxing with Unpointed Types" yesterday and was quite impressed. They seemed to offer a particular elegant framework for dealing with a lot of these issues. I am now reading my way through Johann and Voigtlander's "The Impact of seq on Free Theorems-Based Program Transformations". Someday I'll have to sit down and read "A History of Haskell:being lazy with class" too. Cheers! -Tyson