Combine environments, fresh variables, local requirements, and substitutions in a working engine.
By the end: trace the supported inference process without treating it as a parser or a production compiler.
The explorer starts from authored expression trees, not parsed user source. It visits expressions, creates unknowns, instantiates names, and solves constraints. Once requirements succeed, it applies the accumulated substitution to the result. The displayed term is a readable rendering of that same tree.
The core supports bounded integers, booleans, names, functions, application, addition, conditionals, pairs, and nonrecursive let. It has no mutable references, subtyping, unions, overloaded operators, recursive definitions, exceptions, or effect inference. Later labs isolate some of those ideas without pretending they are features of this engine.
Inference combines several operations that must remain distinct. An environment maps each in-scope program name to its type information. A fresh type unknown marks a question not yet answered. An expression rule supplies equations, and unification updates what those unknowns mean. The engine performs these operations while visiting an authored expression tree. The readable notation below describes paper examples unless a preset is named explicitly. There is no textbox that parses these terms into programs. A displayed arrow is a type relationship, not a generated runtime instruction or a record of an observed call.
Take the paper term fun f -> fun x -> f(x + 1). Give f unknown a and x unknown b. The integer literal 1 has type Int without any guess. Addition requires b = Int and Int = Int, then has result Int. Applying f to that result introduces fresh output c and requires a = Fn<Int, c>. The inner function therefore has shape Fn<Int, c>, and the complete outer function has shape Fn<Fn<Int, c>, Fn<Int, c>>. No rule has required c to be Int, so specializing that output would lose permitted uses.
| Expression or binding | Type before solving | Requirement | Resolved type |
|---|---|---|---|
| Parameter f | a | None yet | Fn<Int, c> |
| Parameter x | b | b = Int from addition | Int |
| Literal 1 | Int | Int = Int from addition | Int |
| x + 1 | Int | Both operands Int | Int |
| f(x + 1) | c | a = Fn<Int, c> | c |
| Complete function | Fn<a, Fn<b, c>> | Apply accumulated replacements | Fn<Fn<Int, c>, Fn<Int, c>> |
This worked type means that the outer function accepts an integer-input function and returns another integer-input function with the same output type. It does not require f to return its input or to add anything. On a separate paper instantiation, f could be fun z -> true, whose input can be constrained to Int while its output is Bool. The complete term would then return an Int-to-Bool function. The addition constrains the argument passed to f, not the value that f returns. Keeping the outermost input and output distinct prevents that common mistaken inference.
A derivation explains a compound conclusion using smaller premises. Here the lookup premise for x uses the environment assumption x has type b. The addition premise narrows b to Int. The application premise combines the known argument type Int with the still unknown output c. Finally, each function rule removes its parameter from the local context and records that parameter's type in a function input position. These are logical dependencies even if the implementation records completed visits in a particular order. A result table is easier to read when each entry has an identifiable premise behind it.
A small change to the body creates a different dependency. For fun f -> fun x -> f(x) + 1, the result of f(x), rather than x itself, participates in addition. Start again with fresh a for f, b for x, and c for the call result. Application requires a = Fn<b, c>. Addition then requires c = Int, giving a = Fn<b, Int>. The whole type is Fn<Fn<b, Int>, Fn<b, Int>>. The two paper terms have similar spelling, yet their equations constrain opposite sides of the function argument's input/output relationship.
| Premise | fun f -> fun x -> f(x + 1) | fun f -> fun x -> f(x) + 1 |
|---|---|---|
| Initial bindings | f : a; x : b | f : a; x : b |
| Application result | c | c |
| Application equation | a = Fn<Int, c> | a = Fn<b, c> |
| Addition constrains | b = Int | c = Int |
| Final shape | Fn<Fn<Int, c>, Fn<Int, c>> | Fn<Fn<b, Int>, Fn<b, Int>> |
The authored tree determines that difference before inference begins. In the first term, the application node has an addition as its argument child. In the second, the addition node has an application as its left operand. The engine does not infer parentheses or repair an ambiguous source string. This boundary matters when explaining a diagnosis: changing the expression structure changes which rule produces an obligation. It is not merely a different way to display the same constraint. The following comparison makes both trees' type consequences visible together without claiming either is a selectable preset.
The identity function has principal shape a -> a. Int -> Int and Bool -> Bool are instances; Int -> Bool is not. A principal type is most general within the stated language and typing assumptions. Adding advanced features can require annotations or change whether principal types exist.
Trace variables t0, t1, and so on identify unknowns within one run. The final signature renames remaining unknowns to a, b, and so on in first-occurrence order. This is display normalization, not a new substitution that changes the program. A different fresh-variable name does not change the inferred type relationship.
A principal type describes the most general relationship allowed by the expression rules and environment. Its unknowns must be replaced consistently when selecting an instance. For the paper function fun x -> fun y -> x, inference introduces independent unknowns for x and y and returns the type of x from the body. Its final shape is a -> (b -> a). The two a positions are linked, while b is independent. Neither the function's name nor the number of parameters establishes this relationship. It follows from which binding the final occurrence actually looks up.
For that shape, choosing a := Int and b := Bool produces Int -> (Bool -> Int). Choosing a := Bool and b := Int produces Bool -> (Int -> Bool). Int -> (Bool -> Bool) is not an instance because the same a cannot be Int at the outer input and Bool at the final output. These checks concern static type instances, not sample evaluations. Even if some unrelated function prints similar values, that observation cannot replace the repeated-variable obligation. The type describes a consistent classification under the rules, not a table of observed input/output pairs.
Trace names such as t0 and t1 identify fresh unknowns in one inference run. Final names such as a and b make a signature easier to compare by assigning names in first-occurrence order. Suppose an internal type is Fn<t7, Pair<t9, t7>>. Its normalized display is a -> Pair<b, a>. Both occurrences of t7 must become a, and t9 becomes b. Renaming only one occurrence would invent independence. Renaming both t7 and t9 to a would invent equality. Display normalization must preserve the occurrence pattern even though the letters themselves carry no domain meaning.
Lexical scope decides which binding a use denotes. In the paper term fun x -> fun x -> x + 1, entering the inner function introduces a new binding with the same spelling. Its body looks up the inner x, so addition constrains that binding to Int. The outer x remains unused and unconstrained. The resulting shape is a -> (Int -> Int). If a checker stored one global type for the spelling x, it would incorrectly specialize the outer input too. A copied, extended environment keeps the two scopes separate while retaining surrounding assumptions for other names.
There is another distinction between an unknown and a type scheme. A scheme records which variables may receive fresh independent replacements at each use of a binding. A lambda parameter here has no such quantified variables; all its uses share one monotype. A pure let binding can quantify variables independent of its surrounding environment. The next chapter derives that rule in detail. For this chapter's signatures, remember that an arbitrary unknown is not automatically permission to give every occurrence a fresh unrelated type. Independence requires a binding rule, not merely a convenient new letter in a trace.
In particular, a captured outer value must keep its type across inner uses. The Captured outer variable preset makes a function whose inner let-bound function ignores its own argument and returns the surrounding x. Different call arguments can have different types, but the returned components both retain x's type. The displayed shape a -> Pair<a, a> expresses that dependency. A proposed a -> Pair<b, c> would forget that both results come from the same environmental assumption. This example separates independence of call inputs from independence of captured outputs before the live comparison below.
(3 + 4)Accepted: Int
Int7
A value is not the evidence used to infer the type.
| Generated equality | Reason |
|---|---|
| Int = Int | Left addition operand |
| Int = Int | Right addition operand |
| 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.
| Phase | Output |
|---|---|
| Visit expression | Unknowns and requirements |
| Unify | Substitution or failure |
| Apply substitution | Inferred type |
| Evaluate accepted example | Value or interpreter resource limit |
Select Increment application in the explorer above. The tree applies fun x -> x + 1 to 4. The parameter begins as t0; the addition requires t0 = Int and Int = Int. Application introduces t1 for its result and requires Fn<t0, Int> = Fn<Int, t1>. The accumulated substitution already makes t0 equal Int, so decomposition leaves Int = Int and Int = t1. The final signature is Int. The separate evaluation panel returns 5, but that number was not an input to any of these type equations or replacements.
Open Complete visited-expression and solver trace to connect each generated requirement to its reason. The generated-equality table preserves the equation as it was supplied, while solver frames resolve it using accumulated replacements. A t0 still visible in an original equation need not mean t0 remains unknown at the end. On a successful run, recorded expression types are also displayed after applying the final substitution. These views answer different questions: which requirement arose, how it was solved, and what the completed run knows. Treating all three as snapshots from one instant would create apparent contradictions.
| Requirement or result | Recorded form | After known replacements |
|---|---|---|
| Left addition operand | t0 = Int | Bind t0 := Int |
| Right addition operand | Int = Int | Already equal |
| Application | Fn<t0, Int> = Fn<Int, t1> | Fn<Int, Int> = Fn<Int, t1> |
| Application input | Int = Int | Already equal |
| Application output | Int = t1 | Bind t1 := Int |
| Final signature | t1 | Int |
Compare Integer addition with Wrong operand. The accepted tree generates Int requirements for both operands and evaluates to 7. The rejected tree supplies Bool for the right operand, so the Right addition operand requirement reaches Bool = Int. The interface then reports that it did not evaluate the rejected example. It does not try a conversion, ask the runtime which type true really has, or use a successful left operand to approve the entire addition. This single controlled contrast keeps the outer expression form constant while changing the fact that violates its local rule.
Different branch types tests another rule. Its literal true guard satisfies Bool, but the two result branches have Int and Bool types. Their required equality fails even though an evaluator following this fixed guard would choose the integer branch. Untaken bad branch fails earlier for a different reason: the bad addition inside a branch cannot finish its own inference. The engine never needs to reach a final branch-equality constraint to reject that tree. Both presets check statically relevant structure beyond the chosen runtime path, but their recorded reasons identify different failed premises.
Choose Identity function and compare its panels with Increment application. Its type is a -> a, while the runtime display says Function value. The interpreter creates a closure, a value that retains the environment needed to evaluate the function body when called. That runtime object is neither the arrow type nor a proof of the type. Choosing a new preset replaces the whole authored tree and starts inference from an empty environment. No bindings learned while inspecting increment carry over to specialize the next identity function to Int -> Int.
| Preset | Static result | Separate evaluation | Relationship preserved by the type |
|---|---|---|---|
| Identity function | a -> a | Function value | Input and output classifications agree |
| Increment application | Int | 5 | Result is classified as Int |
| Captured outer variable | a -> Pair<a, a> | Function value | Both output components retain the input type |
| Wrong operand | Rejected | Not evaluated in the interface | Right addition operand must be Int |
All twelve examples are available here, including the two let examples and Parameter at two types. Switching among them changes the expression, not an inference option. The separate comparison in the next chapter holds one expression fixed and varies let generalization instead. In the present explorer, every run uses the same pure-let rule. A parameter remains monomorphic, so using f first on 3 and then on true shares an input unknown and fails. The distinction is visible in the generated applications, without treating a runtime function value as permission to instantiate arbitrary types.
The first conflicting requirement depends on traversal and solving order. A later application can expose an earlier mistaken assumption. Use the recorded origin to inspect both sides; do not assume that the last expression mentioned is the only line needing correction.
After successful inference, a separate bounded interpreter computes the example value. It does not call host eval or Function. Resource-limit errors are distinguished from type or unbound-name errors. Passing the tests is implementation evidence, not a proof that every possible program is handled soundly.
A useful diagnosis identifies the failed obligation before proposing a change. Calling an integer supplies Int where application requires a function constructor. Unknown name cannot obtain any type information for absent from its empty environment. Self application reaches a self-containing type equation. These failures happen at different points even though all prevent a final inferred signature. Rewriting every message as a generic type mismatch would discard information about whether to inspect a binding, an application shape, or repeated uses of one unknown. The first failing premise narrows the investigation without uniquely determining the programmer's intention.
Parameter at two types gives a concrete example of that limit. The first application of f to 3 requires its shared parameter type to be Fn<Int, t1>. The second application to true requires that same type to be Fn<Bool, t2>. Unification exposes Int = Bool when comparing the inputs. Possible paper changes include using two distinct parameters or using a suitable pure let-bound identity instead of a function parameter. Those are different programs with different assumptions. The engine cannot infer which change the author intended merely from the equation that failed at the second application.
| Preset | Information available | Failed obligation |
|---|---|---|
| Unknown name | Empty environment | No binding for absent |
| Calling an integer | Function position has Int | Int = Fn<Bool, t0> |
| Self application | Both uses share t0 | t0 = Fn<t0, t1> |
| Parameter at two types | First call fixes input Int | Second call requires the same input Bool |
Inference visits expressions in an implementation-defined order and stops when a requirement fails. This engine visits the function before the argument of an application and visits pair components left to right. Its visited-expression table includes only visits that completed. A parent whose child fails may therefore be absent, even though the parent is part of the displayed tree. Failure records are not a complete derivation for a rejected term. Nor are they an inventory of every possible problem in that term. Later subexpressions may never have been visited, and a different traversal could expose another inconsistent requirement first.
Resource failures need separate interpretation. The input validator bounds expression nodes and depth and restricts authored integer literals to minus 100 through 100. The independent interpreter has an evaluation-visit budget and requires addition results to remain safe integers. An accepted static type cannot remove these implementation limits. Conversely, a resource-limit message does not show that the expression's equations are contradictory. These bounds make a local teaching engine manageable; they are not a proof that every well-typed computation finishes within its allotted visits or that all mathematically meaningful integers fit its representation.
The connection between inferred types and evaluation would require an argument about both sets of rules. Progress would rule out the specified stuck states for closed well-typed terms in a defined semantics. Preservation would require each permitted evaluation step to retain its type. A correct unifier alone establishes neither property for the entire interpreter. It solves equalities supplied to it, so an incorrect expression rule could still supply the wrong equations. Likewise, a correct set of equations would not fix an interpreter that looked up a shadowed variable in the wrong runtime environment.
| Paper implementation mistake | What could still work | What needs checking |
|---|---|---|
| Addition generates no operand equations | Unifier solves every equation it receives | Expression rules generate all required premises |
| Lookup merges shadowed names | Constructor decomposition remains correct | Environments preserve binding scope |
| Interpreter reads the wrong captured binding | Final static signature remains unchanged | Runtime lookup agrees with lexical scope |
| Evaluation visits exceed the budget | Type equations remain consistent | Resource outcome is reported separately |
When transferring this reasoning to another language, identify what the signature actually preserves and which operation generated each requirement. For this engine, a successful a -> Pair<a, a> retains one shared input/output classification, and a successful Int result says nothing about whether the arithmetic met an intended business formula. Runtime validation, effects, and directional compatibility require their own rules in later labs. The complete account here is narrower and more checkable: an authored tree, lexical assumptions, consistent equality replacements, a final signature on success, and an independently computed runtime result only for an accepted example.
Which are instances of a -> a: Int -> Int, Bool -> Bool, and Int -> Bool?
A substitution must replace every occurrence of a consistently.
| Candidate | One consistent substitution? |
|---|---|
| Int -> Int | a := Int |
| Bool -> Bool | a := Bool |
| Int -> Bool | No |
The first two are instances. The last is not, because one substitution for a cannot be both Int and Bool. This repeated-variable relationship is the useful information in the identity type.
The engine rejects absent, 3(true), and a program exceeding its node budget. Are these all evidence of incompatible types?
Separate lookup, typing, and implementation limits.
| Input | Failure category |
|---|---|
| absent | Unbound name |
| 3(true) | Type conflict |
| Oversized expression | Resource limit |
No. absent fails name lookup. 3(true) attempts to equate Int with a function type and fails typing. The oversized tree exceeds a teaching resource limit; that alone says nothing about whether its type equations are consistent.
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 constraint generation, unification, principal-type, and let-polymorphism passages. The lesson uses its own bounded tree-based engine, not a complete OCaml implementation.
Selected progress, preservation, and substitution statements. We do not claim to have independently checked the entire proof development or proved our implementation sound.