Imagine you're writing a datatype for representing sets. You want to hide the internal representation of sets from clients, but you also want to allow clients to perform any operations as efficiently as if the internal representation were exposed. This is not easy, and it's why Data.Set has 36 functions, when all that are really needed to ensure the meaning of a set ("These elements are distinct") are
fromList. Of course, writing
member :: Ord a => a -> Set a -> Bool as
member x y = Data.List.elem x (toList y)is just awful, but the price we pay for efficient
memberis having to open up the module and break the abstraction if one of the 34 other functions doesn't do exactly what we want. In addition to this pain, there's some danger: functions like
mapMonotonicare not really safe, and cannot be made so.
We could alleviate all of this mess with quotient types. Quotient types allow modules to expose their internals with no danger of breaking abstractions. The
quotients are the same as the mathematical quotients in abstract algebra, where they are used frequently. Back on the type theory side, the elimination rule for typing quotients depends not just on types, but on terms, and so requires a type system with dependent types. That's a shame, since dependent types are so tricky to typecheck. It would be great if there were some form of lightweight quotient types that didn't require the full power of dependent types.
The break-the-abstraction vs. lose-efficiency-&-safety issue reminds me of the difference between GADTs and lightweight static capabilities: GADTs are verbose, but they allow the client to safely and efficently operate on datatypes in ways that aren't covered by the library.