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?

• Andrej Bauer: A closure is an implementation concept, as well as heap, so it makes no sense to say "functional programming (FP) language without closures". At best you could say "an implementation of a FP language without closures", in which case we can answer that there are implementations of FP which do not use closures. I think you need to rephrase your question. Perhaps you are asking whether a FP language with only first-order functions is complete? That would make more sense, but then you need to be precise about what primitive types you admit. If you put in nat it'll be Turing complete.
• Andrej Bauer: Thanks for rephrasing. Now it's not a research-level question anymore :-) I recommend that this be migrated to cs.stackexchange.com where we'll provide some standard references and point out that functional programming languages are compiled efficiently on today's hardware. (I can come up with an infefficient way of compiling while-loops, too.)
• user36006: Actually i'm not looking for standard optimizations like tail recursion or the like. I'm interessed in transforming lambda calculus expressions into another formal system. A formal system which does not require closure environments, when implemented.
• user36006: Transforming higher-order functions (lambda expressions) into first-order functions would exactly solve this issue. Unfortunately first-order functions are not Turing complete. As you mentioned in your first comment, first-order functions with the extension of primitive types can be Turing complete. Is there such a well-known formal system? If so, it would be possible to convert lambda expressions into this system.
• Marc: What do you mean by first-order function exactly?

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.

• Blaisorblade: All formalizations of algorithms, except lambda calculus, give Turing-complete formal systems without higher-order functions—starting from Turing machines. Also, defunctionalization is a well-known way to turn a higher-order program into a first-order one. > I'm quite amazed that there seems to be very little research on this topic. Only if you ignore all the research on the topic. I suspect you're not finding answers due to unusual phrasing.