#unlambda

[esoteric-codes]

Interview with David Madore

David Madore is responsible for one of the best-known and most-confounding esolangs of all time: Unlambda. The language is based on the SKI combinator calculus, a super-minimalist computational system used in the mathematical analysis of algorithms, but considered impractical for coding. In Unlambda everything is a function that takes a single variable, so there are no indicators like ()s to take parameters. Like the SKI calculus, it entirely eschews variables and the lambda indicator, and so is described as lambda-without-the-lambda. If this is entirely new to you, the second half of this post is a nice introduction. Madore, an accomplished mathematician, is also responsible for languages that play at the edges of infinity. His main web presence is his webpage from his undergrad days thirty years ago, which remains a fascinating portrait of the sincerity, optimism, and banalities of the early Web. He is also on Twitter with a handle derived from his engagement with The Hackers' Zen.

In response to a flurry of questions about creating Unlambda, Madore gives us some notes:

I think I came up with Unlambda in 1999. I knew very little about other esolangs at the time (and I still don't know much about them), that is to say, I knew a bunch of names but didn't try programming in any of them.

I was reading a book on logic that mentioned the Hilbert-style axioms (S: (A⇒B⇒C)⇒(A⇒B)⇒A⇒C; K: A⇒B⇒A; and I: A⇒A) and I was simultaneously thinking about the Curry-Howard correspondence between proof systems and typing systems, so I thought about what these axioms meant in terms of functional programming and how we could use them to re-explain the lambda-calculus without lambdas: this is how I came up with Unlambda. The 'c' function is because I was also fascinated by call/cc at the time (and still am, I guess), especially as it also has a nice interpretation in the Curry-Howard correspondence as Peirce's law (((A⇒B)⇒A)⇒A). The 'd' is clearly an error of mine, I should never have included it, it's unnecessary (I thought it might be, but it was a misunderstanding on my part of how normalization proceeds) and it makes the language far less elegant (on the other hand, it makes the interpreter's job a bit more complex, which is maybe fair for an obfuscated programming language).

At the time, I was thinking about proposing another obfuscated programming language in a somewhat similar flavor, where everything would be written in continuation-passing-style (no function ever returns), but never got around to it.

I think Unlambda got some attention from various teams writing compilers with multiple front-ends or stuff like that, or in compilation courses, because it can be an interesting test case, toy example or illustration.

I once had a page in Wikipedia because of Unlambda, but it was later decided that I wasn't notable enough. :-(

[Ed note: while Madore's page is gone, Unlambda's lives on]

READ MORE...

[vash3r]

ah this is a fun reminder of when i played around a lot with unlambda. (one of the main benefits of only having pure single argument functions is everything is the same type). it was really interesting how exp was the simplest basic operation to express. n^m = exp n m = `mn so exp=``s`k`sik [apply-to] or exp'=i [identity], while succ, mul and plus are more complex because the actual function or argument to be eventually acted on can't be abstracted as far away (0=`ki, 1=i, 2=\f.``s`kff= ``s``s`kski and so succ=`s``s`ksk, plus = `[applyto][succ], mul=``s`ksk)

(* Type definition for Church numerals. *)

Definition cnat := forall X : Type, (X -> X) -> X -> X.

(* Examples (fun creates an anonymous function) *)

Definition zero : cnat := fun (X : Type) (f : X -> X) (x : X) => x.

Definition one : cnat := fun (X : Type) (f : X -> X) (x : X) => f x.

Definition two : cnat := fun (X : Type) (f : X -> X) (x : X) => f (f x).

(* Arithmetic *)

Definition succ (n : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => f (n X f x).

Definition plus (n m : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).

Definition mult (n m : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => n X (m X f) x.

Definition exp (n m : cnat) : cnat := fun (X : Type) (f : X -> X) (x : X) => (m (X -> X) (n X) f) x.