# Type System Design Theory > Use when designing programming language type systems. - Skill: `loopyluci/type-system-design-theory` (Agent Skill) - Install (CLI): `npx skillmds@latest add loopyluci/type-system-design-theory` - Raw SKILL.md: https://api.skillmd.com/api/skills/loopyluci/type-system-design-theory/raw - Safety review: pending (external: skill-scanner PASS, skillspector PASS) - Works with: Claude Code, Claude.ai, OpenAI Codex - Category: Coding & Dev Tools - License: MIT - Author: LoopyLuci (https://skillmd.com/u/loopyluci) - Updated: 2026-09-08 - Page: https://skillmd.com/skills/loopyluci/type-system-design-theory --- # 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 ```python 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 ```python 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) ```python 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 ```python 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 1. **Undecidable inference** — full type inference for System F is undecidable; restrict to Hindley-Milner or require annotations 2. **Subtyping + generics** — variance matters; get covariance/contravariance/invariance wrong and the type system is unsound 3. **Gradual typing performance** — runtime type checks for gradual types add overhead; optimize hot paths 4. **Error messages** — type errors in complex generic code are cryptic; invest in good error reporting 5. **Soundness vs. completeness** — sound type systems reject some valid programs; trade off for safety 6. **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