Type systems and inference

Inspect typing rules, equality constraints, unification, let polymorphism, variants, subtyping, variance, effects, and runtime boundaries with a working bounded inference engine.

Prerequisite: Familiarity with variables, functions, and conditionals. No type theory or compiler experience required. Twelve lessons and 24 illustrated exercises develop type-checking and inference reasoning. Eight interactive families compare rules, complete solver traces, type schemes, pattern coverage, compatibility, effects, and actual JSON validation. Bounded implementation checks are distinguished from formal soundness proofs and real-language conformance.

Lessons

1. 1

   Separate values, types, and validation

   A type describes permitted values and operations. A declaration is not a runtime inspection.

2. 2

   Read a typing judgment and its premises

   Follow local rules and see why a checker can reject an expression that happens not to fail on one run.

3. 3

   Track input, output, and lexical scope

   Function types connect an argument requirement to a result. Higher-order functions use the same rule.

4. 4

   Turn expression rules into equations

   Generate type requirements locally, while retaining the expression that caused each requirement.

5. 5

   Solve equalities without creating infinite types

   Follow substitutions, structural decomposition, conflicts, and the occurs check.

6. 6

   Reconstruct a type and explain a failure

   Combine environments, fresh variables, local requirements, and substitutions in a working engine.

7. 7

   Generalize only what is independent of the environment

   Let-bound polymorphism permits fresh instances without making captured values change type.

8. 8

   Represent alternatives and check every case

   Products combine components; tagged sums represent alternatives with distinct payloads.

9. 9

   Use a value where a less specific view is sufficient

   Read directional substitutability without confusing it with equality or conversion.

10. 10

    Derive compatibility from reading and writing

    Function inputs reverse the subtype direction; outputs preserve it. Read-write cells need both.

11. 11

    Track what a computation may do

    A result type can be the same while effects differ. Handlers can remove one effect and add another.

12. 12

    Audit a claim that types make a boundary safe

    Combine static assumptions, validation, mutation, and tests into a defensible guarantee.