Propositions as Types for Beginners in Haskell
summary
Claims a practical recipe: translate a proposition into a type and then construct an inhabitant to prove it. Uses standard Haskell 2010 restricted to the sound subset of Haskell (exclude bottom, nontermination, general recursion), examples include tuples, Maybe/Either, unit/Void, function composition and absurd via empty case, and shows why excluded middle and double-negation elimination are unprovable without GHC extensions. Demonstrates probing polymorphic inhabitants (how many times a function applies its arg) and when adding extensions recovers classical axioms.
AI-written summary · about
chapters (13)
- 0:00Start
- 2:16The Curry-Howard Isomorphism
- 2:53Intuition for Haskellers
- 5:24Unsound things
- 11:21Inhabitation
- 14:11Proofs as Programs
- 15:37Modus Ponens
- 16:24Hypothetical Syllogism
- 19:23Contrapositive
- 21:20Intro Double Negation
- 21:57Elim Double Negation
- 22:45Excluded Middle
- 33:09Recovering Classic Logic
related talks
43mPropositions as Types
57mPropositions as Types
01h 12mTruth about Types
01h 39mIsomorphic Reasoning: Counting with Types Part 1
01h 20mA Practical Introduction to Haskell GADTs
02h 28mIsomorphic Reasoning: Counting with Types Part 2
01h 52mIsomorphic Reasoning: Counting with Types Part 3
51mPragmatism, Puritanism and Functional Programming