Enhancing your Haskell with Dependently Typed Programming

on YouTube ↗48m

" summary

Dependently-typed Haskell is used to build a neural‑network implementation whose linear algebra stays identical but whose dimension mismatches move from runtime crashes to compile‑time errors. The code uses HMatrix for BLAS-backed vectors/matrices, GHC extensions (DataKinds, TypeLits, KnownNat), and the singletons pattern to reflect sizes at runtime. Result: backprop and random weight generation compile as before yet become total runNet functions with shape safety and no silent dimension bugs.

AI-written summary · about

" chapters (8)

1. 0:00Neural network basics
2. 2:26Naive Haskell implementation
3. 6:21Issues with untyped code
4. 10:45Limitations of testing
5. 17:51Introduction to data kinds
6. 22:50Typed neural networks
7. 31:58The singleton pattern
8. 38:10Conclusion and Q&A

" related talks

• 39mDependent Types in HaskellStephanie Weirich · Strange Loop 2017
• 50mUsing Dependent Types in Mathematical Optimization AlgorithmsRyan Orendorff · LambdaConf 2019
• 45mDepending on TypesStephanie Weirich · Code Mesh 2015
• 01h 20mA Practical Introduction to Haskell GADTsRichard A. Eisenberg · LambdaConf 2015
• 49mType Theory Behind the Glasgow Haskell Compiler Internals (Part 2)Vitaly Bragilevsky · LambdaConf 2018
• 34mDifferentiable Functional ProgrammingNoel Welsh · Scala Days Berlin 2018
• 01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in HaskellThomas Dietert · LambdaConf 2019
• 01h 01mType Theory Behind the Glasgow Haskell Compiler Internals (Part 6)Vitaly Bragilevsky · LambdaConf 2018