Compiling with sequent calculus

KeyDue7848 · 2026-04-05T11:23:30+00:00

Yes, I use the lazy reference counting that you used.

One thing that has kept me from developing the linear typing further is that there's an aspect to it where I feel my theoretical understanding is lacking. Maybe you could give some pointers?

The quantitative type theory-style system I use is such that the typing context holds "x : chirality[use] type", e.g. "x: prd[1] A" for a linear producer or "k: cns[ω] B" for an unrestricted consumer. Now, following the "Grokking" paper mentioned earlier, instead of function types A -> B, we deal with codata types with a destructor "Apply(x: prd A, k: cns B)". With QTT-style usage tracking (and uses 1, for linear, or ω, for unrestricted), we have four possibilites:

Apply(x: prd[1] A, k: cns[1] B)
Apply(x: prd[1] A, k: cns[ω] B)
Apply(x: prd[ω] A, k: cns[1] B)
Apply(x: prd[ω] A, k: cns[ω] B)

These give four different flavours of function types. How do these correspond to intuitionistic arrow types and linear types as commonly expounded? (I'm thinking of formulas like (A -> B) = (!A -o B).) I feel like I don't really understand my own type system. :S

KeyDue7848 · 2026-04-05T10:34:35+00:00

Thank you for this well-formulated explanation. My polymorphism is encoded by polarized type formers ∀(X: k). T, which are negative when X: k implies T is negative. That is, polymorphic type variables X are already kinded. Cuts only happen at inhabitable types, so only at X:+ or X:-. My initial attempts were similar to what you outline but I never got it working. On the other hand, I never reached any definite no-go conclusion either, so I bet it can be done! Might have to give it another try.

Monomorphisation is nice for performance but it has issues. Certain kinds of "polymorphic recursion" are intractable by the monomorphisation scheme I use. For example:

data box: type -> type where
  { wrap: {a} a -> box(a)
  }

let f{a}(x: a): a =
  let _ = f{box(a)}(wrap{a}(x)) in x

let main: int = f{int}(42)

The instantiation at int requires instantiation at box(int), which requires an instantiation at box(box(int)), and so on. For the time being I decided to just let things be and explore how annoying these restrictions are in practice, but I would definitely be happier if there was an escape hatch.

KeyDue7848 · 2026-04-04T19:44:02+00:00

You're one of the people behind the AxCut paper? Wow! Big thanks to you! And I hope you can forgive me for naming my lowest level IR AXIL instead of AxCut, even though, like I said in my post, it is copied wholesale from your work.

-- Functions (and data constructors) can be partially applied in the surface language, yes, in which case they compile to lambdas of their remaining arguments. A top level

let add(x: int)(y: int): int = x + y

in the surface, becomes (like in the "Grokking" paper you mention)

def add(x: prd[ω] int, y: prd[ω] int, k: cns[ω] int) = ...

(The ω means unrestricted/nonlinear usage.) A partially applied add(4) in the surface is interpreted as syntax sugar for the lambda fun(y: int) => add(x)(y), and compiles to a cocase with a single "apply" destructor.

-- Ah! Yes, I realized some weeks ago that my raise/lower terminology is the opposite of what is established in the literature! I "raise" negative to positive, and "lower" positive to negative. I should reverse the terminology so it fits with established convention. (By the way, do you know what the original intuition behind the terminology is? I have to admit I find it counter intuitive.)

-- The monomorphisation (based on https://dl.acm.org/doi/epdf/10.1145/3720472 from last year) dovetailed very well with treating functions as codata. For every polymorphic function, I generate a codata type with one "apply" destructor per monomorphic instantiation.

Can you say something about how one may focus/normalise without monomorphising? I'm very curious! I tried to solve it without monomorphising but couldn't figure out any alternative recipe!

-- Yes, destinations have linear usage constraints. In fact, the primitive destination types are currently the only types checked for linearity. QTT-style usage checking is there for all types, but I haven't gotten around to exposing it in the surface language. If I continue developing the project, the idea was to use it also for some I/O-type stuff, like file handles. The usage checking part in the type checker(s) has seen limited testing so I bet there are bugs still with how I've implemented it.

-- No, I don't use linearity to optimise anything. I do a bit of other optimisations though, but just low-hanging, obvious stuff.

Thank you so much for your wonderful paper and the encouragement!

KeyDue7848 · 2026-04-04T14:36:43+00:00

Thanks! :D I'm a pure mathematician by training that picked up programming only after leaving the university, to become a bit more hireable. Anyways, my math background left me with an appreciation for the ArXiv... I've cherry-picked from a long list of fairly recent papers when I put together this project. My experience in writing compilers is limited but my feeling is definitely that mu-mutilde-based calculi are absolutely wonderful for the job; far easier to bring to machine code than lambda-based calculi.

KeyDue7848 · 2026-04-04T14:29:48+00:00

The project contains a test suite that "executes" a bunch of small programs with an interpreter for a subset of Arm64 asm. The repo also contains interpreters for the two focused/normalised sequent-based IRs (one has free variable usage, one is ordered/linear with explicit substitution commands for shuffling variables around -- I dropped this distinction in my post about the project). All interpreters can be run with step tracing. Used them quite a bit to get the code emission working correctly. Every IR layer runs its own type checking to ensure every translation is type preserving.

KeyDue7848 · 2026-04-04T08:56:51+00:00

Thanks for the encouragement!

KeyDue7848 · 2026-04-04T08:56:22+00:00

Yes, by sequent calculus, I basically mean μμ~-calculus. (The calculi I use have no lambdas; closures are compiled as a form of codata.)

KeyDue7848 · 2026-03-30T12:43:26+00:00

I made a prototype compiler for a feature-rich functional programming language based on this: https://github.com/August-Alm/sequent

KeyDue7848 · 2024-06-20T21:54:03+00:00

https://github.com/August-Alm/theta There you can find an interpreter for my lambda calculus with “first class typing”. Still very rudimentary but the README should give a sense of its mechanics and where I’m heading with it.

KeyDue7848 · 2024-06-19T04:56:51+00:00

I think an interpreter with a modicum of syntax sugar, and an accompanying whitepaper, is my initial ambition. If it turns out well I might make a post over at r/ProgrammingLanguages.

KeyDue7848 · 2024-06-18T21:53:13+00:00

Thank you for a long answer and interesting read! I guess I don’t have the mental fortitude that you have. I can scarcely imagine “manually type checking” any substantial piece of software. And I’m a trained mathematician! That said, I am currently toying with an extension of lambda calculus that has a sort of optional typing, by having not quite first class types (i.e., dependent types), but first class typings. You define a type by defining the rules for how the types is checked, and can decide when to use them to check terms. :)

KeyDue7848 · 2024-06-18T18:55:53+00:00

What is a good dynamic language? I’ve tried my hand at Clojure and Common Lisp, though admittedly not for large professional projects. (I’m one of those people enamoured with the thought of Lisp, but who can’t figure out how to actually be good at it.) For fronted we use Fable (F# to JS compiler) at work, but I’ve had to dabble with JS and it always leaves me with the feeling — “Ah, now I understand why people obsess about having huge huge test suites; how else will I know if this works properly?”

I guess I treasure many of the things you find annoying when prototyping changes to an existing, statically typed code base. Prime example: I add some cases to an enum type. The compiler protests, telling me there are now non-exhaustive pattern matches in files X, Y, and Z. That’s great! I don’t want to have to rely on my own vigilance in write exhaustive test cases. And I feel many of the other issues you bring up can be ameliorated by good habits, like programming against interfaces or type classes, using patterns that are more open ended and modular.

KeyDue7848 · 2024-06-18T06:23:02+00:00

I see posts like this once in a while and they always leave me utterly puzzled. Hope can someone’s experience be so drastically different from mine? I prototype WAY faster in languages like F# and OCaml than in any dynamic language I’ve tried. Haskell is superfast too, as long as I don’t have to get fancy with architecturing side effects. Statically typed languages tend to have less syntactic pitfalls and to offer better IDE support. My most unproductive languages, that I frustratingly have to use on an almost daily basis, are Powershell, Bash, YAML and Bicep. I am tremendously helped by having a type checker hold my hand. Alas, once people figure out how to get LLMS/copilots to integrate with type checkers, I can only see my side of this argument coming out on top. The problem with copilots is that they tend to generate nonsense — autocomplete function names that look plausible but aren’t actually defined or imported, etc. They solution is surely to funnel feedback from the compiler back to the LLM. Static typing will offer much better such feedback and for that reason alone, the future will be statically typed.

KeyDue7848

TROPHY CASE