Write You Some Proofs for Great Good

on YouTube ↗56m

" summary

Claim: writing machine-checkable proofs gets the compiler to accept precise types. Uses Haskell extensions GADTs and DataKinds, implements examples like Vect (n :: Nat) a and Maybe indexed by Bool, builds propositional equality proofs to convince the type checker (append and index proofs compile but feel brittle). Performance initially suffers at runtime; workarounds include coercion combinators and rewrite rules. Bootstraps GHC naturals to a Peano view for proofs. Code and examples live on the GitHub referenced by the uploader.

AI-written summary · about

" chapters (14)

1. 0:00Introduction
2. 1:28About my employer
3. 2:30Agenda
4. 5:05Liquid Haskell
5. 7:24Interactive Program
6. 9:15Recursion
7. 16:52Bottom Line
8. 18:07Code
9. 27:07Explanation
10. 29:27Equality of Types
11. 32:14Proof
12. 35:49Probe
13. 40:16Natural Numbers
14. 48:09Decidability

" related talks

• 39mDependent Types in HaskellStephanie Weirich · Strange Loop 2017
• 55mKeynote: Propositions as TypesPhilip Wadler · Code Mesh 2015
• 34mCommunication, Expression, and Types: Your Compiler as an AllyAllele Alelle · Code Mesh 2015
• 45mDepending on TypesStephanie Weirich · Code Mesh 2015
• 01h 03mHow to use Phantom Types and Existential Types in ProductionHarold Carr · LambdaConf 2020 Global Edition
• 49mThe Trouble With TypesMartin Odersky · Strange Loop 2013
• 33mStatically Typed InterpretersChristopher Hockenbrocht · LambdaConf 2017
• 01h 12mTruth about TypesBartosz Milewski · Lambda Days 2016