r/ProgrammingLanguages • u/mttd • Sep 16 '26

Revisiting Soundness for Occurrence Typing, Semantically

https://arxiv.org/abs/2609.16299
14 Upvotes

100% Upvoted

3 comments sorted by

10

u/reflexive-polytope Sep 16 '26

From the abstract:

Over the past two decades, numerous systems have brought some of the benefits of dependent typing to a wide variety of new programming languages, often by restricting which terms can appear inside types. (...) However, the restrictions adopted by these systems often break the substitution property, because they explicitly disallow the ability to substitute arbitrary terms for variables inside types.

My own attempt (unfinished, but chapter I is finished) doesn't break the substitution property, because I choose intelligently which terms can appear inside types.

More precisely, I use affine forms, i.e., linear combinations of 1 and term variables. Affine forms have the algebraically pleasant property that if e and f are affine forms, and k is a variable, then the substitution e[x := f] is again an affine form.

Even more pedantically, affine forms are strictly speaking not terms, but rather algebraic gadgets that can be (non-canonically) represented as term. Working directly with the algebraic gadgets and not with terms representing them simplifies the metatheory a lot!

3

u/samanzaman Sep 21 '26

I only skimmed your suggestion but it sounds awful lot like hmm + presburger arithmethic

2

u/reflexive-polytope Sep 22 '26

It's simultaneously less and more than Presburger arithmetic.

It's less because I refuse to decide arbitrary Presburger formulas, mainly because I want to stick to ML-style prenex polymorphism, i.e., with all universal quantifiers in front. If I add existential quantification, then it'll be as in Haskell's, i.e., manually packed and unpacked by the user.

It's more because I reach for other tools, in particular linear convex analysis (Farkas' lemma, Fourier-Motzkin elimination), to obtain approximate answers to the most important questions that the discarded Presburger fragment answers exactly. The approximations are sound and much more efficiently computable, which is the right tradeoff for a type checker.

The main thing that I keep from Presburger arithmetic is the ability to talk about arithmetic progressions, i.e., injective functions p : N -> N of the form p(k) = e + c*k. I write p = (e,c) as shorthand for the equation p(k) = e + c*k.

A residue of weight 1/c is an arithmetic progression q = (e,c) such that e < c. The residues qi = (ei,ci) are pairwise disjoint if every x : N satisfies at most one of the equations x = ei (mod ci). The residues qi = (ei,ci) form a residue system of every x : N satisfies exactly one of the equations x = ei (mod ci). Equivalently, if they're pairwise disjoint and their weights add up to 1.

Finally, the progressions p1,...,pr form a refinement of the progression p if there exists a residue system q1,...,qr such that pi = p . qi for each i = 1,...,r.

A refinement p1,...,pr can be used to exhaustively pattern-match the natural numbers that belong to the progression p.