Generate type requirements locally, while retaining the expression that caused each requirement.
By the end: build equality constraints and separate unsolved variables from universal parameters.
Start each unknown expression or parameter type with a fresh variable. Fresh means a distinct unknown, not a guessed Int or Bool. Reusing a variable intentionally records equality. Reusing it accidentally can reject unrelated uses or incorrectly couple separate scopes.
Application of f to x introduces a fresh result b and requires the type of f to equal the function type type(x) -> b. Integer addition requires both operands to equal Int. Our pair constructor combines component types without requiring them to be equal.
These paper expressions describe trees; the explorer selects authored trees rather than parsing source. A constraint is a requirement that a proposed answer must satisfy. Here each constraint says that two types must be equal. The equality sign neither assigns nor compares runtime values. A type variable names an unanswered type question. Sharing its name across requirements says they concern the same question. Giving distinct questions different names avoids accidentally imposing a relationship the expression never required in the first place.
Keep two kinds of tree separate. An expression tree contains forms such as application, integer literal, and addition. A type tree contains Int, Bool, Fn, Pair, and unknowns. Fn is a type constructor with input and output components, displayed using an arrow. Pair is a constructor with first and second component types. A constructor is a fixed structural form, not a replaceable unknown. Looking at an expression node tells us which typing rule to apply; the rule then relates type trees associated with that node and its children.
A literal 3 supplies Int directly. A literal true supplies Bool. A parameter binding starts with a fresh type variable, meaning one distinct from every unknown already allocated in that run. Looking up that parameter returns the same unknown instead of allocating a new one. For fun x -> x + x, the two operand occurrences therefore have the same a. Addition requires a = Int for both operands, and the result is Int. The duplicate requirements are harmless. Allocating separate unknowns at those two lookups would lose the fact that one binding supplies both operands.
Application needs one additional unknown for its result. In the paper expression f(true), suppose the environment gives f unknown a. The argument has Bool. Name the result b. To call the left child, it must have the entire function shape Bool -> b, so generate a = Bool -> b. The application itself has b, not a and not Bool. At this point b can remain unknown. A surrounding addition would require b = Int; a surrounding conditional guard would require b = Bool. The calling rule alone does not choose either answer.
Pairs illustrate a different relationship. In the paper expression (f(true), 3), keep the application's b and combine it with the literal's Int to form Pair<b, Int>. Constructing that pair does not require b = Int. The pair stores two independently typed components. By contrast, if a later requirement says the pair must have Pair<Int, Int>, comparing matching components would constrain b to Int. The distinction is between constructing a type from components and demanding equality with another type. It prevents incorrectly rejecting mixed pairs such as the plainly valid (3, true).
| Expression part | Type or requirement | Reason |
|---|---|---|
| f(true) | a = Bool → b; result b | Application |
| 3 | Int | Integer literal |
| (f(true), 3) | Pair<b, Int> | Pair construction |
| Additional equality b = Int | Not generated here | No such demand in this tree |
Conditionals add two kinds of equality. Their guard must have Bool, and the two possible result branches must agree in type. For the paper function fun c -> if c then 3 else 4, the parameter begins with a. Guard use supplies a = Bool. The two literals supply Int and Int, so branch agreement already holds. The body is Int and the function is Bool -> Int. Replacing the else literal by true creates a branch equality Int = Bool. A literal true guard would not remove that requirement, since static checking examines both branches.
For the increment function, x starts as t0. Addition produces t0 = Int and Int = Int. Its result is Int, so the function shape starts as t0 -> Int. Solving t0 = Int supplies the final Int -> Int. The equations express static relationships, not assignments executed by the program.
The explorer records each generated equality with a reason, such as Left addition operand or Conditional guard. Our engine generates and solves requirements incrementally, rather than constructing a whole-program unsolved list first. On failure, it shows only requirements reached before the failure.
The implementation solves requirements incrementally. Incrementally means it generates a requirement, updates its current answers by solving it, and then continues visiting expressions. A substitution is the collection of answers mapping type variables to type trees. Applying a substitution replaces every relevant occurrence consistently. Binding a to Int therefore changes both occurrences in a -> a, not whichever one was most recently visited. The starting expression tree remains unchanged. This is bookkeeping for type relationships, whereas a runtime environment associates program names with actual values during execution of a separately interpreted expression.
Work through the paper function fun f -> f(3) + 1. Start with f having a and the application result b. The literal argument supplies Int, so application requires a = Int -> b. Recording that answer makes the parameter a function, but leaves its output unknown. Addition then requires its left operand b to equal Int. Its right literal already has Int. Applying both answers to the parameter type produces Int -> Int. The body's result is Int, so the enclosing function has the larger shape (Int -> Int) -> Int.
| Paper derivation stage | New information | Current f type |
|---|---|---|
| Parameter f | Fresh unknown a | a |
| Call f(3) | a = Int → b | Int → b |
| Add 1 to call result | b = Int; Int = Int | Int → Int |
| Wrap in fun f | Body has Int | Whole type: (Int → Int) → Int |
Immediately after the application requirement, Int -> Bool is still a possible type for f, because b has not yet been constrained. After the addition requirement, it is no longer possible. Conversely, the first equation never justified guessing that f returns Int merely because its argument was an integer. The surrounding addition supplied that evidence. Writing down the source of each requirement distinguishes information supplied by arguments from information supplied by uses of results. That distinction remains useful when the resulting types contain more nested function constructors or pair components.
The explorer's recorded equations retain their origin rather than presenting an unexplained final substitution. An origin such as Left addition operand identifies the operation that requires Int. It does not say which runtime integer appeared there. An application origin identifies the demand for an argument-compatible function. In a larger derivation, an earlier answer may change what that later demand means when solved. The stored original equation and the solver's resolved view are therefore different useful records. One explains how the question arose; the other shows the consequences of answers already obtained.
Consider a separate paper pair of equations a = Pair<b, b> and b = Int. After the first binding, a contains two occurrences of b. Applying the second answer resolves a to Pair<Int, Int>. Updating only the most recently mentioned b would leave an incorrect mixed answer. The same principle applies through several constructors, including function inputs and outputs. Repeated variable names express shared requirements wherever they occur in a tree. Distinct positions do not make those occurrences independent. Substitution must follow the occurrence relationship, not the layout of the printed equation.
The final type is the initial result shape after applying all successful answers. A still-unanswered variable can legitimately remain if the expression never restricts it. For fun f -> f(3), that remaining result unknown appears in both the parameter's output and the enclosing body's output. Renaming it consistently from b to c changes no relationship. Replacing it only at one position changes the claim. The UI's final signature uses canonical names such as a and b for readability; trace names such as t0 remain local identifiers for the questions created during that particular run.
(fun x -> (x + 1))(4)Accepted: Int
Int5
A value is not the evidence used to infer the type.
| Generated equality | Reason |
|---|---|
| t0 = Int | Left addition operand |
| Int = Int | Right addition operand |
| (t0 → Int) = (Int → t1) | Application requires an argument-compatible function |
| Visited expression | Rule | Recorded type |
|---|---|---|
| x | var | Int |
| 1 | int | Int |
| (x + 1) | add | Int |
| (fun x -> (x + 1)) | lambda | (Int → Int) |
| 4 | int | Int |
| (fun x -> (x + 1))(4) | app | Int |
| Step | Solver action | Bindings after step |
|---|---|---|
| 0 | Start these constraints | None |
| 1 | Bind t0 to Int | t0 := Int |
| 2 | Start these constraints | t0 := Int |
| 3 | Already equal: Int | t0 := Int |
| 4 | Start these constraints | t0 := Int |
| 5 | Decompose Fn into corresponding components | t0 := Int |
| 6 | Already equal: Int | t0 := Int |
| 7 | Bind t1 to Int | t0 := Int; t1 := Int |
On failure, visited-expression types and partial bindings are diagnostic state, not a solution. Only successfully completed visits appear.
Beta is a fresh result-type unknown. The application has that result type, not necessarily the argument type.
| Expression form | Generated requirement |
|---|---|
| f(x) | type(f) = type(x) -> fresh result |
| x + y | type(x) = Int; type(y) = Int |
| if c then x else y | type(c) = Bool; type(x) = type(y) |
The constraint explorer offers Increment application, Integer addition, Different branch types, and Self application. A preset replaces the entire authored tree and recomputes inference from an empty environment. It does not append an equation to the currently selected example. These examples deliberately expose different requirements, so a comparison should begin with each displayed tree rather than treating a button as a change to one hidden parameter. The equality table shows requirements reached during that run. The trace supplies solver actions and completed expression visits beneath the panels.
Select Increment application and separate its body requirements from its calling requirement. The parameter's unknown must equal Int because the left addition operand uses it. The right operand already supplies Int. Only afterward does the outer application require the function shape to match an Int argument and a fresh result. That last comparison fixes the application result to Int as well. The returned runtime value is 5, but no equation needed the numeral 5. Every supported integer argument gives the same result type, though evaluation may produce a different number.
| Preset | Decisive requirement | Result |
|---|---|---|
| Increment application | Parameter Int; call matches Int input | Accepted Int |
| Integer addition | Int = Int for both operands | Accepted Int |
| Different branch types | Int = Bool | Constructor conflict |
| Self application | t0 = (t0 → t1) | Occurs check failure |
Select Integer addition next. Both literal children already have Int, so the generated equations compare Int with Int. There is no unresolved parameter to solve. Such an equality still records a premise of addition, even though checking it adds no new information. This explains why an equation table can be nonempty for an expression whose type is immediately apparent. Distinguish recording an obligation from learning something new while solving it. Removing an already satisfied equation is legitimate; replacing it with a guessed variable binding would add an answer that the example never asked for.
Different branch types has a literal true guard, then an integer result and a boolean result. The guard requirement succeeds. Branch agreement then compares Int with Bool and fails. The evaluator panel does not compute the selected integer branch because inference rejected the whole expression. This branch-type failure does not mean evaluating true failed. Both branches belong to the authored tree, and the rule checks both. The displayed result cannot be repaired by choosing a different unknown name because the conflict is between fixed constructors, not between unresolved questions.
Self application selects fun x -> x(x). The parameter's type appears twice in the application requirement, once as callee and once as argument. Solving would require that unknown to contain itself inside a function type. The occurs check rejects this finite-tree requirement. Open the solver trace and compare its action with the constructor conflict in Different branch types. One failure concerns incompatible outer forms; the other concerns an attempted self-containing answer. Both are type failures, but they explain different mistakes in the proposed relationships and need different changes to the expression to resolve them.
| Branch disagreement | Evidence |
|---|---|
| Guard true | Bool = Bool succeeds |
| Branch 1 | Int |
| Branch false | Bool |
| Required agreement | Int = Bool fails |
| Self application | Evidence |
|---|---|
| Callee x | a |
| Argument x | Same a |
| Result | Fresh b |
| Required function | a = (a → b) fails |
The table and visited-expression trace stop when inference fails. An uncompleted parent expression has no completed visit entry, even if some child expressions have already contributed requirements. Therefore absence of a later equation does not show that the remaining source would satisfy its rules. Likewise a partial binding in a failed trace is not a type for the full tree. Switching back to Integer addition recomputes with fresh run-local questions, rather than retaining the failed example's answers. These reading rules explain exactly what evidence the explorer provides without assuming it collects every possible whole-program error before reporting a result.
The core engine solves type equality. Subtyping uses a directional compatibility relation; numeric range checks, overload selection, trait obligations, and effect inclusion require other rules. Calling all these processes constraint solving does not make their algorithms interchangeable.
An unsolved variable in one inference problem is not yet a universally quantified generic parameter. Generalization must check the environment. Keep unknown creation, equality solving, and quantification separate so that a convenient display does not hide an unsound inference step.
An equality problem asks for one consistent answer for each unknown across every equation in that problem. For a = b, either Int for both or Bool for both would satisfy the equation, but neither choice is required. Keeping them as one shared unknown records exactly the information given. Most general means avoiding an extra restriction that the requirements did not impose. It does not mean choosing the largest type or accepting incompatible answers simultaneously. This engine has no universal top type that turns Int and Bool into equal types when a comparison fails.
A useful paper comparison is Pair<a, b> against Pair<c, c>. Matching pair constructors requires a = c and b = c. That connects both original component unknowns through c. If a later requirement supplies a = Int, then b and c must also resolve to Int. If it instead supplies b = Bool at the same time, the combined problem fails. No pair component has a privileged right to keep its earlier answer. All equalities must hold together. Repeated occurrences matter, not whether an unknown is named a or t7.
| Answer to a = b | Satisfies equality? | Remaining choice |
|---|---|---|
| a is the same unknown as b | Yes | Shared type still open |
| a is Int; b is Int | Yes | Int chosen unnecessarily |
| a is Bool; b is Bool | Yes | Bool chosen unnecessarily |
| a is Int; b is Bool | No | Inconsistent replacement |
This sharing differs from a type scheme, a description with explicitly quantified variables that may receive fresh instances at separate uses. Quantified means bound by that permission to instantiate independently. The later polymorphism lesson explains when a pure let binding can receive such a scheme. Merely seeing an unknown in a trace grants no permission to duplicate it into unrelated unknowns whenever convenient. A lambda parameter remains monomorphic, meaning it has one shared type throughout its body here. Its two calls cannot discard an earlier Int-input requirement in order to accept a Bool argument later.
Equality also differs from directional compatibility. Later subtyping examples allow a stipulated Cat value to satisfy an Animal requirement without claiming Cat equals Animal. The current equation solver has no such hierarchy, and Int versus Bool is not a request to search for a conversion. Similarly, the requirement that an age be between zero and 130 concerns runtime data policy, not equality between the constructor Int and a numeral. An engine must define the relationships its constraints express. Reusing the word constraint does not let one algorithm solve equality, range policies, and directional compatibility by the same rules.
A conditional paper example separates type agreement from equal values. In if c then 3 else 4, both results have Int, though their values differ. Conversely, 3 and true cannot satisfy branch-type equality merely because an outside display might print them similarly or a host language might convert one representation to another. Our authored language defines integer addition and boolean guards without coercion. The requirements concern those operations and type constructors. Runtime observations can help explain an example's behavior, but the interpreter's returned data never provides evidence used to choose an inference unknown's answer.
| Claim | Relationship being checked | Evidence needed |
|---|---|---|
| Both conditional results have Int | Type equality | Typing of each branch |
| Both conditional results equal 3 | Value equality | Not established by Int |
| A Cat fits an Animal requirement | Directional compatibility | Separate stipulated subtype relation |
| An age lies between 0 and 130 | Runtime data policy | Separate value validation |
For a new derivation, the transferable question is which expression rule justifies each relationship. A name lookup shares a binding's type; a call connects an argument type to a function input; addition demands Int operands; a conditional demands Bool and branch agreement; a pair combines components without equating them. Once those origins are explicit, a surprising rejection can be traced to a shared unknown or an incompatible constructor rather than blamed on notation. Resource-limit errors remain separate: reaching the bounded engine's budget does not establish that the mathematical equality problem has no solution. It establishes only that this implementation stopped within its stated limits.
Assume f has unknown type a and x has Bool. Write the constraint for f(x), using b for the result.
The argument determines the function input, not its output.
| Known | New unknown | Constraint | Result |
|---|---|---|---|
| x : Bool; f : a | b | a = Bool -> b | b |
Require a = Bool -> b. The application has result type b. Nothing yet forces b to Bool or Int. A later use of the result may constrain b.
What is the type of (3, true)? Does the pair constructor require Int = Bool?
A product stores two components with potentially different types.
| Type shape | Required component relation |
|---|---|
| Pair<Int, Bool> | Each component has its stated type |
| Pair<a, a> | Both components share one type |
The type is Pair<Int, Bool>. Each component satisfies its own typing rule. No equality between Int and Bool is generated by constructing a pair. A repeated variable in Pair<a, a> would impose equal component types, but that is a different type requirement.
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.