Superclass Cycle via Associated Type
Jacques Carette
carette at mcmaster.ca
Mon Jul 25 19:40:22 CEST 2011
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>
More information about the Glasgow-haskell-users
mailing list