Libra: Reaching for the Stars with Dependent Types

on YouTube ↗37m

" summary

Describes using dependent types, singleton types and generic programming to perform dimensional analysis at compile time so numeric values (doubles, floats, ints) carry and enforce physical dimensions. Presents Libra, a library that encodes units and dimensions in the type system to prevent nonsensical operations (like adding different-dimension quantities) during compilation.

AI-written summary · about

" chapters (5)

1. 0:00Introduction
2. 10:39Initial context
3. 22:23Project challenges
4. 30:54Key results
5. 35:57Q&A

" related talks

• 25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)Maximilian Doré · ICFP 2025
• 43mShape-Constrained Array Programming with Size-Dependent TypesTroels Henriksen, Martin Elsman, Lubin Bailly · FHPNC 2023
• 34mFunctional Programming + Dependent Types ≡ Verified Linear..Ryan Orendorff · Scale By the Bay 2021
• 41mPrograms and Proofs — Dependent Typing as a Way to Structure Your CodeGuillaume Andrieu · DevFest Toulouse 2023
• 42mProgramming with MathBartosz Milewski · Øredev 2018
• 40mQuantitative Types in Idris 2Edwin Brady · SPLASH 2020 REBASE
• 58mSeparating Behavior and Data with Type Classes in ScalaRaúl Raja Martínez · WeCodeFest 2018
• 31mDependently-Typed Programming with Logical Equality ReflectionStephanie Weirich, Yiyun Liu · ICFP 2023