Gradual Liquid Type Inference
summary
Combines Liquid Haskell’s liquid refinement type inference with gradual refinement types to solve two problems: global, non-modular inference that needs top-level annotations, and poor error messages on inference failure. The approach uses imprecise (gradual) predicates in argument positions to constrain and modularize liquid inference, and enumerates all safe concretizations from a finite predicate set to explain inconsistencies; implemented as an interactive tool (GuiLT) for Liquid Haskell and evaluated on migrating three Haskell list libraries.
AI-written summary · about
chapters (5)
- 0:00Gradual liquid types intro
- 5:21Refinement types benefits
- 10:43Verification constraints
- 16:38Liquid time certification
- 21:56Conclusion & Q&A
related talks
23mCoinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell
21mLiquid Proof Macros
31mHow to Safely Use Extensionality in Liquid Haskell
01h 02mType Inference in GHC
49mMaking sense of the Haskell type system
23mPartial Type Constructors in Practice
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
47mIndustrial Strength Laziness: What's Next?