Superclass Cycle via Associated Type

[Jacques Carette]

On 25/07/2011 9:55 AM, Edward Kmett wrote:
> If you have an associative (+), then you can use (.*) to multiply by a 
> whole number, I currently do fold a method into the Additive class to 
> 'fake' a LeftModule, but you have to explicitly use it.
>
> class Additive m => LeftModule r m
> class LeftModule Whole m => Additive m
>
> This says that if you have an Additive semigroup, then there exists a 
> LeftModule over the whole numbers, and that every leftmodule is 
> additive, but there can exist other LeftModules than just ones over 
> the whole numbers!
>
> Given LeftModule Integer m, you'd know you have Additive m and 
> LeftModule Whole m.
>
> LeftModule Integer m => LeftModule Whole m <=> Additive m.

I believe that part of the issue here is that you are using a single 
relation (given by class-level => ) to model what are actually two 
different relations: a 'constructive' inclusion and a 'view' (to use the 
terminology from the Specifications community, which is clearly what 
these class definitions are).

Just like inheritance hierarchies fail miserably when you try to model 
more than one single relation, it should not be unsurprising that the 
same thing befalls '=>', which is indeed a (multi-ary) relation.

In my own hierarchy for Algebra, I use two relations.  Slightly 
over-simplifying things, one of them reflects 'syntactic' inclusion 
while the other models 'semantic' inclusion.  There are very strict 
rules for the 'syntactic' one, so that I get a nice hierarchy and lots 
of free theorems, while the semantic one is much freer, but generates 
proof obligations which must be discharged.  The syntactic one generates 
a nice DAG (with lots of harmless diamonds), while the semantic one is a 
fully general graph.

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.

In a general categorical setting, this is not so surprising as 'classes' 
and 'instances' are the same thing.  A 'class' typically has many 
non-isomorphic models while an 'instance' typically has a unique model 
(up to isomorphism), but these are not laws [ex: real-closed Archimedian 
fields have a unique model even though a priori that is a class, and the 
Integers have multiple Monoid instances].

Jacques
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20110725/a578298f/attachment-0001.htm>