A Little Taste of Types
summary
A tiny dependently typed language called Pie (the language) demonstrates concrete features: NAT as linked cons-style numerals, a recursion is total discipline with rec nat and ind nat (mentioned as inter nat), a defined addition that typechecks without general recursion, and a combined even-or-odd proof that also yields the half (so it both proves and computes). The work builds proofs-as-programs (Sigma, Pi, same, either) and shows the proofs actually run and return expected results.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:45Why Care
- 1:35History
- 3:40Dependent Types
- 4:09Program Types
- 8:25Plus
- 12:22Same
- 14:03Evidence
- 15:58There exists something
- 19:55For all
- 23:14Even odd
- 32:32Questions
related talks
48mA gentle introduction to type level programming in Scala
55mKeynote: Propositions as Types
01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in Haskell
50mPinafore: Strongly Typed Information Representation
49mThe Trouble With Types
56mWrite You Some Proofs for Great Good
38mType Systems - The Good, Bad and Ugly
01h 12mTruth about Types