<p dir="ltr">Hi Edward, </p>
<p dir="ltr">Yes, I'm aware of that.  However, I thought Dan's proposal especially droll given that changing seq to a class-based function would be sufficient to make eta-reduction sound, given appropriate instances (or lack thereof).  Meaning we could leave the rest of the proposal unevaluated (lazily!).</p>

<p dir="ltr">And if somebody were to suggest that on a different day, +1 from me. </p>
<p dir="ltr">John</p>
<div class="gmail_quote">On Apr 1, 2014 10:32 AM, "Edward Kmett" <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">John,<div><br></div><div>Check the date and consider the process necessary to "enumerate all Haskell programs and check their types".</div><div><br></div><div>-Edward</div></div><div class="gmail_extra">

<br><br><div class="gmail_quote">On Tue, Apr 1, 2014 at 9:17 AM, John Lato <span dir="ltr"><<a href="mailto:jwlato@gmail.com" target="_blank">jwlato@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<p dir="ltr">I think this is a great idea and should become a top priority. I would probably start by switching to a type-class-based seq, after which perhaps the next step forward would become more clear. </p>
<p dir="ltr">John L.</p>
<div class="gmail_quote"><div><div>On Apr 1, 2014 2:54 AM, "Dan Doel" <<a href="mailto:dan.doel@gmail.com" target="_blank">dan.doel@gmail.com</a>> wrote:<br type="attribution"></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div><div>
<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" target="_blank">http://hackage.haskell.org/package/lens</a><br>[2] <a href="http://hackage.haskell.org/package/unamb" target="_blank">http://hackage.haskell.org/package/unamb</a><br>


[3] <a href="http://r6.ca/" target="_blank">http://r6.ca/</a><br>
<br></div></div>
<br></div></div>_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><br>
<br></blockquote></div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>
</blockquote></div>