Linear Haskell, Today and Tomorrow
summary
GHC 9 ships a working linear-types extension and the talk demos code: identity and map type-check with GHC 9 linear types, lists and functions become multiplicity-polymorphic so one implementation covers both linear and unrestricted map via multiplicity polymorphism, and the unique-object pattern uses a double-negation style — the mkUnique continuation returns an unrestricted A so one created resource can be used any number of times. A linear-base library exists, core-to-core passes are made linearity-preserving, and this enables safer reasoning about one-time behavior and paths for optimization.
AI-written summary · about
chapters (21)
- 0:00Intro
- 4:25Overview
- 4:53Linear Haskell
- 6:13Linear Types
- 8:53Converting linear functions
- 9:57Nonlinear arrow
- 11:00Branch type checker
- 11:43Linearity
- 12:24Elephant in Home
- 13:51Unique Objects
- 16:09combinatorial explosion
- 22:07Implementation Effort
- 23:17Why Functional Programming Matters
- 28:48The Problem
- 34:37The Giant
- 35:17Multiplicities
- 36:57Modalities
- 40:29Conclusion
- 43:12Code
- 47:40Questions
- 57:23Interpretations
related talks
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
31mIs there a use for linear types?
22mLazy Linearity for a Core Functional Language
16mSoundly Handling Linearity
19mPure Borrow: Linear Haskell Meets Rust-Style Borrowing
34mFunctional Programming + Dependent Types ≡ Verified Linear..
38mWhat Haskell Taught Us When We Weren't Looking
01h 04mHaskell - A Peek Inside the Ivory Tower