Lesson 6.5
References & Further Reading
Type systems, static analysis, and compiler optimization resources.
Type systems: the fundamentals.
Types and Programming Languages
Benjamin Pierce
The standard graduate textbook on type theory. Pierce builds up from the simply-typed lambda calculus through subtyping, polymorphism, and recursive types. Rigorous -- proofs throughout. Monk's type model is at the simple end of what this book covers, which is intentional: simple systems are understandable systems.
cis.upenn.edu/~bcpierce/taplCrafting Interpreters, Chapter 8 — "Statements and State"
Robert Nystrom — craftinginterpreters.com
The resolver chapter in Crafting Interpreters is the closest analog to what Monk's checker does -- a second pass over the AST that resolves variable bindings and catches scope errors. Different goals, same architecture. Free to read online.
craftinginterpreters.com/resolving-and-binding.htmlMonk's type system is intentionally simple. Structural typing, nine kinds, one optional flag. The goal is zero annotation burden for common programs while catching the bugs that actually bite people. TAPL shows where the complexity ceiling is -- Monk lives well below it.
Type inference: Hindley-Milner.
Hindley-Milner type system (Wikipedia)
The algorithm behind ML, Haskell, and Rust's type inference. Hindley-Milner infers types globally using unification -- it can infer the type of a function from how it's used, not just how it's defined. Monk uses a simpler, local inference (first-assignment rule) -- but understanding H-M illuminates why full global inference is complex and what trade-offs Monk avoids.
en.wikipedia.org/wiki/Hindley-Milner_type_system"Write You a Haskell" — type inference chapters
by Stephen Diehl
A walkthrough of building a Haskell-like language from scratch. The chapters on constraint generation and unification are excellent practical introductions to full type inference. More complex than what Monk does, but the same conceptual foundation.
dev.stephendiehl.com/fun/006_hindley_milner.htmlStructural vs nominal typing.
TypeScript Handbook — "Type Compatibility"
TypeScript uses structural typing for objects -- compatibility is determined by shape, not name. Monk's record types work the same way: a record is valid if its fields match, regardless of what type name was declared. The TypeScript handbook's explanation of structural compatibility is a clean, practical treatment of the concept.
typescriptlang.org/docs/handbook/type-compatibilityGo's structural typing for interfaces
Go uses structural typing for interfaces -- a type satisfies an interface if it has the right methods, no explicit declaration needed. Monk's compiler is written in Go, and the design philosophy (implicit satisfaction, shape-based compatibility) influenced Monk's own record typing. Reading Go's interface spec shows the practical benefits of structural over nominal.
go.dev/ref/spec#Interface_typesType-directed optimization.
V8 Hidden Classes and Inline Caches
V8 (JavaScript's engine) achieves near-native performance on typed code by tracking the "hidden class" (shape) of objects at runtime and using that to skip dynamic dispatch. Monk's unboxing does the same thing, but at compile time using static types. The V8 approach works without static types -- but needs complex runtime machinery. Monk's approach is simpler because the types are already known.
v8.dev/docs/hidden-classesJulia's type specialization
Julia compiles specialized versions of functions for each combination of argument types it sees. This is why Julia can match C for numerical code -- it generates unboxed, type-specific machine code. Monk uses a simpler static version of the same idea: one unboxed function per known-type signature, generated at compile time rather than JIT-compiled at runtime.
docs.julialang.org/en/v1/manual/performance-tips/#Specialize-on-typesGCC's -O3 and -flto flags
Monk compiles generated C with cc -O3 -flto. O3 enables aggressive optimization passes (loop unrolling, vectorization, function inlining). LTO (link-time optimization) lets GCC inline across translation unit boundaries -- so monk_add gets inlined even when defined in a separate .c file. The combination is what makes unboxed Monk code reach C parity.
Suggested reading order.
Crafting Interpreters, resolver chapter -- the closest practical analog to Monk's checker. Read this if you want to understand the architecture before reading the theory.
TypeScript type compatibility -- structural typing explained through a practical, widely-used language. Monk's records follow the same model.
V8 hidden classes -- understand the problem Monk solves with static unboxing, from the perspective of a JIT that has to solve it dynamically.
Write You a Haskell, H-M chapters -- for understanding what full global inference looks like and why Monk's local inference is simpler.
TAPL -- only if you want the full theoretical foundation. Heavyweight, but the definitive reference.