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.<div>
<div><br></div><div>You may want to read Johann and Voightlander's "Free theorems in the presence of seq" and "The impact of seq on free theorems". </div><div><br></div><div><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.4936">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.4936</a></div>
<div><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.71.1777">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.71.1777</a></div><div><br></div><div>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.</div>
<div><br></div><div>-Edward<br><br><div class="gmail_quote">On Fri, Mar 18, 2011 at 10:54 AM, Tyson Whitehead <span dir="ltr"><<a href="mailto:twhitehead@gmail.com">twhitehead@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
The haskell (2010) report says:<br>
<br>
"The function seq is defined by the equations:<br>
<br>
seq _|_ b = _|_<br>
seq a b = b, if a /= _|_<br>
<br>
seq is usually introduced to improve performance by avoiding unneeded<br>
laziness. Strict datatypes (see Section 4.2.1) are defined in terms of the $!<br>
operator. However, the provision of seq has important semantic consequences,<br>
because it is available at every type. As a consequence, _|_ is not the same<br>
as \x -> _|_ since seq can be used to distinguish them. For the same reason,<br>
the existence of seq weakens Haskell’s parametricity properties."<br>
<br>
As has been noted in the literature (and presumably the mailing lists), this<br>
has important consequences for free theorems. For example, the property<br>
<br>
map f . map g = map (f . g)<br>
<br>
should be derivable from the type of map "(a -> b) -> [a] -> [b]" (i.e., as<br>
map works on all a's and b's, it can't actually do anything other than move<br>
the a's around, wrap them with the given function to get the b's, or pass them<br>
along to other functions which should be similarly constrained).<br>
<br>
However, this last bit about passing them to similarly constrained functions<br>
is not true thanks seq. There is no guarantee map, or some other polymorphic<br>
function it invokes has not used seq to look inside the universally quantified<br>
types and potentially expose _|_. For example, consider<br>
<br>
map' f [] = []<br>
map' f (x:xs) = x `seq` f x : map f xs<br>
<br>
Now "map' f . map' g = map' (f . g)" is not true for all arguments.<br>
<br>
map' (const 0) . map' (const undefined :: Int -> Int) $ [1..10] = [undefined]<br>
map' (const 0 . undefined :: Int -> Int) $ [1..10] = [0,0,0,0,0,0,0,0,0,0]<br>
<br>
My proposal (although I'm sure someone must have brought this up before, so<br>
it's more of a question) is why not take the magic away from seq by making it<br>
a class function like deepSeq<br>
<br>
class Seq a where<br>
seq :: a -> b -> b<br>
<br>
It is easily implemented in haskell by simply forces the constructor for the<br>
underlying data type (something also easily derivable by the compiler)<br>
<br>
instance Seq Int where<br>
seq' 0 y = y<br>
seq' _ y = y<br>
<br>
Now, unless I'm missing something, we have restore the strength of Haskell's<br>
parametricity properties<br>
<br>
map :: (a -> b) -> [a] -> [b]<br>
map f [] = []<br>
map f (x:xs) = f x : map f xs<br>
<br>
map' :: Seq a => (a -> b) -> [a] -> [b]<br>
map' f [] = []<br>
map' f (x:xs) = x `seq'` f x : map f xs<br>
<br>
as the full range of operations that can be performed on universally quantified<br>
types (in addition to moving them around) is reflected in any explicitly and<br>
implicitly (through the dictionaries) passed functions over those types.<br>
<br>
Thanks! -Tyson<br>
<br>_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
<br></blockquote></div><br></div></div>