Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
summary
Stitch is a full STLC interpreter with parser, length-indexed AST, type checker, evaluator, common-subexpression elimination and a REPL, implemented in Haskell using GADTs and type indices plus singletons and a fin-index for de Bruijn indices. The parser uses an n-indexed Parsec monad with a length-indexed Vec environment; type checking uses a singleton context and a CPS trick to emulate exists. A generalized heterogeneous HashMap and ~2,000 lines of code compile and run, and type errors guide every bug fix.
AI-written summary · about
chapters (10)
- 0:00Introduction to Stitch
- 1:49Project overview
- 3:24Indexed syntax and variables
- 7:06Understanding finite sets
- 8:23Parser implementation
- 10:50Type system interactions
- 13:02Type checking logic
- 15:53Type checker continuation
- 19:10Code and error handling
- 21:52Conclusion and recap
related talks
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
42mFunctional interpreters and you
33mAnalyzing Functional Programs
02h 50mIntro to Type Systems and Operational Semantics
16mKnowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative S
14mType-Sensitive Algebraic Macros
46mThe Calculated Typer (Functional Pearl)
10mKnitGIST: A Programming Synthesis Toolkit for Generating Functional Machine-Knitting Textures