Lambda the Ultimate

I’m confused about the relation between closures and the implementation of higher-order functions. My understanding is that closures were first used to implement higher-functions in Scheme and that closures play the same role in languages such as Perl and Python. Other functional languages don’t appear to make explicit mention of closures. In my own experience with the language K, I can directly pass and return functions to and from other functions, with no reference to a lexical closure. So I’m tempted to conclude that closures are simply one technique for implementing higher on functions. However I read in CTM:

Higher-order programming is the collection of programming techniques that become available when using procedure values in programs. Procedure values are also known as lexically-scoped closures.

Can anyone give me some insight here, or just a reference for further study?

The understanding of state is one of the oldest and newest areas of research. The Event Calculus provides a precise logical semantics of state and situation. There is an interesting survey paper at the bottom of the page with all the details: "Event Calculus in Classical Logic" . Also a previous discussion topic: Dynamic Semantics .

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:

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

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.

I like typing, and I see lots of things about programs that could perhaps stand to be typed that aren't. For example, I'd like a type that says if a call is (well, expected to be at any rate) synchronous or not (and then some way of using that information to catch "i assumed..." bugs).

Assuming there is a large raft of concepts that could be turned into useful types and incorporated into a language, how does one prevent the typing annotation (either manually entered or, preferably, automatically derived as much as possible) from being too much of a burden - visually in the source code, if nothing else?

I guess things like annotations or JML are an example of one way to format it all: have laundry lists at the top of the function definition. Having some (multiple) inheritance system might work, although then you are in the painful world of sorting through the hierarchy to figure out what your particular concrete item really is.

While talking about Haskell in this post, I believe the question is more general, and therefore on-topic on LtU.

I use Haskell rarely, so every time I do use it, I catch myself reimplementing standard functions, only because I do not know them by name, or in which module they are.
Sometimes I am not sure, whether some function I need is really standard, or can be obtained by composing several standard functions with a possible minor inclusion of custom code. E.g., should I implement a function with the following type from scratch:

Ord t => [(t, a)] -> [(t, b)] -> [(t, Either a b)]

Could there be a tool that helps me out by suggesting possible implementations?

Note that I intentionally do not describe the meaning of the function, but only its type - the idea is to either imitate "theorems for free" and deduce the only natural implementation, or to find existing functions with matching type, or even better a combination of both.

Can something like that be implemented as mere (IDE) tool on top of existing Haskell type system, or it is not rich enough and I have to use Epigram?

[On edit: I should probably rephrase the question: how far can this tool go using Haskell type system? It is obvious that some degree of deducing is possible, and then again some other is not. E.g., I am not sure it's reasonable to expect the tool to suggest using an existing function with type (x -> y -> Ordering) -> [x] -> [y] -> [Either x y] with additional code to witness isomorphism(?) of these types.

BTW, as soon as I typed the word "isomorphism" I remembered that I probably should look at Frank Atanassow papers...]

I am working on modeling the typed SK calculus in Cat, and I have reached an impasse. I believe it is well established that the type of the K combinator in most functional languages can be expressed:

  K : 'a -> 'b -> 'a

The dilemma I am facing is how I should model this in a typed stack-based language (or concatenative language if you prefer). I am wavering between two possibilities:

  K1 : ('a -> ('b -> 'a))
  K2 : ('a 'b -> 'a)

So far it appears that both approaches are valid, they simply differ in whether the "function application" operation is implied in the K combinator or not. Allow me to demonstrate:

  42 K1 : ( -> ('a -> 42))
  42 K2 : ('a -> 42)

In plain english K1 will push a function onto the stack if given one
argument, while K2 is only partially evaluated if given one parameter.

Adding another argument illustrates the issue more clearly:

  x 42 K1 apply == 42
  x 42 K2 == 42

The same problem can also be framed in terms of the I combinator:

  [f] I == [f]?
  [f] I == f?

I was wondering if anyone has any insight into this problem that they could share?

Heading into the fourth chapter of SICP, I figure that either I could attempt to build a metacircular ML or cheat and just implement a Scheme interpreter. Going down the path of least resistance, I was wondering if there are some minimalist implementations of Scheme available in Standard ML?

Hi all,

Since functional reactive programming has come up here a few times in the past, I figured my posting of this wouldn't be too out-of-place...

I've been working for the past few months on a functional reactive GUI system for O'Caml called "O'Caml Reactive Toolkit". The core FR logic is based heavily on Haskell's Yampa, while the FR API is modelled after PLT Scheme's FrTime (users of FrTime should feel at home with the API), so there is not much new there. The novelty is in the GUI API, which constructs a GUI via functions, in contrast to systems such as Fudgets (which uses arrows), or SuperGlue (which uses objects with explicit signal connections). The goal in API design is simplicity and clarity. As an example, here is a toy temperature conversion program:

open Fr
open FrGui

let _ =
    let temp_box, temp = float_entry 20. in
    let fahrenheit = lift ((@temp -. 32.) *. 1.8)
    and celsuis = lift (@temp /. 1.8 +. 32.) in
    let main_window = window
        ~title: "Temperature converter"
        (hbox [
            hbox [label "Convert "; temp_box; label " to:"];
            vbox [
                hbox [label "degrees Fahrenheit: "; float_view fahrenheit];
                hbox [label "degrees Celsius: "; float_view celsius]]]) in
    run_dialog (main_window, main_window#close)

The temperature entered by the user is instantly converted to both degrees Fahrenheit and degrees Celsius. (Note the definitions of "float_entry" and "float_view", although trivial, have been left out to save space.)

Though O'Caml RT is far from complete I made a prerelease because I want to solicit feedback from others who are interested in functional reactive programming. I made a web page providing links to the source code, documentation, and (coming soon) examples. It's known to compile on Mac OS X and Linux, and it should be possible already to write many simple GUI applications using it.

My questions to you are:

• Am I duplicating work? I know of systems such as Fudgets (arrow-based) and SuperGlue (object-based); would I be better off to use one of those as a model than to create my own?
• What would you want to see in a functional-reactive GUI toolkit? i.e. what things which are often awkward to express in procedural langauges do you think should be made easy in O'Caml RT?
• What are some examples of things which are easy in procedural languages but you think would be awkward in a functional-reactive setting?
• Is the API clear and understandable? e.g. does the above example make sense (even to those who don't know O'Caml)?

Thanks in advance for your feedback!

(P.S. I don't want this to come off as a plug for O'Caml RT... if any of the admins feel this is too specific a topic for LtU I'll try to find a more appropriate forum to discuss it in.)

I don't want to to turn LtU into a branch of Amazon but I've got a copy of "A theory of programming language semantics" by Milne & Strachey (hard cover, 2 volumes, good condition, pub 1976) to dispose of. I'm not a dealer, just a recently retired academic disposing of books I sadly realise I'll never read. I hate giving books to charity shops if I know there a 99% probability they'll just get pulped. Surely on LtU there is someone with an interest in programming language history?

I've just added it to Amazon for £60 (the other copies there are over £100) but if anyone wants to make a case for getting it cheaper (e.g. you are researching the history of programming language semantics - must be thousands of you out there!) they can contact me via Amazon.

The amazon link is: A theory of programming language semantics

I've written a compiler for a subset of the Factor programing language targeting Javascript as the compiled language. The blogposts describing the compiler and its implementation are here:

• Factor to Javascript Compiler
• Factor to Javascript Compiler Updates
• Continuations added to fjsc

The actual working example is at: http://factor.bluishcoder.co.nz/responder/fjsc/

The compiler itself is written in Factor and runs on the server. In the example I take the users input, send it to the server via Ajax and eval the result when it comes back. The compiled javascript returned is displayed in a textarea for testing.

I basically started it as a test project for my post on Compilers and Interpreters in Factor but it was a bit big for that. I shelved it for a while and decided to finish it while I'm not in paid employment.

The main difference from 'real' Factor is that I don't support parsing words and I've not implemented much of the standard library. What parsing word functionality I wanted to support I built into the parser itself. The parser is written using Parser Combinators and produces an abstract syntax tree. I then compile this into Javascript.

There is a parser to convert from a string of Factor code to the AST as well as from already parsed Factor quotations from the server Factor instance. This allows writing code on the server in Factor, and converting it to Javascript without having to do any string generation of Factor or Javascript code manually.

I wanted to support continuations so I ended up generating the Javascript in continuation passing style. It results in ugly code but makes it easy to do callcc. An example of generated code (from '1 2 + alert'):

factor.push_data(1,
       function() {
         factor.push_data(2,
           function() {
             factor.find_word("+").execute(
               function() {
                 factor.find_word("alert").execute(factor.cont.next)
             })
           })
         })

The main problem with this approach is it will blow the browsers call stack pretty quickly. I use a workaround for this by counting the number of times I call the next continuation. When it reaches a certain threshold I pass it to setTimeout instead of calling it. This effectively jumps out of the call stack and starts it again. It also has the side benefit of releasing processor cycles to the browser and avoiding 'time consuming script' messages. I came across this approach in this LtU article. Apart from this I don't do any other optimisations yet.

The continuations are multi-shot and can be attached to event handlers. For example, the following attaches a normal quotation to the onclick event handler of a button with id 'test':

"click" "#test" elements [ "clicked" alert ] bind-event ;

Or a continuation:

[
    [
      >r "click" "#test" elements r> [ continue ] curry bind-event
      "Waiting for click on button" alert
      continue
    ] callcc0
    drop "Click done!" alert 
  ] callcc0

Factor has Erlang style concurrency (processes as lightweight threads and message passing) and I plan to port that library to the javascript version. I have a comet library that allows sending messages to and from the browser to Factor processes - I think it'd be pretty neat to be able to write processes on the browser in Factor that communicate to processes on the server in Factor.

I hope this is interesting enough to post here - I usually don't write about stuff I wrote myself but I thought it would be interesting as other compiler->javascript projects have been discussed. At the very least it might prove useful as a playground for those who want to try out a concatenative language like Factor or Joy.