Superclass Cycle via Associated Type

[Jacques Carette]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20110730/dd190ae5/attachment.htm>