Function types connect an argument requirement to a result. Higher-order functions use the same rule.
By the end: infer simple function shapes and explain why a parameter has one type within its body.
In fun x -> x, start by giving x an unknown type a. Looking up x in the body returns that same type. The function therefore has type a -> a. The repeated variable expresses a relationship: the output type matches the input type. It is not an instruction to convert the value.
For fun x -> x + 1, addition constrains x to Int and the body returns Int. The function has type Int -> Int. Application then requires an argument compatible with the function input; applying the increment function to true fails in this language.
The notation fun x -> body names a function expression in this course. A lambda is such an unnamed function. These text examples are paper notation for expression trees, not parser input. The explorer below selects complete, already authored trees. Its arrow in a type separates the required input type from the resulting output type. Its arrow in a function expression separates the parameter name from the body. Those two arrows describe related things, but one belongs to types and the other to expressions.
To infer fun x -> x + 1, temporarily associate x with an unknown type a. An unknown is a question to be answered by the surrounding requirements, not an unknown runtime value. Looking up x in the body retrieves that same a. The literal 1 already has type Int. Addition requires its left operand to be Int, so a must equal Int. The right operand meets the same requirement immediately. Addition's result is Int. Finally, put the parameter type on the left of the function arrow and the body's type on the right.
The final Int -> Int type follows without choosing an input value or performing an addition. A typing derivation is a record of premises supporting a conclusion. Here the premises about the operands support the body's type, and the body's type under the parameter assumption supports the function's type. The temporary assumption is local to the function body. It does not mean a free name x is available elsewhere. If another expression mentions x outside that scope, it needs its own binding. Reusing the spelling alone cannot supply that missing assumption.
Identity uses fewer requirements. For fun x -> x, the body lookup returns the parameter's unknown a, and no operation requires a particular type such as Int. Consequently the shape is a -> a, with the same unknown in two positions. Replacing a consistently with Bool gives Bool -> Bool. Replacing it consistently with Int gives Int -> Int. Bool -> Int is not an instance of that shape, because it would replace the two occurrences differently. This type relationship does not instruct runtime conversion.
Contrast identity with the paper function fun x -> 1. The parameter still starts with a, but the body has type Int independently of x. Its shape is a -> Int. Supplying a Bool argument is compatible with that function's input when a becomes Bool; identity would instead return Bool for that input type. Both functions can accept an integer and return an integer, so that single observation does not distinguish their general type relationships. The occurrence map below shows the reason. In identity the output refers to the parameter assumption; in the constant function it does not.
| Identity | Type evidence |
|---|---|
| Parameter x | a |
| Body x | Same a |
| Whole function | a → a |
| Bool input instance | Bool → Bool |
| Constant function | Type evidence |
|---|---|
| Parameter x | a |
| Body 1 | Int |
| Whole function | a → Int |
| Bool input instance | Bool → Int |
An application adds a separate obligation after the function has a shape. Applying the increment function to 4 requires its input Int to agree with the argument's Int. The application result then has the function's output Int, and the separate interpreter can calculate 4 + 1 = 5. Applying that same function to true instead requires Int to agree with Bool. It fails before the UI evaluates it. The body did not change, and the function's own derivation still explains Int -> Int. The failed obligation concerns the attempted connection between that function and this argument.
A type (Int -> Bool) -> Bool describes a function that accepts an Int-to-Bool function and returns Bool. Parentheses matter: Int -> (Bool -> Bool) instead accepts an integer and returns another function. Our displays parenthesize every arrow to avoid ambiguity.
Lexical scope determines which binding a name denotes. A nested parameter can shadow an outer binding without changing it. A closure retains the environment needed by its body. Type inference tracks types in environments; evaluation tracks values in environments. Neither should confuse two bindings because their names happen to match.
A type constructor combines component types into a larger type. Fn is the function constructor, with one input component and one output component. Arrow notation displays Fn<Int, Bool> as Int -> Bool. Reading a nested type starts at its outermost constructor, meaning the one containing all the others. In the paper type (Int -> Bool) -> Int, the outer Fn has an entire function type as its input and Int as its output. In Int -> (Bool -> Int), the outer Fn instead has Int as input and another function type as output.
For a concrete higher-order paper example, consider fun f -> f(3). Higher-order means a function receives or returns another function. Give f an unknown a, and give the application result a different unknown b. The literal argument has type Int. The application therefore requires a to be Int -> b. The enclosing function receives f itself, so its input is the whole Int -> b type and its output is b. Its shape is (Int -> b) -> b. No rule yet determines whether b is Int, Bool, or a compound type.
If the body instead adds one to f(3), addition supplies the missing restriction. Its left operand is the application result b, so b must be Int. The shape becomes (Int -> Int) -> Int. That restriction comes from the use of the returned result, not from the integer argument 3. Confusing those sources would make the earlier function unnecessarily restrictive. The same application rule accepts an Int-to-Bool argument function when no addition follows. Receiving a function does not change the rule; it changes which type tree occupies the input position.
A binding is the association introduced by a parameter or a let name. Scope is the region where that association is available. In fun x -> fun y -> x, the outer x is available inside the inner function. Assign a to x and a distinct b to y. The inner body looks up x and gets a, so the inner function has b -> a. The outer function consequently has a -> (b -> a). Its output is a function, not a pair of results. Applying it once returns that inner function with access to the supplied outer value.
Now replace the inner parameter name y with x and keep the body spelling x. The paper expression is fun x -> fun x -> x. The inner binding shadows the outer one, meaning lookup finds the inner binding first. The outer parameter has a, the inner parameter has b, and the body now has b. The result is a -> (b -> b), not a -> (b -> a). Renaming a binder safely requires renaming the occurrences that refer to it. Changing only a binder can change which association a body occurrence denotes.
The type environment records name-to-type assumptions; the runtime environment records values. Neither is a single global dictionary that forgets nested scope. In the first nested example, the interpreter's inner function retains the outer value through a closure, a function value with access to the environment needed by its body. The checker can establish the input/output relationship without knowing that retained value. Keeping these environments separate explains why a captured Bool value and a captured integer yield different runtime data while the same paper function shape describes both possible uses.
(fun x -> x)Accepted: (a → a)
t0t0Function value
A value is not the evidence used to infer the type.
| Generated equality | Reason |
|---|---|
| None generated | This expression needs no equality solving before the result or failure. |
| Visited expression | Rule | Recorded type |
|---|---|---|
| x | var | t0 |
| (fun x -> x) | lambda | (t0 → t0) |
| Step | Solver action | Bindings after step |
|---|
On failure, visited-expression types and partial bindings are diagnostic state, not a solution. Only successfully completed visits appear.
| Term | Relationship |
|---|---|
| fun x -> x | Input and output share a |
| fun x -> x + 1 | Input and output both Int |
| fun f -> f(3) | f must accept Int |
The function explorer offers Identity function, Increment application, Calling an integer, and Parameter at two types. Each button replaces the entire authored expression tree and recomputes from an empty environment. The paper examples above are not additional controls. The panels answer different questions. Static inference records type requirements. Separate evaluation computes a value only when inference accepts. The detailed trace can explain how a result arose even when the visible final signature has renamed its remaining unknowns.
Select Identity function first. The result has the repeated-variable shape a -> a, while the evaluation panel says Function value. That runtime label does not choose a particular argument or test the body at several input types. It reports a function value rather than an integer or boolean. In the visited-expression trace, the body name and enclosing lambda expose the shared unknown. Local trace names such as t0 identify one inference run. The final a is a display name for the remaining unknown, not evidence that a second inference process chose another type.
| Preset | Whole-expression type | Separate evaluation |
|---|---|---|
| Identity function | a → a | Function value |
| Increment application | Int | 5 |
| Calling an integer | Rejected: nonfunction callee | Not run |
| Parameter at two types | Rejected: conflicting inputs | Not run |
Next select Increment application. This preset includes both the increment function and its call with 4. The final result is Int rather than Int -> Int because the whole selected expression is an application. Find the function's type in the visited-expression trace, then compare it with the whole expression's type. The equality table records addition's operand requirements and the later application requirement. Evaluation returns 5 only after those static requirements succeed. The table's equations are not a log of machine additions, and their number is not the number of times the function body runs.
Calling an integer changes the failure mechanism. The selected tree applies 3 to false. The callee has Int; the argument has Bool; the application needs a function accepting Bool and returning a fresh result unknown. The required equality therefore compares Int with a function type. The outer constructors already differ, so choosing a different result unknown cannot fix it. This is distinct from calling an actual Int-input function with Bool. There the callee is a function, but its input component conflicts with the argument. Both failures reject applications for different structural reasons.
Parameter at two types introduces a shared obligation. Its f parameter first receives a call with 3 and then a call with true inside a pair. The first call requires f to have Int -> b for some result b. The second call must use that same parameter type and requires Bool -> c. Comparing their function inputs exposes Int versus Bool. Pair construction itself permits different result types and does not cause this conflict. Even giving the two call results distinct unknowns cannot remove the incompatible requirements on their shared callee.
| Body occurrence | Requirement on the same f | Consequence |
|---|---|---|
| f(3) | f has Int → b | Input fixed to Int |
| f(true) | f has Bool → c | Input required to be Bool |
| Compare function inputs | Int = Bool | Conflict |
| Pair results | Pair<b, c> | No requirement b = c from pairing |
The visited-expression trace identifies the first call fixing f's input and the later contradiction. On this failed run, recorded types and bindings describe work completed before rejection. They are not a final signature for the whole term. A pair entry may be absent because the pair visit never completed. Returning to Identity function starts a new run without the failed run's assumptions. These distinctions let you read a diagnostic as evidence about a particular attempted derivation rather than as a persistent claim about every function named f.
Within one lambda body, a parameter has one monotype. Using f on both 3 and true therefore forces incompatible input types in our core language. This differs from a let-bound identity that can receive a generalized type scheme, introduced later. Rank-one here means polymorphic schemes belong to let bindings, not to function-parameter positions.
A more expressive language can accept explicitly polymorphic function parameters. Our failure is about this language’s rank-one inference rules, not a proof that the computation is impossible. Do not silently add higher-rank polymorphism to explain a result produced by a different language.
A monotype is one type tree without a binder that permits independent replacements at each use. A parameter receives a monotype in this engine, even when that tree still contains unknowns. Unknown does not mean independently changeable. If one occurrence constrains the parameter to Int, every occurrence of that same binding must respect Int. This explains why an unused parameter can remain unconstrained but a multiply used parameter cannot become a different type at each occurrence. The information shared between occurrences is part of the function's requirement, not a restriction on variable spelling.
A useful paper contrast is fun f -> (f(3), f(4)). Both arguments have Int. The first call restricts f to Int -> b; the second restricts the same f to Int -> c. Agreement of the function outputs then requires b and c to be the same type. The pair therefore has Pair<b, b>, and the whole function has (Int -> b) -> Pair<b, b>. Repeated calls need not produce equal values, but they share an output type. A type relationship is weaker than a claim of numerical equality between the results.
| One binder f | Requirement |
|---|---|
| First call f(3) | f has Int → b |
| Second call f(4) | f has Int → c |
| Same f output | b = c |
| Pair result | Pair<b, b> |
| Binders f and g | Requirement |
|---|---|
| Call f(3) | f has Int → b |
| Call g(true) | g has Bool → c |
| Independent outputs | No b = c required |
| Pair result | Pair<b, c> |
Another contrast uses two parameters rather than two uses of one parameter. In fun f -> fun g -> (f(3), g(true)), f and g begin with different unknown types. Their independent requirements become Int -> b and Bool -> c. Nothing equates those inputs or outputs. The whole shape is (Int -> b) -> ((Bool -> c) -> Pair<b, c>). Adding the second binder changed the source of assumptions, so accepting this function would not contradict rejection of Parameter at two types. Distinct binders allow independent requirements; a pair alone does not create that independence.
Later let polymorphism introduces a type scheme, a description that explicitly permits selected type variables to receive fresh instances at separate uses. That permission is different from leaving an ordinary unknown unsolved. The present lambda rule does not grant it to parameters. Passing identity as an argument does not make the receiving parameter independently reusable at Int and Bool inside one body. The receiving function still has to satisfy its own parameter rule. A language with explicitly polymorphic parameter annotations can make a different choice, but that is outside this engine's accepted expression and type forms.
The paper expression fun x -> x(x) exposes another kind of inconsistency. Let x have a and the application result have b. Since the callee and argument are the same parameter, application requires a to equal a -> b. A finite type tree cannot contain itself as a proper descendant. Replacing a by that function shape would introduce another copy of a inside itself, then another, without reaching a finite answer. The occurs check, explained further in unification, rejects that self-containment. It is not the Int-versus-Bool conflict seen in the two-argument example.
To analyze an unfamiliar function, identify binding identities before following its types. Read the outermost function constructor to separate its entire input and output, then follow each occurrence back to the assumption that supplies its type. Operations add requirements to those assumptions; nested binders can create new ones. This method distinguishes an unconstrained identity parameter, a captured outer value, a shared function parameter, and a self-application without executing any of them. Acceptance establishes the stated type relationship under these rules. It still does not establish that the function computes the particular mathematical or business result its author intended.
Which accepts a function: (Int -> Bool) -> Int or Int -> (Bool -> Int)?
Find the outermost arrow and its entire left side.
| Type | Input | Output |
|---|---|---|
| (Int -> Bool) -> Int | Int -> Bool | Int |
| Int -> (Bool -> Int) | Int | Bool -> Int |
The first accepts an Int-to-Bool function and returns Int. The second accepts Int and returns a Bool-to-Int function. Changing parentheses changes the type structure; the strings are not interchangeable.
For fun x -> (fun x -> x + 1), must the outer parameter be Int?
The inner x is a new binding.
| Binding | Use | Type requirement |
|---|---|---|
| Outer x | Unused | Unconstrained a |
| Inner x | x + 1 | Int |
No. Only the inner parameter participates in addition. The outer parameter can have an unconstrained type a. The whole type is a -> (Int -> Int). A checker that merges bindings by spelling without respecting scope would impose an unjustified constraint.
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 constraint generation, unification, principal-type, and let-polymorphism passages. The lesson uses its own bounded tree-based engine, not a complete OCaml implementation.