Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
summary
Constructs a linear typing discipline inside dependent type theory and implements it in Cubical Agda, using supplies (finite multisets) plus a small set of productions as witnesses so resource usage is a runtime term. Dynamic multiplicities come from an exponentiation over supplies (and coinductive naturals/ω for infinity), enabling precise types for safeHead, linear folds, insertion sort and iterate; the implementation reduces supplies computationally and is fully coded, but the system currently lacks native linear function (lollipop) types.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 4:17Static multiplicities problem
- 9:17Supplies in Cubical Agda
- 12:26Linear entailment in Agda
- 14:52Safe head with dynamic types
- 15:57Linear elimination principles
- 18:22Multiplicities with natural numbers
- 20:32Coinductive infinity
- 21:37Summary
- 23:01Q&A
related talks
34mFunctional Programming + Dependent Types ≡ Verified Linear..
01h 04mLinear Haskell, Today and Tomorrow
40mQuantitative Types in Idris 2
46mThe Calculated Typer (Functional Pearl)
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
43mShape-Constrained Array Programming with Size-Dependent Types
41mThe Dialectics of Type-Level Programming
15mLogic Programming with Extensible Types (Lightning talk)