<div dir="ltr"><div class="gmail_default" 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><br>
Now, some may complain about the enumeration above. But this, too, is a simple<br>matter. It is well known that Haskell programs are denumerable. So it is quite<br>easy to enumerate all Haskell programs that produce a value, check whether that<br>
value has the type we're interested in, and compute said value. All of this can<br>be done in Haskell. Thus, every Haskell type is programatically enumerable in<br>Haskell, and we can use said enumeration in our implementation of seq for<br>
function types. I have discussed this with Russell O'Connor [3], and he assures<br>me that this argument should be sufficient even if we consider semantic models<br>of Haskell that contain values not denoted by any Haskell program, so we should<br>
be safe there.<br><br>The one possible caveat is that this implementation of seq is not operationally<br>uniform across all types, so the current fully polymorphic type of seq may not<br>make sense. But moving back to a type class based approach isn't so bad, and<br>
this time we will have a semantically sound backing, instead of just having a<br>class with the equivalent of the current magic function in it.<br><br>Once this machinery is in place, we can eta reduce to our hearts' content, and<br>
not have to worry about breaking semantics. We'd no longer put the burden on<br>programmers to use potentially unsafe hacks to avoid eta expansions. I apologize<br>for not sketching an implementation of the above algorithm, but I'm sure it<br>
should be elementary enough to make it into GHC in the next couple versions.<br>Everyone learns about this type of thing in university computer science<br>programs, no?<br><br>Thoughts? Comments? Questions?<br><br>Cheers,<br>
-- Dan<br><br>[1] <a href="http://hackage.haskell.org/package/lens">http://hackage.haskell.org/package/lens</a><br>[2] <a href="http://hackage.haskell.org/package/unamb">http://hackage.haskell.org/package/unamb</a><br>[3] <a href="http://r6.ca/">http://r6.ca/</a><br>
<br></div></div>