Let's start by kicking off the Palatable Untyped Lambda Calculus project, or PULC, pronounced like "pulse." A while ago I was inspired by John Tromp's Binary Lambda Calculus encoding of the untyped lambda calculus. The interesting property of BLC is its extremely compact, 210-bit universal machine. That's 26¼ bytes, an entire language interpreter within two

*Hello, world!*s. This is due to its compactness and simplicity as a language. There is little to express, and it is very expressive. But what about more sophisticated programs? Does the expressiveness remain when the ideas start piling up? The only way to find out is to try and see.

Sophisticated programs written in untyped lambda calculus are few, however. Every language is bound together with its idioms and usage, and lambda calculus shows its heritage as a mathematical formalism, not a programming language. It is typically used with a "unary" number system, akin to counting on your fingers. In common terms, the time and storage required to add two numbers in this system grow exponentially with the numbers' lengths. This is completely impractical. Lambda calculus is usually used to annotate a mathematical "narrative" in natural language, or in a figurative sense for anonymous functions in a computer program (hence "lambdas" in Python and C++). It is used to write phrases, not stories.

Is there a good reason not to build larger programs in untyped lambda calculus? Poor idioms can be left behind. Tromp suggests a couple binary natural-number encodings in his paper, to solve the unary issue. It is also easy to build definitions upon definitions, to avoid embedding everything within another language. One obvious problem is that it is untyped, hence missing a cornerstone of programming practice. Type verification can be moved outside the language proper, though. It can be treated as part of software testing, manipulated by annotation and interactive tools. Well, I'm beginning to speculate. But it's certainly possible to get far enough in an untyped language to be able to write a typechecker in it. And such a program might expose the high-level qualities of the language.

So I see a challenge, and one which is true to the original spirit of lambda calculus. It is the foundation of all functional programming, but usually it is buried under a load of syntactic sugar. Modifying language syntax is the easy way out, but most problems can be solved with a good idiom instead. What is the most efficient way to represent the essential concepts? When the best idioms, tools, and representation formats are used, how efficient and elegant can this language be?

*How far do you get with only the most fundamental formalization of the notion of abstraction?*

To meet this challenge and answer these questions is the object of PULC. At the least, it will be educational.

This comment has been removed by a blog administrator.

ReplyDelete