Generalize only what is independent of the environment
Let-bound polymorphism permits fresh instances without making captured values change type.
By the end: distinguish monotypes, schemes, instantiation, and safe generalization.
A scheme binds type variables
A monotype is a single type without a forall binder. A type scheme quantifies variables that may receive fresh instances. For let id = fun x -> x, the function has shape a -> a. In this pure rank-one language, let can generalize a into the scheme forall a. a -> a. Each use of id then receives fresh unknowns. One use can become Int -> Int while another becomes Bool -> Bool.
The implementation does not execute two different function bodies. It checks two type instances of one binding. A monomorphic version shares the same unknown across uses and rejects id(3) paired with id(true). The side-by-side comparison changes only the generalization rule.
Fresh instances preserve relationships within each use
The word polymorphic means that a binding can be used at more than one type. That statement needs a scope. In the paper notation forall a. a -> a, forall binds the type variable a throughout the following type. It says that a use may choose a type for a, provided every occurrence in that use receives the same choice. This is different from an unresolved a -> a during inference, where a still names one unknown in the current problem. The printed arrow shape alone does not distinguish these situations.
The examples in this explanation use paper notation for expressions and types. The explorer below instead selects existing authored trees; it has no text parser. Its Let identity at two types preset represents let id = fun x -> x in (id(3), id(true)). Start with the definition. Give x the unknown a. The body looks up that same x, so its type is a, and the whole function has type a -> a. With no surrounding assumptions to restrict a, the let binding records forall a. a -> a.
One new unknown per quantified name, not per occurrence
Each function constructor has an input and output child. Both children share a name within an instance; different lookups use different names. Tree geometry is schematic.
At the first use of id, instantiate the scheme. Instantiation means replacing its quantified variables with fresh unknowns for this use. Replace a by b in both positions, giving b -> b. Applying this function to 3 requires b -> b to equal Int -> r, where r is a fresh result unknown. Function decomposition gives b = Int and b = r. Substitution therefore makes r equal Int. The result type follows from these equations, not from running id and observing that its result happens to be 3.
At the second use, instantiate again with a different unknown c. The function shape is c -> c. Application to true requires c -> c to equal Bool -> s. Decomposition gives c = Bool and c = s, so s becomes Bool. Pair construction then combines r and s into Pair<Int, Bool>. No equation equates b with c. Freshness separates the uses, while the repeated variable inside each function type preserves the connection between that call's input and output. Freshening individual occurrences separately would lose the identity relationship.
Now contrast a binding with no quantifier. Both uses share a single shape a -> a. The first application gives a = Int and its result Int. When the second application requests Bool -> s, substitution has already changed the function shape to Int -> Int. Decomposition demands Int = Bool, which fails. The failure is not that identity cannot accept a boolean at runtime. It is that one monomorphic binding must satisfy both static requirements at once. Generalization changes which unknowns calls share, not the definition's runtime instructions.
One unknown cannot meet both input requirements
Point in checking
Monomorphic id
Required equality
Binding
a → a, with no forall
No choice yet
Apply to 3
a := Int
Int → Int = Int → r; r := Int
Apply to true
Still Int → Int
Int → Int = Bool → s
Decompose second use
No common solution
Int = Bool fails
The monomorphic comparison preserves one variable across lookups. Its second application fails after substitution, despite the first application succeeding.
A scheme can quantify more than one variable, but it still records relationships. In the separate paper type forall a, b. a -> Pair<a, b>, choosing Int for a and Bool for b yields Int -> Pair<Int, Bool>. It does not yield Int -> Pair<Bool, Int>, because the first pair component repeats a. A substitution is consistent across the complete type tree. Count distinct quantified names rather than their occurrences when deciding how many fresh unknowns an instantiation needs. Here there are two choices, even though a appears twice.
Do not generalize captured assumptions
Consider fun x -> let f = fun y -> x in (f(1), f(true)). The type of x belongs to the surrounding environment. f can vary its input type y, but both calls return the same outer x type. The final type is a -> Pair<a, a>, not a -> Pair<b, c>.
Generalization quantifies variables free in the inferred binding type but not free in the current, substituted environment. Apply known substitutions first. Otherwise a variable connected indirectly to an outer assumption might be generalized incorrectly. Instantiation replaces quantified variables only; free environmental variables stay shared.
Subtract environmental unknowns after substitution
A type variable is free in a type when no forall in that type binds it. Thus a and b are free in the monotype b -> a. In the scheme forall b. b -> a, only a is free. The surrounding environment maps program names to schemes. Its free variables are the free variables of those schemes taken together. These definitions explain the generalization rule: find the binding type's free variables, then exclude the environment's free variables. Exclusion preserves assumptions that the surrounding expression already shares with the binding.
Work through the existing Captured outer variable example before looking at the comparison. Give the outer parameter x type a. The local function f has parameter y with fresh type b and returns x, so its type is b -> a. The binding type has free-variable set {a, b}; the environment containing x has set {a}. Braces here list distinct variable names, without counting repeated occurrences. Removing the environmental set leaves {b}. The scheme for f is therefore forall b. b -> a. Only the input can be freshened at each lookup.
The local function returns an outer binding
The dashed binding link crosses the local function boundary to the outer x. Its type a cannot become an independent choice for each call of f.
For f(1), replace b with fresh c while keeping the free a unchanged. The resulting type c -> a must equal Int -> r. Its input equation fixes c to Int, and its output equation equates r with a. For f(true), a separate instance d -> a gives d = Bool and result s = a. Both results consequently share a, producing Pair<a, a>. Restoring the outer function gives a -> Pair<a, a>. This derivation permits different argument types without permitting different types for the captured value returned by both calls.
Known substitutions must affect the environment before this subtraction. Consider the separate paper expression fun g -> let z = g(1) in (z, g(true)). Initially g has unknown a. Inferring g(1) requires a = Int -> b, where b is the application result. The binding z now has type b. If we inspect the old environment literally, it mentions only a, and b might seem independent. After substitution, however, the environment contains g with type Int -> b. The unknown b is therefore environmental and cannot be generalized for z.
This example fails when g(true) requires the already constrained Int input to accept Bool. Even before that failure, giving z the scheme forall b. b would be wrong. That scheme would let a later use demand any result type independently of the one g actually returns. The connection between g and z is indirect through a substitution, but it is still a connection. Applying substitutions before collecting free variables is what preserves it. The rule concerns shared assumptions, not whether a variable's printed name happened to occur in the initial environment.
A fresh result can become part of an outer assumption
Generalization calculation
Binding z
Environment entry for g
Before checking the call
Not inferred yet
a
Call equality
Result unknown b
a = Int → b
After substitution
b
Int → b
Free-variable sets
{b}
{b}
Binding set minus environment set
∅; quantify nothing
b remains shared
This paper fragment is g(1) while checking fun g -> let z = g(1) in the surrounding body. The substituted environment exposes the dependency.
Generalization also respects lexical scope. If a nested function introduces another parameter called x, that new binder replaces the visible assumption for its own body; it does not alter the outer binding. Conversely, let y = x creates an alias whose type is already environmental, not a new independent value of every type. In the paper expression fun x -> let y = x in (y, y), the binding and environment both have free-variable set {a}. Their difference is empty. Both occurrences retain a, yielding a -> Pair<a, a>.
Inspect the rules and their result
Same expression, different let-generalization rule
let id = (fun x -> x) in (id(3), id(true))
Monomorphic let
Rejected: Cannot unify Int with Bool. Application requires an argument-compatible function
Let name
Recorded scheme
id
(t0 → t0)
Polymorphic let
Accepted: Pair<Int, Bool>
Let name
Recorded scheme
id
forall t0. (t0 → t0)
Monomorphic: rejected. Polymorphic: accepted.
Generalize only independent variables
Use the substituted binding type T and substituted environment Gamma. Instantiation later replaces only these quantified variables.
Presets replace the expression in both panels. Everything except let generalization is held equal. Lambda parameters remain monomorphic in both engines. Quantified variables are freshened at each use; free variables from the environment stay shared. There is no mutation or value-restriction implementation in this pure core.
Binding
What can vary across uses?
Pure let-bound identity
Quantified input/output type
Lambda parameter
No fresh independent instance here
Function returning captured x
Input can vary; x type remains shared
Generalization is scoped, not an automatic conversion of every unknown.
Explain the three comparison presets
Use Let identity at two types to compare the two panels while holding the expression fixed. The left panel disables let generalization; the right panel enables it. Both engines still use the same literal, function, application, and pair rules. Predict a conflict on the monomorphic side and Pair<Int, Bool> on the polymorphic side. The recorded let scheme is evidence about the binding step. It is not a list of runtime specializations or a claim that the interpreter constructed different versions of the function for the integer and boolean applications.
The record on a failed run needs particular care. A monomorphic id may be recorded with an unresolved variable at binding time even though the first application later constrains that variable to Int. The panel deliberately preserves the recorded scheme rather than retrospectively rewriting the earlier diagnostic. Read it as what was recorded when id entered the environment. To explain the eventual conflict, carry the later substitution forward yourself. An unquantified variable in that record is shared; its unresolved spelling does not mean a later lookup can instantiate it independently.
A recorded scheme and a later substitution describe different times
Evidence
Recorded at let
After checking id(3)
Monomorphic binding
a → a, unquantified
Shared a constrained to Int
Polymorphic binding
forall a. a → a
Only this use's fresh b constrained to Int
Next lookup
Read the recorded binding
Shared Int → Int, or a new c → c
These are explanatory names, not promises about exact trace numbering. The record stays at binding time; subsequent constraints still restrict its unquantified unknown.
Select Captured outer variable next. The monomorphic panel fails because f shares its argument unknown across f(1) and f(true). The polymorphic panel accepts because f's input unknown is independent of x and can be quantified. Its output unknown remains tied to x in both panels. Compare this with the earlier free-variable calculation rather than interpreting acceptance as permission to freshen the entire type. In particular, the successful result a -> Pair<a, a> says that both pair components have the outer argument's type, even though the calls pass different arguments to f.
Finally select Parameter at two types. This authored tree contains no let binding: it is fun f -> (f(3), f(true)). Consequently the generalization switch has no binding on which to act, and both panels reject it. Give f one unknown a. Its first application requires a = Int -> b. Its second requires a = Bool -> c. Substituting the first equation into the second exposes Int = Bool. The two result unknowns do not repair the incompatible inputs. This example isolates the difference between a let-bound scheme and a lambda parameter.
The useful comparison is across all three trees, not just between accepted and rejected labels. The identity case demonstrates independent instances. The capture case demonstrates partial independence within one scheme. The parameter case demonstrates that a quantifier cannot be invented at every name lookup. None of the presets changes the core into a language with explicitly polymorphic parameters. A more expressive language could ask callers to supply a scheme-bearing argument, but that is a different rule, not an alternative interpretation of this engine's failure. Here each lambda parameter has one monotype throughout its body.
The presets isolate three different sharing rules
Existing preset
Monomorphic let
Polymorphic let
Let identity at two types
Reject: one input unknown
Accept: Pair<Int, Bool>
Captured outer variable
Reject: f input shared
Accept: a → Pair<a, a>
Parameter at two types
Reject: f parameter shared
Reject: f parameter still shared
The same tree feeds both panels. Capturing x restricts the output unknown, while a lambda parameter receives no fresh scheme in either panel.
Final signatures may rename unknowns to a, b, and later letters. Those names summarize relationships, not persistent identities across presets. If the captured example displays one local unknown in its recorded scheme and a different letter in the final signature, compare where that unknown repeats. Two appearances of the same final letter must remain linked; a different local trace name alone does not imply different types. Selecting another preset replaces the whole tree and starts again from an empty environment, so no inference information carries from your previous selection into the next comparison.
Purity matters to this simple rule
A polymorphic mutable cell could be written through an integer instance and read through a boolean instance, breaking safety. Languages with references therefore need restrictions or richer mechanisms. OCaml’s value restriction and relaxed variants address this problem in its own language.
Our core has no mutation, so it uses pure let-generalization. It does not implement OCaml’s full restriction, higher-rank types, polymorphic recursion, or every form of generics. A function parameter remains monomorphic here even when a similarly named let binding could be generalized.
Why shared storage needs a different rule
Pure let generalization relies on the absence of mutable storage in this core. To see what would change, consider a hypothetical extension, not an available preset or permitted operation. A cell is one storage location that can be read and overwritten through several names. Suppose it initially contains the identity function. If the cell itself received the scheme forall a. Cell<a -> a>, separate lookups could claim that the same location stores Int -> Int or Bool -> Bool. Freshening a type description would not allocate separate storage for those claims.
Through the integer view, a program could overwrite that location with an increment function. That function requires Int and returns Int. Through the supposed boolean view, the program could then read the same stored function and apply it to true. The increment function's integer requirement would fail. The error comes from a shared mutable location carrying incompatible promises across views, not from identity's own body. Quantifying a binding must not let a write under one instance invalidate a read under another instance of the same location. The hypothetical scheme allowed exactly that problem.
Fresh descriptions would still name the same writable location
Step
Actual stored function
Claim through the selected view
Allocate one location L
Identity
Proposed forall a. Cell<a → a>
Use integer instance
Overwrite L with increment
Cell<Int → Int> permits the write
Use boolean instance
L still contains increment
Cell<Bool → Bool> claims a boolean function
Read and apply to true
Increment requires Int
Bool input violates that requirement
Hypothetical invalid extension only. No cell operation exists in the core. The incompatible read follows from granting the proposed scheme, not from an operation the current model permits.
The distinction between creating a function and creating storage matters here. A pure identity function contains no writable slot whose contents one call changes for another call. A function returned by another function could, in a language with mutation, retain hidden storage. Its visible arrow type might resemble identity while its behavior depends on values saved by earlier calls. That is why merely looking at an arrow in a printed signature does not establish that generalization is safe in a language with references. The analysis has to account for that language's rules about state.
OCaml uses restrictions on generalization to address such cases. Its manual calls an unknown that must eventually settle on one type a weak type variable. A weak variable is not a universally quantified variable waiting to supply an unrelated instance at each use. After a use constrains it, later uses must agree. The value restriction limits which bindings may receive unrestricted polymorphism in the presence of possible shared state. This explanation does not import OCaml's complete policy into the lesson engine. The engine has neither references nor weak-variable syntax nor a value-restriction implementation.
The hypothetical failure also explains why simply allocating more fresh inference variables is not a universal repair for a type conflict. Fresh variables are justified when a valid scheme binds the replaced names. They are unjustified when the names describe one fixed parameter, captured value, or shared writable location. A rejection may therefore be the intended result of preserving a relationship. The pure core rejects the two-type lambda parameter because its rule preserves one parameter type. The proposed mutable extension would need additional rules to preserve one storage location's compatible read and write expectations.
Only a binder justifies independent instances
Type description
What a lookup may freshen
What remains linked
forall a. a → a
The bound a
Input and output within one use
forall b. b → a
Only b
Environmental output a across uses
Unquantified a → a
Nothing
Both positions across all uses
Alias y for outer x : a
Nothing
x and every occurrence of y
A free unknown remains a single unknown even when unresolved. Quantification authorizes consistent replacement of every bound occurrence within each new instance.
To analyze an unfamiliar let binding, reconstruct the type relationships rather than guessing from its spelling. First infer the binding under the visible assumptions and apply accumulated equalities to both. Then identify which remaining unknowns belong only to the binding. Those are the candidates for quantification under this pure rule. At each subsequent lookup, replace precisely those quantified names, consistently within the resulting type. The environment-owned names remain shared. This account explains both successful mixed-type identity calls and the captured-result relationship, without claiming that bounded implementation tests prove a theorem about every possible language with polymorphism.
Exercises
Why the two uses succeed
Why can let id = fun x -> x in (id(3), id(true)) infer Pair<Int, Bool> under let polymorphism?
Hint
Give the two uses different fresh variables before constraining them.
Worked answer
Use
Fresh shape
Resolved
id(3)
b -> b
Int -> Int
id(true)
c -> c
Bool -> Bool
Fresh instantiation separates uses, not occurrences within one use.
The scheme quantifies its identity variable. The first use receives b -> b and constrains b to Int. The second receives c -> c and constrains c to Bool. The variables are distinct, so no Int = Bool equation arises. A monomorphic binding would share one variable and fail.
Protect the captured variable
In fun x -> let y = x in (y, y), may the two y occurrences receive unrelated types?
Hint
The binding type is already free in the environment through x.
Worked answer
Variable
Free in environment?
Generalize?
Type of outer x
Yes
No
Same type assigned to y
Yes
No
An alias does not create a universally polymorphic value.
No. Let y has no independent variable to generalize. Both occurrences keep x’s type. The result is a -> Pair<a, a>. Treating y as forall a. a would invent a value of any requested type and is unsound.
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 constraint generation, unification, principal-type, and let-polymorphism passages. The lesson uses its own bounded tree-based engine, not a complete OCaml implementation.