How to Safely Use Extensionality in Liquid Haskell
summary
Shows that the naive functional extensionality axiom in Liquid Haskell is inconsistent with semantic subtyping and polymorphism, gives a concrete counterexample that proves false, and presents a library solution: a typed propositional equality PEq plus an intermediary axiomatic equality to safely connect to SMT. The paper builds a small model and metatheory, verifies key properties inside Liquid Haskell using classy induction, provides case studies, and ships artifacts available via cabal.
AI-written summary · about
chapters (8)
- 0:00Liquid Haskell intro
- 3:07Proving program equivalence
- 7:18Functional extensionality attempt
- 11:50Flaws in initial approach
- 14:16Safer equality system
- 18:46Properties of new equality
- 21:55Higher-order laws with extensionality
- 24:46Summary and future work
related talks
24mGradual Liquid Type Inference
49mMaking sense of the Haskell type system
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
01h 22mHaskell for Everyday Programmers
01h 04mHaskell - A Peek Inside the Ivory Tower
38mType-level interfaces in Haskell & Rust: pragmatic type-level programming
28mExpress: applications of dynamically typed Haskell expressions
46mPainless software development with Haskell