A Little Taste of Dependent Types
summary
Builds a tiny language called Pie, shows concrete definitions of plus and double using eliminators because Pie forbids raw recursion, and constructs a proof-as-program that decides parity and returns executable evidence (100 → even with half 50, 113 → odd with half 56). Demonstrates that equality respects computation, that Sigma/Pi types encode exists/for-all, and that the book The Little Typer includes the runnable language and working examples.
AI-written summary · about
chapters (13)
- 0:00Intro
- 2:18Some Momentous Events
- 7:31Types and Programs
- 12:41What's a Type?
- 15:42Addition
- 20:37Double
- 25:00There is Evidence
- 26:40Evidence of Evenness
- 28:52Is Zero Even?
- 29:42Evidence of Oddness
- 30:45All the Evidence
- 33:25Every Natural Number is Even or Odd
- 35:25The Step
related talks
11mWhat are Dependent Types
33mTheory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5
10mWhen Does a Program Typecheck?
01h 04mThe Leibniz Library and Applied Propositions as Types
40mWrite the Other Half of Your Program
01h 02mTheory and Models of Lambda Calculus Untyped and Typed - Part 4 of 5
56mIdris: Programming with Dependent Types
41mWar Time Proofs and Futuristic Programs