[Haskell-cafe] Eta Reduction

Tue Apr 1 21:32:45 UTC 2014

Unfortunately the old class based solution also carries other baggage, like the old data type contexts being needed in the language for bang patterns. :(

-Edward

> On Apr 1, 2014, at 5:26 PM, John Lato <jwlato at gmail.com> wrote:
> 
> Hi Edward,
> 
> 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!).
> 
> And if somebody were to suggest that on a different day, +1 from me.
> 
> John
> 
>> On Apr 1, 2014 10:32 AM, "Edward Kmett" <ekmett at gmail.com> wrote:
>> John,
>> 
>> Check the date and consider the process necessary to "enumerate all Haskell programs and check their types".
>> 
>> -Edward
>> 
>> 
>>> On Tue, Apr 1, 2014 at 9:17 AM, John Lato <jwlato at gmail.com> wrote:
>>> 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.
>>> 
>>> John L.
>>> 
>>>> On Apr 1, 2014 2:54 AM, "Dan Doel" <dan.doel at gmail.com> wrote:
>>>> In the past year or two, there have been multiple performance problems in
>>>> various areas related to the fact that lambda abstraction is not free, though we
>>>> tend to think of it as so. A major example of this was deriving of Functor. If we
>>>> were to derive Functor for lists, we would end up with something like:
>>>> 
>>>>     instance Functor [] where
>>>>       fmap _ [] = []
>>>>       fmap f (x:xs) = f x : fmap (\y -> f y) xs
>>>> 
>>>> This definition is O(n^2) when fully evaluated,, because it causes O(n) eta
>>>> expansions of f, so we spend time following indirections proportional to the
>>>> depth of the element in the list. This has been fixed in 7.8, but there are
>>>> other examples. I believe lens, [1] for instance, has some stuff in it that
>>>> works very hard to avoid this sort of cost; and it's not always as easy to avoid
>>>> as the above example. Composing with a newtype wrapper, for instance, causes an
>>>> eta expansion that can only be seen as such at the core level.
>>>> 
>>>> The obvious solution is: do eta reduction. However, this is not operationally
>>>> sound currently. The problem is that seq is capable of telling the difference
>>>> between the following two expressions:
>>>> 
>>>>     undefined
>>>>     \x -> undefined x
>>>> 
>>>> The former causes seq to throw an exception, while the latter is considered
>>>> defined enough to not do so. So, if we eta reduce, we can cause terminating
>>>> programs to diverge if they make use of this feature.
>>>> 
>>>> Luckily, there is a solution.
>>>> 
>>>> Semantically one would usually identify the above two expressions. While I do
>>>> believe one could construct a semantics that does distinguish them, it is not
>>>> the usual practice. This suggests that there is a way to not distinguish them,
>>>> perhaps even including seq. After all, the specification of seq is monotone and
>>>> continuous regardless of whether we unify ⊥ with \x -> ⊥ x or insert an extra
>>>> element for the latter.
>>>> 
>>>> The currently problematic case is function spaces, so I'll focus on it. How
>>>> should:
>>>> 
>>>>     seq : (a -> b) -> c -> c
>>>> 
>>>> act? Well, other than an obvious bottom, we need to emit bottom whenever our
>>>> given function is itself bottom at every input. This may first seem like a
>>>> problem, but it is actually quite simple. Without loss of generality, let us
>>>> assume that we can enumerate the type a. Then, we can feed these values to the
>>>> function, and check their results for bottom. Conal Elliot has prior art for
>>>> this sort of thing with his unamb [2] package. For each value x :: a, simply
>>>> compute 'f x `seq` ()' in parallel, and look for any successes. If we ever find
>>>> one, we know the function is non-bottom, and we can return our value of c. If we
>>>> never finish searching, then the function must be bottom, and seq should not
>>>> terminate, so we have satisfied the specification.
>>>> 
>>>> Now, some may complain about the enumeration above. But this, too, is a simple
>>>> matter. It is well known that Haskell programs are denumerable. So it is quite
>>>> easy to enumerate all Haskell programs that produce a value, check whether that
>>>> value has the type we're interested in, and compute said value. All of this can
>>>> be done in Haskell. Thus, every Haskell type is programatically enumerable in
>>>> Haskell, and we can use said enumeration in our implementation of seq for
>>>> function types. I have discussed this with Russell O'Connor [3], and he assures
>>>> me that this argument should be sufficient even if we consider semantic models
>>>> of Haskell that contain values not denoted by any Haskell program, so we should
>>>> be safe there.
>>>> 
>>>> The one possible caveat is that this implementation of seq is not operationally
>>>> uniform across all types, so the current fully polymorphic type of seq may not
>>>> make sense. But moving back to a type class based approach isn't so bad, and
>>>> this time we will have a semantically sound backing, instead of just having a
>>>> class with the equivalent of the current magic function in it.
>>>> 
>>>> Once this machinery is in place, we can eta reduce to our hearts' content, and
>>>> not have to worry about breaking semantics. We'd no longer put the burden on
>>>> programmers to use potentially unsafe hacks to avoid eta expansions. I apologize
>>>> for not sketching an implementation of the above algorithm, but I'm sure it
>>>> should be elementary enough to make it into GHC in the next couple versions.
>>>> Everyone learns about this type of thing in university computer science
>>>> programs, no?
>>>> 
>>>> Thoughts? Comments? Questions?
>>>> 
>>>> Cheers,
>>>> -- Dan
>>>> 
>>>> [1] http://hackage.haskell.org/package/lens
>>>> [2] http://hackage.haskell.org/package/unamb
>>>> [3] http://r6.ca/
>>>> 
>>>> 
>>>> _______________________________________________
>>>> Glasgow-haskell-users mailing list
>>>> Glasgow-haskell-users at haskell.org
>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>> 
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140401/22a42c16/attachment-0001.html>