<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Mar 31, 2014 at 11:54 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div style="font-family:arial,helvetica,sans-serif">In the past year or two, there have been multiple performance problems in<br>
various areas related to the fact that lambda abstraction is not free, though we<br>
tend to think of it as so. A major example of this was deriving of Functor. If we<br>were to derive Functor for lists, we would end up with something like:<br><br>    instance Functor [] where<br>      fmap _ [] = []<br>
      fmap f (x:xs) = f x : fmap (\y -> f y) xs<br>
<br>This definition is O(n^2) when fully evaluated,, because it causes O(n) eta<br>expansions of f, so we spend time following indirections proportional to the<br>depth of the element in the list. This has been fixed in 7.8, but there are<br>

other examples. I believe lens, [1] for instance, has some stuff in it that<br>works very hard to avoid this sort of cost; and it's not always as easy to avoid<br>as the above example. Composing with a newtype wrapper, for instance, causes an<br>

eta expansion that can only be seen as such at the core level.<br><br>The obvious solution is: do eta reduction. However, this is not operationally<br>sound currently. The problem is that seq is capable of telling the difference<br>

between the following two expressions:<br><br>    undefined<br>    \x -> undefined x<br><br>The former causes seq to throw an exception, while the latter is considered<br>defined enough to not do so. So, if we eta reduce, we can cause terminating<br>

programs to diverge if they make use of this feature.<br><br>Luckily, there is a solution.<br><br>Semantically one would usually identify the above two expressions. While I do<br>believe one could construct a semantics that does distinguish them, it is not<br>

the usual practice. This suggests that there is a way to not distinguish them,<br>perhaps even including seq. After all, the specification of seq is monotone and<br>continuous regardless of whether we unify ⊥ with \x -> ⊥ x or insert an extra<br>

element for the latter.<br><br>The currently problematic case is function spaces, so I'll focus on it. How<br>should:<br><br>    seq : (a -> b) -> c -> c<br><br>act? Well, other than an obvious bottom, we need to emit bottom whenever our<br>

given function is itself bottom at every input. This may first seem like a<br>problem, but it is actually quite simple. Without loss of generality, let us<br>assume that we can enumerate the type a. Then, we can feed these values to the<br>

function, and check their results for bottom. Conal Elliot has prior art for<br>this sort of thing with his unamb [2] package. For each value x :: a, simply<br>compute 'f x `seq` ()' in parallel, and look for any successes. If we ever find<br>

one, we know the function is non-bottom, and we can return our value of c. If we<br>never finish searching, then the function must be bottom, and seq should not<br>terminate, so we have satisfied the specification.<br></div>
</div></blockquote><div><br></div><div>Love it.  I have always been a fan of "fast and loose" reasoning in Haskell.  Abstracting on seq, and treating it as a bottom if it evaluates to one, fits in perfectly.</div>
</div></div></div>