Abstract
Subtypes and quotient types are dual type abstractions. However, while subtypes are widely used both explicitly and implicitly, quotient types have not seen much practical use outside of proof assistants. A key difficulty to wider adoption of quotient types lies in the significant burden of proof-obligations that arises from their use. In this article, we address this issue by introducing a class of quotient types for which the proof-obligations are decidable by an SMT solver. We demonstrate this idea in practice by presenting Quotient Haskell, an extension of Liquid Haskell with support for quotient types.
Audience
We assume a basic knowledge of Haskell, but to make the article more accessible we do not require expertise with type theory, quotient types or Liquid Haskell.
Code Examples:
Mobiles - commutative trees in which subtrees with the same parent can freely be swapped
data Tree a = Leaf | Bin a (Tree a) (Tree a)
data Mobile a =
Tree a
/ swap :: x:a -> l:Mobile a -> r:Mobile a -> Bin x l r == Bin x r l
Boom Hierarchy - family of datatypes comprising trees, lists, bags and sets
data Tree a = Empty | Leaf a | Join (Tree a) (Tree a)
data List a =
Tree a
/ idl :: x:List a -> Join Empty x == x
/ idr :: x:List a -> Join x Empty == x
/ assoc :: x:List a -> y:List a -> z:List a -> Join (Join x y) z == Join x (Join y z)
data Bag a =
List a
/ comm :: xs:Bag a -> ys:Bag a -> Join xs ys == Join ys xs
data Set a =
Bag a
/ idem :: xs:Set a -> Join xs xs == xs