r/ProgrammingLanguages

Long time lurker here. I've seen a number of posts about using IRs based on sequent calculus and decided to have a go at it myself. My prototype compiler can be found here, for those of you interested in this niche: https://github.com/August-Alm/sequent

The paper that influenced me the most was https://se.cs.uni-tuebingen.de/publications/schuster25compiling.pdf, that has been highlighted on this reddit before. It defines a low-level IR that corresponds to focused/normalized terms of a depolarised sequent calculus calculus and explains how to transpile it to traditional assembly. I copied this pretty much wholesale.

One abstraction level above it, I have a polarised sequent calculus with generalised algebraic data/codata types, higher kinded types, quantitative type theory-style usage tracking, polymorphism and automatic data kinds in the vein of Haskell's DataKinds extension, and primitive "destination" types for type-safe memory writes in destination passing style (in the style of https://arxiv.org/pdf/2503.07489).

Above that sits functional programming language users are meant to write. It supports the same type-level features, but it is not polarised. It has (generalised algebraic) data and codata types, but they have the same kind "type" ("*") -- polymorphism is higher rank and over all types, not over data or codata separately.

The compilation pipeline was pleasantly easy once. I only really faced two big conundrums:

1. The surface functional language is not polarised, but the core sequent calculus is. So, I shift all constructions in the surface language into the positive & producer fragment of the core. Since, e.g., function types in sequent calculus are canonically polarised as ((A:+) -> (B:-)):-, this involves quite a bit of shifting to get right. Similarly, the low-level focused/normalised IR is again unpolarised but still has a chirality division of terms into producers and consumers. The compilation of the core sequent calculus to the focused form is done in such a way that "focused chirality = core chirality + core polarity mod 2". That is, the chirality of terms of negative types flip. Again, the transformations are not really very difficult, the difficulty was realising how it needed to be done. I'm sure it has been written about in the research literature but, not being an academic, I had to reinvent the wheel for myself.

2. The low-level, focused IR does not support polymorphism. In fact, the focusing/normalisation of the core sequent calculus into the focused IR does not support polymorphism, or at least I couldn't figure out how to do it. The issue is that this focusing/normalisation relies crucially on eta-expansion of cuts, in a way that depends on knowing the type of the cut. A cut at a polymorphic type variable cannot be eta-expanded. To get around this, I monomorphise the core sequent terms before normalisation, based on https://dl.acm.org/doi/epdf/10.1145/3720472 That paper does not do it in the setting of a sequent calculus, but it translated very nicely into my setting and allowed me to fully monomorphise higher-rank polymorphism with very little effort.

The compiler "frontend" is very underdeveloped. No source code positions in error messages or etc, the syntax is a bit crude and types annotations could be much more inferred. But for what it is -- a prototype of compilation with sequent calculus-based IRs -- I feel it has achieved its goal. It supports high-level, feature-rich functional programming language and emits surprisingly fast Arm64 assembly, with no external dependencies apart from lexx/yacc for parsing.

A while ago I posted here asking for feedback on Nore, a language idea I've been exploring around data-oriented design.

At that point, one of the main things I was unsure about was whether the idea was actually strong enough to carry a real compiler project, or whether it mostly sounded interesting in theory. The feedback I got here helped me keep pushing on that question instead of backing away from it.

So I wanted to post a small follow-up and say thanks: I've now published the first public release, v0.1.0.

If anyone wants to take a look, the repo is here: Nore

Since that first post, a big part of the work has gone into two things:

• building a small standard library from scratch
• getting the language self-hosted

When I first posted, there really wasn't a stdlib yet. I've tried to keep it intentionally small so the language has to carry its own weight, instead of hiding weak spots behind a large library too early.

The self-hosting part mattered even more to me. My earlier post was mostly about whether this fairly opinionated language model could really express a non-trivial systems project. Getting Nore to the point where it can implement its own compiler feels like the first meaningful validation that the core idea is worth continuing.

A lot of the suggestions from that first discussion were genuinely useful, and I've kept track of them. But this release hasn't really started addressing most of those bigger future ideas yet. I felt it was more important first to get Nore into a somewhat more stable state before taking on more ambitious work.

I definitely don't see this as "the language is done" or anything close to that. There's still a lot to improve in the language, tooling, stdlib, and general ergonomics. But it does feel like an important milestone, and I honestly don't think I would have pushed it this far without the feedback I got here.

So mostly: thanks. This community helped me turn a language idea I wasn't fully sure about into a first public release I feel good enough about to share.

And if anyone wants to take a look, I'd still love feedback, especially on:

• the data-oriented design direction itself
• whether self-hosting changes how convincing the language feels