StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>As far as I know a polymorphic <code>seq</code> function is bad because it weakens free theorems or, in other words, some equalities that are valid without <code>seq</code> are no longer valid with <code>seq</code>. For example, the equality</p> <pre><code>map g (f xs) = f (map g xs) </code></pre> <p>holds for all functions <code>g :: tau -> tau'</code>, all lists <code>xs :: [tau]</code> and all polymorphic functions <code>f :: [a] -> [a]</code>. Basically, this equality states that <code>f</code> can only reorder the elements of its argument list or drop or duplicate elements but cannot invent new elements.</p> <p>To be honest, it can invent elements as it could "insert" a non-terminating computation/run-time error into the lists, as the type of an error is polymorphic. That is, this equality already breaks in a programming language like Haskell without <code>seq</code>. The following function definitions provide a counter example to the equation. Basically, on the left hand side <code>g</code> "hides" the error.</p> <pre><code>g _ = True f _ = [undefined] </code></pre> <p>In order to fix the equation, <code>g</code> has to be strict, that is, it has to map an error to an error. In this case, the equality holds again.</p> <p>If you add a polymorphic <code>seq</code> operator, the equation breaks again, for example, the following instantiation is a counter example.</p> <pre><code>g True = True f (x:y:_) = [seq x y] </code></pre> <p>If we consider the list <code>xs = [False, True]</code>, we have</p> <pre><code>map g (f [False, True]) = map g [True] = [True] </code></pre> <p>but, on the other hand</p> <pre><code>f (map g [False, True]) = f [undefined, True] = [undefined] </code></pre> <p>That is, you can use <code>seq</code> to make the element of a certain position of the list depend on the definedness of another element in the list. The equality holds again if <code>g</code> is total. If you are intereseted in free theorems check out the <a href="http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi">free theorem generator</a>, which allows you to specify whether you are considering a language with errors or even a language with <code>seq</code>. Although, this might seem to be of less practical relevance, <code>seq</code> breaks some transformations that are used to improve the performence of functional programs, for example, <code>foldr</code>/<code>build</code> fusion fails in the presence of <code>seq</code>. If you are intereseted in more details about free theorems in the presence of <code>seq</code>, take a look into <a href="http://www.iai.uni-bonn.de/~jv/p76-voigtlaender.pdf">Free Theorems in the Presence of seq</a>.</p> <p>As far as I know it had been known that a polymorphic <code>seq</code> breaks certain transformations, when it was added to the language. However, the althernatives have disadvantages as well. If you add a type class based <code>seq</code>, you might have to add lots of type class constraints to your program, if you add a <code>seq</code> somewhere deep down. Furthermore, it had not been a choice to omit <code>seq</code> as it had already been known that there are space leaks that can be fixed using <code>seq</code>.</p> <p>Finally, I might miss something, but I don't see how a <code>seq</code> operator of type <code>a -> a</code> would work. The clue of <code>seq</code> is that it evaluates an expression to head normal form, if another expression is evaluated to head normal form. If <code>seq</code> has type <code>a -> a</code> there is no way of making the evaluation of one expression depend on the evaluation of another expression.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload