Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory.
Fri 28 AugDisplayed time zone: Eastern Time (US & Canada) change
10:00 - 11:00
|Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)
Koen Claessen Chalmers University of Technology, SwedenDOI
|Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)
Armando João Isaías Ferreira dos Santos University of Minho, Portugal / INESC TEC, Portugal, Jose Nuno Oliveira University of Minho, Portugal / INESC TEC, PortugalDOI