Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Pearl)
summary
An inductive, block-structured matrix type implements dimensions in the type system so matrices are correct-by-construction and common operations (matrix composition implemented in about five lines) manipulate blocks instead of indices. Equational laws (product/co-product, fusion, divide-and-conquer) let code be derived and simplified. Benchmarks show the library outperforms the common vector-of-vectors library linear by about an order of magnitude while BLAS/LAPACK-backed hmatrix remains faster. A Bayesian-net example computes grass-wet = 44.84%.
AI-written summary · about
chapters (24)
- 0:00Intro
- 0:17Table of contents
- 0:58Authors
- 1:41What is a matrix?
- 1:57Common computable representation
- 2:17On the other hand...
- 3:34What we will see
- 4:25Category Theory?
- 5:17Why does it matter?
- 6:17What about matrices?
- 8:51Linear Algebra of Programming
- 9:55First approach
- 11:08No wrong matrices
- 12:01Matrix construction and manipulation
- 13:28Equational Reasoning
- 14:24Some obstacles
- 14:49Proposed solution
- 15:12New-type wrappers
- 15:53Probabilistic Programming
- 16:38PP Code
- 17:13Combining distributions
- 19:08Performance
- 21:18To takeaway.
- 22:27Future work directions
related talks
49mMaking sense of the Haskell type system
53mCan Haskell Become a Great Language for Data Science?
01h 22mHaskell for Everyday Programmers
59mKeynote: Dependently-Typed Haskell
01h 02mHaskell for Java Programmers
01h 04mHaskell - A Peek Inside the Ivory Tower
01h 09mWhy Functional Programming with Linear Types Matters
28mExpress: applications of dynamically typed Haskell expressions