Using Dependent Types in Mathematical Optimization Algorithms
summary
Uses dependent types in Haskell to encode matrix and vector shapes so linear-algebra calls are type-checked, implements convex optimization (proximal / FISTA-like steps) with matrix-free operators for forward and adjoint actions, and applies it to medical-image inverse problems (magnetic particle imaging). Claims practical wins: a reconstruction pipeline shrinks memory from 12 GB to 30 MB and runs on GPU with about a 20x speedup, producing accurate sparse reconstructions.
AI-written summary · about
chapters (24)
- 0:00Start
- 0:19Using Dependent Types in Numerical Optimization
- 6:11Euclidean Norm
- 10:18Type Level Literals
- 11:49Type Families
- 16:49Vertical Concatenation
- 17:42Type Error
- 20:57L1 Norm
- 21:57Gradient Descent
- 22:47The Gradient Operator
- 24:45Proximal Operator
- 27:06Gradient Step
- 31:29First Order Methods
- 33:43Example Matrix Free Operators
- 34:45Average Function
- 36:19Ways of Constructing Matrices
- 37:39The Fourier Transform
- 38:30Discrete Fourier Transform
- 39:14The Matrix Vector Multiply
- 39:31Transpose
- 42:20Matrix-Multiply
- 42:38Matrix Matrix Multiply
- 45:05Magnetic Particle Imaging Scanner
- 48:06Radon Transform
related talks
48mEnhancing your Haskell with Dependently Typed Programming
01mScale By the Bay 2021 intro video by Ryan Orendorff
11mGeometric Methods for Machine Learning and Optimization
01h 18mOptimization I
01h 06mOptimization on Manifolds
04mInterview
51mAre Single-Loop Algorithms Sufficient for Unbalanced Minimax Optimization?
27mTalk by Ali Kavis (UT Austin)