kena

Haskell’s magic wand is stunted, on purpose

In lecture on November 25, 2012 at 12:00

An absolutely stunning feature of the lambda calculus is that it allows us to define functional recursion without using recursion. That is, the concept of recursion is fundamentally a by-product of being able to reproduce multiple copies of a function’s input in its output.

In other words, the “essence” of functional languages does not require recursion, because it is theoretically possible to define recursion from other functional concepts without using recursion itself.

But Haskell can’t do.

The gist of this feature is the existence of non-recursive fixed-point combinators.

To simplify, a fixed point combinator is a function which can equip other, non-recursive, functions a posteriori with the ability to call themselves, that is, recurse. So if a language has non-recursive functions and a fixed-point combinator, it becomes possible to define recursion with it. The beauty of the whole affair is that lambda calculus allows us to write fixed-point combinators without using recursion in their definition. One such fixed-point combinator is called Y, and looks as follows:

Y = λf.(λx.f (x x)) (λx.f (x x))

Y is obviously not recursive: if it was, its name would be part of the right hand side of its definition. But once Y is defined, we can turn a non-recursive function into a recursive one, for example as follows:

add = λf.λn.(if (n == 0) then n else n + (f (n-1)))

add_r = (Y add)

In this example, “add” is obviously not defined recursively; it merely accepts a functional argument “f” and uses it when its second argument “n” is not zero. The second function “add_r” is also not defined recursively. However, the result of applying Y to “add” makes the resulting function recursive. In this example, “add_r 10” evaluates to 55 as expected.

Because functions like Y exist, one can bring the ability to recurse in any language sufficiently akin to lambda calculus, even if the language does not provide the ability to simultaneously name a function (i.e. write “X” in the right-hand side of “=”) and use the name in the function’s definition (i.e. write “X” in the left-hand side of “=”).

This is possible in Lisp, Python, ML, JavaScript, as well as most other functional languages in use nowadays.

But strangely, Haskell, the famously acclaimed state-of-the-art functional language, cannot define recursive functions without using recursion from another part of the language.

As discussed in this thread, any fixed point combinator in Haskell must be either defined recursively, for example

C = λf.(C f)

or it must be defined using a recursive data type, for example as follows:

newtype Mu a = Roll (Mu a → (a → a))
unroll (Roll x) = x
C’ = λf.( (λx.λz.(f ((unroll x) x z)))
(Roll (λx.λz.(f ((unroll x) x z))))  )

Here C’ is not recursive, but uses the type Mu which is.

What gets in the way is Haskell’s type system.

The Haskell implementers chose to reject (make invalid) all non-recursive fixed-point combinators defined without recursive types because it solves another problem much more interesting to programmers: the ability of the language’s compiler to automatically determine the type of any function, even lazy functions definitions that operate on “infinite” data definitions. Indeed, it would not be possible in Haskell to automatically compute the type of all functions if non-recursive fixed-point combinators were also supported, because that would be equivalent to solving the Halting problem.

Because lazy function definitions were deemed so useful, support for non-recursive fixed-point combinators was abandoned as a trade-off.

This choice costs Haskell the loss of the most sexy feature of (untyped) lambda calculus, in order to promote functional laziness and recursive data definitions to software engineers.

Advertisements
  1. Could you elaborate on how much of a loss it is to not have fixed-point combinators in a programming language?
    I mean, if Haskell could support Y, would you use it in your code? I have never felt that need, in any language.

    I have no doubt that fixed-point combinators are an elegant mathematical concept. I see no problem about considering their applicability to real-world languages. But I fail to see the point of presenting their absence as a drawback of a language; it feels so out-of-place…

    I can think of two reasons I could be wrong. First, maybe they could actually be used to make my code better and I haven’t understood how.
    Second, maybe there are people trying to prove theorems on Haskell and they can’t because of the lack of fixed-point combinators. But considering that Haskell does support recursion, I suppose it would not be a problem to fix their proofs.

  2. The argument was mostly about elegance vs. real-world (engineering) priorities. Nowhere did I mention the word “drawback.”

    As you have intuited already, integrating recursion as a basic language feature (instead of a derived feature, as in pure lambda calculus) does not get in the way of proofs.

    The only “benefit” of being *able* to express non-recursive fixed-point combinators is that it suggests a certain form of *additional* flexibility in the core language if you want to add language extensions or domain-specific languages in the future. Haskell trades this extra flexibility, which is seldom used in practice, for a quite useful type system.

  3. We seem to agree. But that ‘additional flexibility’ remains a bit unclear to me. I can’t imagine how to make use of it… Maybe something related to continuations?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: