A programmer writes `let f = fun x -> x in (f 5, f "hello")`. Which best explains why this typechecks in HM?
Af has type int when applied to 5 and type string when applied to 'hello', showing HM supports runtime type dispatch
BThe let binding generalizes f to ∀α. α → α, so each use independently instantiates α as int or string
CHM generates two separate monomorphic copies of f at compile time for each use site
DType inference fails here and the programmer must add an explicit type annotation
The let binding is HM's generalization point. When `let f = fun x -> x` is processed, the type variable α is universally quantified, yielding ∀α. α → α. Each subsequent use site independently instantiates α — once as int, once as string. Without the let (e.g., passing the same lambda directly to a function expecting it at two types), you'd need higher-rank polymorphism, which HM cannot infer.
Question 2 Multiple Choice
Why can HM infer all types in a program while System F (arbitrary-rank polymorphism) cannot?
ASystem F allows side effects that interact with types in ways the inference algorithm cannot predict
BHM restricts universal quantifiers to the outermost level (prenex polymorphism), keeping inference decidable
CSystem F uses a larger set of type variables that causes the unification algorithm to loop indefinitely
DHM only supports type inference for programs without recursive functions
HM's rank-1 restriction confines ∀ to the outermost level — you can have ∀α. α → α but not (∀α. α → α) → int. This prenex restriction means the algorithm only needs to instantiate quantifiers at let-binding call sites, which is decidable. System F allows ∀ nested inside argument positions, which requires the programmer to guide instantiation — inference becomes undecidable because the algorithm cannot search the infinite space of possible type instantiations.
Question 3 True / False
In Hindley-Milner, a let-bound identifier can be used at different types in different parts of the program.
TTrue
FFalse
Answer: True
This is the defining feature of HM parametric polymorphism. When `let id = fun x -> x` is bound, its type is generalized to ∀α. α → α. Every use site instantiates α independently — id can be applied to an int in one expression and a string in another. This is possible because the let binding creates a type scheme (a quantified type), not a monotype.
Question 4 True / False
Adding explicit type annotations to nearly every function in an HM-typed program allows the type checker to accept programs that inference alone would reject.
TTrue
FFalse
Answer: False
HM inference is complete: it always finds the principal type — the most general type consistent with the program. Annotations can only narrow a type to something less general or document what inference already knows. They cannot discover more general types than Algorithm W would infer, and overly restrictive annotations can actually prevent valid programs from type-checking. Annotations are documentation aids, not correctness requirements.
Question 5 Short Answer
Explain why the `let` binding plays a special role in HM generalization, and what would go wrong if HM tried to generalize type variables inside every lambda abstraction instead.
Think about your answer, then reveal below.
Model answer: The let binding is HM's designated generalization point: only here are type variables universally quantified to form a polymorphic type scheme. If HM attempted to generalize inside lambda arguments — allowing a single function parameter to be used at multiple types within one function body — it would require the parameter's type to be a higher-rank polymorphic type (e.g., a function expecting an argument that works at both int and string simultaneously). Inference for such types is undecidable. By restricting generalization to let bindings and keeping quantifiers at the top level (rank 1), HM guarantees that every well-typed program has a unique principal type that Algorithm W can find.