The Leibniz Library and Applied Propositions as Types
summary
Library implements Leibniz equality, coercion, substitution and composition in Scala, with proofs encoded as types and macros to produce runtime evidence. It claims decidable type comparison via TypeId hashes, quantified-context emulation (hidden-type trick) and axioms for phantom parameters because Scala lacks needed rules. Examples include runtime-safe matrix-dimension checks and coercions; the code largely works but requires extra axioms and has caveats for singleton and higher-kinded types.
AI-written summary · about
chapters (12)
- 0:00Start
- 10:58Mere Propositions
- 12:45Bracket Types
- 20:14Type Equality
- 20:48Subtyping
- 35:02Coercion
- 42:02Type Id
- 43:07Quantified Context in Haskell
- 45:15Imply Switch
- 49:14Uses
- 52:12Matrix Multiplication
- 1:01:33Types of Singleton
related talks
22mA Certifying Proof Assistant for Synthetic Mathematics in Lean
10mWhen Does a Program Typecheck?
33mTheory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5
11mWhat are Dependent Types
01h 08mLean: Machine-Checked Mathematics and Verified Programming, Past and Future
44mSome History of Functional Programming Languages
41mWar Time Proofs and Futuristic Programs
01h 00mTheory and Models of Lambda Calculus Untyped and Typed - Part 3 of 5