Taking Resources to the Type Level
summary
Granule is a Haskell-like, linear by default language with parametric polymorphism, indexed types and graded modalities that let types track exact resource usage (intervals like 0..1, bounded counts, semirings). The project has ~1500 commits, 10k LOC and demoed concrete features: linear file handles that thread updated handles, session-typed channels, safe mutable arrays, and a provable leftPad whose length index and usage annotation rule out copying or discarding the input. An SMT-backed solver discharges arithmetic constraints so many resource invariants typecheck automatically.
AI-written summary · about
chapters (4)
related talks
22mLazy Linearity for a Core Functional Language
01h 04mLinear Haskell, Today and Tomorrow
42mProgramming with Math
21mGraded Monoids for Dependently Typed Array Programming
41mThe Dialectics of Type-Level Programming
31mBoring use cases for exciting types
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
36mConcrete Functional Programming