Hacker News Reader

Comment by js8 | Hacker News Reader

I used to be a fan of these languages like Lisp and Forth and Joy (and Factor and Haskell), but then I found that what I a really long for is just (untyped) lambda calculus (as a universal language). (Combinatory logic is just a similar representation of lambda calculus, but the differences go away quickly once you start abstracting stuff.)

I think expressing semantics of all (common) programming languages in lambda calculus would give us a solid foundation for automated program translation. And we should aim for that, the babel tower of languages doesn't really help anyone.

The current issue I have is with type theory. So I am trying to embed notion of types directly into the lambda terms, so they would sort of "automatically typecheck" when composed. The crucial in this, in my opinion, are lambda terms that do not use lambda abstraction in their body, because you can think of these terms as a kind of mini-DSLs that have yet to be interpreted.

Anyway, once we can translate calculus of constructions (and other common formal logics) into untyped lambda calculus, it will also help us doing automated theorem proving. It must be theoretically possible, but to my knowledge nobody has really done this sort of hardcore formalization.

View on HN

I implemented the Calculus of Constructions in untyped lambda calculus in order to shorten the 643 byte C program computing Loader's Number to 1850 bits (under 232 bytes) [1], as one of the milestones reached by my functional busy beaver function [2].

[1] https://codegolf.stackexchange.com/questions/176966/golf-a-n...

[2] https://oeis.org/A333479

I think this is great. I think you should write a paper on it.

I suspect it might need some kind of commutative diagram proof, i.e. if you express things in CoC formalized within BLC you will get the same result as when you express in BLC formalized within CoC, I am not sure from the top of my head.

(Kind of similar to showing that self-interpreting quoted interpreter on quoted program is the same as quoting the result of running the interpreter on the program.)

And of course, this proof of equivalence should have formalization both in CoC (Lean?) and BLC.

My hope is eventually someone writing a book on logic where the metalogic will be just untyped lambda calculus. Proofs will be just beta-reduction and judgemental equality. And everything will be in the form, let's study properties of these lambda terms that I came up with (the terms will of course represent some other logic such as CoC, simply typed LC, or even LC itself etc.).

Grounding programming languages in mathematics like this is essentially the goal of Strachey and Scott's denotational semantics, which has been very influential in programming language theory:

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

All approaches to semantics of programming languages are mathematical, the denotational one is not "more mathematical" than the rest.

Not really a big fan, because the formalization of DS always left something desired, but I think a big difference with formalization in ULC is that ULC is (mostly) materialist while DS is structuralist.

So the initial formalization into ULC can be automated - if you have semantics of your language already implemented as an interpreter in another language, you can use this as a starting point.

With DS - I am not sure. I feel most people who build new languages don't provide DS specification.

A lot of languages(including forth) maps really poorly to LC. Read some of the Forth writing on portability at all costs:

http://www.ultratechnology.com/antiansi.htm

Simple pure concatenative languages map quite well though [1].

[1] https://github.com/tromp/AIT/blob/master/ait/mlatu.lam

Joy, right? Not Forth.

Conversion between spagetti stacks and pure stack programming(in which the stack contains numbers and no GC) has a massive translation cost if you go from LC to Forth and back.

Forth is an imperative language and as such you will have to model memory state (at least) somehow, if you want to use purely functional language as a representation. But that's the cost of doing business.

The thing is though, you don't translate to LC for performance, but for understanding. At any point, the LC evaluator might recognize a known subterm and replace it with a known equivalent. Depending on the goal, that might help to improve evaluation performance (skip known steps of beta reduction), reduce memory consumption (reduce size of the term), or improve readability (refactor code to use better known abstractions).

It's difficult to understand what they were actually doing, but reading between the lines, it sounds like an advantage of 'machine Forth' is writing some Forth words in assembly? I can see why that would run much faster for a jpeg decoder.

It's a real cool idea to compile everything down to lambda calculus and then you solve all semantics issues. (If something fits) you can convert 1:1, use general libraries in one language in others without loss etc. Ah, what a beautiful world it could be!

> And we should aim for that, the babel tower of languages doesn't really help anyone.

What exactly do you mean with this? That the amount of programming languages available isn't actually helpful, it's detrimental?

Well, I feel that lot of code is written again and again, just in different languages. If we could automatically compare and translate different implementations, I think it would be beneficial for finding bugs.

Everytime somebody comes up with a new programming language, I am like, yeah, so you added these abstraction, just in a different syntax. I think people who come up with new languages should implement the primitives on top of lambda calculus (which really is the simplest logical system we know), then we could potentially have automated translators between languages, and that way we could cater to everyone's preferences, and expand a standard library across different languages.

So in short, yes, I think proliferation of programming languages without formal understanding of their differences is detrimental to interoperability of our computer systems.

It would also allow wider notion of metaprogramming - automated manipulation of programs. For example, let's say I need to upgrade my source code from one interpreter version to another. If both interpreters are represented as a set of terms in lambda calculus, I can see how express one in the other, and formalize it as some kind of transformation. No more manual updates when something changes.

It would also allow to build a library of universal optimizations, etc. So I think programmers would benefit from having a single universal language.

> Everytime somebody comes up with a new programming language, I am like, yeah, so you added these abstraction, just in a different syntax.

I got this feeling too, until I started to explore languages outside of the C/Algol-like syntaxes. There is a wide range of languages out there, from array languages to lisps, and they don't give me the feeling of "just a different syntax" but actually changed the way I think.

So yeah, I love lisp now and spend most of my days writing it, but it also comes with the downside that now Java, C# and Golang look more similar than different to each other.

> It would also allow to build a library of universal optimizations, etc. So I think programmers would benefit from having a single universal language.

I think assuming everyone would use the same hardware, same environment and same workflows to solve the same problems, this would make a lot of sense and would be hugely beneficial!

But in reality lots of problems need different solutions, which has to be made in different ways, by different people who think differently. So because the world is plural, we need many programming languages too. Overall I feel like that's a benefit.

> they don't give me the feeling of "just a different syntax" but actually changed the way I think.

Not only that, but languages that enable more concise expression of an idea (without losing clarity for readers) reduces the error rates of programs written in them.

It's been proven that when not accounting for constraints imposed by a compiler/interpreter (like the Rust borrow checker), the average error rate per unit size of programs across widely varying languages is constant. So reducing the number of lines/expressions required to express ideas reduces the number of errors by the same factor. Brevity pays when readability isn't sacrificed.

> assuming everyone would use the same hardware, same environment and same workflows

They don't have to. I would ideally represent HW, OS and compiler in the LC as well. Then primitives of the language that could be proven to be HW/OS/compiler independent could be abstracted and readily translated. For the ones that could not - well you have exact description of what the differences are.

Racket is at least related to the kind of metalanguage system you're talking about. I've never actually done it, but to implement a new "#lang" in Racket, your job is essentially to write a "reader" for it that transliterates it to the classic Schemey Racket language. Libraries written in one #lang can then be called from one another (or not, if that's what you want -- a lot of the point of this in Racket is building little restricted teaching languages that have limited capabilities).

But why stop at Racket? Why not reduce the needed primitives even further down to LC?

Everyone should be free to unite behind my choices. It's obviously what is best for everyone.

That's a rather cheap retort. I am not saying everybody should use raw untyped lambda calculus for their programming, just that we would all benefit if we could translate languages we use to and from it, because then we could interoperate with any other code, refactor it, etc.

Has even a single programming language made the complete documentation and implementation effort you're describing? It'd be interesting to read about.

Isn’t structure lost in the compilation process?

I mean, we already have bits and pieces of what you want, like an assembler to C decompiler, but the output isn’t very nice without the types.

And how many languages can run on the CIL in dotnet. Say we create a CIL to lambda calculus compiler. Where do we go from there?

A CIL to LC compiler is effectively an emulator of CIL in LC. That is, every primitive of CIL has a corresponding LC term, which operates on the CIL execution state. So then you can express functions from .NET standard library as terms in LC.

Now let's say you do the same for JVM. Now you can start looking at all these lambda terms and search for some similarities. For example, you might notice that some list functions are equivalent if you transform the representation in a certain invertible way. This gives you a way to express functions from one standard library in the other.

In general, I think we should try to translate wide variety of human programs into lambda calculus and then try to refactor/transform the lambda terms to spot the common patterns.

That sounds very thankless, but on the other hand we have very fast computers and maybe "the bitter lesson" of just throwing more compute at finding patterns can be applied here, as well.

Certainly that is how I read it.

It divides effort, spreads it too thinly among too many disparate projects with essentially the same goals, and as a result, they all advance much more slowly.

Examples: how many successors to C are there now? Hare, Odin, Joy, Zig, Nim, Crystal, Jai, Rust, D... And probably as many again that are lower-profile or one-person efforts.

For a parallel example, consider desktop environments on FOSS xNix OSes.

I have tried to count and I found about 20.

A "desktop" here meaning that it provides a homogenous environment, including things like a file manager and tools to switching between apps, plus accessories such as text editors, media viewers, and maybe even an email client, calendar, and/or address book. I am trying to explicitly exclude simple window managers here.

The vast majority are simply re-implementations of the Windows 9x desktop. Taskbar along 1 edge of the screen, with buttons for open apps, start menu, system tray, hierarchical file explorer, a Control Panel app with icons for individual pages, etc.

This includes:

* KDE Plasma (and Trinity)

* GNOME Flashback (AKA GNOME Classic, including the Consort fork)

* Cinnamon

* Xfce

* Budgie

* MATE

* LXDE (including Raspberry Pi PIXEL)

* LXQt

* UKUI (from Ubuntu Kylin, openKylin, etc.)

* DDE (from Deepin but also UOS, Ubuntu DDE and others)

* Enlightenment (and Moksha etc.)

* ChromeOS Aura

And more that are now obsolete:

* EDE

* XPde

* Lumina

That's about 15, more if you count variants and forks. There are more.

The main differences are whether they use Gtk 2, 3 or 4, or Qt. That's it.

It's easier to count the ones that aren't visibly inspired by Windows >= 95:

* GNOME Shell, ElementaryOS's Pantheon, Ubuntu's Unity.

Arguably: GNUstep (whose project lead angrily maintains is not a desktop after all), and the long-dormant ROX Desktop...

So, arguably, 3 you can run on a modern distro today.

CDE is older than Linux or Free/NetBSD so doesn't count. I only know 1 distro that offers it, anyway: Sparky Linux.

MAXX Interactive Desktop looks interesting but it's not (yet?) FOSS.

All that effort that's gone into creating and maintaining 8-10 different Win9x desktops in C using Gtk. It's tragic.

And yet there is still no modern FOSS classic-MacOS desktop, or Mac OS X desktop, or GEM desktop, or Amiga desktop, or OS/2 Workplace Shell... it's not like inspiration is lacking. There are at least 3 rewrites of AmigaOS (AROS, MorphOS, AmigaOS 4.x) but despite so much passion nobody bothered to bring the desktop to Linux?

Defenders of each will vigorously argue that theirs is the best and there are good reasons why it's the best, I'm sure, but at the end of the day, a superset of all of the features of all of them would not be visibly different from any single one.

That's rather sad, IMHO.

> There are at least 3 rewrites of AmigaOS (AROS, MorphOS, AmigaOS 4.x) but despite so much passion nobody bothered to bring the desktop to Linux?

The passion is there for the whole AmigaOS, of which the desktop metaphor, Workbench, is just a part. What fun is AmigaOS without Exec, Intuition and AmigaDOS? The passion is to see AmigaOS run, not to see Linux wearing its skin.

GUIs for manipulating files a-la Workbench are readily available, nobody seems to have built an Amiga-skinned one when a Win95 one will do. DOpus is already a clone of Midnight Commander, and there are clones of that aplenty, the most DOPus-like one I've seen is Worker (http://www.boomerangsworld.de/cms/worker/)

The rest of the Workbench metaphor is available via AmiWM (https://www.lysator.liu.se/~marcus/amiwm.html), or requires apps to play along (e.g. Gadtools, MUI, Commodities, ARexx)

Well, you do you, and indeed, the entire community is free to do as it wishes.

What I find surprising is that there are multiple entire Amiga-themed Linux distros – for example:

https://www.commodoreos.net/CommodoreOS.aspx

I reviewed it. I was not very impressed.

https://www.theregister.com/2025/05/06/commodore_os_3/

And ones which put an Amiga emulator front and centre:

https://cubiclenate.com/pimiga/

https://wilkiecat.wordpress.com/2025/05/31/pimiga4-by-chris-...

(Which I looked at, but decided that there wasn't enough here to review.)

And new hardware like the A1200NG:

https://www.a1200.com/index.php/the-a1200-ng/

Which is an Arm board running Linux running a full-screen Amiga emulator.

And AROS Portable:

https://arosnews.github.io/aros-portable/

Which I also reviewed:

https://www.theregister.com/2025/05/22/aros_live/

Given this visible interest in running Amiga stuff on Linux and integrating AmigaOS (and AROS) I am very surprised that in ~30 years, nothing has progressed beyond a simple window manager.

Intuition isn't that big or complicated. It's already been recreated several times over, in MorphOS and in AROS.

I am so tired of seeing Linux desktops that are just another inferior recreation of Win95.

I want to see something different and this seems such an obvious candidate to me.

I think you can categorise Amiga enthusiasts in various ways, this is my taxonomy:

1. Hardware enthusiasts who specifically love the Amiga's original hardware, its peripherals, and the early post-Commodore direction (PowerPC accelerators), and/or modding all of the above. These sort of people used WarpOS back in the day and probably use MorphOS or AmigaOS 4 today. The question is whether, for these people, modern single-board computers "count" as Amigas or not.

2. Nostalgic enthusiasts of the system that the Amiga was, who are happy with a real Amiga, or with an emulated one, or an emulated one running on some board in a box shaped like an Amiga. Possibly with a non-Amiga UI to boot some classic games. These enthusiasts may enjoy fake floppy drive sounds that remind them of booting disks in their youth.

3. Software enthusiasts of the Amiga's OS, and the directions it took that were different from its contemporaries, and the software ecosystem that came from it. These people have a longer user-startup than startup-sequence. They probably have most of Aminet downloaded. These people might be interested in other alternative OSes, e.g. QNX or BeOS. If they're still using Amiga hardware, or emulators, they'd be interested in AmigaOS 3.5/3.9 and 3.1.4/3.2. This can also include AROS and the work to get it running on native hardware, not just m68k but also x86 and arm... but it's unlikely that it will ever support as broad a range of hardware that Linux does, which limits how many people would want to use it, because it's unlikely to be able to drive a random modern laptop.

4. The reverse of 3, Amiga users that were big UNIX fans, e.g. Fred Fish, the sort of people who ran GeekGadgets and replaced their AmigaShell with pdksh. They probably just moved wholesale to Linux and didn't look back.

There are probably other categories, but I think the one you're looking for is 5: enthusiasts of the Amiga's look and feel, but not its broader OS or its software. If they did care about that, they'd be in groups 2 and 3, and emulators or alternative AmigaOSes would satisfy them most.

I can't say why there aren't many alternative desktops for Linux. Probably because it takes a lot of resources to build a full desktop environment for linux - a Window Manager, or even just an existing Window Manager theme is not enough. A file browser is not enough. Ultimately it takes the applications themselves to play along, which only works when have the clout to make people write software in your style (e.g. KDE, GNOME, Windows, macOS, Android, etc.).

The only alternative UI taken from retro machines to Linux, that I can think of, is ROX Desktop (https://en.wikipedia.org/wiki/ROX_Desktop) with its ROX-Filer... and even that doesn't look entirely like RISC OS, which you could be running instead of Linux.

Interesting analysis. Thanks for that.

I'm well aware of ROX Desktop and have used it in the past. I've written about it:

https://www.theregister.com/2025/01/14/the_end_of_absolute_l...

ROX's AppDirs provided the app format used in AppImage.

I am sure I remember a Mac-like one, and I've asked -- https://news.ycombinator.com/item?id=29937562 -- but to no avail.

You say a WM isn't enough, and I agree, but in this case, amiwm is still right there.

I own an Amiga and I'm interested and I try to cover Amiga news, but back in the 1980s, I was an Archimedes owner. I loved RISC OS and I never mastered AmigaOS. This is not something I personally want, although I'd love to write about it.

I feel the same, too many people doing similar stuff in slightly different syntax, too few people looking at how things are similar and could be unified.

I think it's time to look beyond syntax in programming and untyped lambda calculus is the simplest choice (that is universal and can easily express new abstractions).

Mathematics suffers to some extent from a similar problem, but recent formalization efforts are really tackling it.

The thing is, the most fundamental obstacle to unification, is that unification is a very hard feature to obtain. Even in an LC formalization, do you expect that two "text editor" programs would be interchangeable? Would only a canonical text editor be allowed? Does the LC facilitate arbitrary extensions, that perhaps follow some rules at the interface/boundary? While I also lament what is, on the whole, wasted work and interest, I think the alternative is not some much simpler solution, but rather to offer something that is better. https://xkcd.com/927 is a warning, as true as it is annoying. We gravitate towards variety because it is simpler and natural to how we act; how will your proposal fundamentally improve on this? You call out misguided "defenders", and again I note the same problem, but you seem to be calling for One True Way with no significant realizable improvement.

Sometimes you can prove mathematically that two different approaches are equivalent, but differ only in name or some parameter, and that's a unification of sorts, without proliferation of standards.

In case of UIs, this is still an open problem and will be for many years, but I suspect we could do it by defining, in some kind of fuzzy logic for example, what a good UI does look like. Then we could transfer elements from one UI into another.

Or we could just start at the edge. For example, we can unify what a "user input" is, and what a "widget on the screen" is. Formalizing everything would allow us to do such transformations on programs, for example, universal input/output remapping. And then we could continue to unify into more specific logic of what input is being read and how things are drawn on the screen.

Untyped lambda calculus (and its sibling combinatory logic) is just language for expressing logic, nothing more. And it already exists (arguably it's one of the first programming languages, predates Forth and Lisp by at least two decades) and is among the simplest ones we know. I actually became interested in LC so much recently because, believe it or not, expressing things in classical logic is often more complicated than expressing things in LC.

> Sometimes you can prove mathematically that two different approaches are equivalent, but differ only in name or some parameter, and that's a unification of sorts, without proliferation of standards.

Certainly, but that would already be supposing most of the work to unify at the source level is done, unless an extremely strong normalization is possible.

> Untyped lambda calculus (and its sibling combinatory logic) is just language for expressing logic, nothing more. And it already exists (arguably it's one of the first programming languages, predates Forth and Lisp by at least two decades) and is among the simplest ones we know. I actually became interested in LC so much recently because, believe it or not, expressing things in classical logic is often more complicated than expressing things in LC.

(Personally, I prefer combinators slightly more)

I don't deny the power of LC for some uses, but taking one program, reducing it down to an LC equivalent, and then resurfacing as another program (in a different language, but otherwise equivalent), or some other program transformations you may desire, would certainly be elegant in some sense, but very complex. It's like programming in Brainfuck; the language itself is very simple, and making mechanistic tooling for it is very simple, but I don't think the tooling we could invent in 50 years would be sufficient to make Brainfuck simple to read or write. Moreover, formalizations of, say, "button" are not a problem, but scaling to different screens, devices, use cases, and so on will greatly increase the scope. This OS represents input events this way, this hardware provides that sort of data. I think this is the same problem as to why people, everyday, don't bother to make formal arguments almost all of the time. It's not that a formal argument along the lines of "you didn't take out the trash today, so I have reason to be frustrated with you" can't be formulated or proven, but rather that the level of rigor is generally considered both fatiguing and unnecessary.

Any time someone suggests something that should make things much simpler, I'm skeptical. There are things that have essential complexity too great to be made simple, and then humans maybe have an inherent overhead of accidental complexity, above and beyond the accidental complexity we accidentally add. I'm still interested to see where your efforts lead, but I'm not expecting to see cheap nuclear fusion for another 10 years at least, so.

Why specifically untyped?

Because it is the simplest thing we have, and has a pretty straightforward self-interpreter.

It feels like you need a lot more metamathematics to deal with typed lambda calculus than with untyped one, and types are something that comes without a justification.

Anyway, the idea is, if you have a language, you can think of source code written in the language as a giant lambda term, where you have all lambdas upfront and only composition in the body. A tree of symbols to be composed, essentially. And then to interpret this source code in a language, you supply definitions of the language's primitives as arguments to the source code term.

Now if your language is typed, the primitives need to be chosen in such a way, so that the interpreted term (the source code applied to language primitives) fails to normalize if the program is not typed correctly.

You can then have a correspondence between the primitives of the typed language that typecheck and simpler set of primitives of the same language used purely for computation, used under the assumption that the program typechecks. This correspondence "defines" the typing mechanism of your language (in untyped lambda terms).

> have all lambdas upfront and only composition in the body

That is only possible for a very limited subset of lambda terms. For example, it's not possible for the one-point basis

    A = λx λy λz. x z (y (λw. z))

from which any closed lambda term can be constructed by composition.

Yes, that's deliberate though. (I will call these "concrete" terms, because they lack abstraction in the body, but I am looking for a good name. In fact, no universal one-point basis can be expressed as a single term like that, you need a composition of two; the concrete property is not preserved in composition, although it might be preserved in weaker bases than S,K, such as B,C,K - kind of affine logic.)

Anyway, the reason I am interested in concrete terms is I want to define typing judgements in ULC somehow. (In CoC, all mathematical questions can be rephrased as is there an object of given type T, and you need to be able to formalize questions somehow to formalize metamathematics.)

An obvious definition of typing judgement in ULC would be: term x is of type B in a typed language A (both A and B are given terms) iff there exists a term x that satisfies Ax = B (the equality is judgemental after beta-normalization).

However, this definition doesn't work, because a general term x can just disregard A and return B directly. But - I think if we restrict x to be a concrete term in the above definition (possibly with a given number of upfront lambdas - not sure if that is required), then I think we can make the definition to work.

I also suspect concrete terms can be sort of "deconstructed from the outside". In general, we cannot resolve equality of terms, but I suspect that concrete terms can be analyzed (and quoted) within ULC.

One thing I realized about your CoC implementation - I think you embed CoC into ULC in an indirect way, working with CoC terms in a quoted way. And that's fine, but what I want is to have CoC in ULC directly, i.e. have a base set of ULC terms for the primitives of CoC language. But that also can be thought of as the CoC interpreter being restricted to apply on concrete terms, giving them meaning by substituting the base inside.

In other words, concrete terms are kind of "inside view" of quoting. (Maybe we should call them "data terms", because they effectively carry only data and no executable payload.) Having the concept of concrete terms in the ULC metalanguage can also help to define interaction to the external world, that you only accept data not executables, something that you kinda do through the "monadic" interface. (You need to "remember" that a term only accepts quoted data, it cannot be made explicit in ULC language. The advantage of concrete terms is they are independent on your choice of quoting operator.)

Anyway, I am not sure if I am making sense, I am trying to grapple with this myself, so it's OK if you don't think concrete terms are a useful concept.

> there exists a term x that satisfies Ax = B

Don't you mean xA = B ?

> x can just disregard A and return B

Not if you require x to be strict, i.e. it must use its argument.

> Don't you mean xA = B ?

No, that equation can be created as a special case from equation TAx = B (where Txy = yx is a transposition combinator).

> Not if you require x to be strict, i.e. it must use its argument.

I am not sure it would generally help but maybe you mean it only in case of equations xA=B (not Ax=B as I suggested). I also think this strictness condition would be too limiting.

In equation Ax=B, we can take A of the form R_n A_1 .. A_n, where R_n reduces Ax to x A_1 .. A_n (R_n rotates x in front of n arguments).

So if x is concrete and takes n arguments, we can think of it as "text" (parenthesised expression) in symbols that are to be interpreted as A_1, .. A_n. Requiring that every possible symbol is used in a language text fragment is a weird condition, which doesn't make much sense to me.

In any case, my definition of typing judgment then allows to put a chosen condition on a text composed from chosen symbols, which is quite powerful and can be used to e.g. determine whether a quoted expression is valid. And arguably it is a very natural definition in the context of ULC. (I read to Mock a Mockingbird 30 years ago - in partial Slovak translation - and most problems there could be formulated as the Ax=B equation for x being a concrete term.)

The typed lambda calculus is not Turing complete.

Not quite true, depends on the flavor of the type system you use. Church's simply typed is not, but other type systems are.

I think one way to make it Turing complete is to add typing rule for Y combinator as an axiom to your simple type system, but I am not sure.

Yes, I had Church's simply typed lambda calculus in mind. You need to add a fix point combinator or general recursion.

Reply on news.ycombinator.com