Type checking is a derivation over syntax

Prerequisites: Abstract syntax trees, functions, booleans, and integers.

Learning objectives

• Use a typing environment to derive expression types.
• Reject incompatible branches under a stated language rule.
• Explain the scope and limits of progress and preservation.

A type judgment records assumptions

Write Γ ⊢ e : T to mean that expression e has type T under environment Γ. The environment records types assigned to variables. This is a mathematical judgment about a particular language, not a claim that every language uses the same rules.

Define a small language with integers, booleans, variables, integer addition, and conditional expressions. Integer literals have type Int, boolean literals have type Bool, and a variable receives the type recorded in Γ. Addition requires two Int operands and returns Int. A conditional requires a Bool condition and two branches of the same type, then has that shared branch type.

Derive a result from the leaves upward

Let Γ contain x:Int and ready:Bool. For the expression if ready then x+1 else 0, lookup gives ready:Bool and x:Int. Literal 1 has type Int, so x+1 has type Int. Literal 0 also has type Int. The condition and branch premises are satisfied, so the complete expression has type Int.

Now replace the else branch with false. The branches have types Int and Bool. Under the deliberately simple same-branch-type rule, the expression is rejected. Another language could define a union type or a coercion, but that would be a different specified rule, not an exception invented by the checker when convenient.

Function types extend the idea. A value of type Int→Bool accepts an Int argument and produces a Bool result when it returns according to the language semantics. Applying it to a Bool argument fails the application rule unless an explicit conversion or other rule permits it.

Safety theorems require a defined machine

Progress says, roughly, that a well-typed closed expression is already a value or can take a permitted evaluation step. Preservation says that taking such a step preserves its type. Together, under their formal assumptions, these results exclude the particular stuck states modeled by the language. They do not establish every property users might mean by “safe.”

A well-typed program can still loop forever, produce the wrong business answer, exhaust resources, or perform authorized but undesirable effects. Integer overflow, exceptions, null values, mutation, and concurrency require explicit semantic and typing treatment. Omitting them from a toy language does not prove them harmless in a production one.

A practical checker should report the failed rule with source context, such as an expected Int and an actual Bool at a specific operand. This makes errors explainable as missing premises. Type inference may discover some annotations automatically, but it still operates under rules and does not eliminate the need to define the language’s meaning.

Primary reading

• Software Foundations: Programming Language Foundations (University of Pennsylvania).

Practice problem

Assume Γ contains flag:Bool, n:Int, and predicate:Int→Bool. Derive the type of predicate(n+2). Decide whether if flag then predicate(n) else 0 is accepted under the same-branch-type rule. Explain one important program defect that successful type checking would not rule out.

Worked solution

The variable n has type Int and literal two has type Int, so n+2 has type Int by the addition rule. Predicate expects an Int and returns Bool, so predicate(n+2) has type Bool. In the conditional, flag satisfies the Bool condition requirement, but predicate(n) has type Bool while zero has type Int. The branch types disagree, so the stated rule rejects the expression. A successful check would still not prove the application computes the intended answer. For example, a function intended to test whether an integer is positive could return false for every input while remaining correctly typed as Int→Bool. Termination and resource usage are also separate properties unless the language’s rules explicitly address them.

Check your understanding

What does Γ contain in the presented typing judgment?

• The CPU’s cache replacement policy.
• Assumptions about variable types.
• Only runtime numeric values.
• Every possible program output.

Explanation

The typing environment supplies the premises used for variable references.

What does preservation establish in the stated formal setting?

• Every program terminates quickly.
• A permitted evaluation step maintains the expression’s type.
• Every business requirement is satisfied.
• All exceptions are impossible in every language.

Explanation

Preservation is a specific relation between typing and evaluation, not a universal correctness certificate.

Primary reading

• Software Foundations: Programming Language Foundations: University of Pennsylvania

Open the study and save your work →