Intro to Type Systems and Operational Semantics

on YouTube ↗02h 50m

" summary

Stepwise construction of five toy languages shows how type rules map directly to Haskell code: infer/check via Maybe, big‑step vs small‑step evaluation, and an evaluator producing weak‑head or full normal forms. Implementation uses GHCi, simple monads and de Bruijn indices with explicit shift/subst to avoid name capture. The repo provides versioned code and exercises; the implementations prioritize clarity over performance or production usability and successfully demonstrate preservation/progress reasoning.

AI-written summary · about

" chapters (34)

1. 0:00Start
2. 8:46Type Inference
3. 14:29Type Rules
4. 21:05Type System Is Syntax Directed
5. 30:10Successor Rule
6. 42:31Equality on Types
7. 44:41Implementation
8. 46:40Inference
9. 52:33Bidirectional Type Checking
10. 55:04Purpose of Type Systems
11. 56:27Eager Evaluation
12. 1:05:01Pattern Matching
13. 1:05:42Implementation of Equality
14. 1:10:20Evaluation Rules
15. 1:10:57Denotational Semantics
16. 1:12:28Operational Semantics
17. 1:13:19Small Step Operational Semantics
18. 1:17:04Context Rules
19. 1:20:30How Do You Specify Evaluation Order
20. 1:24:15Preservation and Progress
21. 1:25:11Smaller Step Semantics and Big Step Semantics
22. 1:25:32Small Step Semantics
23. 1:27:35Infinite Reduction Sequence
24. 1:29:18Summary of the Code
25. 1:32:21Add Variables
26. 1:36:30Type Class Constraints
27. 1:47:02The Significance of the Weak Head Normal Form
28. 1:48:58Type Checking In with a Context
29. 1:56:07Semantics of Substitution
30. 1:57:38Alpha Renaming
31. 1:59:12Substitution
32. 2:00:52Free Variable
33. 2:03:49Higher Order Abstract Syntax
34. 2:05:17The Brine Indexing

" related talks

• 01h 07mBuilding a Dependently Typed Language in Haskell Part 1Andres Loeh · ZuriHac 2026
• 36mFlexible Instruction-Set Semantics via Abstract MonadsAdam Chlipala, Thomas Bourgeat, Andres Erbsen, Samuel Gruetter, Ian J Clester, Pratap Singh, Andy Wright · ICFP 2023
• 19mIll-Typed Programs Don't EvaluateSteven Ramsay, Charlie Walpole · POPL 2024
• 12mOn the power of syntactic methods: It is all syntax after all…Amr Sabry · TyDe 2022
• 14mType-Sensitive Algebraic MacrosApril Gonçalves, Robert Atkey · PEPM 2025
• 20mDeveloping a Monadic Type Checker for an Object-Oriented LanguageKiko Fernandez-Reyes, Ella das · SLE 2019
• 41mThe Dialectics of Type-Level ProgrammingAaron Levin · Lambda World 2016
• 52mType Theory and its Meaning ExplanationsJon Sterling · LambdaConf 2015