Follow local rules and see why a checker can reject an expression that happens not to fail on one run.
By the end: distinguish a derivation from execution and interpret progress and preservation.
A context records assumptions
A typing judgment reads: under context Gamma, expression e has type T. Gamma records the types of names currently in scope. Looking up a name uses that context; the checker does not execute the variable to discover a value. A missing name is a separate error from an incompatible type.
For integer addition, both operands must have type Int, and the result has type Int. These are premises and a conclusion. Checking a compound expression means establishing its premises recursively. A derivation records why the conclusion follows from the language’s rules.
Build a derivation from the leaves
A judgment states a claim together with the assumptions under which it holds. In the notation Γ ⊢ e : T, Γ is the context, e is the expression, and T is its type. The symbol ⊢ reads 'establishes'; the colon reads 'has type'. Gamma is simply the name of the context, not a calculation. Thus a context containing x : Int can establish x : Int by looking up x. The claim says nothing about x's particular integer value, and it does not require running a function to find that value.
A typing rule describes how several judgments justify another judgment. The required judgments are called premises, and the justified judgment is the conclusion. Written as a fraction-like display, a rule places premises above a horizontal line and its conclusion below. The line means 'if these premises hold, this conclusion follows', not division. An integer literal needs no smaller expression checked before it has type Int. Such a rule forms a leaf in a derivation, a tree recording how rules combine to establish the type of a larger expression.
The outer addition consumes a completed inner derivation
Read upward to find required premises and downward to justify conclusions. The rule lines represent implication, not arithmetic division.
Work through the paper expression (2 + 3) + 4. These parentheses describe an authored addition tree with the inner addition as the outer addition's left child; they are not input to a free-text parser. First, the literal rules give 2, 3, and 4 type Int. The inner addition consumes the first two facts and establishes that 2 + 3 has type Int. The outer addition then consumes that result and the fact about 4. Its conclusion is that the whole expression has type Int, without calculating the integer 9.
Now replace the inner 3 with true. The boolean literal rule establishes Bool for true. It does not establish Int. The inner addition still requires two Int premises, so its second premise fails. Without a type for that addition under the required rule, the outer addition cannot obtain its left premise either. The failure propagates through the justification tree. There is no rule saying that a larger addition can overlook an invalid child because its other operand is an integer. Local requirements matter because larger conclusions depend on their successful completion.
Scope determines which assumption a variable lookup finds. Scope is the part of an expression where a binding supplies a name's meaning. A binding associates a name with a parameter or value. In the paper function fun x -> (fun x -> x + 1), the inner parameter introduces a new x that hides the outer x within its body. The addition constrains the inner x to Int. It says nothing about the unused outer parameter. The context used inside the addition contains the nearer binding, rather than combining every assumption with the spelling x.
The inner occurrence belongs to the nearer parameter
Binding identity follows lexical scope, not spelling alone. Only the inner parameter supplies the addition's variable premise.
An expression is closed when it has no variable occurrence that lacks an enclosing binding. The whole function above is closed, although looking at its body in isolation requires a context for x. The paper expression x + 1 by itself is open, meaning it has such an unbound occurrence. Under an assumed context x : Int, it has a derivation. From the empty context it does not. The lab starts each preset with an empty context, so an unknown name cannot acquire a type merely because a plausible assumption would make the expression work.
Check all relevant branches
Our conditional rule requires a Bool guard and equal types for the two branches. An if with Int and Bool results is rejected; this language has no implicit Int-or-Bool union. That is a language-design choice rather than a universal law about conditionals.
Both branches are checked even when a literal guard chooses only one at runtime. The Untaken bad branch preset evaluates its else branch to 4, but its other branch contains true + 1 and fails static checking. A rejection means the rules cannot establish the requested guarantee, not necessarily that every execution fails.
Keep branch requirements separate from branch selection
A conditional has three immediate children: the guard, the then branch, and the else branch. Its typing rule has a different obligation for the guard than for the results. The guard must have type Bool. Both branches must have one common result type, and that common type becomes the conditional's type. The guard's type is not the result type. For the paper expression if true then 2 else 5, the guard supplies Bool while the branches each supply Int. The complete expression therefore has type Int, even though it contains a boolean.
Consider if true then 1 else false. The guard meets its Bool requirement. The then branch has type Int, and the else branch has type Bool. Those branch results cannot supply one common type under this language's equality rule. The literal true does not remove the else branch from the typing obligation. A language with a type describing alternatives could make a different choice, but this core has no such conditional result rule. Rejection here reports that the expression does not satisfy these specific rules, rather than that conditionals can never return different kinds of values anywhere.
A valid guard cannot replace branch agreement
Paper conditional
Guard premise
Branch types
Conclusion
if true then 2 else 5
Bool, passes
Int and Int
Int
if true then 1 else false
Bool, passes
Int and Bool
No common result type
if 1 then 2 else 5
Int, fails
Not enough to repair guard
Rejected
The guard and branches supply different premises. A true guard satisfies only the guard premise, not the common-result requirement.
There are two distinct ways a branch can prevent a derivation. A branch may have a valid type that disagrees with the other branch, as in the preceding example. Alternatively, a branch may fail its own internal rule, as true + 1 does. In if false then (true + 1) else 4, the then branch cannot establish an addition result in the first place. Changing the other branch from 4 to another integer would not repair that failure. The repair must address the missing operand premise or change the expression's operation.
Static checking asks what the expression's form permits the rules to establish. Runtime evaluation asks what happens when the expression executes. For a conditional, evaluation first obtains the guard's boolean value and then evaluates only the selected branch. This is why a hypothetical independent evaluation of the fixed false-guard expression can return 4 without encountering the bad addition. The UI does not perform that experiment on a rejected term. The evaluation path is a semantic explanation of the distinction, not an extra Run rejected program control that the lab provides.
Checking both branches makes the guarantee independent of which boolean value the guard produces. This matters when the guard is not a literal. Under a paper context flag : Bool, if flag then 2 else 5 has an Int result whichever permitted flag value is supplied. Its derivation does not need to know that value. Replacing 5 with false destroys that common result type. The checker uses a uniform conditional rule even when a particular literal would allow a more specialized argument. That conservative choice accepts fewer expressions than an analysis that reasons about each guard's possible values.
One fixed conditional has different checking and evaluation paths
Static obligation
if false then true + 1 else 4
Guard
Bool requirement passes
Then branch
Bool operand fails Int requirement
Whole term
Rejected
Hypothetical evaluation
Same authored tree
Guard
false selects else
Then branch
Not executed
Else branch
Returns 4
Independent evaluation here is a paper explanation. The actual UI does not run this rejected term to obtain its result.
The same separation appears in ordinary functions. An Int → Int signature says that an integer argument connects to an integer result under the language's function rules. It does not say that the result equals the argument plus one. A body that adds two instead can satisfy the same signature. Function types and conditional rules describe selected structural properties, not all arithmetic relationships. Recognizing the exact property avoids two opposite mistakes: dismissing a useful type because it is incomplete, and treating its successful derivation as evidence for a specification it never expressed.
Inspect the rules and their result
Inspect the expression, constraints, and result
(3 + 4)
Static inference
Accepted: Int
Int
Separate evaluation
7
A value is not the evidence used to infer the type.
Generated equality
Reason
Int = Int
Left addition operand
Int = Int
Right addition operand
Complete visited-expression and solver trace
Visited expression
Rule
Recorded type
3
int
Int
4
int
Int
(3 + 4)
add
Int
Step
Solver action
Bindings after step
0
Start these constraints
None
1
Already equal: Int
None
2
Start these constraints
None
3
Already equal: Int
None
On failure, visited-expression types and partial bindings are diagnostic state, not a solution. Only successfully completed visits appear.
Read the integer-addition rule
Gamma is the context of name assumptions. Premises are above the line; the conclusion is below. x and y here stand for expressions.
Presets replace the entire authored expression tree and recompute from an empty environment. This is teaching syntax, not JavaScript or a free-text parser. The engine checks both conditional branches and uses pure let polymorphism. Trace names t0, t1, etc. are local unknowns; the final signature renames remaining unknowns to a, b, etc. Rejected examples are not automatically evaluated.
Expression
Required premise
Outcome
3 + 4
Both Int
Int
3 + true
Right operand Int
Fails
if true then 1 else false
Equal branch types
Fails
The checker applies rules, not just the branch chosen on one run.
Use the presets to locate the failed premise
Select Integer addition in the explorer. Its authored tree represents 3 + 4. The static panel accepts it as Int, while the separate evaluation panel reports 7. These are different outputs with different justifications. The first follows the integer-literal and addition typing rules; the second follows the interpreter's arithmetic. The generated equality rows require each operand type to equal Int. Since both already are Int, those requirements add no new type information. Opening the trace shows the visits and checks without making the runtime value an input to static inference.
Switch to Wrong operand. The preset replaces the entire tree with 3 + true and starts inference again from an empty context. The first operand meets the Int requirement. The second has Bool, so its equality with Int fails. The static panel rejects the expression, and the runtime panel says it was not evaluated. This is not a record of the interpreter trying addition and throwing an error. It is evidence that a static premise failed before the UI allowed evaluation. The trace's partial progress cannot justify accepting the whole expression.
Changing one literal changes the addition's second premise
Existing preset
Left requirement
Right requirement
UI evaluation
Integer addition
Int = Int
Int = Int
7
Wrong operand
Int = Int
Bool = Int, fails
Not evaluated
The equalities are static obligations. The accepted value is computed separately, and rejection prevents automatic evaluation in the interface.
Now select Untaken bad branch. The guard false meets its Bool requirement, after which the checker visits the then branch and encounters true + 1. The left addition operand immediately requires Bool to equal Int. That conflict prevents a successful type for the branch. Because inference stops at failure, the generated equality list need not contain a completed check of the else branch or a final branch agreement check. A short diagnostic trace does not mean the rule exempts the unvisited parts; it means an earlier required premise already prevented the derivation.
Select Different branch types to isolate the other failure. Its tree represents if true then 1 else false. Neither branch contains a malformed operation, and the guard is valid. The branch agreement requirement itself fails because Int and Bool differ. Contrast this with the untaken-error preset while keeping both explanations in view. One fails within a branch; the other fails when combining two valid branch types. Distinguishing those locations tells you which rule to inspect. Merely saying that both examples contain Int and Bool would miss why one mixture is allowed in guards but not in results.
The explorer records equalities because it uses inference, the process of finding a type rather than requiring every intermediate type in advance. Equality here means two type descriptions must denote the same type. A fresh unknown is a temporary name for a type not yet determined; later lessons explain how the solver resolves these names. The simple presets already give their literals fixed types, so their failure does not depend on a complicated unknown. Bool cannot equal Int under these constructors, regardless of which temporary names appear in a trace elsewhere.
A failed branch body differs from disagreeing branch results
Existing preset
Guard
First decisive failure
Later obligation
Untaken bad branch
Bool = Bool
Bool = Int inside addition
Branch agreement not reached
Different branch types
Bool = Bool
Int = Bool between branches
Both literal branches already visited
The first conflict determines where this implementation stops. Requirements absent from a failed trace are not thereby waived.
Read the acceptance status together with the trace, not instead of it. Successful child visits explain some premises, while the final result states whether the entire check completed. After failure, the engine can retain types and bindings reached before the conflict. A binding in this diagnostic state is an intermediate association for a type unknown, not a runtime assignment and not a solution to every requirement. Each preset recomputes independently, so a later successful example does not reuse a rejected example's assumptions. This separation keeps a partial explanation from being mistaken for a complete derivation.
What soundness would say
Progress says a closed well-typed term is already a value or can take a permitted evaluation step. Preservation says a permitted step preserves typing. Together they rule out the specified stuck states when the language and semantics satisfy the corresponding theorems.
They do not automatically prove business correctness, useful output, secrecy, absence of every exception, or termination in an arbitrary language. The cited formal development proves properties of its defined calculus. Our tests inspect this implementation on bounded cases; they are not a machine-checked soundness proof.
Read progress and preservation as conditional claims
A value is a completed result according to an evaluation system's rules. An evaluation step is one permitted transition toward such a result. A stuck expression is neither a completed value nor able to take an allowed step. For example, applying an integer as if it were a function has no successful function-application meaning in this core. The interpreter reports an error if asked to perform that operation, while the type rules reject it first. To discuss soundness precisely, specify the unwanted states and the evaluation rules instead of treating every reported failure as the same event.
Progress addresses the next step. In the formal calculus cited here, a closed expression with a valid typing derivation is either already a value or has a permitted evaluation step. The closed condition matters. A context might give an open expression x + 1 a type, but execution without a value for x cannot perform the lookup. Progress does not say that any expression with convenient imagined assumptions can execute by itself. It applies only after the theorem's premises hold, including its requirement about free names and its particular language definition.
Changing the expression can leave its type unchanged
Paper state
Typing justification
Type
(2 + 3) + 4
Inner Int addition supplies outer left operand
Int
5 + 4
Both literal operands are Int
Int
9
Integer literal rule
Int
This paper reduction illustrates preservation for addition. It is not an emitted interpreter trace or a proof covering the implementation.
Preservation addresses what happens after a step. If an expression has type T and makes a permitted evaluation step, the resulting expression still has type T under the theorem's assumptions. Consider the paper sequence (2 + 3) + 4, then 5 + 4, then 9. Each expression has type Int. Intermediate values change, but the result type does not. This is a schematic arithmetic illustration of the property, not a trace emitted by the lesson's evaluator. The cited calculus needs its own rules and proof; adding integers requires corresponding reasoning rather than automatic inheritance of a theorem.
Together these properties support a repeated argument. Start with a closed well-typed expression. Progress supplies either completion or a step. If it steps, preservation supplies the type needed to apply progress again. Repeating this argument rules out reaching a stuck state covered by those semantics. It does not by itself establish that there will be only finitely many steps. A system might continue stepping forever without getting stuck. A termination argument would need an additional property. The present implementation does not claim that progress and preservation have been proved for its complete engine.
Implementation limits add another distinction. This engine accepts expression trees only within its node and depth bounds, and its interpreter permits 512 evaluation visits before reporting a limit. It also checks safe-integer addition. A limit message describes an implementation budget or numeric representation boundary, not an equation proving Int inconsistent with Bool. Formal arithmetic rules can omit such budgets, but then their theorem says nothing about those particular failure messages. To connect a formal theorem to running software, you must account for the software's extra behaviors as well as the idealized expression rules.
Different failure claims require different evidence
Question
Relevant evidence
Insufficient substitute
Can a closed typed term take a step or finish?
Progress theorem for its calculus
One successful run
Does a permitted step retain the type?
Preservation theorem for its calculus
Matching one output value
Will this implementation stay within its budget?
Evaluation resource analysis
An Int result type
Does the function add exactly one?
Arithmetic specification and verification
Int → Int signature alone
Progress and preservation concern the specified evaluation rules. Budget exhaustion and incorrect intended arithmetic require separate implementation or specification arguments.
Finally, an error in intended behavior need not be a stuck state at all. A function intended to increment an integer might return that integer plus two. It can finish normally with the promised result type and still violate the application's requirement. Conversely, a rejected literal-guard conditional may have a successful single evaluation path without meeting the static rule. These cases distinguish a type derivation, an execution result, and a functional specification. Each provides evidence for a different claim, so neither one successful run nor one type signature can substitute for all the reasoning required by the others.
Exercises
A wrong but well-typed function
A function intended to add one instead returns its integer argument plus two. Would an Int -> Int type alone detect the mistake?
Hint
The result is still an integer for integer input.
Worked answer
Implementation
Type
Meets add-one specification?
x + 1
Int -> Int
Yes
x + 2
Int -> Int
No
Type correctness and functional correctness are different claims.
No. Both implementations satisfy the input/output type. The intended arithmetic relation needs a stronger specification, tests, or a proof. A type can be useful without representing the entire requirement.
An untaken error
Why does if false then (true + 1) else 4 fail in this language? What does its runtime evaluator do if called independently?
Hint
Static checking examines both branches; evaluation follows the guard.
Worked answer
Process
Examined parts
Result
Static rules
Both branches
Reject
Evaluation of this fixed term
Guard and else branch
4
One successful path does not establish a derivation for the whole expression.
The then branch violates the Int operand rule. Static checking rejects the expression. The independent evaluator follows false to the else branch and returns 4 without executing the bad addition. Our lesson does not run rejected terms automatically; the distinction explains conservative checking.
Sources and further reading
Selected reference passages support the definitions and algorithms below. The examples, explanations, and implementations are original. Terminology and assumptions are stated within each lesson; source review is not an independent audit of this course. Optional links are not runtime dependencies.
Selected contexts, function application, and typing-rule explanations. The formal chapter defines its own calculus; our additional integers, pairs, and let inference are not automatically covered by its theorems.
Selected progress, preservation, and substitution statements. We do not claim to have independently checked the entire proof development or proved our implementation sound.