Eliminating Bugs with Dependent Haskell (Experience Report)
summary
Facebook uses Dependent Haskell to harden the Haskell Thrift compiler and Sigma rules, proving practical at production scale. The Haskell compiler encodes resolved vs unresolved ASTs, type-level schemas and membership proofs so it prevents invalid enum constants and avoids the C++ compiler’s infinite loop. Type distinctions uncover hundreds of bugs (silent drops of synchronous responses) and make data fetches and cache lookups type safe while keeping runtime performance acceptable.
AI-written summary · about
chapters (22)
- 0:00Intro
- 0:51Haskell @ Facebook
- 1:33Programming with Dependent Types
- 2:41The Thrift IDL
- 3:23Thrift Examples
- 4:18The Haskell Thrift Compiler
- 4:49Basic AST Design
- 5:41Constrained Data Structures
- 7:21Bug: Infinite Loops
- 8:18Sync vs Async Rules
- 9:19Sync vs Async Code
- 10:26Associated Types
- 12:30Typed Data Fetches
- 14:06Struct Schemas
- 15:13Typechecking Structs
- 15:55Enum Schemas
- 16:44Typechecking Enums
- 18:08More Bugs: Enum Typechecking
- 18:47More Bugs: Implicit Coercions
- 19:25More Bugs: Ambiguous References
- 20:19Schematized Inputs
- 21:00Solution: Type-Level Schemas
related talks
51mStretching the Glasgow Haskell Compiler: Nourishing GHC with Domain-Driven De...
01h 04mHaskell - A Peek Inside the Ivory Tower
57mReal-world Haskell: Good, Bad, & Ugly
27mLimiting side-effects of applications at compile-time
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
53mIntro to Haskell for Erlangers
24mCatching space leaks at compile-time using th-deepstrict
38mWhat Haskell Taught Us When We Weren't Looking