Proposal: Add a Semigroup-equivalent superclass of Alternative

[wren romano]

On Sun, Apr 5, 2015 at 1:05 PM, Mario Blažević <blamario at ciktel.net> wrote:
>     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