Combining Dependency, Grades, and Adjoint Logic
summary
Two new dependent type systems appear: a graded dependent/linear system that links graded usage annotations (from a semiring) to a linear fragment via modal operators, and a generalization that assigns each mode its own semiring with homomorphisms between them (modes with semiring homomorphisms). The paper proves graded substitution for both systems, and for the first develops an operational semantics with subject reduction. Concrete benefits shown include relevance analysis, automated GC, and safe in-place updates for vectors; control of contraction remains unresolved.
AI-written summary · about
chapters (17)
- 0:00Combining dependency grades and adjoint logic
- 1:23Motivation for grades and linear types
- 2:25Graded type system overview
- 3:49Graded type system rules
- 5:35Integrating linear types with graded fragments
- 6:38Modal operators in graded/linear fragments
- 7:43Extending to adjoint logic
- 9:53Controlling contraction in adjoint logic
- 10:56Contraction challenges in graded systems
- 11:18Summary
- 11:39Q&A: Contraction control status
- 12:44Q&A: Grades vs modes vs linearity
- 14:06Q&A: Why linearity with grading
- 15:30Q&A: Affinity vs linearity
- 16:34Q&A: Resource tracking levels
- 17:16Q&A: Resources in adjoint logic
- 18:49Q&A: Equality type formation
related talks
20mTowards Graded Modal Dependent Types
27mPractical Extensions for Graded Monads
17mMonadic and Comonadic Aspects of Dependency Analysis
34mGraded Monads and Type-Level Programming for Dependence Analysis
19mDeriving Dependently-Typed OOP from First Principles
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
12mA Unified View of Modalities in Type Systems
25mBinding Syntax for Dependently-Typed Programs