Quotient Haskell: Lightweight Quotient Types for All

on YouTube ↗21m

" summary

Quotient Haskell extends Liquid Haskell to add quotient types whose proof obligations are decidable by an SMT solver, so functions are automatically checked for respectfulness and quotient equalities are injected into the refinement logic via a built‑in rewriting algorithm. It implements quotient inductive types, auto‑verifies many examples (rationals, modular arithmetic, bags, alpha‑equivalence) and offers a manual‑proof fallback; polymorphism, GADTs and some extensionality cases remain work in progress.

AI-written summary · about

" chapters (12)

1. 0:00Quotient Haskell intro
2. 1:27Subtypes vs quotient types
3. 3:35Challenges with quotients
4. 4:19Quotient Haskell approach
5. 5:21Quotient inductive types
6. 7:04Defining quotient types
7. 9:30Respectfulness and SMT
8. 10:33Quotient equalities in logic
9. 11:41Subtyping rules for quotients
10. 13:04Examples and use cases
11. 13:46Future work
12. 14:52Q&A