How to implement a functional programming language efficiently?

Question

Thanks to Petr and Andrej for their feedback. I'm rephrasing my question and give a bit of a context:

Functional programming languages are mostly based on lambda calculus. Implementing a functional language straight forward is inefficient on today's hardware. For example:

\begin{eqnarray} f &\equiv&\ \lambda x.\lambda y.\ x+y \\ g &\equiv&\ f\ v \end{eqnarray} Those functions will have the following types: \begin{eqnarray} f &\colon& a \rightarrow b \rightarrow c \\ g &\colon& a \rightarrow b \end{eqnarray}

Now the function $g$ needs to store the variable $v$ in an runtime environment, when the variable $v$ is only accessible in a specific context. This concept is known as closure.

I'm looking for an method to eliminate all closures in a given program and avoid the allocation of environments at runtime.

• Is this even possible?
• What are the disadvantage of such an algorithm?

Thanks to Petr for mentioning the S-K basis. As I understand, the combinator graph reduction will put any function in a point-free style. However by applicate arguments partially, there is still some form of environment necessary.

Original question:

• Is a purely functional programming language like Haskell still turing complete without the concept of closures?

• Or the other way around: Is it possible to eliminate all closures in a Haskell program in order to use no heap space?

Answer 1

It's not entirely clear what do you mean by a functional programming language without closures. Can you give an example?

Functional programming languages are usually based on lambda calculus, whose essential part is that you can have open lambda terms. For example the term for the constant function (the K-combinator) $\lambda x . \lambda y . x$ can be viewed as a function that given $x$ returns a constant function that returns $x$ on any argument - a closure of the open term $\lambda y . x$.

However you can use another basis, a combinatory calculus such that it's power is equivalent to the lambda calculus. Then you can take a lambda term and convert it into an equivalent combinator that doesn't use any variables at all, so there are even no closures to talk about - see Completeness of the S-K basis. Which I believe answers yes to your question.

This is actually what Haskell compilers do under the hood. Evaluating lambda terms with variables is very inefficient and cumbersome, so they convert the program to a representation without variables and use techniques such as combinator graph reduction.

I can recommend two books on the subject which are both available online, the first one more theoretical, the second one focused more on the actual implementation techniques:

• The Implementation of Functional Programming Languages, Simon Peyton Jones, published by Prentice Hall, 1987.
• Implementing functional languages: a tutorial

Answer 2

I answer to my own questions since I found a partial answer.

The Kappa calculus sounds very promising. From the Wikipedia article:

Unlike lambda calculus, kappa calculus has no higher-order functions; its functions are not first class objects. Kappa-calculus can be regarded as "a reformulation of the first-order fragment of typed lambda calculus".

Because its functions are not first-class objects, evaluation of kappa calculus expressions does not require closures.

Because the kappa calculus does not use any higher-order functions, there is no need for closures. Unfortunately the kappa calculus is not Turing complete and for this reason there is also no way to transform any lambda calculus into to a kappa calculus.

So this answer is not completely satisfying, but it gives some insights what is needed to avoid closures. The goal of this question is to find a formal system with the following properties:

• The formal system does not require closures
• The formal system is Turing complete

From my understanding this is achievable if the system..

• is based on first-order functions
• allows recursion
• has primitive types as $\mathbb N$

First-order functions must be used to avoid closures and the two other requirements should guarantee Turing completeness. If someone can name such a system, I will mark it as accepted answer.

There is also a related Post on Stackoverflow. The accepted answer mentions MLton, which apparently reduces in some way higher-order functions to first-order. Sadly I can not find any documentation regarding this system.

I'm quite amazed that there seems to be very little research on this topic.