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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
