Linear Types

Monad's design calls for linear and affine types for resource-safe programming, inspired by Rust's ownership system and Idris's Quantitative Type Theory (QTT).

[!WARNING] The syntax parses; nothing is enforced. Struct fields, def parameters, lambda parameters and destructured parameters all accept !, ? and % in the self-hosted compiler. Every one of those annotations is then dropped before type checking — no use is counted, and every binder the checker builds is Many.

So today a multiplicity is documentation that the compiler carries as far as its own AST and no further. This chapter documents the intended design; see Where this actually stands for the state of the implementation.

Overview

Every variable in Monad is meant to carry a multiplicity controlling how many times it may be used:

What Parses Today

Struct fields accept all four, in both implementations:

struct Buffer {
    !data : String,
    ?label : String,
    size : I64
}

So do parameters, on definitions and on typed lambda parameters:

def f (!a : I64) (?b : I64) (%c : I64) (d : I64) : I64 := a + b + c + d
def h : I64 -> I64 := fn (!x : I64) => x

Two things about the parameter form are easy to get wrong:

• The prefix applies to the whole group, not one name. (!x y : I64) marks both x and y linear. Write separate groups if you meant otherwise.
• A lambda parameter must be parenthesised and annotated. Bare \ !x => x is a parse error in both implementations.

A destructured parameter takes a prefix too:

struct Coord { fst : I64, snd : I64 }

// Self-hosted only -- the bootstrap host rejects a prefix on this form.
def sum_coord (!{fst, snd} : Coord) : I64 := fst + snd

All of it is recorded on the parse tree and then discarded.

Usage Rules (design)

The intent is that these are checked at compile time, with no run-time overhead:

1. Linear (!x): must appear exactly once in the body
2. Affine (?x): must appear at most once
3. Many (x): unrestricted
4. Zero (%x): must not appear in run-time position at all

def ok (!x : I64) : I64 := x           // intended: passes
def unused (!x : I64) : I64 := 42      // intended: fails — never used
def overused (!x : I64) : I64 := x + x // intended: fails — used twice
def affine_ok (?x : I64) : I64 := 42   // intended: passes
def many_ok (x : I64) : I64 := x + x   // passes

Today all five compile, in both implementations.

Where This Actually Stands

Parsing is done. What is left is everything after it:

1. Lowering keeps nothing. The parser records a multiplicity on each parameter, and the pass that builds the core pi/lam terms has nowhere to put it — those terms have no multiplicity field. It is dropped there.
2. Usage checking, in both implementations. Counting machinery was written against an earlier version of the host's type checker. That checker has been replaced and the current one does not call it — every function type it builds uses Many.
3. Codegen use, in the self-hosted backend. Nothing consumes multiplicities.

So the annotations are documentation that the compiler carries as far as its own parse tree.

Why It Matters Beyond Correctness

Multiplicities are also the intended basis for memory management. Compiled binaries currently reach for a conservative garbage collector because codegen never emits a free — see Compiling and Running. The plan is for linear and affine information to tell the backend exactly where a value's last use is, so it can free deterministically and drop the GC.

That is the strongest argument for finishing this work, and it is why the GC is described as a stopgap rather than a design choice.

Comparison to Rust

Roadmap

Roughly in order:

• Wire multiplicity_prefix into the self-hosted definition- and lambda-parameter parsers — done, destructured parameters included
• Carry the multiplicity through lowering, so pi and lam can hold one
• Reinstate usage checking in the current type checker
• Track let-bound variables, not just parameters
• Check arrow multiplicity at application sites
• Enforce multiplicities on constructor fields under pattern matching
• Subsumption: Many should subsume Linear and Affine
• Drive codegen's memory reclamation from multiplicities, replacing the GC
• noalias attributes on linear parameters in the emitted LLVM IR

Next, we'll explore concurrency.