I just thought of an additional consideration regarding this part of the design space.

On 25/07/2011 2:02 PM, Edward Kmett wrote:
(I had said):
Here is another way to look at it:  when you say

class LeftModule Whole m => Additive m
you are closer to specifying an *instance* relation than a *class constraint* relation. 

This is very true. 

However, as mentioned at the outset specifying such instance requires newtype noise (on m, to avoid incoherent overlap with the other instances) that leads to a particularly hideous programming style.

newtype NaturalModule m = NaturalModule { runNaturalModule :: m }
instance Monoidal m => LeftModule Natural (NaturalModule m) where

It isn't so bad when working with simple examples like

fiveTimes m = runNaturalModule (5 .* NaturalModule m)

but it gets progressively worse as the hierarchy gets deeper, and I have to deal with putting on and taking off more and more of these silly wrappers.

Placing the superclass constraint enforces that such instances will always be available to me, and admits optimized implementations, which I currently have to shoehorn into the main class and expose by convention.


My understanding is that in Coq, using either Canonical Structures (as George Gonthier does it) or Matthieu Sozeau's implementation of type classes, one still defines the infrastructure as you have it, i.e. the equivalent of

newtype NaturalModule m = NaturalModule { runNaturalModule :: m }
instance Monoidal m => LeftModule Natural (NaturalModule m) where

but then the inference mechanism is powerful enough to figure out that
fiveTimes m = 5 .* m
is to be resolved using that instance.  Essentially because it 'knows' that NaturalModule is a (named) identity Functor, and it is the only one that has been encountered (and could work) during the unification phase of type inference.  So it is able to insert the necessary (identity!) coercions.  While general coercions are very evil, those which are automatically-provable identities 'by construction', are perfectly OK.

Jacques