Lazy Linearity for a Core Functional Language
summary
Linear Core statically accepts Haskell-style lazy semantic linearity and proves soundness by an instrumented big-step semantics that tracks runtime resource use. Multiple GHC optimisations (including inlining) are shown to preserve linearity in Linear Core even when they break syntactic linearity in Core. A GHC plugin implements the system, validates it against linear-base and other libraries, accepts the vast majority of intermediate programs, and rejects a few dozen cases that expose problematic rewrite rules and missing multiplicity coercions.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:53Syntactic linearity fails
- 5:44Typing lazy linearity
- 8:58Let bindings in lazy linearity
- 10:25Pattern matching and WHNF
- 12:12Irrelevant variables
- 13:37Soundness and optimizations
- 14:41Beyond lazy languages
- 15:05Q&A
related talks
01h 04mLinear Haskell, Today and Tomorrow
46mLambda Core – HardCore
52mLambda Core – HardCore
41mLambda Core - Hardcore
36mWorking Hard to Keep Things Lazy
36mTaking Resources to the Type Level
58mKeynote: Why Functional Programming Matters
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)