Correct. I think of it this way: The reduction rules prescribe an encoding for functions, but don't describe it for other (traditional) data. But there are very canonical choices of course, which the demos on the website follow:
* false := t and true := t t
* Pairs are t first_elem second_elem
* Lists could be encoded as (t first_elem (t second_elem (t third_elem ...))) with empty list being t
* Natural numbers as lists of booleans (LSB first)
* Strings as lists of natural numbers (unicode code points)
These choices will affect what the functions that operate on data look like, concretely.
Super cool, thanks for the pointer! I'll note, though, that one of the main value adds of (this) TC is that it is also intensional.
See website for some elaboration and examples, I'd particularly recommend looking at https://treecalcul.us/live/?example=demo-fusion which demos a little stream fusion optimizer, entirely from scratch, including small test.
Reduction rules (1) and (2) correspond to those of K and S, respectively. Reduction rule (3) corresponds to the elimination form for a Scott-encoding of a datatype like `X = Leaf | Stem X | Fork X X`. The cases of rule (3) are essentially parsing the argument into one of these three forms, and dispatching on the result.
Correct! The huge value add of TC is that it is also intensional, which SKI or LC are not. This is a property one is not commonly confronted with (which is a shame), but means that all the things you say (and more) can be defined right in TC. The crucial thing to see is that, while I can surely write a (say) program analysis for C in C, the analysis will have to work on a quoted version of programs! For instance a string, or AST. In TC, thanks to being intensional, you can do this directly. Concretely, say you had a function "add", in one line you can call "add 123 234", in the next line you can all "type_check add yadayada" to check its type. Or to serialize it. Or to compile it into x86.
To be very clear, there are other calculi and even programming languages that are intensional, TC is not first. But it is the most compact formulation, having just one combinator. And IMO the most practical, as I try to prove with the various demos on the website. E.g. I'd recommend looking at https://treecalcul.us/live/?example=demo-fusion which demos stream fusion. All demos are 100% self contained, in line 1 nothing but "t" is defined, and in less than 200 lines we have both a working program optimization and a little demo of it!
Thanks for the feedback! Tree Calculus is a calculus/logic, see Specification page or the book by Barry Jay (linked on that page) for way way better and detailed verbose explanations. It only defines what I chose to call "t" on the website, Barry uses "Δ" in his book and papers.
So without anything else, we'd have to talk about programs in terms of "(t t) t ..." or binary trees, which gets unwieldy quickly. The first natural step, for practical purposes, is to allow definitions "foo = ...", then some syntactic sugar for lists, functions, etc. Ooops and now we have a "language". If you open the "Playground" page there's a summary of what exactly is TC and what is syntactic sugar (and really nothing more!) on top of it.
I like to think that the line is so blurry precisely because TC needs nothing but a bit of syntactic sugar to feel like a usable PL haha.
Right, it's a programming language the way the lambda calculus or pi calculus or whatever are programming languages—I did understand that much!
I love the idea of having a website like this to introduce people to one of the less popular calculi, and the playground is a great touch. It might be helpful to have an introductory paragraph that explains exactly what the tree calculus is, starting from what a "calculus" is—your target audience seems to be people who aren't otherwise going to go out of their way to read Barry's papers, which means you can't assume as much background as you currently do. As a reference, I'm a casual PL nerd who actually has read academic papers related to some of the less well-known calculi with an eye towards implementing them, so I'm on the more informed end of the spectrum of your target audience.
Have you considered making this site open source? No pressure if not, but if so I'd be happy to contribute to polishing up the landing page. I'm very interested in learning more about this anyway, and I'm more than willing to help!
Note that it refers to his book on the "Specification" page :)
> Seems to be a pattern for them sadly, not sure why
Can you elaborate? Agreed I could (and will) attribute more explicitly on the website, but the intention is in no way to grab credit. I just posted this reply for more background on everything: https://news.ycombinator.com/item?id=42375914
English is likely not your first language and it’s fairly obvious what you mean, but the word you’re using a lot is spelled “intention”. Not at all how it sounds, stupid English.
(It’s also likely that this minor error is spawned by the use of intension, a very uncommon word, in the description of Tree Calculus.)
Ooops, thanks for catching, typo fixed. That Tree Calculus is intenSional (https://plato.stanford.edu/entries/logic-intensional/) is one of its main selling points, so that spelling must've rewired too many motor neurons.
Thanks for the feedback! The target audience I had in mind was certainly developers (like me), not "all people". And the wording was indeed inspired by PL talks and blog posts I consumed over the years.
Here is a (slightly provocative) thought: We developers were promised "first class functions" with functional programming languages. And it's true, you can pass them around like any other value! Cool.
But first: What about inspecting those values? I can "look inside of" a number or string or array any day. But functions, I can only call. Huh, so an intensional view (not that anyone thinks that out loud) for all kinds of values, except functions. Yes sure, many languages do allow you do dig into functions. But it is all not the same as or as powerful as supporting it right down at the logic level! TC is also not first to do that. But IMO the most compact and practical calculus/language to do so, yet.
Second, a practical example: We had "first class functions" for decades now. But where is our main stream config language (JSON etc) that has first class support for them? Of course the answer is: Because it remains tricky. In industry I've seen all sorts of work arounds, usually involving strings that get compiled/interpreted on the fly. Which usually means some amount of scary security, and no static guarantees whatsoever. With TC, a parser/runtime for arbitrary (but pure) functions is a few dozens lines of code. And thanks to being intensional, one can imagine type checking those functions at the time of loading the config, not only when executing! Concrete demo/blog post for exactly this is in the works.
So anyways, I do belive this enables truly fundamental shifts, hence "democratizing".
Why don't you put a short version of this explanation on your main website instead of a vague "democratising functions"? What you wrote makes sense, but if all I see when I'm visiting your website is "democratizing functions/metatheory" and some contextless code examples, I'm not gonna be able to tell why I should care.
Hi all, author of the website here (I'm https://johannes-bader.com/). Wow, thanks for the reactions and many good suggestions! I thought I'd add a bit of context here.
As has correctly been pointed out, Tree Calculus was developed by Barry Jay! The "Specification" page links to his book. And a preview of his PEPM 2025 paper (hi chewxy!) can now be found here: https://github.com/barry-jay-personal/typed_tree_calculus/bl...
Compared to how long Barry has been professionally researching this, I entered the picture yesterday and joined the effort to help. Potential mistakes on the website are mine, not Barry's, but I do firmly believe in some of the "ambitious" wording there. Blog posts and more concrete demos or details to come!
Just for the curious, here is my angle in all this:
I happened to (hobbyist!) research tiny, yet practical, languages for over a decade (see e.g. https://lambada.pages.dev/). In that work I started noticing that the Iota combinator (https://en.wikipedia.org/wiki/Iota_and_Jot) is not a combinator in the most traditional sense: It is usually defined as behaving like "\x x S K", but like, how can we just refer to a lambda in the definition of a logic? One could write reduction rules such as "Iota Iota x -> x", but now Iota appears on the left hand side, in argument position! Doesn't that allow reflecting on arguments? Horror! I just started realizing that, while SK is perfectly Turing complete and sane, forcing down the number of combinators from 2 to 1 magically forces some amount of intensionality! Curious, isn't it?
And that's when I came across Barry's work and book! A calculus that embraces intensionality. So I reached out to see if I can help. How can I be most useful? Barry has been figuring out theory, professionally, before I could think. So I felt like helping spread the word, maybe to a less academic developer crowd, would be a more effective way to contribute. I spent my entire career building developer tools, so I have some ideas what could be useful and what might be necessary to convince various kinds of developers. That's how the website came to be, and it is very much a work in progress. We sync regularly, for instance Barry had excellent ideas for demos and I suggested slightly tweaked reduction rules at some point (not more powerful in theory, just more convenient in practice), see "triage calculus" in typed_program_analysis.pdf
Would help a lot if somewhere at the very top it explained what tree calculus is (may be extend the animation of the addition example to first show what the t is)
It took me a while on the website to understand what it was all about. As it is it looks more like a website for a functional programming language.
Are the tweaked reduction rules what you have on this website? I might be misunderstanding, but rule 3 certainly looks different on your website than in Barry’s book.
Could you link typed_program_analysis.pdf? I can’t seem to find it.
These choices will affect what the functions that operate on data look like, concretely.