Dependent Types in Haskell
summary
Claims that GHC can host useful dependent‑style programming and shows a working library that parses regexes into a compile‑time occurrence map, uses Template Haskell to lift syntax, and encodes dictionaries with GADTs indexed by type‑level symbols so invalid field access fails at compile time. Singleton types bridge type indices to runtime for printing and typeclass‑based proofs handle equivalences needed for optimizations. Several proofs require explicit instances but the design compiles, runs, and lives in the dth GitHub repo.
AI-written summary · about
chapters (12)
- 0:00Intro
- 1:12Dependent Haskell
- 2:34Regular expression capture groups
- 11:53How does this work? 1. Compile-time parsing
- 13:292. Type functions run by type checker
- 19:37Types Constrain Data with GADTS
- 20:46Indexed Types constrain data
- 23:30Dependent types
- 25:24GHC's take: Singletons
- 27:37Working with type indices
- 31:40Type classes to the rescue
- 34:32Four Capabilities of Dependent Type Systems
related talks
45mDepending on Types
33mStatically Typed Interpreters
48mEnhancing your Haskell with Dependently Typed Programming
01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in Haskell
56mWrite You Some Proofs for Great Good
01h 03mHow to use Phantom Types and Existential Types in Production
40mScala vs Idris: Dependent types, now and in the future
49mThe Trouble With Types