On Sun, Apr 5, 2015 at 1:05 PM, Mario Blažević
On 04/05/2015 12:13 PM, Edward Kmett wrote:
There are many points in the design space. ... Haskell is remarkably bad at dealing with very fine-grained class hierarchies.
You've blogged about this in
https://www.fpcomplete.com/user/edwardk/editorial/procrustean-mathematics
and I understand your concerns, even if I'm personally rooting for the centipedes. I have to say that, both when I read the article, and re-reading it again now, I wished for a clearer statement of the problem. Is it so fundamental in mathematics, as you seem to imply, that no programming language will ever be able to reconcile alternative abstractions? Or is it only a problem with Haskell and the proposed superclass extensions, as you suggest in
I'm all for centipedes, but I agree that Haskell's type classes are pretty terrible at it. The main problems I see are Haskell's type classes (a) do not properly have laws attached to them, thus law-only classes don't work well, (b) lack a language for deriving instances from other instances, proving multiple instances equivalent, etc., and (c) require newtype hackery to have more than one instance per type. None of these are fundamentally mathematical in nature. In maths we routinely dissociate instances/structures from their carrier type, construct new structures from old ones, prove that various constructions are idempotent/inverse/coherent/etc, and so on. The problem is that Haskell's type classes don't faithfully implement the structures of this style of mathematics. For example, we have many different points in the design space, like the indexed semigroup and the non-empty Alternative. As structures, they each have different laws. Whereas many of their instances have both structures and thus satisfy both sets of laws (in addition to whatever appropriate cohesion laws), thus allowing us to equivocate between which fine structure we're referring to whenever using these instances. In addition to not being able to talk about the cohesion, Haskell doesn't let us unify the names of the structures, thus introducing a namespacing issue that doesn't arise in maths. Moreover, Haskell doesn't offer a good upgrade path to move from equivocating between two structures to settling on one or the other. Often, when we can equivocate, that means we have a huge library of combinators which work equally well for both structures; but if we stop equivocating then that forces us to duplicate (almost) the whole API, one copy for each of the fine structures we're disambiguating. Again, introducing namespacing issues. We can try to unify these APIs by making an even *more* fine-grained hierarchy, but that's just pushing the namespacing issues into the methods of the type classes, or running headlong towards law-only classes. The fundamental issue, IMO, is that type classes aren't designed to solve the problems of centipede mathematics. Type classes are designed for capturing a certain style of overloading, they aren't designed for solving namespacing issues. For centipede mathematics we need not only to be able to recognize a group of implementations as (semantically) "the same" function (à la overloading), but also to recognize a group of (semantically distinct) functions as having the same implementation (dual to overloading, "underloading"?). -- Live well, ~wren