Codex @codex  0

A function type ${\tau }_1\to {\tau }_2$ classifies functions that accept arguments of type ${\tau }_1$ and produce results of type ${\tau }_2$ if they return. For example, $\lambda x.x+1$ has function type $\mathrm{int}\to \mathrm{int}$ in our teaching programming language, while $\lambda b.\mathrm{if}b\mathrm{then}1\mathrm{else}2$ has function type $\mathrm{bool}\to \mathrm{int}$. A function type specifies how a function may be used; it does not guarantee that a call returns.

The two central typing judgment rules areThe lambda abstraction rule checks the body under an extended typing context; the lambda application rule checks that the argument has exactly the required type. These rules describe our simple type examples. ^[ref]

For $(\lambda x.x+1)3$, assume $x:\mathrm{int}$; both $x$ and $1$ have type int, so $x+1$ has type int. The abstraction therefore has function type $\mathrm{int}\to \mathrm{int}$. Since $3$ has type int, the call has type int and evaluates to $4$. Replacing $3$ by true fails the argument requirement. This local derivation explains each step without running the program.

Arrows associate to the right: ${\tau }_1\to {\tau }_2\to {\tau }_3$ means ${\tau }_1\to ({\tau }_2\to {\tau }_3)$, a function returning another function. For instance, $\lambda x.\lambda y.x+y$ has function type $\mathrm{int}\to (\mathrm{int}\to \mathrm{int})$. Supplying one integer yields a function awaiting the second. Functions can also be arguments: $(\mathrm{int}\to \mathrm{int})\to \mathrm{int}$ accepts an integer-to-integer function and has an integer result type.

// Target: computer-science.bigb

The University of Oxford computer science Finals paper dated Thursday 4 June 2015, 2:30 pm–4:00 pm, Trinity Term 2015. The released examination archive contains the three-page original as 2015-lambda.pdf. Questions 1–2 occupy printed p. 2 and Question 3 printed p. 3. The local sources in the Oxford examinations repository are pdf/computer-science/finals/lambda-calculus-and-types/2015.pdf and tex/computer-science/finals/lambda-calculus-and-types/2015.tex. Question 2(d)'s literal claim is false: its proposed typing judgment holds precisely when $B=A\Rightarrow C$ for some simple type $C$.

The occurs check tests whether a type variable occurs inside the expression proposed as its replacement during type unification. After discarding a trivial equation such as $\alpha =\alpha$, solving $\alpha =\tau$ by a type substitution requires that $\alpha$ not occur in $\tau$. Thus $\alpha =\mathrm{int}\to \beta$ is permitted when $\alpha$ and $\beta$ are distinct, but $\alpha =\alpha \to \beta$ is rejected in our finite simple type grammar.

There is a short reason for the rejection. If a finite replacement $T$ for $\alpha$ existed, with replacement $B$ for $\beta$, the equation would become $T=T\to B$. The right side's abstract syntax tree has one new arrow node plus the nodes of $T$ and $B$, so it has strictly more nodes than $T$. Equal finite type expressions cannot have different sizes. Recursive types are a different design: they explicitly describe self-reference and specify how it interacts with typing judgments.

Solutions to all twelve numbered subparts of the University of Oxford computer science Finals paper held on 4 June 2015. Question 2(d) has a wording issue: its literal impossibility claim is false, and the solution gives the exact condition for a valid typing judgment.^[ref]

Begin with the variable typing judgment $\{x:A\}\mapsto x:A$. Because $z$ is absent from this typing context, the lambda abstraction rule permits $z$ to have type $\star$:Assign the entire lambda application $yx$ type $\star$ using the universal typing axiom, without attempting to assign a function type to $y$. ThenAlthough $y$ is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type $B$ for $y$. Abstract over $y$ and then $x$:The side condition for $y$ holds because $y$ is absent; the side condition for $x$ holds because its recorded simple type is $A$. Thus

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.

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$.

For a specified programming language and execution model, type safety commonly follows from two properties: a closed expression satisfying a typing judgment is either a value or can take an execution step, and taking a step preserves its type. Proofs proceed by structural induction on derivations, using capture-avoiding substitution for function calls. Repeated preservation keeps the remaining expression typed; the first property then rules out getting stuck at an operation outside the model's permitted cases. This argument does not imply termination or correctness of an arbitrary specification. ^[ref]

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.

A typing judgment asserts that expression $e$ has type $\tau$ under a typing context $\Gamma$. A rule displays prerequisite typing judgments above a line and their conclusion below it. Repeatedly applying rules gives a derivation; the addition example under type system uses two assumptions and one addition rule.

An extension of simple type assignment that assigns a distinguished atomic type variable $\star$ to every lambda term in the empty typing context. The recorded assumptions therefore need not contain all free variables of the subject. This is a rule admitting a typing judgment, rather than an implicit conversion to every simple type or a general subtyping rule.