Intensional Datatype Refinement
summary
A refinement type system verifies that pattern-match failures cannot occur by adding finitely many constructor-subset refinements and solving set constraints; inference is fully automatic, linear-time under reasonable size and interface bounds, and implemented as a ghc plugin that analyzes real Haskell code from Hackage packages in milliseconds. The method enforces an intentionality restriction on recursive constructors, saturates and restricts constraints to interface variables, and produces sound, compositional, polyvariant typings that catch real bugs.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:17The Pattern Match Safety Problem
- 3:32Intensional Refinements
- 4:57Scalable Verification
- 6:35Refinement Types
- 11:21Set Constraints
- 14:45Interface
- 15:21Worst Case Complexity
- 16:53What went wrong?
- 18:55A Guess-Free Solution
- 22:28Constraint Normalisation
- 23:21Saturation
- 25:13Restriction
- 25:59Extension
- 26:56Complexity Revisited
- 28:11Future Work