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