LoopyLuci Type System Design
Designing type systems for programming languages — from simple type checkers through generics, traits, dependent types, and type-level computation.
When to Use
- Designing a new programming language or DSL
- Adding a type system to an existing dynamic language
- Implementing type inference, generics, or advanced type features
- Understanding type theory concepts (soundness, completeness, decidability)
- Building static analysis tools that reason about types
Type System Spectrum
| System | Expressiveness | Inference | Complexity | Examples |
|---|---|---|---|---|
| Untyped | None | N/A | Trivial | Assembly, B |
| Simple types | Basic safety | Full | Low | C (basic) |
| Hindley-Milner | Parametric polymorphism | Full (HM) | Medium | ML, Haskell |
| Gradual | Dynamic + static opt-in | Partial | Medium | TypeScript, Python |
| System F | Higher-rank types | Undecidable | High | GHC Haskell |
| Dependent | Values as types | Partial | Very high | Idris, Coq |
| Linear/Substructural | Resource tracking | Limited | High | Rust |
Type Checker Implementation
Base Type System
from dataclasses import dataclass
from typing import Dict, List, Optional, Set
class Type:
"""Base type class."""
pass
@dataclass
class IntType(Type):
pass
@dataclass
class BoolType(Type):
pass
@dataclass
class FunctionType(Type):
param_type: Type
return_type: Type
@dataclass
class TypeVariable(Type):
name: str
@dataclass
class GenericType(Type):
name: str
params: List[Type]
class TypeChecker:
"""Simple type checker for a lambda calculus with let-polymorphism."""
def __init__(self):
self.env = {} # name -> Type
self.constraints = []
def check(self, expr, env=None):
"""Infer/check type of expression."""
if env is None:
env = self.env
# Literals
if isinstance(expr, int):
return IntType()
if isinstance(expr, bool):
return BoolType()
# Variables
if isinstance(expr, str):
if expr in env:
return env[expr]
raise TypeError(f"Unbound variable: {expr}")
# Lambda: λx: T. e
if expr[0] == 'lambda':
_, param, param_type, body = expr
body_type = self.check(body, {**env, param: param_type})
return FunctionType(param_type, body_type)
# Application: e1 e2
if isinstance(expr, tuple) and len(exp) == 2:
fn_type = self.check(exp[0], env)
arg_type = self.check(exp[1], env)
if isinstance(fn_type, FunctionType):
if fn_type.param_type != arg_type:
raise TypeError(f"Type mismatch: expected {fn_type.param_type}, got {arg_type}")
return fn_type.return_type
raise TypeError(f"Expected function, got {fn_type}")
raise ValueError(f"Unknown expression: {expr}")
Hindley-Milner Type Inference
class HindleyMilner:
"""Hindley-Milner type inference with unification."""
def __init__(self):
self.var_counter = 0
self.substitutions = {}
def fresh_var(self):
name = f"t{self.var_counter}"
self.var_counter += 1
return TypeVariable(name)
def unify(self, t1: Type, t2: Type):
"""Unify two types, updating substitutions."""
t1 = self.apply(t1)
t2 = self.apply(t2)
if t1 == t2:
return
if isinstance(t1, TypeVariable):
if self.occurs_check(t1, t2):
raise TypeError(f"Occurs check: {t1} in {t2}")
self.substitutions[t1.name] = t2
return
if isinstance(t2, TypeVariable):
if self.occurs_check(t2, t1):
raise TypeError(f"Occurs check: {t2} in {t1}")
self.substitutions[t2.name] = t1
return
if isinstance(t1, FunctionType) and isinstance(t2, FunctionType):
self.unify(t1.param_type, t2.param_type)
self.unify(t1.return_type, t2.return_type)
return
raise TypeError(f"Cannot unify {t1} with {t2}")
def infer(self, expr, env=None):
"""Infer the type of an expression."""
if env is None:
env = {}
if isinstance(expr, int):
return IntType()
if isinstance(expr, bool):
return BoolType()
if isinstance(expr, str):
if expr not in env:
raise TypeError(f"Unbound: {expr}")
return self.apply(env[expr])
if expr[0] == 'let':
_, var, value, body = expr
# Polymorphic let: generalize then instantiate
var_type = self.infer(value, env)
# Generalize (simplified)
generalized = self.generalize(var_type, env)
env[var] = generalized
return self.infer(body, env)
if expr[0] == 'lambda':
_, param, body = expr
param_type = self.fresh_var()
body_type = self.infer(body, {**env, param: param_type})
return FunctionType(param_type, body_type)
if isinstance(expr, tuple) and len(expr) == 2:
fn_type = self.infer(expr[0], env)
arg_type = self.infer(expr[1], env)
result_type = self.fresh_var()
self.unify(fn_type, FunctionType(arg_type, result_type))
return result_type
Gradual Typing (TypeScript-style)
class GradualTypeChecker:
"""Gradual typing: static + dynamic types with consistency."""
DYNAMIC = TypeVariable("any") # Dynamic type
def consistent(self, t1, t2):
"""Consistency relation: like equality but 'any' matches anything."""
if t1 == self.DYNAMIC or t2 == self.DYNAMIC:
return True
if isinstance(t1, FunctionType) and isinstance(t2, FunctionType):
return self.consistent(t1.param_type, t2.param_type) and \
self.consistent(t1.return_type, t2.return_type)
return t1 == t2
def check_annotation(self, annotated_type, inferred_type):
"""Check annotated type against inferred type with consistency."""
if not self.consistent(annotated_type, inferred_type):
raise TypeError(
f"Type annotation mismatch: declared {annotated_type}, "
f"inferred {inferred_type}"
)
Subtyping
class SubtypeChecker:
"""Structural subtyping (like TypeScript's type compatibility)."""
def is_subtype(self, t1, t2):
"""Is t1 a subtype of t2 (t1 <= t2)?"""
if t1 == t2:
return True
# Top type
if isinstance(t2, Top):
return True
# Bottom type
if isinstance(t1, Bot):
return True
if isinstance(t1, RecordType) and isinstance(t2, RecordType):
# Width subtyping: t1 has all fields of t2 (and possibly more)
for field, field_type in t2.fields.items():
if field not in t1.fields:
return False
if not self.is_subtype(t1.fields[field], field_type):
return False
return True
# Function types (contravariant parameter, covariant return)
if isinstance(t1, FunctionType) and isinstance(t2, FunctionType):
return self.is_subtype(t2.param_type, t1.param_type) and \
self.is_subtype(t1.return_type, t2.return_type)
return False
Common Pitfalls
- Undecidable inference — full type inference for System F is undecidable; restrict to Hindley-Milner or require annotations
- Subtyping + generics — variance matters; get covariance/contravariance/invariance wrong and the type system is unsound
- Gradual typing performance — runtime type checks for gradual types add overhead; optimize hot paths
- Error messages — type errors in complex generic code are cryptic; invest in good error reporting
- Soundness vs. completeness — sound type systems reject some valid programs; trade off for safety
- Recursive types — without equi-recursive or iso-recursive handling, infinite types crash the checker
Verification Checklist
- Type checker passes standard test suite (PLT redex, etc.)
- Soundness: well-typed programs don't have type errors at runtime (progress + preservation)
- Inference terminates on all inputs (no infinite loops)
- Error messages include source location and expected/actual types
- Subtyping is transitive (A <: B, B <: C => A <: C)
- Generic instantiation is correct (no unsound escapes)
- Gradual types degrade gracefully to dynamic checking
See Also
- compiler-interpreter-basics — implementing type checkers in compilers
- formal-verification-methods — type-based verification
- functional-programming-concepts — type systems in FP