Tic Tac Types
summary
Implements Tic‑Tac‑Toe with dependent types: starts from unsafe |String| boards, moves to vectors that know their length, then encodes moves as data constructors so invalid move sequences fail to compile. Introduces a type‑level Tic‑Tac‑Titanium and a recursive nested‑board variant where wins cascade up the tree; the compiler enforces soundness but implementation time and complexity grow substantially, so it works reliably at the cost of significant developer overhead.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:11Tic Tac Toe with types
- 3:43Game logic and wins
- 5:07Type-level Tic Tac Toe
- 6:56Lessons and limitations
- 7:59Recursive structure
- 9:47Indexed syntax functors
- 10:09Conclusion
related talks
16mGradually Typing Strategies
19mIll-Typed Programs Don't Evaluate
56mOn Type-Based Techniques for Program Manipulation
37mTypes that Change: The Extensible Type Design Pattern
24mChoice Trees: Representing Nondeterministic, Recursive, and Impure Programs in C...
28mTyping Records, Maps, and Structs
26mType Narrowing the Hard Way
46mThe Calculated Typer (Functional Pearl)