Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

https://woodrush.github.io/blog/lambdalisp.html

by woodrush • 4 years ago

189 100 4 years ago

woodrush.github.io

lisper18• 4 years ago

This is one of the most mind-blowing things I have ever seen. Words fail me, so I'll appropriate some of the author's:

"Lisp has been described by Alan Kay as the Maxwell’s equations of software. In the same sense, I believe that lambda calculus is the particle physics of computation. LambdaLisp may therefore be a gigantic electromagnetic Lagrangian that connects the realm of human-friendly programming to the origins of the notion of computation itself."

BTW, if you have no idea what is going on here, eight years ago I took a whack at writing a gentle introduction to this same sort of thing, but done in a more half-assed way, and with a much less ambitious scope:

https://flownet.com/ron/lambda-calculus.html

eointierney• 4 years ago

Delightful, thank you

bobbylarrybobby• 4 years ago

Fantastic read, thanks.

haskellandchill3• 4 years ago

Then what is System F?

invisiblerobot2• 4 years ago

polymorphic typed lambda calculus.

it's the theoretical basis for ML and Haskell.

https://en.wikipedia.org/wiki/System_F

invisiblerobot2• 4 years ago

Oh I see, you were asking rhetorically :)

smitty1e• 4 years ago

Here is a PDF showing its entire lambda term, which is 42 pages long:

Elsewhere, Douglas Adams smiles.

zentr1c3• 4 years ago

This

lisper18• 4 years ago

Hm, I wonder if the authors fine-tuned the feature set (and font size!) to achieve this outcome :-)

somewhereoutth9• 4 years ago

Ah but this is where it becomes interesting! Because we can then guage how much work this abstraction is doing for us - and indeed whether or not it might stray from the 'one true path' (whatever that might be)

zentr1c3• 4 years ago

Maybe I am stupid but what's the point in reimplementing lisp in lambda? Just to prove how beautiful simple lambda calculus is? The lambda functionality is allready in lisp. And lisp is beautiful simple!

() is nothing and (is something) What does the implementation show more beautiful than that?

tromp13• 4 years ago

Binary Lambda Calculus is indeed beautifully simple [1]. LISP is rather complex by comparison, but then it's full-fledged non-esoteric programming language.

[1] https://www.ioccc.org/2012/tromp/hint.html

jart• 4 years ago

We do what we must because we can.

actually_a_dog• 4 years ago

This is undoubtedly cool, but I'd be really impressed if it wasn't stupidly slow. (I'm not saying it is stupidly slow, because I haven't had a chance to run it, just that I'd be impressed if it wasn't.)

lisper18• 4 years ago

I haven't tried it either, but I would not bet my life savings on it being slow. I tried something similar to this a few years ago (see my top-level comment for a pointer) and was amazed at how fast it turned out to be.

quickthrower23• 4 years ago

It has to be slow. Multiplication will be O(N^2)!

sudosysgen• 4 years ago

Multiplication is generally done in O(n^2) of the number of bits so I'm not sure what you mean to say. Do you mean O(n^2) of the size of the operands?

woodrush3• 4 years ago

Thanks for your feedback, I forgot to mention the execution speed in the post. The number guessing game example (44 lines long) in the Usage section actually runs with an instantaneous response time on the terminal. I added some remarks on the execution speed.

tromp13• 4 years ago

As author of the Binary Lambda Calculus (BLC), I find this quite fascinating. It implements LISP in 163,654 bits of BLC. For comparison, minimal esoteric languages like BLC itself can be implemented in 232 bits of BLC, and Brainfuck in 893 bits.

I'm still reading the document, but one thing that caught my eye is the List encoding with cons and nil, which is claimed to be a Mogensen-Scott one.

Rather, cons \x\y\c. c x y is the Scott encoding of infinite lists that have no nil terminator (also known as streams) and thus only one constructor, while nil is the Scott encoding in nil-terminated lists with 2 constructors.

Thus the given encoding is some non-standard hybrid of streams and lists that helps BLC achieve its conciseness. In Wikipedia [1] it's described as

Alternatively, with NIL := FALSE, the construct l (λh.λt.λz.deal_with_head_h_and_tail_t) (deal_with_nil) obviates the need for an explicit NULL test

[1] https://en.wikipedia.org/wiki/Lambda_calculus#Pairs

lisper18• 4 years ago

It implements LISP in 163,654 bits of BLC. For comparison, minimal esoteric languages like BLC itself can be implemented in 232 bits of BLC, and Brainfuck in 893 bits.

That's hardly a fair comparison. LambdaLisp includes a ton of features that BLC and BF do not.

keithalewis2• 4 years ago

Slap yourself and reread the rest of the post.

tromp13• 4 years ago

Writing in continuation-passing style also helps the lambda calculus interpreter to prevent re-evaluating the same term multiple times. This is very, very important and critical when writing programs for the 521-byte binary lambda calculus interpreters Blc, tromp and uni, since it seems that they lack a memoization feature, although they readily have a garbage collection feature.

Note that Melvin Zhang added a memoization feature (call-by-need evaluation with result sharing) in his refactoring [1] of my BLC interepreter.

[1] https://github.com/melvinzhang/binary-lambda-calculus

tromp13• 4 years ago

The pattern \lambda a. \lambda b. \lambda w. \lambda x. \lambda y. yλa.λb.λw.λx.λy.y is noticable in many places in lambdalisp.pdf, since isnil is used a lot of times in LambdaLisp.

Sadly, this heavy use of the isnil operator derived in section [1] adds a lot of unnecessary verbosity, since instead of writing

    isnil list
      result1
      (let { head = car list, tail = cdr list} in result2)

one can simply write

    list
      (\head \tail \_ . result2)
      result1

[1] https://woodrush.github.io/blog/lambdalisp.html#deriving-isn...

woodrush3• 4 years ago

Thank you for taking a look, and many thanks for your constructive comments. I found the BLC language and interpreter to be elegant and that was what brought me here.

I was unaware of the nil-test-free method for Scott-encoded lists. It's true that it would remove a lot of bits from LambdaLisp's implementation. I'll also be using this for future projects. I was also unaware of Melvin Zhang's interpreter. I suspect that result sharing would improve the execution speed. I'll try to add that in one of the supported interpreters in the repository. Thank you very much for thoroughly reading my post and pointing these facts out. It has deepened my understanding and interest for binary lambda calculus.

I also want to say that Lazy K is one of my all-time favorite languages, as I mentioned in the post. It was about 10 years ago when I first found out about Lazy K - at that time I wrote a blog post about a language I made that directly transpiles to Lazy K (written in Japanese). Although at that time I couldn't fully grasp the language, I'm happy that now I could write large programs for Lazy K. I was thrilled to find that the Lazy K language proposal was now published on your website.

somewhereoutth9• 4 years ago

Lambda calculus is mathematically foundational in a way that Lisp of course isn't.

The question is what does Lisp give us as an interpretation of those foundations? Or does it admit issues that might be unhelpful? (Are macros a good thing?)

lisper18• 4 years ago

Let's not sell Lisp short here. LC might be mathematically foundational, but I think it's fair to say that Lisp is computationally foundational. Mathematics and computation are related, of course, but they are not identical. Computation is the study of mechanical processes for doing math. As such, Lisp's identification of CONS/CAR/CDR/COND as a sufficient set of primitives for a universal Turing machine is important because it's obvious (or at least it was obvious by 1958) how those primitives can be implemented as a mechanical process. Implementing LAMBDA in all its generality is far less obvious, which is why it took 20 years of further research to go from Lisp 1 to Scheme.

somewhereoutth9• 4 years ago

I'd say that all foundations are mathematical (at least for 'concrete' stuff, and more besides). If lisp was foundationaly interesting presumably mathematicians would have given it more study? (perhaps they did?)

I would disagree that computation is process for doing math - it is math in its own right, specifically that for operating over a discrete state space (urgh help needed to tighten this statement up)

LC is basically a rewrite engine, so I'm not sure it would be so hard to implement? Probably some plastic bags, in two colours, paper scraps, and a marker pen would do it? (Edit - one colour bag would need 2 ordered compartments - or if you really have lots of spare time you could build it all with just plain bags and some set theory) However as you say perhaps Lisp is a better abstraction over the Turing tape (yuck).

kazinator20• 4 years ago

LC is only computationally foundational; it describes recursive functions. It's just another universal turing machine.

LC has a great disadvantage: it's difficult to write a LC interpreter in LC. This project shows exactly what that means. To write an LC interpreter, you need a data structure for representing expressions. You need a symbolic data type.

LC does not know what a LC expression is. Papers about LC know what that is, but they are not executable.

In Lisp we can say, okay, lambda calculus can be represented sort of like this:

  (lambda (x) x)

and so on. That's a nested list. It contains symbols. We can use an assoc list to associate symbols with the terms that are their values. And so on ...

Lisp has the programmatic vocabulary to talk about lambda calculus formally, in a way that is executable.

I don't suspect there is a significantly easier way for LC to interpret LC than to use the 42 page expression to create a Lisp, and then write the interpreter in that lisp.

pmcjones2• 4 years ago

which is why it took 20 years of further research to go from Lisp 1 to Scheme.

Actually it only took Peter Landin a few years. For example see:

P. J. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, Volume 6, Issue 4, January 1964, Pages 308–320, https://doi.org/10.1093/comjnl/6.4.308

tromp13• 4 years ago

Lambda Calculus is computationally foundational. Lisp carries a lot of non-foundational baggage, some of which (like number primitives) makes it far more efficient for running on actual hardware.

As such, Lisp's identification of CONS/CAR/CDR/COND as a sufficient set of primitives for a universal Turing machine

You don't need any of those for universality. They are trivially expressible in Lambda Calculus. LAMBDA is really the only necessary primitive.

armchairhacker• 4 years ago

Lisp is more expressive: I can write any program in LC but I'd much rather use Lisp.

Similarly someone could write C or JavaScript or Swift or Haskell in LC. Although I'd argue Lisp is a bit better as it's one of the first languages, one of the first to involve functional concepts like code-as-data, and itself is based on really simple concepts like LC.

somewhereoutth9• 4 years ago

Yes expressiveness is a crucial quality.

I'd suggest that code-as-data is in fact not a functional concept, and indeed may not necessarily be as helpful as we might like to think.

Lisp strayed from the path somewhat when it embarked on runtime enclosure (if my understanding is correct), and anyway it was never going to be as elegant as a true rewrite system.

tromp13• 4 years ago

Haskell is more expressive. I can write any program in LISP but I'd much rather use Haskell. Btw, Haskell is much closer in spirit to LC than LISP is.

kazinator20• 4 years ago

Lisp gives you a programming language in which you don't have to write a cryptic 42 page one-liner to have an implementation of lambda calculus.

Lisp gives you a way to talk about lambda calculus, in a way that executes. For instance, papers about lambda calculus may talk about "beta reduction" and things of that nature. Those concepts are not in lambda calculus; they are about lambda calculus.

In lambda calculus examples you have terms like \x x and whatnot. But lambda calculus doesn't explain what x is; x is an identifier and that is part of the description of lambda calculus, and not in lambda calculus.

Lisp has the batteries included for describing languages, such as lambda calculus. It has an answer for what is x: it's a symbol, available as a data type. It has an answer for what is "beta reduction"; it's a function you can write, and execute on some piece of lambda calculus.

Lisp closes the circle; the stuff you talk about in a paper can become code, and code which is not far from what the paper talks about.

somewhereoutth9• 4 years ago

Beta reduction is in fact the essence of LC - without it all you'd have is a nice tree.

The beauty and generality of LC is that x doesn't need an explanation, it is just a placeholder, yet that is enough to define interesting (perhaps all) things.

Lisp is an abstraction, that per article can be built upon the deeper abstraction of LC - question is, what does it give us in terms of expressiveness and understanding?

tromp13• 4 years ago

Lisp gives you a programming language in which you don't have to write a cryptic 42 page one-liner to have an implementation of lambda calculus.

You totally misunderstood what the 42 pages are. They are not an implementation of LC, but an implementation of LISP in LC.

Lisp gives you a way to talk about lambda calculus, in a way that executes.

LC gives you that too; it allows you to encode lambda terms as bitstrings, which can be represented as lambda terms themselves.

But lambda calculus doesn't explain what x is

In the binary encoding, x is a de-Bruijn index: a natural number indicating the nesting level of the binding lambda.

Lisp closes the circle

So does Binary Lambda Calculus.

contravariant• 4 years ago

Here I was wondering what a lambda expression implementing lisp would look like.

Page 33:

(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((...

Yeah that seems about right.

somewhereoutth9• 4 years ago

Yes but isn't it beautiful? But seriously, instead of seeing lots of brackets, see the whole as a texture, a texture that has some importance (per Lisp advocates). See it in context with other textures, indeed all possible textures.

ducktective• 4 years ago

Page 32 of the pdf...omg the legends were true!

https://woodrush.github.io/lambdalisp.pdf

Show HN: LambdaLisp – A Lisp interpreter that runs on lambda calculus

Related Stories