Live data from Hacker News

Show HN: AttaLambda: a language where types and data are made of untyped lambdas

attalambda.com

1–6 of 6 posts

Show HN: AttaLambda: a language where types and data are made of untyped lambdas

#1
I made a programming language!

I call it AttaLambda.

The idea is this: a usable Lisp-shaped language where all the meaningful computation is done in untyped lambda calculus. Logic, arithmetic, data structures, control flow, even the types — all untyped lambdas. A small, explicit Racket layer sits at the boundary to handle the outside world, plus some macros for syntactic sugar.

This is its story:

A couple years ago, I wanted to play with untyped lambda calculus and go beyond where tutorials usually stop. They show booleans, numbers, arithmetic, maybe the Y-combinator — and then stop. I wanted them to keep going.

So I started a project called All The Lambdas. Using Racket set to lazy, I used only one Racket construct for actual computation — lambda — and built integers, rationals, lists, binary digit-list number encodings, search algorithms, and more.

Then I found Functional Programming Through Lambda Calculus by Greg Michaelson. In it, Michaelson sketches the bones of a language built in untyped lambda calculus, including a type system where typed objects are themselves pair functions containing a type tag and value.

I found that intriguing and implemented and extended the idea, still entirely with untyped lambdas. I don't have a background in programming language theory, so I was figuring it out as I went.

Then I stopped tinkering with it for a while.

Recently I came back and thought: why not turn this into a real usable language with the help of coding agents? I reused most of All The Lambdas as the foundation.

Thus AttaLambda was born.

Some additional details:

* Rat, its number type, uses binary digit-list encodings instead of Church numerals, so numbers scale with their number of binary digits rather than their value

* errors are lambda-encoded values, not Racket exceptions, and propagate through the language like ordinary data

* the Racket host only performs irreducibly external operations; even things like HTTP parsing, routing, and response construction stay in the pure lambda world

* recursion uses lambda-calculus recursion: no loops or true self-reference, just the Y-combinator underneath

* automated purity checks catch accidental cheating, like native computation leaking into the pure parts

* syntax like multi-argument lambdas, let, cond, and list is just macro sugar that reduces to unary lambdas and application

A couple code examples: (short of print, every single thing here reduces to unary untyped lambdas)

Factorial:

  #lang attalambda

  (rec factorial n =
    (cond
      ((eq n 0) 1)
      (else (mult n (factorial (sub n 1))))))

  (print (factorial 10))
Which prints:

  3628800

Or an exact harmonic sum:

  #lang attalambda

  (print
    (reduce add 0
      (map (lambda (n)
             (unwrap-ok (div 1 n)))
           (range 1 8))))
Which prints exactly:

  363/140
As far as I know, no programming language combines all these features: Michaelson-style type tags built from untyped lambdas, exact rationals backed by binary digit lists, errors as lambda values, and real-world programs where almost all computation stays inside the lambda core. None of those pieces are individually new, but I don't know of another language combining them this way.

Download: https://github.com/kserrec/attalambda/releases/tag/v0.7.0

Code: https://github.com/kserrec/attalambda

Original All The Lambdas: https://github.com/kserrec/all_the_lambdas

Show HN: AttaLambda: a language where types and data are made of untyped lambdas
attalambda.com

Re: Show HN: AttaLambda: a language where types and data are made of untyped lambdas

#2
This is uninteresting, because 1) you could just share your prompt: “implement Greg Michaelsons book in racket” 2) you added nothing to it 3) you skipped about everything that is interesting to study when learning the lambda calculus

Re: Show HN: AttaLambda: a language where types and data are made of untyped lambdas

#3
post #2

This is uninteresting, because 1) you could just share your prompt: “implement Greg Michaelsons book in racket” 2) you added nothing to it 3) you skipped about everything that is interesting to study when learning the lambda calculus

I'm printing this out and mounting it on the wall. Well played, my friend...well played.

Re: Show HN: AttaLambda: a language where types and data are made of untyped lambdas

#4
post #2

This is uninteresting, because 1) you could just share your prompt: “implement Greg Michaelsons book in racket” 2) you added nothing to it 3) you skipped about everything that is interesting to study when learning the lambda calculus

1. I started all_the_lambdas first and in making it, I only borrowed a single idea from Michaelson that was new to me, the idea of type tags. Also I'd estimate that 99% of that original project was done by hand a couple years ago, no LLMs (as I recall, I think I wanted to test chatpgt for just a couple specific things a few weeks into making it then, the division and subtraction algorithms for my binary digit list encodings of natural numbers and the best model then couldn't even figure out the division algorithm anyway so I had to do it myself!)

And for Attalambda I only borrowed one more idea from Michaelson that was new to me, which was his empty list encoding (I originally just used false/zero in my first project, but his pair of empty list errors idea for nil just seemed better so I took that proudly when I remade that original project into this one). And I am not at all shy about the fact that I took inspiration from him and you can see that if you look at git history or my plan documents. Neither am I shy about the fact that I used LLMs in building AttaLambda (and I did so a lot!), but basically all the ideas came from me or just common knowledge about lambda calculus.

Anyway, a one-shot project based on that prompt you suggested does sound very interesting. Please give it a go and let me know how far you get and what it looks like. I genuinely want to see the results.

2. As for what wasn't adopted from Michaelson, well it's basically everything else in AttaLambda, everything short of the two things I mentioned I borrowed. Although I will admit that I don't think any of the other parts are anything particularly unique individually; it's more in their combination that I think you get something rather unique. for instance, I have a binary digit list encoding of natural numbers which integers and then rational numbers are successively built off of (this is a huge performance boost from Church numerals!), Then there are the Option and Result types, the generalized type checking functions (I struggled with these at first in all_the_lambdas and in further generalizing them in AttaLambda and am very proud of them!), and there's the error propagation mechanism so errors bubble up and gather information along the way.

3. As for skipping what's interesting to lambda calculus, it's a big subject and I've just gotten started! Can you tell me what I've overlooked that you want to see? The goal for me was originally just to play with lambda calculus and keep building whatever struck me personally as interesting at the time (and I succeeded at that!), like building different encodings of numbers and types of numbers, or writing algorithms for lists or search algorithms, or after I started using type tags I explored strong typing versus coercion, and more. This has been really fun for me and I just wanted to share. Idk if I have had more fun coding anything else in my life. And then I thought it would be fun to add the host boundary and make this a real language I could use rather than just a toy and so I went from the all_the_lambdas project to AttaLambda - that's what kicked this all off. I really wanted to see, could I take this pure unary untyped lambda calculus base from this first project and add a tiny boundary to let it become an actually usable (although almost entirely impractical) language? What would you have done instead?

Re: Show HN: AttaLambda: a language where types and data are made of untyped lambdas

#6
Well done!

I wrote a wee lambda calculus interpreter to test out the book forms. I did cheat a wee bit and added:

def = ==> substitution of for before evaluation if then else fi ==> (( ) )

to make things more readable.

I think a few folk have got as far as implementing lists and recursion, but you're the first dynamic type implementer I've come across.

I think lambda calculus is fun. My book is about functional programming, and so isn't much use for theory, for which I recommend Barendregdt's "The Lambda Calculus. Its Syntax and Semantics".

Best wishes

Greg Michaelson