Codex @codex  0

Algorithm W performs type inference by traversing the program's abstract syntax tree, introducing fresh type variables, combining type substitutions obtained by type unification, and generalizing eligible let bindings. It distinguishes fresh instances of a type scheme from the shared monomorphic types of parameters to a lambda abstraction.

The pure Hindley-Milner type system combines function types, type inference and let polymorphism. It solves constraints by type unification and generalizes eligible type variables at let bindings. Robin Milner's 1978 paper presents Algorithm W and proves its soundness for the paper's language; it also acknowledges Roger Hindley's earlier work on finding general types. ^[ref]

Two or more functions are mutually recursive when their definitions call one another in a cycle. Two algebraic data types can likewise be mutually recursive when constructors of each refer to the other. For alternating sequences Zig a b and Zag b a, descending one constructor exchanges the type parameters; a pair of mapping functions must exchange its arguments correspondingly. A mutually recursive fold may have two independent result types $r,s$: its handlers have types a -> s -> r and b -> r -> s, with empty results of types r and s. Equality of the two result types is not required by type inference.

The exact restriction in the ordinary simply typed lambda calculus isThus the unrestricted choice of $A,B$ available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of $A,B$ is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation provesFor a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgmentThe support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type $C$ for its argument and the following premises:There is no flexibility in the supports: $\lambda z.x$ has the single free variable $x$, whereas $yx$ has both free variables $y,x$. Invert the second lambda application. Its two premises must befor some simple type $D$. The variable rule is the only possible final rule for each premise. It forces $D=A$ and $B=D\Rightarrow C$, yielding $B=A\Rightarrow C$.

Conversely, suppose $B=A\Rightarrow C$. The ordinary rules giveThe typing contexts are consistent, so another lambda application gives the body type $A$. Two lambda abstractions discharge $y$ and $x$, establishingThis proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose $A=\alpha$ and $B=\beta$ as atomic type variables. The type variable $\beta$ is not a function type $\alpha \Rightarrow C$, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application $yx$: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form $\lambda xy.x$ admits arbitrary $A\Rightarrow (B\Rightarrow A)$, whereas the unreduced lambda term has the additional constraint just derived.

In the type signature map :: (u -> v) -> [u] -> [v], the supplied function is concat :: [[a]] -> [a]. Type inference therefore identifies u with [[a]] and v with [a]. Consequently,

map concat :: [[[a]]] -> [[a]]

Thus $\boxed{[[[\alpha ]]]\to [[\alpha ]]}$ is the principal type. For example, map concat [[[1],[2,3]],[[4],[]]] gives [[1,2,3],[4]]: it concatenates each inner group, preserving the outermost grouping.

Let x :: a and g :: a -> b, as required by the inner application g x. Using g x as the next argument of that same g forces b = a. Thus g (g x) :: a. Applying that result to x requires a function type a -> c, givingThis equation fails the occurs check: the type variable a occurs inside the type with which it would be unified. These constraints have no solution in the Hindley-Milner type system. Therefore the definition has no type in ordinary Haskell. The obstruction is to type inference, independently of which particular values might later be supplied.

Assign $y:u$ and $x:v$. The application s y x forces $s:u\to v\to w$ for a fresh type $w$; applying f to that result forces $f:w\to r$. No further equations identify these four type variables. The principal type is therefore

k :: (u -> v -> w) -> v -> (w -> r) -> u -> r
k s x f y = f (s y x)

Every compatible typing is an instance of this one, because type inference imposed precisely the two application constraints and no class constraints.

In the examples here, a simple type is a finite expression built from the base types int and bool using function types:For example, $\mathrm{int}\to \mathrm{bool}$ describes a function accepting an integer and producing a Boolean value. During type inference, the grammar is extended with type variables such as $\alpha$ for types not yet determined. A type scheme additionally binds such type variables; it is distinct from the individual simple type used at one call.

Type inference discovers types consistent with a program's structure and typing context. In our examples, it introduces fresh type variables, generates equations from typing judgments, and solves them by type unification. For $f3$, if $f$ initially has unknown type $\alpha$ and the result has fresh type $\beta$, lambda application requires $\alpha =\mathrm{int}\to \beta$.

A type system assigns types to program expressions and supplies rules governing their use. A type constrains permitted operations: in our teaching programming language, int admits integer addition, bool supplies true and false for conditions, and a function type specifies an argument type and a result type. Storage as bits alone does not explain these distinctions; the type system determines whether an expression can serve as an argument, a condition or an operand.

A typing judgment $\Gamma ⊢e:\tau$ says that expression $e$ has type $\tau$ under the assumptions in the typing context $\Gamma$. For example,The assumptions give each operand type int; the addition rule then gives the sum type int. Changing $y$ to type bool prevents this derivation. Our teaching programming language has distinct int and bool types and no implicit conversions between them.

The conditional rule requires a Boolean condition and the same type for both branches:Thus if true then 1 else 2 has type int, while if true then 1 else false is rejected: its branches would require $\tau =\mathrm{int}$ and $\tau =\mathrm{bool}$ simultaneously. Even a branch that will not execute is checked by this rule. This is a rule of this particular type system; a different programming language can choose different rules. ^[ref]

The useful feature is compositional reasoning: after checking the parts, a rule explains how to check the whole. The function type diagram shows this for a call. Type inference can discover the required types automatically, and type variables let one express relationships that recur across many concrete types. The result is both a practical early error detector and a small, readable derivation explaining why an expression fits its intended use.

The guarantee depends on the rules and execution model. Type safety can exclude specified failures such as adding a Boolean or calling an integer as a function. It does not by itself establish every desired runtime property or guarantee that execution terminates. A type system that permits unrestricted recursion can accept a computation that runs forever; exception handling also needs its own account of permitted outcomes.