Typesspec

Typing Rules: Reading the Notation With the Line Through It

Premises above the line, conclusion below, and a name in brackets. Once you can read one aloud you can read a language specification, and the shape of the rule set tells you what the checker’s algorithm has to be.

The question

How do I read the fraction-looking notation in a language specification or a types paper?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute

What the program is here

The program as a *derivation tree*. Each node is a judgment — “under these assumptions, this expression has this type” — and each edge is one instance of a rule. The tree the checker builds is literally a proof, which is why the best phrasing of a type error is “no rule applies here”, not “this type is wrong”.

What this phase may assume or do

A rule set is usable by a straightforward algorithm only if it is *syntax-directed*: at most one rule may match each expression form, so the checker never has to guess or backtrack. Two rules break this on purpose — subsumption in [[subtyping]], which applies to every expression, and overload resolution in [[ad-hoc-polymorphism]], which offers several candidates. Both buy expressiveness and pay in algorithmic complexity, and every real checker restricts *where* they may fire to get determinism back.

Key points

Premises above the line, conclusion below, rule name in brackets. Say “if” before the top and “then” before the bottom.
A rule with nothing above the line is an axiom, true under any assumptions.
The colon is read “has type”; the turnstile ⊢ is read “under these assumptions”.
A derivation is a proof tree, and the typed AST a checker produces is that tree with the rule names dropped.
A type error is best described as “no rule applies at this node”, which is both more accurate and more actionable than “wrong type”.
Rules are declarative: they say which judgments hold, not how to find them. Turning them into an algorithm is a separate, provable step.
Subsumption and overloading are the two rules that destroy syntax-directedness, and every real checker restricts where they may fire.

How to read one out loud

The notation looks like a fraction and is not one. Everything above the line is a list of *premises*: things that must already have been shown. The single thing below the line is the *conclusion*: what you are then entitled to conclude. The name in brackets on the right is just a label so people can refer to the rule.

Here is the addition rule in the simplest form it ever appears in. Read it left to right, top to bottom, and put the word “if” in front of the top and “then” in front of the bottom.

The addition rule, and how to say it

        e₁ : int        e₂ : int
       ───────────────────────────  (T-Add)
              e₁ + e₂ : int

Aloud:
  "If e-one has type int, and e-two has type int,
   then e-one plus e-two has type int."

Or, closer to how a compiler engineer says it:
  "To type an addition, type both operands. If they are
   both int, the whole thing is an int. Otherwise this
   rule does not apply and you must look for another."

The colon is read "has type". It is not assignment,
and it is not a dictionary entry.

Axioms, rules, and where the assumptions live

simplifiedThis rule set is the simply typed lambda calculus with a couple of constants, and it is deliberately smaller than any usable language. It has no polymorphism ([[parametric-polymorphism]]), no subtyping ([[subtyping]]), no recursion, no mutation and no inference — fun x : T₁ requires the annotation because there is no rule that could invent it. Every one of those additions changes the algorithm, not just the rule list, which is the point of the last section.

A rule with no premises at all is an *axiom* — you may conclude it unconditionally. The line is usually still drawn, with nothing above it, which is a small notational joke that confuses everyone exactly once.

A rule set that only mentions closed expressions cannot say anything about variables, because x : int is not true unconditionally; it is true *under an assumption*. That assumption set is carried in every judgment as Γ, pronounced “gamma”, and the full form of every rule above is Γ ⊢ e : T. The turnstile ⊢ is read “entails” or, more usefully, “under these assumptions”. [[type-environment]] is entirely about what Γ is and where a compiler keeps it; for now, read it as “the things we are currently allowed to assume”.

Below is a small but complete rule set — enough to type any expression built from integers, booleans, addition, conditionals, variables, functions and application. It is worth noticing how small this is. A language’s core type system is usually a page; the other four hundred pages of its specification are the library, the syntax and the corner cases.

T-Int and T-True have no premises: they are axioms, true under any assumptions at all.
T-Var is the only rule that reads Γ. Everything else either passes it down unchanged or extends it.
T-If requires both branches to have the *same* T. That single requirement is why languages without union types make you restructure conditionals, and why [[union-types]] exist.
T-Abs is the only rule that *extends* Γ, and it extends it only for the premise about the body. That is lexical scope, falling out of the notation rather than needing separate machinery — see [[lexical-scope]].
T-App is where almost every real type error in a real language originates: the argument’s type did not match the parameter’s.

A complete rule set for a tiny expression language

  ─────────────── (T-Int)          ──────────────── (T-True)
   Γ ⊢ n : int                      Γ ⊢ true : bool

        x : T ∈ Γ
       ───────────── (T-Var)
        Γ ⊢ x : T

     Γ ⊢ e₁ : int      Γ ⊢ e₂ : int
    ───────────────────────────────── (T-Add)
           Γ ⊢ e₁ + e₂ : int

   Γ ⊢ c : bool    Γ ⊢ e₁ : T    Γ ⊢ e₂ : T
  ─────────────────────────────────────────── (T-If)
        Γ ⊢ if c then e₁ else e₂ : T

        Γ, x : T₁ ⊢ e : T₂
   ───────────────────────────── (T-Abs)
    Γ ⊢ (fun x : T₁ => e) : T₁ → T₂

     Γ ⊢ e₁ : T₁ → T₂      Γ ⊢ e₂ : T₁
    ──────────────────────────────────── (T-App)
              Γ ⊢ e₁ e₂ : T₂

A derivation is a proof tree

Applying the rules to a concrete expression produces a tree. The leaves are axioms and variable lookups; each interior node is one rule application; the root is the judgment you wanted. That tree is the proof, and a type checker that accepts a program has built it — usually implicitly, as the call stack of a recursive walk, rather than as a data structure.

The tree below is the derivation for if b then x + 1 else 0 under the assumptions b : bool and x : int. Read it bottom-up as the checker builds it, or top-down as the proof reads.

Derivation of Γ ⊢ if b then x + 1 else 0 : int, with Γ = { b: bool, x: int }

Typed AST — same shape, with symbols and types attached

T-If: if b then x + 1 else 0: int— Needs three premises: the condition is bool, and both branches share one type T. Here T = int, so the whole expression is int.

├── T-Var: b: bool→ b : bool ∈ Γ— A leaf. The premise of T-Var is a lookup in Γ, not another judgment.

├── T-Add: x + 1: int

│ ├── T-Var: x: int→ x : int ∈ Γ

│ └── T-Int: 1: int— An axiom: no premises above the line.

└── T-Int: 0: int

Read it asEvery node names the rule that justified it. Delete the rule names and this is just the typed AST a checker hands to lowering — which is the useful realisation: the typed AST *is* the derivation, stored. If x were a string, no rule would justify node d2, and the checker would report there. That is what “no rule applies” means concretely, and it is a more accurate description of a type error than “wrong type”.

What the notation buys, and what it does not say

The notation buys unambiguity. A specification written in prose — “the operands of + must be of numeric type, or one may be a string, in which case…” — has to be interpreted, and two implementations will interpret it differently. A rule set has exactly one reading, can be transcribed into a proof assistant, and can be mechanically checked for the soundness properties in [[what-a-type-system-proves]]. WebAssembly’s specification is written this way, which is a large part of why independent implementations agree.

What the notation deliberately does not say is *how to find the derivation*. The rules are declarative: they describe which judgments are valid, not the order in which to establish them. Turning a declarative rule set into an algorithm is a separate step, and where it is hard, it is hard for a nameable reason.

Subsumption is the canonical difficulty. In a language with subtyping, Γ ⊢ e : S and S <: T licenses Γ ⊢ e : T — for *any* e. That rule matches everywhere, so a naive checker would have to guess where to apply it. The standard fix is to prove an equivalent algorithmic rule set in which subsumption is folded into the places it is actually needed (argument positions, assignment, returns) and appears nowhere else. When you read a specification and find two rule sets, a declarative one and an algorithmic one with a theorem connecting them, this is what you are looking at.

What each addition to the rule set costs the algorithmtypical

Feature added	New rule	What breaks	What checkers do about it
Subtyping	T-Sub: from `e : S` and `S <: T`, conclude `e : T`	Syntax-directedness — the rule matches every expression	Fold subsumption into argument, assignment and return positions only; prove the algorithmic system equivalent
Overloading	Several T-App variants for one name	Determinism — more than one candidate may apply	Rank candidates by conversion sequence, require a unique best, report ambiguity as an error
Inference	T-Abs without the annotation on x	Nothing to synthesize the parameter type from	Generate a fresh type variable and a constraint; solve later by `[[unification]]`
Polymorphism	T-Gen and T-Inst around let-bindings	A variable no longer has one type in Γ but a scheme	Instantiate at each use, generalize at each let — see `[[hindley-milner]]`
Recursion	T-Fix, or a self-reference in Γ before the body is typed	Γ must contain the function while checking its own body	A pre-pass that populates Γ from signatures before checking any body — see `[[declaration-order]]`
Mutation	Reference types with a store typing	Generalization becomes unsound	The value restriction, or effect tracking — see `[[hindley-milner]]`

How it works

The steps, in the order the compiler takes them.

Write one rule per expression form of the language, with the premises stating what must hold of the sub-expressions.
Thread an assumption set Γ through every judgment; only variable lookup reads it and only binding forms extend it.
Check syntax-directedness: for each expression form, count the rules whose conclusion could match. More than one means the checker will need ranking or search.
Derive the algorithm by reading each rule as “to type this node, first type these children, then verify these side conditions”.
Where a rule needs a type that cannot be synthesized, either demand an annotation or introduce a variable and a constraint.
Prove — or at least argue — that the algorithm accepts exactly the programs the declarative rules do, which is the standard soundness-and-completeness pair for a type checker.

How it breaks

What the engineer observes when it goes wrong — not what goes wrong internally.

An engineer reads the line as a fraction or as an implication running the wrong way, concludes the rules say something backwards, and derives a confidently wrong mental model of the language.
A language designer writes rules that are not syntax-directed, implements the obvious recursive checker anyway, and ships a compiler whose acceptance depends on the order it happened to try things — so two versions of the same compiler disagree on the same file.
The declarative rules and the implemented algorithm drift apart over releases, and a program accepted by the specification is rejected by the compiler, or the reverse. The bug report reads “the spec says this is legal”.
A rule requires both branches of a conditional to have the same type, the implementation quietly takes the first branch’s type instead, and a value of the wrong type flows out of an if with no diagnostic.
Recursion is checked without a pre-pass that seeds Γ, so a mutually recursive pair type-checks in one file order and fails in another — the error moves when someone reorders declarations.

When it helps

Reading a language specification, a types paper, or an RFC for a new language feature — this notation is the shared vocabulary of all three, and it is the only entry cost.
Designing a DSL or a schema language, where writing the rules down catches the case you had not considered far more cheaply than the implementation does.
Arguing precisely about a proposed feature: “what is the rule, and is it syntax-directed?” cuts through a design discussion in one question.
Debugging a checker of your own: locate which rule should have applied, then find why its premises were not established.

When it hurts

As a teaching device for people who will never implement a checker. The notation is a compression of things sayable in English, and for a working engineer the English version is often enough.
As a source of algorithms. The rules do not describe an implementation, and reading them as one produces checkers that are exponential or that quietly depend on rule-trial order.
When the language’s real behaviour has diverged from its written rules — reading the rules then tells you what was intended, which is useful history and unreliable documentation.

What it costs

Every one of these is paid by something.

Formal rules buy an unambiguous specification and the possibility of a machine-checked soundness proof, and pay in author effort, reader entry cost, and a specification that far fewer contributors can safely edit.
Keeping the rule set syntax-directed buys a linear deterministic checker and clean error messages, and pays in expressiveness: no subsumption, no overloading, and often no inference.
Maintaining separate declarative and algorithmic rule sets buys both a readable specification and an implementable one, and pays in a proof of equivalence that must be redone every time the language grows.
Prose specification buys accessibility and pays in divergent implementations; every language that started in prose and later formalised a core (Java, JavaScript, WebAssembly) did so after interoperability bugs, not before.

What else you could do

What a different compiler or language does instead, and when that is better.

Specify by reference implementation: the compiler is the specification. Fast to change, impossible to reason about, and the strategy Python and early Ruby used for years.
Specify in prose with worked examples, as C, C++, Java and Go largely do. Readable by more people, and the source of long-running disputes about what a paragraph means.
Specify by mechanised semantics in a proof assistant — CompCert’s CompCert C, the K framework’s C and Java semantics, WebAssembly’s Isabelle and Coq formalisations. Highest confidence, highest cost, and the only route to [[verified-compilers]].
Specify by conformance test suite, which is what most schema and wire-format standards do in practice: the rules are whatever passes. Good coverage of the cases someone thought of, and silent on everything else — see [[golden-tests]].

See it for yourself

The flag, dump or tool that shows you this directly.

The WebAssembly core specification’s “Validation” chapter is written entirely as typing rules in exactly this notation, and is the most approachable real example of a shipped language specified this way.
The Java Language Specification chapter 15 and the C++ standard’s [over.match] are the prose counterpart — read a rule from each and compare the ambiguity.
Any implementation of the simply typed lambda calculus (Pierce’s *Types and Programming Languages* chapter 9 code, or a hundred repositories called stlc) shows the rules and the corresponding recursive checker side by side in under 200 lines.
For a checker you can actually step: our type-inference stepper at /compilers/types shows the derivation being built node by node with the rule name on each step.
rustc --explain on any type-error code prints, in prose, the premise that failed — a rule set translated for humans.

Plausible wrong readings

Stated the way a confident engineer states them.

“The line means division.” It means implication: everything above must hold for the thing below to be concluded.
“The rules tell you how the checker works.” They tell you what is *valid*. The algorithm is a separate artifact and, for anything with subtyping or inference, a substantially different one.
“Γ is a global symbol table.” It is a per-judgment assumption set that grows as you descend into binding forms and shrinks as you leave them. That scoping *is* lexical scope.
“If I can write the rule, I can implement it.” Writing T-Sub takes one line. Implementing a checker with subtyping that terminates, is complete, and gives good errors is a research-scale problem in some type systems.
“The typed AST and the derivation are different things.” They are the same tree; the derivation additionally records which rule justified each node, and most compilers do not bother to store that.

Misconceptions

The claim, and what is actually true.

Typing rules are academic notation with no bearing on real compilers.

WebAssembly’s validation rules ship in this form and independent implementations agree because of it. Every type-error message in Rust and TypeScript corresponds to a rule whose premise failed; the notation is what the implementers were working from.

A bigger language needs many more rules.

The core rule set of a large language is usually one or two pages. What grows is the subtyping relation, the conversion lattice and the overload-ranking function — the side conditions, not the rules.

If the rules are written down, the implementation follows mechanically.

Only for syntax-directed rule sets. Adding subsumption or overloading turns transcription into algorithm design with a proof obligation attached.

Go deeper

The same idea at increasing depth. Stop wherever it stops being useful.

overview

The notation is a fill-in-the-blanks “if … then”. Things above the line are what must already be known; the thing below is what you may then conclude; the bracketed name is a label. e₁ : int and e₂ : int above the line with e₁ + e₂ : int below it says: if both operands are integers, the sum is an integer. That is all. Once you can read that, you can read the validation chapter of a language specification, which is where the real answers about a language live.

practical

The habit worth forming is to restate compiler errors as “no rule applies”. When a checker rejects something, ask which rule you expected to fire and which premise it could not establish — the answer is almost always a specific sub-expression whose type is not what you assumed. This reframing also improves how you write checkers and validators of your own: report the rule and the failed premise, cite where the expectation came from, and the message stops being “type mismatch” and starts being usable. And when you propose a language or DSL feature, write the rule before writing the parser. If you cannot write the rule, the feature is not specified yet.

advanced

The gap between declarative and algorithmic rule sets is where most of the real work is. A declarative system says what is derivable; an algorithmic one says how to derive it deterministically, and the theorem you owe is that the two accept the same programs. Subsumption is the standard obstacle — it applies at every node, so a direct implementation would search. The standard resolution restricts it to a small number of positions and proves the restriction complete. Overloading is the other, and it has no fully satisfying resolution: a ranking function is a heuristic dressed as a rule, which is why C++ overload resolution has pages of tie-breakers and still surprises people. When a language feature feels arbitrarily restricted — where a lambda must be annotated, why generic inference gives up on an overloaded call, why numeric literals need a suffix — the restriction is usually the price of keeping the algorithmic system deterministic and complete.

How much this depends on

Nothing in this domain is true of every compiler. These say how much.

specThe notation is standard across the programming-languages literature and across the specifications that use it (WebAssembly, Standard ML’s Definition, the formal cores of Java and Scala). Individual specifications vary in small ways: some write ⊦ or |-, some put the environment on the right, some name rules (add) rather than (T-Add). The shape — premises above, conclusion below — does not vary.

simplifiedThe rule set shown is the simply typed lambda calculus plus constants. It has no polymorphism, subtyping, recursion, mutation or inference, and cannot type any program you would actually write. Every addition in the final matrix changes the checking algorithm, not merely the rule list, and that is the reason to see the small version first.

typicalThe claim that a checker builds the derivation implicitly as its call stack describes the recursive-descent checkers that mainstream compilers use. Constraint-based checkers (Hindley–Milner implementations, TypeScript’s inference for generics) build a constraint set first and solve it afterwards, so there is no single moment at which a derivation exists — which is precisely why their error messages are harder to localise.

If you were asked this in an interview

Read this rule aloud and tell me what it means. [Show T-If.]
What is the difference between a declarative and an algorithmic rule set, and why do specifications sometimes contain both?
Why does adding subtyping to a language complicate the checker even though it only adds one rule?
The T-If rule requires both branches to have the same type. What does a language do when they do not?

Connections

DSAbinary-tree recursion

API Designwhat-is-an-api-contract

Domains that do not exist yet

Testing & Reliability Engineering — Conformance suites as an alternative to formal specification
Where a rule set is not written, a test suite becomes the de-facto specification. Judging what that costs in coverage and interoperability is a testing question rather than a compiler one.