Let-polymorphism is implemented via TypeScheme:
The implementation is in ~/hm.py (~400 lines). It is a full Hindley-Milner type inference engine (Algorithm W) for a simply-typed lambda calculus with let-polymorphism.
Types (class hierarchy with subst, ftv, pprint):
- TVar(id) — type variable (e.g., t0, a)
- TCon(name) — base type constructor (Int, Bool)
- TFun(arg, res) — function type (a -> b)
AST (dataclass sum type Expr):
- Var(name), Abs(param, body), App(func, arg), Let(name, value, body)
- Lit(value) — int or bool literals
- BinOp(op, left, right) — +, -, *, ==, <, >, and, or
Algorithm W core (w(env, expr) → (Subst, Type)):
def w(env: TypeEnv, expr: Expr) -> tuple[Subst, Type]:
match expr:
case Var(name=x):
scheme = env[x]
ty = scheme.instantiate() # fresh type variables for each use
return {}, ty
case Abs(param=x, body=e):
beta = TVar(fresh_tvar())
new_env = env | {x: TypeScheme([], beta)}
s1, t1 = w(new_env, e)
return s1, TFun(beta.subst(s1), t1)
case App(func=f, arg=e):
s1, tf = w(env, f)
env2 = apply_subst(env, s1)
s2, ta = w(env2, e)
beta = TVar(fresh_tvar())
s3 = unify(tf.subst(s2), TFun(ta, beta))
return compose(s3, compose(s2, s1)), beta.subst(s3)
case Let(name=x, value=ev, body=eb):
s1, t1 = w(env, ev)
new_env = apply_subst(env, s1)
scheme = TypeScheme.generalize(new_env, t1) # ∀ vars not free in env
new_env[x] = scheme
s2, t2 = w(new_env, eb)
return compose(s2, s1), t2
case Lit(value=v):
return {}, TInt if isinstance(v, int) else TBool
case BinOp(op=op, left=l, right=r):
# unify left and right with expected type (Int or Bool)
# return result type (Int for arith, Bool for comp/bool)
...
Let-polymorphism is implemented via TypeScheme:
- generalize(env, ty): quantifies over type variables that are not free in the environment
- instantiate(): replaces quantified variables with fresh ones on each use
Unification with occurs check:
- unify(t1, t2): structural unification, handles TVar/TCon/TFun
- bind(var, ty): checks occurs condition before creating substitution
- compose(s1, s2): composes substitutions with transitive application
Error reporting: TypeMismatch, OccursCheck, UnboundVariable — all subclasses of TypeError_, providing descriptive messages locating the conflict.
All **63 tests** pass across two test suites: **Built-in tests** (`hm.py` — 16 tests): | Category | Tests | Status | |---|---|---| | Basic abstractions | identity, const | ✓ | | Applications | app_id_int, app_id_id, higher_order | ✓ | | Let polymorphism | poly, poly_chain, usage, skip | ✓ | | Operators | add, lt, and | ✓ | | Type errors | add_mismatch, unbound, apply_nonfunc | ✓ | | Church numerals | church2 (`(a→a)→a→a`) | ✓ | **Comprehensive tests** (`test_hm.py` — 47 tests): | Category | Count | Edge Cases Verified | |---|---|---| | Literals | 3 | Int, Bool, both boolean values | | Abstractions | 3 | identity, const, flip_const | | Applications | 6 | Church 2/3, S combinator | | Let polymorphism | 6 | single use, chain, nested, higher-rank, free var gen | | Binary operators | 11 | arith, compare, bool, nested, mixed | | Type errors | 11 | unbound, mismatched args (both sides), non-func apply, extra arg | | Occurs check | 3 | self-apply, triple self-apply, Y combinator | | Complex | 4 | add/comparison via lambda, compose, twice | **Additional edge cases verified separately** (15 tests): - Nested let bindings, shadowing, `type_infer` helper - Deeply nested applications (3-level currying) - Let-polymorphism with chain of 3 uses (`f (f (f 5))`) - Higher-order let (`apply f x = f x`) - Complex arithmetic with polymorphic identity - Boolean lambdas (`Bool -> Bool -> Bool`) - Correct non-generalization of free vars (`λy.let x=y in x` → `a -> a`) ---
{"model": "deepseek-v4-flash", "result": "completed"}The implementation is in ~/hm.py (~400 lines). It is a full Hindley-Milner type inference engine (Algorithm W) for a simply-typed lambda calculus with let-polymorphism.
Types (class hierarchy with subst, ftv, pprint):
- TVar(id) — type variable (e.g., t0, a)
- TCon(name) — base type constructor (Int, Bool)
- TFun(arg, res) — function type (a -> b)
AST (dataclass sum type Expr):
- Var(name), Abs(param, body), App(func, arg), Let(name, value, body)
- Lit(value) — int or bool literals
- BinOp(op, left, right) — +, -, *, ==, <, >, and, or
Algorithm W core (w(env, expr) → (Subst, Type)):
def w(env: TypeEnv, expr: Expr) -> tuple[Subst, Type]:
match expr:
case Var(name=x):
scheme = env[x]
ty = scheme.instantiate() # fresh type variables for each use
return {}, ty
case Abs(param=x, body=e):
beta = TVar(fresh_tvar())
new_env = env | {x: TypeScheme([], beta)}
s1, t1 = w(new_env, e)
return s1, TFun(beta.subst(s1), t1)
case App(func=f, arg=e):
s1, tf = w(env, f)
env2 = apply_subst(env, s1)
s2, ta = w(env2, e)
beta = TVar(fresh_tvar())
s3 = unify(tf.subst(s2), TFun(ta, beta))
return compose(s3, compose(s2, s1)), beta.subst(s3)
case Let(name=x, value=ev, body=eb):
s1, t1 = w(env, ev)
new_env = apply_subst(env, s1)
scheme = TypeScheme.generalize(new_env, t1) # ∀ vars not free in env
new_env[x] = scheme
s2, t2 = w(new_env, eb)
return compose(s2, s1), t2
case Lit(value=v):
return {}, TInt if isinstance(v, int) else TBool
case BinOp(op=op, left=l, right=r):
# unify left and right with expected type (Int or Bool)
# return result type (Int for arith, Bool for comp/bool)
...
Let-polymorphism is implemented via TypeScheme:
- generalize(env, ty): quantifies over type variables that are not free in the environment
- instantiate(): replaces quantified variables with fresh ones on each use
Unification with occurs check:
- unify(t1, t2): structural unification, handles TVar/TCon/TFun
- bind(var, ty): checks occurs condition before creating substitution
- compose(s1, s2): composes substitutions with transitive application
Error reporting: TypeMismatch, OccursCheck, UnboundVariable — all subclasses of TypeError_, providing descriptive messages locating the conflict.
All **63 tests** pass across two test suites: **Built-in tests** (`hm.py` — 16 tests): | Category | Tests | Status | |---|---|---| | Basic abstractions | identity, const | ✓ | | Applications | app_id_int, app_id_id, higher_order | ✓ | | Let polymorphism | poly, poly_chain, usage, skip | ✓ | | Operators | add, lt, and | ✓ | | Type errors | add_mismatch, unbound, apply_nonfunc | ✓ | | Church numerals | church2 (`(a→a)→a→a`) | ✓ | **Comprehensive tests** (`test_hm.py` — 47 tests): | Category | Count | Edge Cases Verified | |---|---|---| | Literals | 3 | Int, Bool, both boolean values | | Abstractions | 3 | identity, const, flip_const | | Applications | 6 | Church 2/3, S combinator | | Let polymorphism | 6 | single use, chain, nested, higher-rank, free var gen | | Binary operators | 11 | arith, compare, bool, nested, mixed | | Type errors | 11 | unbound, mismatched args (both sides), non-func apply, extra arg | | Occurs check | 3 | self-apply, triple self-apply, Y combinator | | Complex | 4 | add/comparison via lambda, compose, twice | **Additional edge cases verified separately** (15 tests): - Nested let bindings, shadowing, `type_infer` helper - Deeply nested applications (3-level currying) - Let-polymorphism with chain of 3 uses (`f (f (f 5))`) - Higher-order let (`apply f x = f x`) - Complex arithmetic with polymorphic identity - Boolean lambdas (`Bool -> Bool -> Bool`) - Correct non-generalization of free vars (`λy.let x=y in x` → `a -> a`) ---
{"model": "deepseek-v4-flash", "result": "completed"}