Lambda the Ultimate

A recent enlightening discussion on recursive type inference at comp.lang.functional brought the following tutorial paper on ML type inference to my attention.

A modern eye on ML Type Inference by Francois Pottier INRIA September 2005.

Hindley and Milner’s type system is at the heart of programming languages such as Standard ML, Objective Caml, and Haskell. Its expressive power, as well the existence of a type inference algorithm, have made it quite successful. Traditional presentations of this algorithm, such as Milner’s Algorithm W, are somewhat obscure. These short lecture notes, written for the APPSEM’05 summer school, begin with a presentation of a more modern, constraint-based specification of the algorithm, and explain how it can be extended to accommodate features such as algebraic data types, recursion, and (lexically scoped) type annotations. Then, two chapters, yet to be written, review two recent proposals for incorporating more advanced features, known as arbitrary-rank predicative polymorphism and generalized algebraic data types. These proposals combine a traditional constraint-based type inference algorithm with a measure of local type inference.

By now theories of computation are a dime a dozen. What makes any such theory interesting, at this stage of the game, is the perspective such a theory offers on computation. One aspect of algebraic theories -- like the lambda or the pi-calculus -- that has long intrigued me is that they are typically predicated on a theory of names. They'll tell you what a computation is as long as you are willing to pony up some notion of a name. Moreover, this notion of name has got to come equipped with a notion of equality to effect things like substitution in lambda and pi or synchronization in pi. And, since having an infinite set of atomic entities over which you specify an equality leads to too much computational power, a notion of name, equipped with an equality, sneaks in a notion of computation -- the very thing the algebraic theory is attempting to give an account of. In this light, even the 'pure' lambda calculus doesn't seem so pure.

Of course, the process calculi suffer this critique more severely than lambda does because there are natural name-free accounts of lambda, e.g. SKI, while proposals for name-free accounts of pi are turgid at best and it is unclear whether they extend naturally to variants like ambients. Further, i would argue that SKI loses much of the flavor of lambda and, more importantly, doesn't set up the theory of computation to extend well to other programming notions, like reference and mutability especially in higher-order situations. This may be a matter of taste, more than anything else, but as i argued above, theories of computation are cheap, at this point, and taste and sensibility seems to be the essential differentiating factor amongst them.

With this little preamble, let me give you, dear reader, a taste of a treatment of a reflective account of computation that side-steps this little conundrum about names. The presentation below presents a reflective account of lambda that is derived from a reflective account of pi, published in a workshop at ETAPS in 2005. The reason i went back to treat lambda after giving an account of pi is that it turns out that such an account for lambda is a wee bit trickier because lambda is implicitly higher-order while plain vanilla pi is not. An account that gives a lambda calculus emerging just out of term constructors in which there is a kind of alternation of name constructors and program constructors -- a feature whose rationale we will visit at the end of this little note -- turns out to be fairly tightly constrained and therefore may be of some interest to this community.

So, without further ado, here's the syntax:

M,N	::=		x	// terms are names
			P	// or programs
P	::=		L	// programs are the ur-program, L
			λx.M	// or abstractions
			MN	// or applications
			*x	// or unquoted or 'dropped' names
x	::=		^P^	// names are quoted programs

Two things to note about this grammar immediately:

1. There's a production for names! Names are quoted programs.
2. There's a strict alternation between name constructors and program constructors, i.e. there are no terms of the form ^^...P...^^; rather, '^' and '^' must surround programs.

As usual, we calculate bound occurrences of names recursively, via

FN(L)	=	{}
FN(x)	=	{x}
FN(λx.M)	=	FN(M)\{x}
FN(MN)	=	FN(M)∪FN(N)
FN(*x)	=	{x}

Next, we whack this set of terms down by the usual alpha-equivalence plus

^*x^ == x

Note, we could have achieved the same effect by moving *x from the production for P into the production for M,N; but, for uniformity (especially with the ETAPS presentation for a reflective pi) it was more natural to leave dequote (a.k.a. drop) among the program ctors -- because it is one.

Before giving the operational semantics, let me also point out the relationship between L -- another departure from the standard presentation of lambda -- and quotation. It turns out to get names to emerge just out of quoted programs you have to have a base, atomic program. In pi this is straightforward, it's the null process, 0. In lambda the choice of the base program turns out to be somewhat interesting; but, apart from it's dynamics, you have to have one and L is our base, atomic program. It's the first or ur-program. From the first program one can form the first name, ^L^. With this name one can form the first abstraction, λ^L^.L . With this one can form another name ^λ^L^.L^, evidently distinct from ^L^ and you're off to the races. You've got -- at least -- the terms of a lambda calculus where the variables are a bit funny, but no funnier than deBruijn numbers, to my taste, anyway.

Equipped with a set of (equivalence classes of) terms over which to compute, lets' write down the operational semantics. We have the usual beta reduction

(λx.M)N -> M[N/x]

but with a catch M[N/x] denotes semantic substitution, which we give now.

x[N/x] := N
y[N/x] := y (y <> x)
(λx.M)[N/x] := λx.M
(λy.M)[N/x] := λz.(M[z/y][N/x]) (y <> x, z ∉ FN(M)∪FN(N)∪{x,y})
(M1 M2)[N/x] := (M1[N/x])(M2[N/x])

all bog standard, so far, but now we get to the fresh tofu

*x[N/x] := *x (N not a name, i.e. of the form ^M^)
*x[^M^/x] := M
*y[N/x] := *y
L[N/x] := L

The upshot of these rules is that a dropped name is a place-holder to drop in a program frozen in a name. This is not terribly magical in lambda -- which is already higher-order -- but it is very powerful in pi and ultimately gives rise to a mechanism for interpreting the fresh name generator.

Ok, so we've got beta-reduction sorted, but we also have other terms, in particular, L, that have to be given semantics. It turns out there are a lot of possibilities for the dynamics of L, but here is one that seems very natural: it's a lambda constructor. I.e.,

L^M^N -> λ^M^.N

Note that some care must be exercised here. If we were to have the rule

LMN -> λ^M^.N

then because names are terms -- lambda is implicitly higher-order -- you could form

L^M^N which would reduce to λ^^M^^.N

defeating the strict alternation of name constructors and program constructors.

Finally, we add a minimal context rule

M -> M' => MN -> M'N

which makes our calculus reasonably lazy.

So, this gives you a calculus into which you can embed the lambda calculus (built over the name set of your choice) by the obvious translation scheme. But, this calculus is pure. It doesn't demand its user to pony up a set of names. It's a complete theory in and of itself. A notion of name equality can be built, recursively, using the notions of computational equality and straightforward syntactic equality of the finite set of term constructors.

Another perspective on these same statements is that we have a 'machine code'. Expressions in this calculus are completely closed with no need for dereferencing of symbols. It is name-free, like SKI, and could be used to build a different sort of virtual machine that is in many ways like the categorical abstract machine, but still retains much of traditional stack machine shape. But there is another intriguing possibility. First, i leave it as an exercise to the reader to write down an encoding of this calculus into binary. But, here's an open question: is there an arithmetic formula that corresponds to the reduction rule? More formally, is there a binary encoding

B : M -> {0,1}*

and a function

R : {0,1}* x {0,1}* -> {0,1}*

s.t.

R(B(M),B(N)) = B(D) whenever MN ->* D and D doesn't reduce?

If such a function did exist it might be the basis for a really, really fast implementation of lambda.

Finally, let me point out an intriguing connection with games semantics that gives some support for the alternation of name constructor and program constructor as desiderata. i discovered this when thinking about adding quotation to set theory. The basic idea is that you can interpret program constructor as question and name constructor as answer and role of player versus opponent as the dividing line between program and environment.

It's these connections and questions, apart from any real affection for 'purity', that make an account of this shape interesting to me and i hope to others as well.

The Joins Concurrency Library. Claudio Russo.

Comega extended C# 1.x with a simple, declarative and powerful model of concurrency - join patterns - applicable both to multithreaded applications and to the orchestration of asynchronous, event-based distributed applications. With Generics available in C# 2.0, we can now provide join patterns as a library rather than a language feature. The Joins library extends its clients with an embedded, type-safe and mostly declarative language for expressing synchronization patterns. The library has some advantages over Comega: it is language neutral, supporting other languages like Visual Basic; its join patterns are more dynamic, allowing solutions difficult to express with Comega; its code is easy to modify, fostering experimentation.

In the Joins library, the scheduling logic that would be compiled into the corresponding Comega class receives a separate, first-class representation as an object of the special Join class. The Join class provides a mostly declarative, type-safe mechanism for defining thread-safe synchronous and synchronous communication channels and patterns. Instead of (a)synchronous methods, as in Comega, the communication channels are special delegate values (first-class methods) obtained from a common Join object. Communication and/or synchronization takes place by invoking these delegates, passing arguments and optionally waiting
for return values.

The library also supports dynamic joins, which are not available in Comega, implemented by joining arrays of channels (with the size of the array being determined at runtime).

The major weakness of the Joins library is speed, since the static apporach of Comega provides more room for optimization (see the brief discussion in sec. 6).

This will be of interest to LtU readers in India and maybe for others as well.

Data Parallel Haskell: a status report. Manuel M. T. Chakravarty, Roman Leshchinskiy, Simon Peyton Jones, Gabriele Keller, and Simon Marlow.

We describe the design and current status of our effort to implement the programming model of nested data parallelism into the Glasgow Haskell Compiler. We extended the programming model and its implementation, both of which were first popularised by the NESL language, in terms of expressiveness as well as efficiency of its implementation. Our current aim is to provide a convenient programming environment for SMP parallelism, and especially multicore architectures. Preliminary benchmarks show that we are, at least for some programs, able to achieve good absolute performance and excellent speedups.

NESL was mentioned here in the past a few times, as was data parallelism in general.

I just heard about Papert's tragic accident. Thankfully, what I am reading suggests that his condition is improving.

Papert is the father of the Logo programming language which, apart from being the first programming language I learned, is one of the most important attempts to use computers, and programming in particular, in education.

Flowers for Seymour is an attempt to create a virutal flower album to provide emotional support for Papert and his family. This is a nice gesture, and I hope the LtU community will contribute to it. The album includes only a few flower images created in Logo, which is a shame. It would be nice to see more images created using the wonderful tool Papert gave us.

Our prayers are with Seymour Papert and his family.