Functional Programming + Dependent Types ≡ Verified Linear..
summary
Claims that representing matrices as functions plus dependent types yields verified linear algebra with proofs in Agda; implements matrices as linear functions (forward, transpose, inner-product proof) and encodes sizes with dependent vectors so mismatched shapes are impossible. Compares to Python/NumPy and Haskell approaches, provides a library, and reports an applied win in magnetic particle imaging where dense matrix storage drops from 150 GB → tiny function pointers and runtime improves about 30× speedup.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:17Common linear algebra errors
- 8:55Functional matrix definition
- 15:52Linear function properties
- 21:27Correct by construction matrices
- 26:23Benefits and costs of proofs
- 27:04Example applications
- 32:59Correctness trade-offs
related talks
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
28mFunctional Linear Algebra in Scala
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
43mShape-Constrained Array Programming with Size-Dependent Types
42mEvaluating Linear Functions to Symmetric Monoidal Categories
45mAPLicative Programming with Naperian Functors
01h 04mLinear Haskell, Today and Tomorrow
49mFinite functional programming via graded effects and relevance types