The Type Environment: What Γ Is, and Where the Compiler Keeps It
Γ = { x: int, name: string }, and `Γ ⊢ x + 1 : int` says “under those assumptions, this holds”. In a real compiler Γ is not a new structure — it is the symbol table, read by the type checker instead of by the resolver.
What is the Γ in Γ ⊢ x + 1 : int, and what data structure is it in an actual compiler?
A finite map from names to types, threaded through every judgment in the derivation. It is the *assumption set* under which a typing claim is made, and in a compiler it is the same table [[symbol-table]] describes — the resolver writes the bindings, the checker reads their type field. Γ exists to answer one question: when the checker meets a bare name, what is it entitled to assume about it?
A rule may use only bindings that are present in Γ at that point in the derivation. Γ may be extended only by a binding form — a lambda parameter, a let, a block declaration — and the extension is scoped to the premise it appears in and to nothing else. That single restriction is what makes [[lexical-scope]] and [[shadowing]] consequences of the rules rather than separate machinery bolted on afterwards.
Key points
Γ ⊢ e : Tmeans “under the assumptions in Γ, e has type T”. The turnstile separates assumptions from claim.- Γ is a finite map from names to types, and in a compiler it is the type column of the symbol table, not a new structure.
- Only variable lookup reads Γ; only binding forms extend it; the extension is scoped to the premise it appears in.
- Lexical scope and shadowing are consequences of where the rules put the extension, not features requiring separate machinery.
- An unbound name and a type mismatch are different failures from different phases, even though both look like “Γ has no answer”.
- The symbol table carries much more than Γ — mutability, spans, storage, visibility — because later phases need it, not because the rules do.
- The choice of environment structure is really a choice about whether an old environment can be recovered later, which decides how well the compiler serves an IDE.
Under these assumptions
x + 1 : int is not a statement that can be true or false on its own, because x is a name and names mean nothing in isolation. What is true or false is the conditional version: *given* that x is an int, x + 1 is an int. Γ is where the “given” lives, and ⊢ is the symbol that separates the assumptions from the claim.
Read Γ ⊢ e : T aloud as “under the assumptions in Γ, e has type T”. Some people read ⊢ as “entails” or “proves”; “under these assumptions” is the version that makes the rules make sense the first time.
The empty environment ∅ is worth a moment. ∅ ⊢ 1 + 1 : int holds — no assumptions needed. ∅ ⊢ x + 1 : int does not hold, and the reason is not that x has the wrong type but that there is *nothing to look up*. In a compiler that is not a type error at all: it is an unresolved-name error, produced by [[name-resolution]] before the checker ever ran, which is why “undefined variable” and “type mismatch” are different diagnostics from different phases.
Γ = { x : int, name : string, f : int → bool }
Γ ⊢ x + 1 : int ✓ T-Var gives x : int, T-Add applies
Γ ⊢ f x : bool ✓ T-App: argument int matches parameter int
Γ ⊢ name + 1 : ✗ no rule: T-Add needs int, name is string
Γ ⊢ f name : ✗ no rule: T-App needs int, name is string
Γ ⊢ y + 1 : ✗ y ∉ Γ — nothing to assume, so nothing to check
∅ ⊢ x + 1 : ✗ same reason: the environment is empty
The last two look identical to the checker and are
reported by different phases: an unbound name is caught
by name resolution, a mismatch by the type checker.The same table, two readers
rustc splits the work across query-based passes so that “the type of this declaration” is a memoised query rather than a field read. Constraint-based checkers such as TypeScript’s keep a separate inference context on top of the symbol table because a name’s type may not be known yet. The conceptual identity holds in all three; the code layout does not.The mistake worth avoiding is treating Γ as a new data structure the type checker builds. In a real compiler the resolver has already built a table mapping each name occurrence to a declaration, and each declaration to everything known about it. Γ is a *projection* of that table: the name-to-type column, restricted to what is in scope at the point being checked.
This matters practically because it tells you where to look when something is wrong. If the checker reports a type you did not expect for a name, the bug is at least as likely in the resolver as in the checker — the name may have bound to a different declaration than you assumed, and the checker faithfully read that declaration’s type. Shadowing bugs present exactly this way.
It also tells you what Γ deliberately omits. The symbol table carries mutability, storage class, the declaration’s span, visibility, whether the name is captured by a closure, and eventually a stack slot or register. None of that appears in a typing rule, because none of it is needed to establish a judgment. Compilers keep it on the same record anyway, which is why the two are the same structure in code and different in the notation.
| Field on the declaration | Written by | In Γ? | Who needs it |
|---|---|---|---|
| Name → declaration | Name resolution | Implicitly — Γ is keyed by name | Everyone downstream |
| Declared or inferred type | Parser, or the checker itself | Yes — this is Γ | The type checker |
| Mutability / assignability | Parser | No, in most calculi | The checker, as a side condition on assignment; borrow checking in Rust |
| Source span of the declaration | Parser, from [[spans-and-ranges]] | No | Diagnostics, and go-to-definition in [[language-server]] |
| Visibility / export status | Parser | No | Module checking and [[interface-files]] |
| Storage: local slot, capture, global | A later resolution pass | No | Lowering and [[closure-conversion]] |
| Overload set (several declarations, one name) | Name resolution | Only in languages that have it | Overload resolution — see [[ad-hoc-polymorphism]] |
Extension is where scoping comes from
Γ grows at exactly one kind of place: a form that binds a name. The notation for that is a comma — Γ, x : T means “Γ with the additional assumption that x has type T”. The crucial detail is *where the extended environment appears*: only in the premise about the body, never in the conclusion and never in sibling premises.
Read the let rule below with that in mind. e₁ is typed under plain Γ, because x is not in scope in its own initializer. e₂ is typed under the extended environment. Move the extension one premise to the left and you have specified a language where let x = x + 1 refers to the new x — which is a real design (Rust’s let rebinding is close, though it still evaluates the initializer under the old binding), and the point is that the rule is where that decision is written down.
Shadowing falls out for free. If Γ already contains x : int and the rule extends it with x : string, the comma is right-biased: lookups find the new binding. Nothing else in the system needs to know. That is the whole implementation of [[shadowing]], and it is why a language with shadowing is not more complicated to type-check than one without — it is a property of how the map is extended and consulted.
Γ ⊢ e₁ : T₁ Γ, x : T₁ ⊢ e₂ : T₂
─────────────────────────────────────── (T-Let)
Γ ⊢ let x = e₁ in e₂ : T₂
Note where the extension is NOT: e₁ is typed under plain Γ,
so `let x = x + 1` refers to an outer x, or fails.
Γ, x : T₁ ⊢ e : T₂
──────────────────────────────── (T-Abs)
Γ ⊢ (fun x : T₁ => e) : T₁ → T₂
A parameter is a binding form. Same mechanism.
Shadowing, worked:
Γ = { x : int }
Γ, x: string = { x : string } the comma is right-biased
Γ ⊢ let x = "hi" in x + 1 : ✗
because the body is typed under { x : string },
and T-Add has no rule for string.
Recursion needs the binding BEFORE the body is typed:
Γ, f : T₁ → T₂, x : T₁ ⊢ e : T₂
────────────────────────────────── (T-LetRec)
Γ ⊢ let rec f x = e in ... : ...
which is why a language with mutual recursion needs a
pre-pass that seeds Γ from signatures — `[[declaration-order]]`.How it is actually implemented
The notation says “a finite map”, and every practical structure is a different answer to one question: what happens when you leave a scope?
A stack of hash maps is the standard imperative answer. Entering a scope pushes a map, leaving it pops. Lookup walks the stack from the top. It is simple, it is what most production compilers do, and its cost is that lookup is O(depth) in the worst case and that you cannot cheaply keep a snapshot of an old environment — which matters if the checker needs to revisit a scope, as a [[language-server]] constantly does.
A persistent (immutable) map is the functional answer: extending Γ returns a new map sharing structure with the old one, so every environment ever created remains valid and cheap to hold. This is what most ML and Haskell compilers use, and what makes incremental and demand-driven checking natural — see [[incremental-compilation]]. The cost is allocation pressure and a constant factor on every lookup relative to a flat hash map.
A flat table with scope numbers is what a compiler optimising for memory does: one array of entries, each tagged with the scope it belongs to, and a separate index. Cache-friendly and awkward to snapshot. And de Bruijn indices dispense with names entirely — a variable is “three binders up” — which makes alpha-equivalence free and the debugger’s job miserable, so it appears in cores and proof assistants rather than in user-facing compilers.
- The lookup structure is a hash table in almost every case; the interesting design choice is the scoping strategy layered over it.
- Persistent maps make “what was the environment at this point?” answerable after the fact, which is the query a language server and an incremental checker both need constantly.
- A stack of maps makes it unanswerable, which is why compilers built for batch compilation are hard to retrofit into IDE backends — a real, expensive lesson from the history of both
tscandrustc. - Whatever the structure, the checker must be able to extend Γ with a binding whose type is not yet known (a fresh type variable), because that is how
[[type-inference]]works.
How it works
The steps, in the order the compiler takes them.
- Name resolution walks the tree with a scope stack, binding each identifier occurrence to a declaration and recording the declaration’s type field.
- The checker begins at the top level with Γ containing the module’s imports, its top-level declarations, and the language’s built-in names.
- At each binding form the checker extends Γ with the bound name and its type, then checks the body under the extension.
- On leaving the binding form the extension goes away — by popping a scope, or by simply not passing the extended map any further.
- At each variable occurrence the checker looks the name up in Γ and returns the associated type, which is T-Var and the only rule that touches Γ at all.
- Where the bound type is not yet known, the checker inserts a fresh type variable and records a constraint to be solved later by
[[unification]]. - For mutually recursive declarations a pre-pass seeds Γ with every signature in the group before any body is checked, so that each body can refer to the others.
How it breaks
What the engineer observes when it goes wrong — not what goes wrong internally.
- A variable resolves to an outer declaration the author did not intend, the checker reports its type faithfully, and the error message is about a type the engineer cannot find in the function they are reading.
- A scope is popped one statement too early, and a name that should be visible reports as undefined — the classic off-by-one in a hand-written resolver, and it moves with formatting changes.
- A scope is popped one statement too late, and a name leaks out of a block. Nothing errors; a later declaration silently shadows nothing and the wrong value is read.
- Mutually recursive functions type-check in one declaration order and fail in another, because Γ was seeded lazily rather than by a pre-pass. The bug report says “moving this function up fixed it”.
- A compiler built on a stack of maps is retrofitted into a language server, and each keystroke re-checks the whole file because no earlier environment can be recovered — the observable symptom is completion latency that grows with file size.
- Two type variables in Γ are unified in a way that changes an *outer* binding’s type mid-check, and a name’s type appears to change between two uses in the same function.
When it helps
- Debugging a resolver or checker of your own: almost every wrong-type-for-a-name bug is an extension in the wrong place or a scope popped at the wrong time.
- Reading typing rules from a specification, where Γ is threaded through everything and it is easy to stop seeing it — until a rule extends it and the whole meaning of the premise changes.
- Understanding why a language allows or forbids a particular self-reference:
let x = x, a class referring to itself, a type alias referring to itself. The answer is always where the rule puts the extension. - Designing an incremental or IDE-facing checker, where the ability to recover a past environment is the difference between per-keystroke and per-file work.
When it hurts
- Treating Γ as a runtime concept. It exists only during checking. At runtime the names are gone — see
[[information-loss]]— and what survives is a stack slot or a captured cell. - Assuming Γ contains everything the compiler knows. It contains what the typing rules need, and it is a deliberately small projection of a much larger record.
- Reasoning about dynamic scoping with this model. Under dynamic scoping the environment is a runtime call-stack property and cannot be threaded through a static derivation at all — see
[[static-vs-dynamic-scoping]].
What it costs
Every one of these is paid by something.
- A persistent environment buys recoverable snapshots — incremental checking, IDE queries, backtracking during inference — and pays in allocation on every binding and a constant factor on every lookup.
- A stack of mutable maps buys the fastest possible batch check and the simplest code, and pays in an environment that cannot be revisited, which is a structural obstacle to serving an IDE from the same compiler.
- Keeping Γ and the symbol table as one record buys locality and one source of truth, and pays in a record that every phase can see all of — which is precisely how a checker ends up depending on a field that lowering had not filled in yet.
- Seeding Γ with all signatures in a recursive group before checking bodies buys order-independence for the programmer, and pays in a mandatory extra pass and in the requirement that signatures be written or inferrable *without* checking the bodies.
What else you could do
What a different compiler or language does instead, and when that is better.
- De Bruijn indices, replacing names with binder distances. Alpha-equivalence becomes syntactic equality and the environment becomes a list, at the cost of every diagnostic and debugging aid; used in proof assistants and compiler cores, not in frontends.
- A global flat table with qualified names, as C’s single global namespace plus block scopes effectively is. Simple, and it forces every language on top of it to invent mangling — see
[[name-mangling]]. - Demand-driven queries instead of a threaded environment:
rustcasks “what is the type of this definition?” and memoises, so there is no single Γ being carried anywhere. This makes incrementality the default and the control flow much harder to follow. - Runtime environments, as a dynamically scoped language or an interpreter uses: the environment is a chain of frames consulted at execution time rather than a static assumption set — see
[[static-vs-dynamic-scoping]].
See it for yourself
The flag, dump or tool that shows you this directly.
clang -Xclang -ast-dumpprints eachDeclRefExprwith a pointer to the declaration it resolved to — that pointer is the Γ lookup, made visible.rustc -Z unpretty=hir,typedon nightly prints the HIR with types attached, showing what the checker concluded for each name.- In TypeScript, hover in an editor is a Γ lookup rendered as a tooltip;
tsc --listFilesplus the language service’sgetTypeAtPositionis the programmatic version. python -c "import symtable; ..."exposes CPython’s own symbol table, including which names a scope treats as local, global or free — the resolver’s output without the types.- Our scope and symbol-table viewer at
/compilers/semanticssteps through a program showing the environment growing and shrinking as scopes open and close.
Plausible wrong readings
Stated the way a confident engineer states them.
- “Γ is the symbol table.” It is a projection of it: the name-to-type map that the typing rules need. The symbol table also carries storage, mutability, spans and visibility, none of which appear in a rule.
- “The turnstile means implies.” It separates assumptions from a claim. The implication in a rule runs vertically, across the line; the turnstile runs horizontally, within one judgment.
- “Extending Γ modifies it.” In the notation it does not —
Γ, x : Tis a new environment. Whether the implementation mutates a stack or allocates a new map is a choice with consequences, and confusing the two is how scope-leak bugs get written. - “Undefined variable is a type error.” It is a name-resolution error, produced before the checker runs. They present similarly and come from different phases with different fixes.
- “Γ exists at runtime.” Nothing named survives to runtime unless the compiler deliberately emitted it as debug metadata —
[[debug-information]].
Misconceptions
The claim, and what is actually true.
Go deeper
The same idea at increasing depth. Stop wherever it stops being useful.
overview
Γ, said “gamma”, is just the list of what the checker currently knows about names — { x: int, name: string }. The turnstile ⊢ means “under those assumptions”. So Γ ⊢ x + 1 : int reads “given that x is an int, x + 1 is an int”. In a real compiler this list is the symbol table, which name resolution filled in first. When a name is bound — by a parameter, a let, a declaration — the list temporarily grows, and it shrinks again when the scope ends. That growing and shrinking is exactly what scoping means.
practical
When a checker tells you a name has a type you did not expect, do not start by doubting the type rules. Start by finding which declaration the name actually bound to. Shadowing, a wildcard import, a method on a base class, a macro-introduced binding — any of these makes the resolver hand the checker a different declaration than you were reading, and the checker then reports that declaration’s type perfectly correctly. Editors make this fast: go-to-definition on the name is literally a Γ lookup, and if it lands somewhere surprising you have found the bug without reading a single typing rule.
advanced
The environment structure is one of the few frontend decisions that determines whether a compiler can ever become a good IDE backend. A batch compiler threads a mutable scope stack, discards it as it goes, and is therefore constitutionally unable to answer “what was in scope at line 340?” without redoing the work. A compiler built on persistent environments or memoised queries can answer it in constant time, which is what per-keystroke completion, inline diagnostics and semantic rename require. Both tsc and rustc reorganised substantially to serve [[language-server]] workloads, and in both cases the reorganisation was about making intermediate results — the environment prominently among them — recoverable rather than transient. If you are building a checker you expect an editor to use, choose the structure for that at the start; retrofitting it is a rewrite of the frontend.
How much this depends on
Nothing in this domain is true of every compiler. These say how much.
rustc uses memoised queries with no single threaded environment, GHC uses persistent maps, and TypeScript keeps a separate inference context alongside the symbol table because names may not have types yet. The concept is shared; the code is not.If you were asked this in an interview
- What does the turnstile mean in
Γ ⊢ x + 1 : int? - Where does Γ come from in a real compiler, and who wrote the entries?
- Show me, using the
letrule, whylet x = x + 1does not refer to the newx. - Why do mutually recursive functions need a pre-pass over signatures before any body is checked?
Connections
- Programming Languages & Runtime Internals — Runtime environments: activation records, closure environments, and the scope chainΓ disappears at the end of checking. What replaces it at runtime — a frame, a captured cell, a scope chain in a dynamically scoped or reflective language — is the runtime’s structure, and it is a different thing that happens to be described with the same word.