Is there a use for linear types?
summary
Argues that linear types and linear logic are different theories with different claims, and tests practical promises by tracing models, polarities and effect theory; shows kind-based linearity survives scrutiny while simple mappings to Rust-style ownership often fail; demonstrates mixing linearity with control breaks because the error monad lacks strength and forces explicit destructors (C++/Rust style) or awkward error-threading; proposes forgetting linearity via homomorphism not subtyping and stresses polarities, closures and strictness as the concrete tools to explore.
AI-written summary · about
chapters (7)
- 0:00Linear types introduction
- 3:36Linear logic foundations
- 7:33Linear logic and polarities
- 13:41Linear types case study
- 18:23Linearity with control effects
- 22:47Linearity versus uniqueness
- 26:23Conclusions and future
related talks
01h 04mLinear Haskell, Today and Tomorrow
16mSoundly Handling Linearity
19mMechanizing Session-Types using a Structural View: Enforcing Linearity without ...
01h 08mRegular Types and Why Do I Care ?
22mA Calculus of Inductive Linear Constructions
42mProgramming with Math
41mThe Dialectics of Type-Level Programming
25mYou Only Linearize Once: Tangents Transpose to Gradients