Introduction to Linear Type Systems and Linear Haskell
summary
Claims that linear types let the compiler guarantee resource protocols rather than runtime checks, demonstrated by a Linear Haskell extension that rejects programs where a file handle gets weight 0 or Ω. Concrete tools include a linear IO monad and a linear-base resource-safe IO wrapper that forces close-on-exception; the typechecker flags exact misuse. Comparison uses Rust’s ownership/move semantics (copy vs move types, borrow lifetimes). Examples extend to session-typed channel protocols and modeling a scanner as a linear resource; the examples typecheck and catch the intended errors.
AI-written summary · about
chapters (8)
- 0:00Introduction to subtyping
- 1:15The problem with resources
- 5:19Substructural type rules
- 10:40Linear Haskell extension
- 19:25Safe file handling in Haskell
- 26:36Ownership and types in Rust
- 34:23Session types for protocols
- 39:48Medical imaging applications
related talks
01h 20mA Practical Introduction to Haskell GADTs
51mPragmatism, Puritanism and Functional Programming
39mLinear Logic Programming
01h 12mTruth about Types
12mSingletons and You in Haskell
01mScale By the Bay 2021 intro video by Ryan Orendorff
41mWar Time Proofs and Futuristic Programs
30mλS: Computable Semantics for Diff'ble Programming with HO Functions and Datatypes