Typesspec

Type Inference: Leaving the Type Off

`let x = 42` gives `x : int` in every language that has inference at all. The differences start at the second line, and the reason most mainstream languages infer locally rather than globally is error messages, not difficulty.

The question

When can I leave the type off, and why do most mainstream languages only let me do it locally?

Source→Lexing→Tokens→Parsing→AST→Semantics→Typed→IR→Optimize→Codegen→Machine code→Link→Execute
What the program is here

A tree with *holes*: expression and declaration nodes whose type is not written anywhere in the source. Inference fills the holes so that the whole tree has a derivation under the existing rules. The question this form answers is not “what type should this be” but “is there an assignment to the unwritten positions that makes the program well-typed, and is that assignment unique?”

What this phase may assume or do

Inference must produce a type the *declared* rules would have accepted; it may never invent a rule. Local inference additionally assumes the initializer is fully typed before the variable is used, which is why [[declaration-order]] matters here: auto x = f(); requires f’s return type to be already known, and a mutually recursive group must have its signatures seeded first. Where a language permits an inferred type to appear in a public signature, inference also becomes an API-stability question — a change in a body silently changes the contract.

Key points

  • let x = 42 agrees across languages; the mechanisms behind the agreement do not, and the differences appear on the next line.
  • Classify a language by the *unit* its inference solves over: one declaration, one function body, or a whole module. That number predicts annotation burden, error quality and API stability together.
  • Full inference was not avoided because it is hard. Algorithm W is small and old.
  • It was avoided because errors land far from mistakes, because subtyping and overloading destroy principal types, and because an inferred public signature is a contract that changes silently.
  • Annotations act as firewalls: they localise errors to a type the programmer actually wrote.
  • The converged design rule is annotate boundaries, infer interiors — which is also what keeps separate compilation cheap.
  • An annotation that changes the inferred type is load-bearing; deleting it is a behaviour change, not a cleanup.

The easy line, and where the languages part company

specRust’s integer-literal fallback to i32 in the absence of any other constraint is specified, as is Go’s default type for untyped constants and Java’s restriction of var to local variables with an initializer (JEP 286). TypeScript’s widening of literal types for mutable bindings and preservation for const is specified in its checker’s behaviour and has been stable since 2.1. What differs across these is not implementation detail — it is the language definition, so carrying the intuition from one to another will be wrong in a specific, predictable way.

let x = 42 infers x : int more or less everywhere, and the agreement is misleading. It hides three separate decisions each language made: how far the inference reaches, what the default type of an unconstrained integer literal is, and whether later uses are allowed to change the answer.

That third one is the sharpest divide. In C++, C# and Java, auto/var is decided the moment the initializer is typed and nothing afterwards can revise it. In Rust, the literal 42 starts as an unconstrained integer and a later use may pin it — let x = 42; foo(x) where foo takes u8 makes x : u8, and with no such use a fallback rule makes it i32. In TypeScript the literal type 42 is *widened* to number for a mutable binding and kept as the literal type 42 for a const. Same line, three different mechanisms.

The same line in seven languages, with the mechanism named
1C++     auto x = 42;      // int, fixed at the initializer. Uses cannot revise it.
2C#      var  x = 42;      // int, same. `var` is local-only, by design.
3Java    var  x = 42;      // int. Local variables only — never a field or a parameter.
4Go      x := 42           // int, the default type of an untyped integer constant.
5TS      let x = 42        // number  (literal type 42 widened for a mutable binding)
6TS      const x = 42      // 42      (the literal type is kept)
7Rust    let x = 42;       // inferred from USES; i32 only if nothing constrains it
8OCaml   let x = 42        // int, by whole-program Hindley-Milner inference

The Rust line is the odd one and the most instructive: inference there runs over the whole function body, so a use three statements later can decide the type of this declaration. In C++, C# and Java it cannot. The mechanism, not the answer, is what transfers between languages.

How far the inference reaches

The useful classification is not “does it have inference” but *what is the unit over which it solves*. That single number predicts the annotation burden, the error quality and the API-stability behaviour of the whole language.

Local inference solves one declaration at a time from its initializer, left to right. Function-body inference solves a whole body at once and lets uses inform declarations. Whole-program inference, in the Hindley–Milner sense, solves the entire module with no signatures required at all — the subject of [[hindley-milner]].

The unit of inference, and what it decidestypical
ReachLanguagesMust still be writtenWhat it buysWhat it costs
NoneC89, Java before 10, Go’s var x T formEverythingErrors point exactly at the declaration that disagreedEvery local variable is annotated, including obvious ones
One declaration, from its initializerspecC++ auto, C# var, Java var, Go :=All function signatures, all fieldsRemoves the most redundant annotations; errors stay localNothing later can inform the choice, so a mismatch is reported at the initializer even when the mistake is downstream
One function bodyimplementationRust, Swift, Kotlin, C# with target-typed new, TypeScript within a functionFunction signatures (Rust and Swift require them; TS and Kotlin often infer returns)Uses can inform declarations; closures and collection literals need no annotationErrors can surface at any point in the body, and a body edit can change an inferred return type
A whole recursive group / modulespecStandard ML, OCaml, Haskell, Elm, F#Nothing, in principleThe maximum annotation savings available; principal types existError locality collapses; a mistake here reports there — see [[unification]]

Why most languages stopped short of full inference

implementationRust and Swift require annotations on function signatures as a language rule, not as a limitation of their solvers — both run full unification inside a body. Kotlin and TypeScript will infer a public return type and offer explicitApi mode and the explicit-module-boundary-types lint respectively to turn it off. Haskell’s monomorphism restriction can be disabled with NoMonomorphismRestriction, at which point inferred top-level bindings generalise and can become unexpectedly slower. In each case the restriction is a chosen policy and can be located in the language’s design discussion.

The usual explanation — that full inference is hard to implement — is false. Algorithm W fits comfortably in a few hundred lines and has been well understood since 1978. Languages declined it for three concrete reasons, all of which are about the experience of using the language rather than the difficulty of building it.

Error messages. In a constraint-solving system, a failure is discovered where two constraints conflict, which need not be anywhere near the mistake. Delete a parameter from a function in Haskell and the error may land in a caller two modules away, described in terms of types you never wrote. Annotations act as *firewalls*: they pin down the answer at the boundary, so a mismatch is reported against a type the programmer wrote, in the file they are editing. This is the reason most often given by language designers, and it is a good one.

Subtyping and overloading. Hindley–Milner’s guarantee is a *principal* type — a single most-general answer. Add subtyping and principal types generally cease to exist: given x used both as a Dog and as an Animal, there is no canonical choice, and the system must either pick and be wrong sometimes or generate subtype constraints and solve a much harder problem. Add overloading and + no longer has one type, so constraint solving becomes search. Every mainstream object-oriented language has both features, which rules out plain HM before any other consideration.

API stability. If a public function’s type can be inferred, then editing its body can silently change its published signature, and a downstream consumer breaks with no visible change to the interface. Rust and Swift both require signatures on functions specifically for this: the type is a contract, and contracts are written, not derived. Haskell has the milder version of the same problem in the monomorphism restriction, which exists to stop a top-level binding from silently generalising into something whose runtime cost is different from what was intended.

  • The design rule almost everyone converged on: annotate boundaries, infer interiors. Signatures, public fields and module exports are written; locals and closures are not.
  • That rule is also what keeps [[interface-files]] and [[separate-compilation]] cheap — a module can be checked against its neighbours’ signatures without reading their bodies.
  • An inferred return type on a public function is a small convenience with an unbounded blast radius. Languages that allow it (TypeScript, Kotlin) usually also offer a lint to forbid it on exported declarations.
  • Inference quality is measured in *where the error lands*, not in how few annotations are required. A language that infers everything and blames the wrong line has made the tradeoff badly.

When an annotation is load-bearing

specRust specifies that integer overflow panics when debug assertions are enabled and wraps as two’s complement otherwise; this is a documented, deliberate difference between profiles rather than undefined behaviour. In C and C++ the corresponding signed overflow is undefined behaviour and the compiler may assume it does not occur — a materially different situation, covered in [[ub-and-optimization]].

The practical question is never “should I annotate everything” but “is this particular annotation doing work?” An annotation that inference would have produced anyway is noise; an annotation that *changes* the inferred type is load-bearing, and deleting it is a behaviour change wearing the costume of a cleanup.

The transformation below is the one to keep in mind. It looks like removing redundancy. In Rust it changes the arithmetic width, and the resulting overflow is a panic in a debug build and a wrap in a release build — one of the few places in safe Rust where build profile changes observable behaviour.

Deleting an annotation, in a language with use-directed inference
Before
let total: i64 = 0;
// ... later
let total = total + 3_000_000_000;
After
let total = 0;
// ... later
let total = total + 3_000_000_000;
Legal only when

Removing an annotation preserves the program’s meaning only if inference derives exactly the same type — that is, if some other constraint in scope already pins it. If a parameter, a return type, a trait bound or a later use forces i64, the annotation was redundant and its removal is behaviour-preserving.

Illegal when

When nothing else constrains the binding, so the literal falls back to the default numeric type. Here total becomes i32, 3_000_000_000 does not fit, and the addition overflows — a panic under the debug profile and a two’s-complement wrap under release, per Rust’s specified overflow behaviour. The same shape appears in TypeScript, where const xs: string[] = [] becomes const xs = [] inferred as any[] (or an implicit-any error under noImplicitAny), and in C++, where auto x = 0 gives int where long was intended.

How it works

The steps, in the order the compiler takes them.

  • Walk the tree. Where a type is written, use it. Where one is not, create a fresh type variable standing for the unknown.
  • Type-check as normal, except that whenever a rule demands two types be equal, record a constraint rather than comparing immediately.
  • For local inference, solve immediately and greedily: the initializer’s synthesized type becomes the declaration’s type and the variable is discharged before the next statement.
  • For body-wide inference, collect constraints across the whole body first, then solve them together by [[unification]], so later uses can inform earlier declarations.
  • Apply the resulting substitution to every node, replacing each type variable with its solution.
  • Where a variable remains unconstrained at the end, apply the language’s defaulting rule (Rust’s i32/f64, Haskell’s default declarations, Go’s untyped-constant defaults) or report an ambiguity error.
  • Record the final types on the tree, because everything downstream — overload resolution, [[monomorphization]], codegen — reads them rather than re-deriving them.

How it breaks

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

  • An error is reported in a file the engineer did not edit, describing types they never wrote, because a constraint from their change conflicted with one generated somewhere else.
  • A numeric literal defaults to a narrower type than intended and a value silently overflows — a panic in Rust’s debug profile, a wrap in release, and undefined behaviour in C++.
  • An inferred public return type changes when someone edits the body, and a downstream package stops compiling with no visible change to the interface it depends on.
  • A collection literal infers an element type from its first element and then rejects the second, and the reported error blames the second element rather than the missing annotation.
  • Inference succeeds and produces a type nobody expected — any[], Object, impl Trait capturing a lifetime — and the failure appears much later as a method that “should exist” but does not.
  • Checking time explodes on a deeply nested generic expression, because the constraint set grew super-linearly; observed as a single file taking tens of seconds while the rest of the build is fast.

When it helps

  • Removing genuinely redundant annotations — Map<String, List<Order>> m = new HashMap<>() and its equivalents — where the type is stated twice on one line.
  • Writing closures and callbacks, where the parameter types are determined by the function being passed to and writing them adds nothing.
  • Prototyping in an ML-family language, where the ability to write a whole module with no signatures and have the compiler tell you what you built is genuinely useful feedback.
  • Deciding where to spend annotations in an existing codebase: put them on module boundaries first, because that is where they buy both error locality and interface stability.

When it hurts

  • On public APIs, where an inferred type is a contract nobody wrote down and everybody depends on.
  • In numeric code, where the defaulting rule decides a width and the consequence is silent and arithmetic.
  • In large generic expressions, where inference succeeds, produces something enormous, and the error message quotes the whole of it.
  • When it is used to avoid understanding the type. auto, var and := make it possible to write code without ever knowing what a value is, which is fine until the day it matters.

What it costs

Every one of these is paid by something.

  • Wider inference buys fewer annotations and pays in error locality: every annotation removed is a firewall removed, and the compiler must guess further from the mistake to find a contradiction.
  • Use-directed inference buys the ability to write let xs = Vec::new() and let a later push decide the element type, and pays in a body that must be solved as a whole — so a single edit can change types anywhere in it, and incremental checking gets harder.
  • Requiring signatures buys interface stability, separate compilation and localised errors, and pays a per-function annotation cost that falls hardest on small helper functions.
  • A defaulting rule for unconstrained variables buys programs that compile instead of ambiguity errors, and pays in a silent choice — most consequentially numeric width, where the cost is an overflow the reader has no annotation to check against.

What else you could do

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

  • Full Hindley–Milner inference over the whole module, requiring no annotations at all — the ML and Haskell answer, and the subject of [[hindley-milner]].
  • Bidirectional typing with mandatory signatures and no solving: annotations propagate down, everything else is synthesized, and there is never a constraint set. Simple, predictable, and it requires more writing.
  • No inference at all, with concise type syntax to compensate. Go’s original position was close to this, and the language added := rather than a solver — a deliberate choice to keep the mechanism explainable in a paragraph.
  • Inference by a separate tool rather than by the language — TypeScript’s --declaration emit, or Python’s mypy --generate-stubs, which derives signatures once and writes them into the source so that they become explicit and reviewable.

See it for yourself

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

  • Rust: let x = 42; then let () = x; deliberately — the resulting error prints the inferred type. cargo expand and rust-analyzer’s inlay hints show the inferred types inline.
  • C++: template <typename> struct WhatIs; then WhatIs<decltype(x)> _; produces a compile error naming the deduced type exactly. Cruder than an IDE and never wrong.
  • TypeScript: tsc --declaration --emitDeclarationOnly writes out every inferred public signature, which is the fastest way to see what your module is actually promising.
  • Haskell: ghci with :type +v prints the inferred type including its constraints; -Wmissing-signatures reports every top-level binding you left to inference.
  • Go: go vet plus gopls hover; untyped-constant surprises are best seen with %T in a fmt.Printf.
  • Our type-inference stepper at /compilers/types shows constraints being generated and solved one at a time on a small program.

Plausible wrong readings

Stated the way a confident engineer states them.

  • “Inference means the language figures out what I meant.” It finds a type consistent with the rules. If several are consistent it applies a defaulting rule, and defaulting is where the surprises live.
  • “Rust’s let works like C++’s auto.” It does not. auto is fixed by the initializer; Rust solves the whole body, so a later use can change the answer.
  • “Fewer annotations means better inference.” Better inference means the error lands where the mistake is. Those goals are in tension, and mainstream languages chose locality.
  • “Adding an annotation cannot change behaviour.” In any language with defaulting or literal-type widening, it can and does — the width of an integer, the mutability of an array literal, whether a TypeScript const keeps its literal type.
  • “Full inference is too hard to implement.” It is a well-understood algorithm of modest size. What is hard is producing a good error message from it.

Misconceptions

The claim, and what is actually true.

Type inference means the language is dynamically typed underneath.
Inference is a static process that runs before anything executes. The result is a fully typed program; the only thing missing was the writing down.
Whole-program inference is strictly better because you write less.
You write less and you debug worse. Every mainstream language that could have adopted it declined, and the reason given, repeatedly, is error messages.
If the compiler can infer it, writing it is redundant.
On a public boundary the annotation is the contract. Inference derives it from the body, which means the body can change it — the opposite of what a contract is for.
Inference is the same as auto in C++.
auto is one point on a spectrum — solve one declaration from its initializer. Rust solves a body, ML solves a module, and the three behave differently on the same source.

Go deeper

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

overview

Type inference means the compiler works out a type you did not write. let x = 42 gives an integer everywhere. The differences between languages are about how far the compiler is willing to look: C++, C# and Java decide from the initializer alone and never revise; Rust and Swift look at the whole function, so a later line can decide an earlier one; ML and Haskell look at the entire module and need no annotations at all. More reach means less writing and worse error messages, and that trade is the whole story.

practical

Annotate boundaries, infer interiors. Put explicit types on function signatures, public fields and module exports — they are contracts, and they keep errors local by giving the checker a written type to blame. Leave locals, closure parameters and obvious constructions to inference. Be specifically careful with numbers: an unannotated integer literal takes a default width, and a value that does not fit will overflow with no diagnostic pointing at the declaration. And treat annotation deletion as a code change, not a formatting change — if removing one changes the inferred type, you changed the program.

advanced

The reason mainstream languages cannot simply adopt Hindley–Milner is not effort, it is feature interaction. HM’s value is the principal-types property: every typeable expression has a single most-general type, so inference is deterministic and complete. Subtyping destroys that property — x used at both Dog and Animal has no canonical most-general type — and overloading destroys determinism, since + no longer denotes one function. A language with classes and overloaded operators has already given up both before inference is designed. What such languages implement instead is local unification inside a body with mandatory signatures at the edges: enough solving to make closures and generics pleasant, with annotations as firewalls that keep the constraint sets small and the errors attributable. Seen that way, [[hindley-milner]] is not the goal that everyone fell short of — it is a different point in the design space that requires giving up subtyping and ad-hoc overloading to reach.

How much this depends on

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

specJava restricts var to local variables with initializers, explicitly excluding fields, parameters and return types, and the JEP states the reason: keeping the inference local keeps the reader’s reasoning local and keeps the public interface written down. C# imposes the same restriction on var for the same stated reason. This is a language rule, not a solver limitation.
specRust specifies integer-literal fallback to i32 and float fallback to f64 when no other constraint applies, and specifies that overflow panics with debug assertions on and wraps otherwise. Both matter for the annotation-deletion transform above, and neither transfers to C or C++, where signed overflow is undefined behaviour.
implementationTypeScript widens the literal type of a mutable binding to its base type and preserves it for const; this behaviour has been stable since TypeScript 2.1 but is a checker rule rather than a standardised one, and interacts with as const, contextual typing and satisfies in ways that have changed across releases. Verify against the version in the repository rather than from memory.
typicalThe claim that annotations improve error locality is an observation from language-design practice — it is why Rust, Swift, Java and C# all require signatures — rather than a theorem. Counter-examples exist: an over-constrained annotation can move an error *away* from the real mistake by making a caller the first place a contradiction appears.

If you were asked this in an interview

  • What is the difference between C++’s auto and Rust’s let when it comes to inference?
  • Why do Rust and Swift require type annotations on function signatures when their solvers could infer them?
  • You delete : i64 from a local and the program starts overflowing. Explain what happened.
  • Give two reasons mainstream languages avoided whole-program inference. Neither of them is “it is too hard to implement”.

Connections

Computer Architectureinteger-overflowsigned-integers
API Designbackward-compatibilityconsumer-driven-evolution
Backenddtos-and-api-models
Domains that do not exist yet
  • DevOps / Production Engineering — Build times and the cost of a checker that solves over large units
    The compile-time cost of wide inference shows up as CI duration and developer feedback latency, and deciding what that is worth is a build-pipeline question rather than a type-theory one.