← Back to all projects

LEARN TYPE SYSTEMS

Learn Type Systems: From Zero to Type Theorist

Goal: Deeply understand type systems—from basic type checking through advanced type inference, polymorphism, and dependent types. Build real type checkers and infer types for real languages, understanding both the theory and practice of making programs safer through types.

Why Type Systems Matter

Types are everywhere. Every time a compiler tells you “expected int, got string,” a type system saved you from a runtime crash. But type systems go far deeper:

  • Safety: Catch errors before running code
  • Documentation: Types explain what functions expect and return
  • Optimization: Compilers use types to generate faster code
  • Abstraction: Generic types let you write code once for many types
  • Theorem Proving: Advanced types can prove properties about your programs

After completing these projects, you will:

  • Understand exactly how type checkers work inside compilers
  • Implement type inference from scratch (the magic behind “auto” and “let”)
  • Know when static typing helps and when it gets in the way
  • Appreciate the design tradeoffs in TypeScript, Rust, Haskell, and other typed languages
  • Be able to design type systems for your own languages

Core Concept Analysis

What is a Type?

A type is a classification of values that determines:

  1. What operations are valid on those values
  2. How the values are represented in memory
  3. What properties the values satisfy
Type = Set of values + Allowed operations

Int = {..., -2, -1, 0, 1, 2, ...} + {+, -, *, /, <, >, ==, ...}
Bool = {true, false} + {&&, ||, !, ...}
String = {"", "a", "ab", ...} + {++, length, charAt, ...}

Type System Components

  1. Types: The classifications themselves
    • Base types: Int, Bool, String
    • Compound types: Int -> Bool (functions), List<Int> (generics)
    • Type constructors: List, Maybe, Result (types that take type parameters)
  2. Typing Rules: How to determine what type an expression has
    • If e1 : Int and e2 : Int, then e1 + e2 : Int
    • If f : A -> B and x : A, then f(x) : B
  3. Type Checker: The algorithm that applies typing rules
    • Takes: Abstract Syntax Tree (AST)
    • Returns: Typed AST (or errors)
  4. Type Inference: Deducing types without annotations
    • “You called + on it, so it must be a number”
    • Hindley-Milner: Complete inference for polymorphic types

The Type System Hierarchy

                    Dependent Types
                    (types depend on values)
                         |
              Polymorphic Types + Effects
              (generics, linear types, effect systems)
                         |
               Polymorphic Types
               (List<T>, Option<T>)
                         |
              Simple Types + Subtyping
              (OOP, structural typing)
                         |
                   Simple Types
                   (Int, Bool, Int -> Bool)
                         |
                     Untyped
                     (pure lambda calculus)

Key Type System Properties

  1. Soundness: If it type checks, it won’t have type errors at runtime
    • “Well-typed programs don’t go wrong” — Robin Milner
  2. Completeness: If a program is valid, the type checker accepts it
    • Undecidable for complex type systems
  3. Decidability: Type checking terminates
    • Simply-typed: Always
    • With polymorphism: Usually
    • With dependent types: Sometimes
  4. Principal Types: There exists a most general type
    • id has type ∀a. a -> a, not Int -> Int

Static vs Dynamic Typing

Static Typing Dynamic Typing
Types checked at compile time Types checked at runtime
Errors caught early Errors caught late
Requires type annotations (sometimes) No annotations needed
Can limit expressiveness Maximum flexibility
Examples: C, Java, Haskell, Rust Examples: Python, JavaScript, Ruby

Gradual Typing: The best of both worlds (TypeScript, Python with mypy)

Project List

Projects progress from fundamental concepts to advanced type theory. Each project builds a working type system component.

Project 1: Type Checker for a Calculator Language

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Python
  • Alternative Programming Languages: OCaml, Haskell, Rust
  • Coolness Level: Level 2: Practical but Forgettable
  • Business Potential: 1. The “Resume Gold”
  • Difficulty: Level 1: Beginner
  • Knowledge Area: Type Checking / AST
  • Software or Tool: Type Checker
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapters 1-3)

What you’ll build: A type checker for a simple expression language with integers, booleans, and conditionals. It will reject programs like if 5 then 1 else 2 (condition must be boolean) and 1 + true (can’t add int and bool).

Why it teaches type checking: This is the minimal viable type checker. You’ll understand the fundamental algorithm: traverse the AST, apply typing rules, report errors. Every type checker—from GCC to TypeScript—uses this same core idea.

Core challenges you’ll face:

  • Representing types as data → maps to designing type representations
  • Traversing the AST → maps to recursive type checking
  • Reporting useful errors → maps to error message design
  • Handling conditionals → maps to type equality checking

Key Concepts:

  • Abstract Syntax Trees: “Crafting Interpreters” Chapter 5 - Robert Nystrom
  • Typing Rules: “Types and Programming Languages” Chapter 3 - Benjamin C. Pierce
  • Recursive Descent: “Compilers: Principles and Practice” Chapter 3 - Parag Dave

Difficulty: Beginner Time estimate: Weekend Prerequisites: Basic programming, understanding of recursion. Familiarity with trees helpful but not required.

Real world outcome:

$ ./typechecker "1 + 2 * 3"
Type: Int

$ ./typechecker "true && false"
Type: Bool

$ ./typechecker "if true then 1 else 2"
Type: Int

$ ./typechecker "if 5 then 1 else 2"
Error at position 3: Expected Bool in condition, found Int
  if 5 then 1 else 2
     ^

$ ./typechecker "1 + true"
Error at position 4: Cannot apply + to Int and Bool
  1 + true
      ^^^^

$ ./typechecker "(1 < 2) && (3 > 4)"
Type: Bool

Implementation Hints:

Start with a simple AST:

Expr = Num(int)
     | Bool(bool)
     | BinOp(op, Expr, Expr)    -- op is +, -, *, /, <, >, ==, &&, ||
     | If(Expr, Expr, Expr)      -- if cond then e1 else e2

Type representation:

Type = TInt
     | TBool

The type checking function (pseudocode):

typecheck(expr) -> Type:
    match expr:
        Num(_):
            return TInt

        Bool(_):
            return TBool

        BinOp(op, left, right):
            t1 = typecheck(left)
            t2 = typecheck(right)
            if op in [+, -, *, /]:
                if t1 != TInt or t2 != TInt:
                    error("Expected Int operands")
                return TInt
            if op in [<, >, ==]:
                if t1 != t2:
                    error("Operands must have same type")
                return TBool
            if op in [&&, ||]:
                if t1 != TBool or t2 != TBool:
                    error("Expected Bool operands")
                return TBool

        If(cond, then_branch, else_branch):
            t_cond = typecheck(cond)
            if t_cond != TBool:
                error("Condition must be Bool")
            t_then = typecheck(then_branch)
            t_else = typecheck(else_branch)
            if t_then != t_else:
                error("Branches must have same type")
            return t_then

Implementation steps:

  1. Define the AST types (can use Python dataclasses or named tuples)
  2. Write a simple parser (or hardcode ASTs for testing)
  3. Implement typecheck as a recursive function
  4. Add error messages with source positions
  5. Test with valid and invalid programs

Learning milestones:

  1. AST representation works → You understand how compilers see code
  2. Basic expressions type check → You understand typing rules
  3. If-expressions work → You understand type equality
  4. Error messages are helpful → You understand user experience

Project 2: Type Checker with Functions and Variables

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Python
  • Alternative Programming Languages: OCaml, Haskell, TypeScript
  • Coolness Level: Level 3: Genuinely Clever
  • Business Potential: 1. The “Resume Gold”
  • Difficulty: Level 2: Intermediate
  • Knowledge Area: Type Environments / Lambda Calculus
  • Software or Tool: Functional Language Type Checker
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapters 8-9)

What you’ll build: Extend your type checker to support variables, let-bindings, and functions. This introduces the critical concept of a type environment (Γ, “gamma”) that tracks what variables are in scope and what their types are.

Why it teaches type environments: Real type checkers must handle scope. When you write let x = 5 in x + 1, the type checker must know that x is an Int inside the body. The type environment is how this works—it’s the “memory” of the type checker.

Core challenges you’ll face:

  • Managing the type environment → maps to scope and shadowing
  • Function types (A -> B) → maps to higher-order type reasoning
  • Lambda expressions → maps to introducing new bindings
  • Function application → maps to checking argument types

Key Concepts:

  • Type Environments: “Types and Programming Languages” Chapter 9 - Benjamin C. Pierce
  • Simply-Typed Lambda Calculus: Stanford CS 242 Lectures
  • Function Types: “Types and Programming Languages” Chapter 9.1 - Pierce

Difficulty: Intermediate Time estimate: 1 week Prerequisites: Project 1 completed. Familiarity with lambda expressions helpful.

Real world outcome:

$ ./typechecker "let x = 5 in x + 1"
Type: Int

$ ./typechecker "let f = (fn x: Int => x + 1) in f(10)"
Type: Int

$ ./typechecker "fn x: Int => fn y: Int => x + y"
Type: Int -> Int -> Int

$ ./typechecker "(fn x: Int => x + 1)(true)"
Error: Expected Int, found Bool in function argument
  (fn x: Int => x + 1)(true)
                       ^^^^

$ ./typechecker "let x = 5 in y"
Error: Undefined variable 'y'
  let x = 5 in y
               ^

$ ./typechecker "
  let add = fn x: Int => fn y: Int => x + y in
  let add5 = add(5) in
  add5(10)
"
Type: Int

Implementation Hints:

Extended AST:

Expr = ... (from Project 1)
     | Var(name)                           -- variable reference
     | Let(name, Expr, Expr)               -- let name = e1 in e2
     | Lambda(name, Type, Expr)            -- fn name: Type => body
     | App(Expr, Expr)                     -- function application

Extended types:

Type = TInt
     | TBool
     | TFun(Type, Type)    -- T1 -> T2

The type environment:

Env = Dict[str, Type]   -- maps variable names to types

Type checking with environments (pseudocode):

typecheck(env, expr) -> Type:
    match expr:
        Var(name):
            if name not in env:
                error(f"Undefined variable '{name}'")
            return env[name]

        Let(name, value, body):
            t_value = typecheck(env, value)
            new_env = env.copy()
            new_env[name] = t_value
            return typecheck(new_env, body)

        Lambda(param_name, param_type, body):
            new_env = env.copy()
            new_env[param_name] = param_type
            t_body = typecheck(new_env, body)
            return TFun(param_type, t_body)

        App(func, arg):
            t_func = typecheck(env, func)
            if not isinstance(t_func, TFun):
                error("Expected function type")
            t_arg = typecheck(env, arg)
            if t_arg != t_func.param_type:
                error(f"Expected {t_func.param_type}, found {t_arg}")
            return t_func.return_type

        # ... other cases from Project 1, but pass env through

Key insight: The environment is immutable from the caller’s perspective. When you add a binding, you create a new environment; the old one isn’t modified. This naturally handles shadowing:

let x = 5 in         -- env = {x: Int}
  let x = true in    -- new_env = {x: Bool}
    x                -- looks up x in new_env, gets Bool

Learning milestones:

  1. Variables resolve correctly → You understand environment lookup
  2. Let-bindings work → You understand scope extension
  3. Lambdas have function types → You understand function type construction
  4. Application checks argument types → You understand function type elimination
  5. Curried functions work → You understand higher-order functions

Project 3: Hindley-Milner Type Inference Engine

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: OCaml
  • Alternative Programming Languages: Haskell, Python, Rust
  • Coolness Level: Level 5: Pure Magic (Super Cool)
  • Business Potential: 4. The “Open Core” Infrastructure
  • Difficulty: Level 4: Expert
  • Knowledge Area: Type Inference / Unification
  • Software or Tool: Type Inference Engine
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapter 22)

What you’ll build: A complete Hindley-Milner type inference engine that can determine the types of expressions without any type annotations. This is the magic behind Haskell’s and OCaml’s type inference.

Why it teaches type inference: This is where type systems become truly beautiful. The algorithm discovers the “most general type” (principal type) through constraint solving. Understanding Hindley-Milner unlocks how modern functional language compilers work.

Core challenges you’ll face:

  • Generating type variables → maps to placeholder types
  • Generating constraints → maps to what must equal what
  • Unification algorithm → maps to solving type equations
  • Generalization and instantiation → maps to polymorphism
  • The occurs check → maps to preventing infinite types

Resources for key challenges:

Key Concepts:

  • Unification: “Types and Programming Languages” Chapter 22 - Benjamin C. Pierce
  • Algorithm W: Wikipedia - Hindley-Milner Type System
  • Let-Polymorphism: “Types and Programming Languages” Chapter 22.7 - Pierce

Difficulty: Expert Time estimate: 2-3 weeks Prerequisites: Project 2 completed. Familiarity with substitution and equational reasoning. OCaml or Haskell recommended (Python works but is more verbose).

Real world outcome:

$ ./infer "fn x => x"
Inferred type: 'a -> 'a

$ ./infer "fn x => x + 1"
Inferred type: Int -> Int

$ ./infer "fn f => fn x => f(f(x))"
Inferred type: ('a -> 'a) -> 'a -> 'a

$ ./infer "let id = fn x => x in (id(5), id(true))"
Inferred type: (Int, Bool)

$ ./infer "fn x => x(x)"
Error: Cannot construct infinite type: 'a = 'a -> 'b
       (occurs check failed)

$ ./infer "let compose = fn f => fn g => fn x => f(g(x)) in compose"
Inferred type: ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b

$ ./infer "
  let fix = fn f =>
    let g = fn x => f(fn v => x(x)(v)) in
    g(g)
  in fix
"
Inferred type: (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b

Implementation Hints:

The Hindley-Milner algorithm has three phases:

Phase 1: Generate fresh type variables Every expression gets a type variable. Every time you encounter a polymorphic value, create fresh instances.

Type = TInt
     | TBool
     | TVar(name)               -- Type variable: 'a, 'b, etc.
     | TFun(Type, Type)
     | TForall([names], Type)   -- Polymorphic: ∀a b. a -> b -> a

fresh_var() -> TVar:
    global counter
    counter += 1
    return TVar(f"'t{counter}")

Phase 2: Generate constraints Walk the AST and generate equations that must hold.

infer(env, expr) -> (Type, Constraints):
    match expr:
        Num(_):
            return (TInt, [])

        Var(name):
            scheme = env[name]
            return (instantiate(scheme), [])  # Fresh type vars for polymorphic types

        Lambda(param, body):
            param_type = fresh_var()
            new_env = env + {param: param_type}  # No generalization here!
            (body_type, constraints) = infer(new_env, body)
            return (TFun(param_type, body_type), constraints)

        App(func, arg):
            (t_func, c1) = infer(env, func)
            (t_arg, c2) = infer(env, arg)
            result_type = fresh_var()
            new_constraint = (t_func, TFun(t_arg, result_type))
            return (result_type, c1 + c2 + [new_constraint])

        Let(name, value, body):
            (t_value, c1) = infer(env, value)
            subst = unify(c1)
            t_value = apply_subst(subst, t_value)
            scheme = generalize(env, t_value)  # Polymorphism happens here!
            new_env = env + {name: scheme}
            (t_body, c2) = infer(new_env, body)
            return (t_body, c2)

Phase 3: Unification (solving constraints)

unify(constraints) -> Substitution:
    subst = {}
    for (t1, t2) in constraints:
        t1 = apply_subst(subst, t1)
        t2 = apply_subst(subst, t2)
        subst = compose(subst, unify_one(t1, t2))
    return subst

unify_one(t1, t2) -> Substitution:
    if t1 == t2:
        return {}

    if t1 is TVar:
        if occurs(t1, t2):  # Occurs check!
            error("Infinite type")
        return {t1.name: t2}

    if t2 is TVar:
        return unify_one(t2, t1)

    if t1 is TFun and t2 is TFun:
        s1 = unify_one(t1.param, t2.param)
        s2 = unify_one(apply(s1, t1.result), apply(s1, t2.result))
        return compose(s1, s2)

    error(f"Cannot unify {t1} and {t2}")

Generalization and Instantiation:

generalize(env, type) -> Scheme:
    # Free variables in type that are NOT free in env become bound
    free_in_type = free_vars(type)
    free_in_env = union(free_vars(t) for t in env.values())
    to_generalize = free_in_type - free_in_env
    return TForall(to_generalize, type)

instantiate(scheme) -> Type:
    # Replace bound variables with fresh ones
    fresh = {name: fresh_var() for name in scheme.bound_vars}
    return substitute(scheme.body, fresh)

The key insight: let generalizes (creates polymorphism), but lambda parameters don’t. This is why:

  • let id = fn x => x in (id 5, id true) works (id is polymorphic)
  • (fn id => (id 5, id true))(fn x => x) fails (id has one concrete type)

Learning milestones:

  1. Simple expressions infer correctly → You understand constraint generation
  2. Unification produces substitutions → You understand solving
  3. The identity function gets ‘a -> ‘a → You understand type variables
  4. Let-polymorphism works → You understand generalization/instantiation
  5. Occurs check catches infinite types → You understand the soundness check

Project 4: Algebraic Data Types and Pattern Matching

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Haskell
  • Alternative Programming Languages: OCaml, Rust, Scala
  • Coolness Level: Level 4: Hardcore Tech Flex
  • Business Potential: 3. The “Service & Support” Model
  • Difficulty: Level 3: Advanced
  • Knowledge Area: ADTs / Pattern Matching / Exhaustiveness
  • Software or Tool: ADT Type Checker
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapter 11)

What you’ll build: Extend your type system with user-defined algebraic data types (sum types and product types) and pattern matching with exhaustiveness checking.

Why it teaches ADTs: Algebraic data types are the cornerstone of typed functional programming. Understanding how to type check Option<T>, Result<T, E>, and custom data types unlocks how Rust, Haskell, and modern languages handle data.

Core challenges you’ll face:

  • Representing type definitions → maps to type constructors and data constructors
  • Type checking constructors → maps to instantiating polymorphic types
  • Pattern matching → maps to introducing variables and checking coverage
  • Exhaustiveness checking → maps to ensuring all cases are handled

Key Concepts:

  • Sum and Product Types: “Types and Programming Languages” Chapter 11 - Pierce
  • Pattern Matching: OCaml from the Ground Up - Algebraic Types
  • Exhaustiveness: “The Implementation of Functional Programming Languages” - Simon Peyton Jones

Difficulty: Advanced Time estimate: 2-3 weeks Prerequisites: Project 3 completed. Familiarity with ML-family languages helpful.

Real world outcome:

$ ./typechecker "
type Option<T> = None | Some(T)

let map = fn f => fn opt =>
  match opt with
  | None => None
  | Some(x) => Some(f(x))
in
  map(fn x => x + 1)(Some(5))
"
Type: Option<Int>

$ ./typechecker "
type List<T> = Nil | Cons(T, List<T>)

let rec length = fn list =>
  match list with
  | Nil => 0
  | Cons(_, tail) => 1 + length(tail)
in
  length(Cons(1, Cons(2, Cons(3, Nil))))
"
Type: Int

$ ./typechecker "
type Bool = True | False

let not = fn b =>
  match b with
  | True => False
"
Warning: Non-exhaustive pattern match
  Missing case: False

$ ./typechecker "
type Result<T, E> = Ok(T) | Err(E)

let unwrap = fn result =>
  match result with
  | Ok(x) => x
"
Error: Non-exhaustive pattern match
  Missing case: Err(_)
  This match does not have type T because the Err case is unhandled

Implementation Hints:

Extended type representation:

Type = ... (from before)
     | TApp(TypeConstructor, [Type])   -- Option<Int>, List<String>
     | TConstructor(name)               -- Just the name before application

TypeDef = {
    name: str,                          -- "Option"
    params: [str],                      -- ["T"]
    constructors: [(name, [Type])]      -- [("None", []), ("Some", [TVar("T")])]
}

Type environment now includes type definitions:

Env = {
    variables: Dict[str, Type],
    types: Dict[str, TypeDef],
    constructors: Dict[str, (TypeDef, int)]  -- Constructor name -> (typedef, variant index)
}

Type checking a constructor:

typecheck(env, Constructor(name, args)):
    (typedef, _) = env.constructors[name]
    # Find the constructor definition
    (_, param_types) = find_constructor(typedef, name)

    # Instantiate type parameters with fresh variables
    fresh = {p: fresh_var() for p in typedef.params}
    instantiated_params = [substitute(t, fresh) for t in param_types]

    # Check arguments
    for (arg, expected) in zip(args, instantiated_params):
        actual = typecheck(env, arg)
        unify(actual, expected)

    # Return the constructed type
    return TApp(typedef.name, [fresh[p] for p in typedef.params])

Pattern matching:

typecheck(env, Match(scrutinee, cases)):
    t_scrutinee = typecheck(env, scrutinee)
    result_type = fresh_var()

    for (pattern, body) in cases:
        # Pattern introduces bindings
        (pattern_type, bindings) = check_pattern(env, pattern)
        unify(t_scrutinee, pattern_type)

        # Type check body with new bindings
        new_env = env.extend(bindings)
        t_body = typecheck(new_env, body)
        unify(result_type, t_body)

    # Exhaustiveness check (see below)
    check_exhaustive(env, t_scrutinee, [p for (p, _) in cases])

    return result_type

Exhaustiveness checking (simplified):

check_exhaustive(env, type, patterns):
    typedef = get_typedef(env, type)
    covered = set()

    for pattern in patterns:
        match pattern:
            PWildcard or PVar(_):
                return  # Catches everything

            PConstructor(name, _):
                covered.add(name)

    all_constructors = {c[0] for c in typedef.constructors}
    missing = all_constructors - covered

    if missing:
        warning(f"Missing cases: {missing}")

Learning milestones:

  1. Type definitions parse and store → You understand type representations
  2. Constructors type check → You understand polymorphic instantiation
  3. Pattern matching binds variables → You understand pattern typing
  4. Exhaustiveness warnings work → You understand coverage analysis
  5. Recursive types (List) work → You understand type recursion

Project 5: Parametric Polymorphism (Generics) System

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: TypeScript
  • Alternative Programming Languages: Rust, Java, C#
  • Coolness Level: Level 4: Hardcore Tech Flex
  • Business Potential: 4. The “Open Core” Infrastructure
  • Difficulty: Level 3: Advanced
  • Knowledge Area: Generics / Parametric Polymorphism
  • Software or Tool: Generic Type Checker
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapter 23)

What you’ll build: A type system with explicit generic type parameters, constraints (bounds), and variance annotations—similar to Java/C#/TypeScript generics.

Why it teaches generics: While HM gives you polymorphism for free, mainstream languages use explicit generics with constraints. Understanding how <T extends Comparable> works is essential for typed OOP languages.

Core challenges you’ll face:

  • Type parameter scope → maps to where type variables are valid
  • Generic instantiation → maps to substituting type arguments
  • Constraints/bounds → maps to T extends X
  • Variance → maps to covariance, contravariance, invariance

Key Concepts:

  • System F: “Types and Programming Languages” Chapter 23 - Pierce
  • Bounded Quantification: “Types and Programming Languages” Chapter 26 - Pierce
  • Variance: TypeScript Handbook - Generics

Difficulty: Advanced Time estimate: 2-3 weeks Prerequisites: Project 2-3 completed. Familiarity with Java/TypeScript generics helpful.

Real world outcome:

$ ./typechecker "
interface Comparable<T> {
  compareTo(other: T): Int
}

function max<T extends Comparable<T>>(a: T, b: T): T {
  if (a.compareTo(b) > 0) {
    return a
  } else {
    return b
  }
}

class IntWrapper implements Comparable<IntWrapper> {
  value: Int
  compareTo(other: IntWrapper): Int {
    return this.value - other.value
  }
}

max<IntWrapper>(new IntWrapper(5), new IntWrapper(3))
"
Type: IntWrapper

$ ./typechecker "
function identity<T>(x: T): T {
  return x
}

identity<Int>(5)
identity<String>(\"hello\")
identity(true)  // Type argument inferred
"
Types: Int, String, Bool

$ ./typechecker "
class Box<T> {
  value: T
  map<U>(f: (T) => U): Box<U> {
    return new Box<U>(f(this.value))
  }
}

new Box<Int>(5).map<String>(fn x => x.toString())
"
Type: Box<String>

$ ./typechecker "
function broken<T>(x: T): T {
  return 5  // Error!
}
"
Error: Expected T, found Int
  return 5
         ^

Implementation Hints:

Type representation with bounds:

Type = TInt | TBool | TString
     | TVar(name, bound?)         -- T, T extends X
     | TFun(params, return_type)
     | TGeneric(params, body)     -- <T>(...) => body
     | TApp(generic, args)        -- Box<Int>
     | TInterface(name, methods)

Type parameter environment:

Env = {
    vars: Dict[str, Type],
    type_params: Dict[str, Type?],  -- name -> bound (or None for unbounded)
}

Checking generic function definition:

typecheck_generic_function(env, params, bounds, body):
    # Add type parameters to environment
    new_env = env.copy()
    for (param, bound) in zip(params, bounds):
        new_env.type_params[param] = bound

    # Type check body with type parameters in scope
    return_type = typecheck(new_env, body)

    return TGeneric(params, TFun(..., return_type))

Checking generic instantiation:

typecheck_instantiation(env, generic_type, type_args):
    if len(type_args) != len(generic_type.params):
        error("Wrong number of type arguments")

    # Check bounds
    for (arg, (param, bound)) in zip(type_args, generic_type.params):
        if bound and not satisfies_bound(arg, bound):
            error(f"{arg} does not satisfy bound {bound}")

    # Substitute
    return substitute(generic_type.body, dict(zip(generic_type.params, type_args)))

Variance (for containers like Box<T>):

Covariant (+T):     Box<Dog> <: Box<Animal>  (if Dog <: Animal)
Contravariant (-T): Handler<Animal> <: Handler<Dog>
Invariant (T):      MutableBox<Dog> is not related to MutableBox<Animal>

Rule: Read-only positions are covariant, write-only are contravariant,
      read-write are invariant.

Learning milestones:

  1. Generic functions work → You understand parametric polymorphism
  2. Bounds restrict type arguments → You understand constrained generics
  3. Generic classes work → You understand type constructor polymorphism
  4. Variance is checked → You understand subtyping with generics
  5. Inference fills in type args → You understand local type inference

Project 6: Subtyping and Structural Typing

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: TypeScript
  • Alternative Programming Languages: Scala, OCaml (modules)
  • Coolness Level: Level 4: Hardcore Tech Flex
  • Business Potential: 3. The “Service & Support” Model
  • Difficulty: Level 3: Advanced
  • Knowledge Area: Subtyping / OOP Types
  • Software or Tool: Structural Type Checker
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapters 15-17)

What you’ll build: A type checker with subtyping relationships, supporting both nominal (class-based) and structural (shape-based) typing, like TypeScript’s type system.

Why it teaches subtyping: Subtyping is fundamental to OOP. When can you pass a Dog where an Animal is expected? Why are function types contravariant in their arguments? This project answers these questions.

Core challenges you’ll face:

  • Subtype relation → maps to when is A <: B
  • Structural vs nominal → maps to name-based vs shape-based
  • Function subtyping → maps to contravariant inputs, covariant outputs
  • Width and depth subtyping → maps to extra fields, more specific fields
  • Least upper bound → maps to type joins for if-expressions

Key Concepts:

  • Subtyping: “Types and Programming Languages” Chapter 15 - Pierce
  • Structural Types: TypeScript Handbook
  • Variance in Subtyping: “Types and Programming Languages” Chapter 15.5 - Pierce

Difficulty: Advanced Time estimate: 2-3 weeks Prerequisites: Project 5 completed. Understanding of OOP concepts.

Real world outcome:

$ ./typechecker "
type Animal = { name: String }
type Dog = { name: String, breed: String }

let greet = fn (animal: Animal) => 'Hello, ' + animal.name

let fido: Dog = { name: 'Fido', breed: 'Labrador' }
greet(fido)  // OK: Dog <: Animal (width subtyping)
"
Type: String

$ ./typechecker "
type Handler<T> = { handle: (T) => Void }

let animalHandler: Handler<Animal> = { handle: fn a => print(a.name) }
let dogHandler: Handler<Dog> = animalHandler  // OK: contravariance
"
Type: Handler<Dog>

$ ./typechecker "
type ReadonlyBox<T> = { get: () => T }
type MutableBox<T> = { get: () => T, set: (T) => Void }

let rb: ReadonlyBox<Animal> = mutableDogBox  // Error!
"
Error: MutableBox<Dog> is not a subtype of ReadonlyBox<Animal>
  The 'set' method makes T invariant, not covariant

$ ./typechecker "
let x = if someCondition then 5 else 'hello'
"
Type: Int | String  // Union type (least upper bound)

$ ./typechecker "
type Point2D = { x: Int, y: Int }
type Point3D = { x: Int, y: Int, z: Int }

let p: Point2D = { x: 1, y: 2, z: 3 }  // Structural: OK, extra field ignored
"
Type: Point2D

Implementation Hints:

Subtype relation (recursive):

is_subtype(sub, super) -> bool:
    # Reflexivity
    if sub == super:
        return True

    # Records: width and depth subtyping
    if sub is TRecord and super is TRecord:
        # sub must have all fields of super
        for (name, super_type) in super.fields:
            if name not in sub.fields:
                return False
            if not is_subtype(sub.fields[name], super_type):
                return False
        return True

    # Functions: contravariant in parameter, covariant in return
    if sub is TFun and super is TFun:
        return (is_subtype(super.param, sub.param) and    # Contravariant!
                is_subtype(sub.return, super.return))     # Covariant

    # Generics: depends on variance annotations
    if sub is TApp and super is TApp:
        if sub.constructor != super.constructor:
            return False
        for (s, p, variance) in zip(sub.args, super.args, constructor.variances):
            if variance == COVARIANT:
                if not is_subtype(s, p): return False
            elif variance == CONTRAVARIANT:
                if not is_subtype(p, s): return False
            else:  # INVARIANT
                if s != p: return False
        return True

    return False

Type checking with subtyping:

typecheck(env, App(func, arg)):
    t_func = typecheck(env, func)
    t_arg = typecheck(env, arg)

    if not is_subtype(t_arg, t_func.param):  # Changed from equality!
        error(f"Expected {t_func.param}, found {t_arg}")

    return t_func.return

Least upper bound (for if-expressions):

lub(t1, t2) -> Type:
    if is_subtype(t1, t2):
        return t2
    if is_subtype(t2, t1):
        return t1

    # Neither is a subtype of the other -> union type
    return TUnion(t1, t2)

Learning milestones:

  1. Width subtyping works → You understand structural subtyping
  2. Depth subtyping works → You understand field type refinement
  3. Function subtyping is contravariant → You understand the hard part
  4. if-expressions compute LUB → You understand type joins
  5. Variance is enforced → You understand generic subtyping

Project 7: Recursive Types and Type Operators

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: OCaml
  • Alternative Programming Languages: Haskell, Rust
  • Coolness Level: Level 4: Hardcore Tech Flex
  • Business Potential: 1. The “Resume Gold”
  • Difficulty: Level 4: Expert
  • Knowledge Area: Recursive Types / Type-Level Programming
  • Software or Tool: Recursive Type System
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapters 20-21)

What you’ll build: A type system supporting recursive types (like List that refers to itself), iso-recursive vs equi-recursive semantics, and higher-kinded types (type constructors that take type constructors).

Why it teaches recursive types: How does type List = Nil | Cons(Int, List) work without infinite regress? Understanding recursive types is essential for understanding any data structure more complex than a primitive.

Core challenges you’ll face:

  • Representing recursive types → maps to μ notation or named recursion
  • Iso-recursive vs equi-recursive → maps to explicit fold/unfold vs implicit
  • Checking type equality → maps to coinductive reasoning
  • Higher-kinded types → maps to types of type constructors

Key Concepts:

  • Recursive Types: “Types and Programming Languages” Chapter 20 - Pierce
  • Iso vs Equi-recursive: “Types and Programming Languages” Chapter 21 - Pierce
  • Type Operators: “Types and Programming Languages” Chapter 29 - Pierce

Difficulty: Expert Time estimate: 2-3 weeks Prerequisites: Projects 3-4 completed. Comfort with μ notation.

Real world outcome:

$ ./typechecker "
type List<T> = μL. Unit + (T × L)

let nil: List<Int> = fold[List<Int>](inl(()))
let cons = fn (x: Int) => fn (xs: List<Int>) =>
  fold[List<Int>](inr((x, xs)))

let rec length: List<Int> -> Int = fn xs =>
  case unfold(xs) of
  | inl(_) => 0
  | inr((_, tail)) => 1 + length(tail)
"
Type: List<Int> -> Int

$ ./typechecker "
// Higher-kinded type: Functor takes a type constructor (* -> *)
type Functor<F<_>> = {
  map: forall A B. (A -> B) -> F<A> -> F<B>
}

let listFunctor: Functor<List> = {
  map = fn f => fn xs => ...
}
"
Type: Functor<List>

$ ./typechecker "
// Equi-recursive: these types are considered equal
type A = { x: Int, next: A }
type B = { x: Int, next: { x: Int, next: B } }

let a: A = ...
let b: B = a  // OK with equi-recursive
"
Type OK (equi-recursive interpretation)

Implementation Hints:

Recursive type representation (iso-recursive):

Type = ...
     | TRec(name, body)    -- μX. body (X can appear in body)
     | TRecRef(name)       -- Reference to recursion variable

Example: List<T> = μL. Unit + (T × L)
         TRec("L", TSum(TUnit, TProd(T, TRecRef("L"))))

Fold and unfold (iso-recursive):

unfold(μX. T) = T[X := μX. T]    -- Substitute the whole type for X
fold(μX. T) creates μX. T from T[X := μX. T]

typecheck(Fold(type, expr)):
    expected_unfolded = substitute(type.body, type.name, type)
    actual = typecheck(expr)
    if actual != expected_unfolded:
        error("Type mismatch in fold")
    return type

typecheck(Unfold(expr)):
    t = typecheck(expr)
    if not isinstance(t, TRec):
        error("Expected recursive type")
    return substitute(t.body, t.name, t)

Type equality with recursive types (equi-recursive):

// Use coinduction: types are equal if they "unfold" the same way forever
types_equal(t1, t2, seen=set()) -> bool:
    // Check for cycles
    key = (t1, t2)
    if key in seen:
        return True  // Coinductive hypothesis
    seen = seen | {key}

    // Unfold recursive types
    t1 = unfold_head(t1)
    t2 = unfold_head(t2)

    // Structural comparison
    match (t1, t2):
        (TInt, TInt): return True
        (TFun(a1, r1), TFun(a2, r2)):
            return types_equal(a1, a2, seen) and types_equal(r1, r2, seen)
        ...

Higher-kinded types:

Kind = * | Kind -> Kind

* = type of types (Int, Bool, String)
* -> * = type of type constructors (List, Option)
* -> * -> * = type of binary type constructors (Either, Map)

Kind checking:

kind_check(env, type) -> Kind:
    match type:
        TInt, TBool, ...:
            return KStar  -- *

        TFun(param, result):
            check kind_check(param) == KStar
            check kind_check(result) == KStar
            return KStar  -- * (functions are types)

        TApp(constructor, args):
            k_ctor = kind_check(constructor)
            for arg in args:
                if not isinstance(k_ctor, KArrow):
                    error("Too many type arguments")
                check kind_check(arg) == k_ctor.param
                k_ctor = k_ctor.result
            return k_ctor

        TLambda(param, body):  -- Type-level lambda!
            new_env = env + {param: param_kind}
            k_body = kind_check(new_env, body)
            return KArrow(param_kind, k_body)

Learning milestones:

  1. Recursive types represent properly → You understand μ notation
  2. Fold/unfold work → You understand iso-recursive semantics
  3. Type equality handles cycles → You understand coinduction
  4. Kind checking works → You understand the type of types
  5. Higher-kinded types work → You understand type-level functions

Project 8: Gradual Typing System

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Python
  • Alternative Programming Languages: TypeScript, Racket
  • Coolness Level: Level 4: Hardcore Tech Flex
  • Business Potential: 4. The “Open Core” Infrastructure
  • Difficulty: Level 3: Advanced
  • Knowledge Area: Gradual Typing / Dynamic-Static Boundary
  • Software or Tool: Gradual Type Checker (like mypy)
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce + Jeremy Siek’s papers

What you’ll build: A type system that allows mixing typed and untyped code, with the Any type that’s compatible with everything. Like TypeScript or Python with mypy.

Why it teaches gradual typing: Real-world codebases can’t be fully typed overnight. Gradual typing lets you add types incrementally. Understanding how Any interacts with other types is essential for TypeScript/Python developers.

Core challenges you’ll face:

  • The Any type → maps to the dynamic type that matches everything
  • Consistency relation → maps to when types are “compatible”
  • Runtime checks → maps to dynamic casts at boundaries
  • Blame tracking → maps to which code caused runtime errors

Resources for key challenges:

Key Concepts:

  • Gradual Typing: Jeremy Siek’s original papers
  • Consistency: “Gradual Typing for Functional Languages” - Siek & Taha
  • Blame Calculus: “Blame for All” - Wadler & Findler

Difficulty: Advanced Time estimate: 2-3 weeks Prerequisites: Project 2 completed. Familiarity with TypeScript or Python type hints.

Real world outcome:

$ ./gradual "
// Fully typed code
let add = fn (x: Int, y: Int): Int => x + y
add(1, 2)
"
Type: Int (fully static)

$ ./gradual "
// Untyped code
let add = fn (x, y) => x + y
add(1, 2)
add('a', 'b')  // Also OK - no type checking
"
Type: Any (fully dynamic)

$ ./gradual "
// Gradually typed: typed function called with untyped value
let typed_add = fn (x: Int, y: Int): Int => x + y
let untyped_value: Any = get_input()
typed_add(untyped_value, 5)
"
Type: Int
Warning: Runtime cast from Any to Int at line 4
         If untyped_value is not an Int, this will fail at runtime

$ ./gradual "
// Migration path
let old_code = fn (x) => x.name  // Returns Any

// New typed code calling old
let process: (Person) => String = fn (p) =>
  old_code(p)  // Warning: Any flowing into String
"
Type OK with warnings about Any->String boundary

$ ./gradual "
// Runtime type error tracking
let f: (Int) => Int = fn x => x + 1
let g: Any = f
let h: (String) => String = g  // OK at compile time (Any is flexible)
h('hello')  // Runtime error: expected Int, got String
            // Blame: line 3 (the bad cast)
"
Runtime Error: Type mismatch
  Expected: Int, Got: String
  Blame: Cast from (Int -> Int) to (String -> String) at line 3

Implementation Hints:

Type with Any:

Type = TInt | TBool | TString
     | TFun(Type, Type)
     | TAny              -- The dynamic type

Consistency relation (≈) instead of equality:

consistent(t1, t2) -> bool:
    // Any is consistent with everything
    if t1 == TAny or t2 == TAny:
        return True

    // Otherwise, structural
    if t1 is TInt and t2 is TInt:
        return True

    if t1 is TFun and t2 is TFun:
        return consistent(t1.param, t2.param) and consistent(t1.ret, t2.ret)

    return False

Type checking uses consistency:

typecheck(env, App(func, arg)):
    t_func = typecheck(env, func)
    t_arg = typecheck(env, arg)

    if t_func == TAny:
        return TAny  // Calling Any returns Any

    if not consistent(t_arg, t_func.param):
        error("Inconsistent types")

    // Insert runtime check if needed
    if t_arg == TAny and t_func.param != TAny:
        insert_cast(arg, t_func.param)

    return t_func.return_type

Runtime casts (for compiled output):

Compiled code: cast<T>(value: Any) -> T:
    if typeof(value) != T:
        raise BlameError(source_location)
    return value as T

Blame tracking:

Cast = { from: Type, to: Type, location: SourceLoc }

// At runtime
if cast fails:
    error(f"Cast from {cast.from} to {cast.to} failed at {cast.location}")

The gradual guarantee (important property):

  • If you add types to untyped code and it type checks, it behaves the same
  • If you remove types from typed code, it still behaves the same (just less safely checked)

Learning milestones:

  1. Any compiles with anything → You understand the dynamic type
  2. Consistency differs from equality → You understand gradual semantics
  3. Casts are inserted → You understand the static-dynamic boundary
  4. Blame points to the cast → You understand error tracking
  5. Migration path is smooth → You understand gradual typing’s value

Project 9: Effect System and Tracked Side Effects

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Haskell
  • Alternative Programming Languages: Koka, OCaml (with effects), Rust (for comparison)
  • Coolness Level: Level 5: Pure Magic (Super Cool)
  • Business Potential: 4. The “Open Core” Infrastructure
  • Difficulty: Level 4: Expert
  • Knowledge Area: Effect Systems / Purity Tracking
  • Software or Tool: Effect Type Checker
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce (Chapter 13 for refs)

What you’ll build: A type system that tracks what effects a function can have (IO, exceptions, state mutation), allowing you to prove that certain code is pure.

Why it teaches effect systems: Modern languages like Rust, Koka, and Haskell’s IO monad track effects in types. Understanding effect systems explains why async fn is different from fn, why Haskell has monads, and how Rust prevents data races.

Core challenges you’ll face:

  • Representing effects in types → maps to effect annotations
  • Effect polymorphism → maps to functions generic in their effects
  • Effect inference → maps to computing minimal effect sets
  • Effect handlers → maps to catching/interpreting effects

Key Concepts:

  • Effect Systems: “Practical Foundations for Programming Languages” - Robert Harper
  • Algebraic Effects: Koka language documentation
  • Monadic Effects: “Real World Haskell” - O’Sullivan, Stewart, Goerzen

Difficulty: Expert Time estimate: 3-4 weeks Prerequisites: Project 3-4 completed. Familiarity with monads helpful.

Real world outcome:

$ ./effectcheck "
// Pure function: no effects
let add: (Int, Int) -> Int ! {} = fn (x, y) => x + y
"
Type: (Int, Int) -> Int ! {}  (pure)

$ ./effectcheck "
// Function with IO effect
let greet: (String) -> Unit ! {IO} = fn name =>
  print('Hello, ' + name)
"
Type: (String) -> Unit ! {IO}

$ ./effectcheck "
// Function with exception effect
let divide: (Int, Int) -> Int ! {Throw<DivByZero>} = fn (x, y) =>
  if y == 0 then throw DivByZero else x / y
"
Type: (Int, Int) -> Int ! {Throw<DivByZero>}

$ ./effectcheck "
// Effect polymorphism
let map: forall E. ((A) -> B ! E, List<A>) -> List<B> ! E = fn (f, xs) =>
  match xs with
  | Nil => Nil
  | Cons(x, rest) => Cons(f(x), map(f, rest))
"
Type: forall E. ((A) -> B ! E, List<A>) -> List<B> ! E

$ ./effectcheck "
// Effect handling
let result: Int = handle divide(10, 0) with
  | return x => x
  | throw DivByZero => 0  // Default value on error
"
Type: Int ! {}  (effect was handled!)

$ ./effectcheck "
// Error: pure context, impure function
let badPure: Int -> Int ! {} = fn x =>
  print('called with ' + x)  // Error: IO effect not allowed
  x
"
Error: Function declared pure but has effect {IO}
  print('called with ' + x)
  ^^^^^^^^^^^^^^^^^^^^

Implementation Hints:

Type with effects:

Type = TInt | TBool | ...
     | TFun(params, return_type, effects)  -- fn params -> return ! effects

Effect = IO | State(Type) | Throw(Type) | Async | ...
Effects = Set[Effect] | EffectVar(name)  -- For effect polymorphism

Effect checking:

typecheck(env, expr) -> (Type, Effects):
    match expr:
        Num(_):
            return (TInt, {})  // Pure

        Print(arg):
            (t_arg, e_arg) = typecheck(env, arg)
            return (TUnit, e_arg | {IO})  // Adds IO effect

        Throw(exn_type, value):
            (t_val, e_val) = typecheck(env, value)
            return (TBottom, e_val | {Throw(exn_type)})

        Lambda(param, body, declared_effects):
            (t_body, actual_effects) = typecheck(env + {param: t_param}, body)
            if not actual_effects <= declared_effects:
                error(f"Function has undeclared effects: {actual_effects - declared_effects}")
            return (TFun(t_param, t_body, declared_effects), {})

        App(func, arg):
            (t_func, e_func) = typecheck(env, func)
            (t_arg, e_arg) = typecheck(env, arg)
            return (t_func.return, e_func | e_arg | t_func.effects)

        Handle(body, handlers):
            (t_body, e_body) = typecheck(env, body)
            handled = effects_from_handlers(handlers)
            remaining = e_body - handled
            return (t_body, remaining)

Effect polymorphism (like map):

// map has effect E that depends on the function argument
forall E. ((A) -> B ! E, List<A>) -> List<B> ! E

// When instantiated:
map(print, [1, 2, 3])  -- E = {IO}
map(fn x => x + 1, [1, 2, 3])  -- E = {}

Effect subtyping:

{} <: {IO}  -- Pure is a subtype of effectful
{Throw<A>} <: {Throw<A>, IO}  -- Fewer effects is more restrictive

Learning milestones:

  1. Basic effects annotate functions → You understand effect representation
  2. Effect inference works → You understand effect propagation
  3. Handle removes effects → You understand effect handlers
  4. Effect polymorphism works → You understand generic effects
  5. You appreciate Rust’s safety → You understand how effects catch bugs

Project 10: Linear and Affine Types

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Rust
  • Alternative Programming Languages: Idris 2, Clean
  • Coolness Level: Level 5: Pure Magic (Super Cool)
  • Business Potential: 4. The “Open Core” Infrastructure
  • Difficulty: Level 4: Expert
  • Knowledge Area: Linear Types / Resource Management
  • Software or Tool: Linear Type Checker
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce + Idris 2 documentation

What you’ll build: A type system where values must be used exactly once (linear) or at most once (affine), preventing resource leaks and double-frees.

Why it teaches linear types: Rust’s ownership system is based on affine types. Linear types explain why you can’t use a moved value, why Drop is special, and how Rust prevents data races. This is cutting-edge type theory in practice.

Core challenges you’ll face:

  • Tracking usage counts → maps to how many times is each variable used
  • Linearity in functions → maps to consuming vs borrowing arguments
  • Unrestricted types → maps to what can be freely copied
  • Multiplicities → maps to 0, 1, or many uses

Resources for key challenges:

Key Concepts:

  • Linear Logic: Girard’s original papers
  • Affine Types: “Types and Programming Languages” Chapter 13.7 (references)
  • Quantitative Type Theory: Idris 2 documentation

Difficulty: Expert Time estimate: 3-4 weeks Prerequisites: Project 3 completed. Familiarity with Rust ownership helpful.

Real world outcome:

$ ./linear "
// Linear: must use exactly once
let file: File[1] = open('data.txt')
let contents = read(file)  // file consumed
close(file)  // Error!
"
Error: Variable 'file' used 2 times, but has multiplicity 1
  let contents = read(file)  // first use
  close(file)                // second use (not allowed)

$ ./linear "
// Correct linear usage
let file: File[1] = open('data.txt')
let contents = read(file)  // file consumed, returns (String, File[1])
close(file')
"
Type: String

$ ./linear "
// Affine: at most once (Rust-style move)
let buffer: Buffer[0..1] = allocate(1024)
process(buffer)  // buffer moved
// buffer not used again - OK
"
Type: Unit

$ ./linear "
// Unrestricted: can copy freely
let x: Int[*] = 5
let y = x + x + x  // OK, Int is unrestricted
"
Type: Int

$ ./linear "
// Linear function
let swap: forall A B. (A[1], B[1]) -> (B[1], A[1]) = fn (a, b) => (b, a)
// Both arguments consumed exactly once ✓
"
Type OK

$ ./linear "
// Dropping linear value is an error
let conn: Connection[1] = connect('localhost')
// function ends without using conn
"
Error: Linear variable 'conn' not used
  Hint: Did you mean to call close(conn)?

Implementation Hints:

Type with multiplicities:

Type = TInt | TBool | ...
     | TLinear(inner_type)      -- Must use exactly once
     | TAffine(inner_type)      -- At most once
     | TUnrestricted(inner_type) -- Any number of times

// Or with explicit multiplicity
Multiplicity = Zero | One | Many | Interval(min, max)
Type = BaseType × Multiplicity

Usage tracking in environment:

Env = Dict[str, (Type, UsageCount)]

typecheck(env, Var(name)):
    (type, used) = env[name]
    if used >= multiplicity_limit(type):
        error(f"Variable {name} used too many times")
    env[name] = (type, used + 1)
    return type

Checking function bodies:

typecheck_function(env, params, body):
    // Initialize usage counts
    for (param, type) in params:
        env[param] = (type, 0)

    result = typecheck(env, body)

    // Check all linear params were used exactly once
    for (param, type) in params:
        (_, used) = env[param]
        required = required_uses(type)
        if used != required:
            error(f"Parameter {param} used {used} times, expected {required}")

    return result

Splitting the environment (for branching):

typecheck(env, If(cond, then_branch, else_branch)):
    typecheck(env, cond)

    // Both branches must use linear variables the same way
    env_then = env.copy()
    t_then = typecheck(env_then, then_branch)

    env_else = env.copy()
    t_else = typecheck(env_else, else_branch)

    // Merge: both branches should have used same variables
    for var in linear_vars(env):
        if env_then[var].used != env_else[var].used:
            error("Branches disagree on usage of linear variable {var}")

Multiplicities for functions:

// Function that consumes its argument
fn process(x: Buffer[1]) -> Result  // x used exactly once inside

// Function that borrows (doesn't consume)
fn inspect(x: &Buffer) -> Int  // x not consumed, returned implicitly

// In Rust terms:
fn consume(x: String) -> ...  // takes ownership
fn borrow(x: &String) -> ...  // borrows

Learning milestones:

  1. Linear values must be used once → You understand linear types
  2. Affine allows not using → You understand the Rust model
  3. Branching splits the environment → You understand linear control flow
  4. Functions can consume or borrow → You understand ownership transfer
  5. You understand Rust’s borrow checker → Linear types become intuitive

Project 11: Dependent Types Introduction

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Idris
  • Alternative Programming Languages: Agda, Coq, Lean
  • Coolness Level: Level 5: Pure Magic (Super Cool)
  • Business Potential: 1. The “Resume Gold”
  • Difficulty: Level 5: Master
  • Knowledge Area: Dependent Types / Theorem Proving
  • Software or Tool: Dependent Type Checker
  • Main Book: “Type-Driven Development with Idris” by Edwin Brady

What you’ll build: A simple dependently-typed language where types can depend on values—for example, Vec n where n is an actual number, not just a type variable.

Why it teaches dependent types: Dependent types are the frontier of type systems. They blur the line between types and programs, enabling proofs of correctness. Understanding them unlocks Idris, Agda, and the future of type-safe programming.

Core challenges you’ll face:

  • Types containing values → maps to types that compute
  • Type equality is undecidable → maps to normalization and conversion
  • The Curry-Howard correspondence → maps to proofs as programs
  • Universes → maps to types of types of types…

Resources for key challenges:

Key Concepts:

  • Dependent Types: “Type-Driven Development with Idris” - Edwin Brady
  • Curry-Howard: “Lectures on the Curry-Howard Isomorphism” - Sørensen & Urzyczyn
  • Type Theory: “Homotopy Type Theory” - The Univalent Foundations Program

Difficulty: Master Time estimate: 4-6 weeks Prerequisites: Projects 3-7 completed. Comfort with proof assistants or functional programming.

Real world outcome:

$ ./dependent "
// Length-indexed vector: Vec n a
// The type knows its length!

data Vec : Nat -> Type -> Type where
  Nil  : Vec 0 a
  Cons : a -> Vec n a -> Vec (n + 1) a

// Type-safe head: can ONLY be called on non-empty vectors
head : Vec (n + 1) a -> a
head (Cons x _) = x

// This is a TYPE ERROR, not a runtime error:
// head Nil
"
Type OK

$ ./dependent "
// Type-safe append: result length is sum of input lengths
append : Vec n a -> Vec m a -> Vec (n + m) a
append Nil         ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

// The type system PROVES this is correct!
"
Type OK

$ ./dependent "
// Matrix multiplication with type-safe dimensions
Mult : Matrix m n -> Matrix n p -> Matrix m p

// These are TYPE ERRORS:
// mult (3x4 matrix) (5x6 matrix)  -- 4 ≠ 5
"
Type Error: Cannot unify 4 with 5 in matrix dimensions

$ ./dependent "
// Proofs as types!
data Equal : a -> a -> Type where
  Refl : Equal x x

// Prove that addition is commutative (sketch)
plusCommutes : (n : Nat) -> (m : Nat) -> Equal (plus n m) (plus m n)
plusCommutes Z     m = ... (proof by induction)
plusCommutes (S n) m = ... (uses plusCommutes n m)
"
Type OK (theorem proved!)

Implementation Hints:

Core syntax:

Expr = Var(name)
     | Lambda(name, type, body)
     | App(func, arg)
     | Pi(name, domain, codomain)      -- Dependent function type: (x : A) -> B(x)
     | Type(level)                     -- Universe: Type 0, Type 1, ...
     | Nat | Zero | Succ(Expr)         -- Natural numbers as example

The key insight: Pi(x, A, B) generalizes both:

  • Regular function types: Int -> Bool is Pi(_, Int, Bool) (x not used in B)
  • Dependent types: (n : Nat) -> Vec n Int (n IS used in result type)

Type checking with normalization:

typecheck(env, expr) -> Type:
    match expr:
        Var(name):
            return env[name]

        Lambda(param, param_type, body):
            check typecheck(env, param_type) is Type(_)
            new_env = env + {param: param_type}
            body_type = typecheck(new_env, body)
            return Pi(param, param_type, body_type)

        App(func, arg):
            t_func = typecheck(env, func)
            check t_func is Pi(x, domain, codomain)
            t_arg = typecheck(env, arg)
            check convertible(t_arg, domain)  # Type equality up to computation!
            return substitute(codomain, x, arg)  # Substitute value into type!

        Pi(x, domain, codomain):
            l1 = universe_level(typecheck(env, domain))
            l2 = universe_level(typecheck(env + {x: domain}, codomain))
            return Type(max(l1, l2))

Conversion checking (are two types equal?):

convertible(t1, t2) -> bool:
    n1 = normalize(t1)  # Reduce to normal form
    n2 = normalize(t2)
    return syntactically_equal(n1, n2)

normalize(expr) -> Expr:
    match expr:
        App(Lambda(x, _, body), arg):
            return normalize(substitute(body, x, arg))  # Beta reduction

        Succ(n):
            return Succ(normalize(n))

        # ... other reductions

Universe hierarchy (to avoid paradoxes):

Type 0 : Type 1 : Type 2 : ...

Nat : Type 0
Vec : Nat -> Type 0 -> Type 0
Vec 3 Int : Type 0

Learning milestones:

  1. Dependent function types work → You understand Pi types
  2. Types compute (substitution) → You understand dependent application
  3. Vec n tracks length → You understand indexed types
  4. Proofs type check → You understand Curry-Howard
  5. You can prove simple theorems → You’re doing constructive math!

Project 12: Complete Type System for a Mini-Language

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: OCaml
  • Alternative Programming Languages: Haskell, Rust
  • Coolness Level: Level 5: Pure Magic (Super Cool)
  • Business Potential: 5. The “Industry Disruptor”
  • Difficulty: Level 5: Master
  • Knowledge Area: Language Implementation / Compiler Design
  • Software or Tool: Complete Language Implementation
  • Main Book: “Types and Programming Languages” by Benjamin C. Pierce

What you’ll build: A complete type checker for a small but real language with: HM type inference, algebraic data types, pattern matching, type classes/traits, and modules—essentially a mini-Haskell or mini-Rust.

Why this is the capstone: This integrates everything: inference, ADTs, polymorphism, subtyping, and modularity. Building a complete type system shows you truly understand how production compilers work.

Core challenges you’ll face:

  • Integrating all features → maps to feature interactions
  • Type classes/traits → maps to ad-hoc polymorphism
  • Modules and namespaces → maps to type system for large programs
  • Error messages → maps to user experience
  • Performance → maps to real compiler constraints

Key Concepts:

  • All previous projects
  • Type Classes: “A History of Haskell” - Simon Peyton Jones
  • Modules: “Types and Programming Languages” Chapter 24 - Pierce

Difficulty: Master Time estimate: 6-10 weeks Prerequisites: All previous projects, or strong equivalent experience.

Real world outcome:

$ ./minilang "
module List where

data List a = Nil | Cons a (List a)

class Functor f where
  map : (a -> b) -> f a -> f b

instance Functor List where
  map f Nil = Nil
  map f (Cons x xs) = Cons (f x) (map f xs)

class Eq a where
  eq : a -> a -> Bool

instance Eq Int where
  eq = primIntEq

instance Eq a => Eq (List a) where
  eq Nil Nil = True
  eq (Cons x xs) (Cons y ys) = eq x y && eq xs ys
  eq _ _ = False

// Using type class constraints
elem : Eq a => a -> List a -> Bool
elem _ Nil = False
elem x (Cons y ys) = if eq x y then True else elem x ys

// Let's test it!
main : IO ()
main = do
  let xs = Cons 1 (Cons 2 (Cons 3 Nil))
  let found = elem 2 xs
  print (if found then 'Found!' else 'Not found')
"

Compiling module List...
Type checking: 12 definitions
Type classes: 2 (Functor, Eq)
Instances: 3
All OK!

Running main...
Output: Found!

Implementation Hints:

This project combines:

  1. HM inference (Project 3) - Base type inference
  2. ADTs (Project 4) - User-defined types
  3. Polymorphism (Project 5) - Generics
  4. Type classes (new) - Constrained polymorphism

Type classes require:

// Type representation
Type = ... | TClass(name, [Type])  -- Eq a, Functor f

// Constraints
Constraint = (ClassName, [Type])
QualifiedType = ([Constraint], Type)  -- Eq a => a -> a -> Bool

// Instance resolution
resolve_instance(constraint, available_instances) -> Instance | Error

Type checking with constraints:

typecheck(env, expr) -> (Type, [Constraint]):
    match expr:
        App(Var("eq"), arg):  // eq is a class method
            (t_arg, c_arg) = typecheck(env, arg)
            fresh_a = fresh_var()
            c_eq = (Eq, [fresh_a])
            return (TFun(fresh_a, fresh_a, TBool), c_arg + [c_eq])

        // At the end, resolve or defer constraints

Module system:

Module = {
    name: str,
    exports: [str],
    types: Dict[str, TypeDef],
    values: Dict[str, Type],
    instances: [Instance]
}

// Import resolution
resolve_name(env, "List.map"):
    module = env.modules["List"]
    if "map" not in module.exports:
        error("map is not exported from List")
    return module.values["map"]

Error message quality (crucial!):

// Bad:
"Type mismatch: expected 'a, got Int"

// Good:
"Type mismatch in function application:
  Function 'map' expects argument of type: (a -> b)
  But you provided: Int

  Hint: Did you mean to pass a function?

  3 | map 5 [1, 2, 3]
          ^
          This should be a function
"

Performance considerations:

  • Memoize type equality checks
  • Use efficient unification (union-find)
  • Incremental type checking for large files
  • Lazy constraint resolution

Learning milestones:

  1. Basic HM works → Foundation solid
  2. ADTs and patterns work → Data structures handled
  3. Type classes resolve → Ad-hoc polymorphism works
  4. Modules scope correctly → Large programs supported
  5. Error messages are helpful → Ready for real users

Capstone Project: Type Inference for a Real Language Subset

  • File: LEARN_TYPE_SYSTEMS.md
  • Main Programming Language: Rust
  • Alternative Programming Languages: OCaml, Haskell
  • Coolness Level: Level 5: Pure Magic (Super Cool)
  • Business Potential: 5. The “Industry Disruptor”
  • Difficulty: Level 5: Master
  • Knowledge Area: Complete Compiler Frontend
  • Software or Tool: Real Language Type Checker
  • Main Book: All of “Types and Programming Languages” + Rust/TypeScript documentation

What you’ll build: A type checker for a subset of a real language (TypeScript, Rust, or Python with type hints), able to type check real-world code files.

Why this is the ultimate test: Taking on a real language means dealing with real complexity: dozens of features, edge cases, backward compatibility, and actual user expectations. This is what working on GCC, rustc, or the TypeScript compiler feels like.

Core challenges you’ll face:

  • Language complexity → maps to feature explosion
  • Parsing real syntax → maps to grammar ambiguity
  • Standard library types → maps to built-in type definitions
  • Compatibility → maps to matching official behavior
  • Performance → maps to incremental checking, caching

Key Concepts:

  • Everything from all previous projects
  • Real language specifications
  • “Engineering a Compiler” by Keith Cooper

Difficulty: Master Time estimate: 3-6 months Prerequisites: All previous projects. Significant programming experience.

Real world outcome:

$ ./mypy-clone example.py

Checking: example.py

def greet(name: str) -> str:
    return "Hello, " + name

def add(x: int, y: int) -> int:
    return x + y

result = add(1, "two")  # Line 8

Error: example.py:8
  Argument 2 to "add" has incompatible type "str"; expected "int"

  result = add(1, "two")
                  ^^^^^

Found 1 error in 1 file

$ ./mypy-clone --version
MyPyClone 0.1.0 (compatible with mypy 1.0)
Supports: basic types, functions, classes, generics, unions

$ ./mypy-clone django_app.py
Checking: django_app.py (247 lines)
...
All checks passed! (2.3 seconds)

Implementation Hints:

Choose your target wisely:

  1. TypeScript subset: Mature, well-documented, structural typing
  2. Python with mypy: Gradual typing, good documentation
  3. Rust subset: Complex (borrow checker) but rewarding

Phases:

Source Code
    ↓ (parsing - use existing parser library!)
Abstract Syntax Tree
    ↓ (name resolution)
Resolved AST (names → definitions)
    ↓ (type inference)
Typed AST
    ↓ (error reporting)
Diagnostics

Start minimal:

Phase 1: Literals, variables, simple functions
Phase 2: Conditionals, loops
Phase 3: User-defined types, generics
Phase 4: Classes/structs
Phase 5: Modules, imports
Phase 6: Standard library stubs

Use existing infrastructure:

  • Parser: tree-sitter, ANTLR, or language-specific parsers
  • Error formatting: Ariadne (Rust), similar libraries
  • Testing: Compare output against official type checker

Type stub files (describing types of libraries):

# builtins.pyi
def print(*args: object) -> None: ...
def len(x: Sized) -> int: ...
def range(start: int, stop: int, step: int = 1) -> range: ...

class int:
    def __add__(self, other: int) -> int: ...
    def __sub__(self, other: int) -> int: ...
    ...

Testing strategy:

# Test against official type checker
for file in tests/*.py:
    official_output=$(mypy $file)
    our_output=$(./mypy-clone $file)
    diff $official_output $our_output

Learning milestones:

  1. Parse real syntax → You can handle real languages
  2. Basic types work → Foundation complete
  3. Generics/polymorphism work → Core features done
  4. Classes/modules work → Real programs type check
  5. Standard library works → Ready for real-world use
  6. Performance is acceptable → Production quality

Project Comparison Table

Project Difficulty Time Depth of Understanding Fun Factor
1. Calculator Type Checker Beginner Weekend ⭐⭐ ⭐⭐⭐
2. Functions & Variables Intermediate 1 week ⭐⭐⭐ ⭐⭐⭐
3. Hindley-Milner Inference Expert 2-3 weeks ⭐⭐⭐⭐⭐ ⭐⭐⭐⭐⭐
4. ADTs & Pattern Matching Advanced 2-3 weeks ⭐⭐⭐⭐ ⭐⭐⭐⭐
5. Parametric Polymorphism Advanced 2-3 weeks ⭐⭐⭐⭐ ⭐⭐⭐⭐
6. Subtyping Advanced 2-3 weeks ⭐⭐⭐⭐ ⭐⭐⭐
7. Recursive Types Expert 2-3 weeks ⭐⭐⭐⭐⭐ ⭐⭐⭐
8. Gradual Typing Advanced 2-3 weeks ⭐⭐⭐⭐ ⭐⭐⭐⭐
9. Effect Systems Expert 3-4 weeks ⭐⭐⭐⭐⭐ ⭐⭐⭐⭐
10. Linear Types Expert 3-4 weeks ⭐⭐⭐⭐⭐ ⭐⭐⭐⭐⭐
11. Dependent Types Master 4-6 weeks ⭐⭐⭐⭐⭐ ⭐⭐⭐⭐⭐
12. Complete Mini-Language Master 6-10 weeks ⭐⭐⭐⭐⭐ ⭐⭐⭐⭐⭐
Capstone: Real Language Master 3-6 months ⭐⭐⭐⭐⭐ ⭐⭐⭐⭐⭐

Path A: The Complete Journey (6-12 months)

  1. Weeks 1-2: Projects 1-2 (Type Checking Fundamentals)
  2. Weeks 3-5: Project 3 (Hindley-Milner - the core insight)
  3. Weeks 6-8: Project 4 (ADTs and Pattern Matching)
  4. Weeks 9-11: Projects 5-6 (Polymorphism and Subtyping)
  5. Weeks 12-14: Projects 7-8 (Recursive Types and Gradual Typing)
  6. Weeks 15-18: Projects 9-10 (Effects and Linear Types)
  7. Weeks 19-24: Project 11 (Dependent Types)
  8. Months 7-12: Projects 12 + Capstone

Path B: Practical Focus (3-4 months)

If you want to understand real-world type systems quickly:

1 → 2 → 3 → 5 → 6 → 8 → Capstone (TypeScript subset)

This covers: basic checking, inference, generics, subtyping, gradual typing—everything you need for TypeScript/Java/C# development.

Path C: Research/Theory Focus (4-6 months)

If you want to understand type theory deeply:

1 → 2 → 3 → 4 → 7 → 9 → 10 → 11

This covers: inference, ADTs, recursive types, effects, linear types, dependent types—the cutting edge of type theory.

Recommendation Based on Your Background

If you know Haskell/OCaml: Start with Project 3 (you’ll pick it up fast), then do 4, 9, 10, 11.

If you know TypeScript/Java: Start with Projects 1-2, then 5-6 (generics/subtyping), then 8 (gradual typing).

If you know Rust: Start with Projects 1-2, then jump to 10 (linear types) to understand ownership deeply.

If you’re a beginner: Do Projects 1-3 carefully. HM type inference (Project 3) is where everything clicks.

Essential Resources

Books

  1. “Types and Programming Languages” by Benjamin C. Pierce
    • THE textbook on type systems
    • Comprehensive, rigorous, with OCaml implementations
    • Covers simple types through polymorphism and subtyping
  2. “Advanced Topics in Types and Programming Languages” by Benjamin C. Pierce (editor)
    • Follow-up covering dependent types, effects, and more
    • Research-oriented
  3. “Type-Driven Development with Idris” by Edwin Brady
    • Practical dependent types
    • Great for Project 11
  4. “Haskell Programming from First Principles” by Allen & Moronuki
    • Great for understanding typed functional programming in practice

Online Resources

Tools and Languages to Study

  • OCaml/Haskell: Best languages for implementing type systems
  • Idris/Agda: For experiencing dependent types
  • TypeScript: Great example of gradual typing done well
  • Rust: Best example of linear/affine types in practice

Summary

# Project Name Main Language
1 Type Checker for Calculator Language Python
2 Type Checker with Functions & Variables Python
3 Hindley-Milner Type Inference Engine OCaml
4 Algebraic Data Types & Pattern Matching Haskell
5 Parametric Polymorphism (Generics) TypeScript
6 Subtyping and Structural Typing TypeScript
7 Recursive Types and Type Operators OCaml
8 Gradual Typing System Python
9 Effect System Haskell
10 Linear and Affine Types Rust
11 Dependent Types Introduction Idris
12 Complete Type System for Mini-Language OCaml
Capstone Type Checker for Real Language Subset Rust

The type system is your friend. It’s not there to make your life difficult—it’s there to catch bugs before they catch you. After these projects, you’ll see types not as constraints but as superpowers.