<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#ffffff">
On 25/07/2011 9:55 AM, Edward Kmett wrote:<br>
<blockquote
cite="mid:CAJumaK9-ivapXLmCWTdTaHJKu+PRM=MWT08O-coK5w8Eb8kspg@mail.gmail.com"
type="cite">
<div class="gmail_quote">
<div>
<div style="color: rgb(0, 0, 0);">
<span class="Apple-style-span" style="color: rgb(31, 73,
125);">If you have an associative (+), then you can use
(.*) to multiply by a whole number, </span><span
class="Apple-style-span" style="color: rgb(31, 73, 125);">I
currently do fold a method into the Additive class to
'fake' a LeftModule, but you have to explicitly use it.</span></div>
<div><font class="Apple-style-span" color="#1f497d"><br>
</font></div>
<div style="color: rgb(0, 0, 0);"><span
class="Apple-style-span" style="color: rgb(31, 73, 125);">class
Additive m => LeftModule r m</span></div>
<div style="color: rgb(0, 0, 0);">
<span class="Apple-style-span" style="color: rgb(31, 73,
125);">class LeftModule Whole m => Additive m</span></div>
<div style="color: rgb(0, 0, 0);"><span
class="Apple-style-span" style="color: rgb(31, 73, 125);"><br>
</span></div>
<div style="color: rgb(0, 0, 0);"><span
class="Apple-style-span" style="color: rgb(31, 73, 125);">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! </span></div>
<div style="color: rgb(0, 0, 0);"><span
class="Apple-style-span" style="color: rgb(31, 73, 125);"><br>
</span></div>
<div style="color: rgb(0, 0, 0);"><span
class="Apple-style-span" style="color: rgb(31, 73, 125);">Given
LeftModule Integer m, you'd know you have </span><span
class="Apple-style-span" style="color: rgb(31, 73, 125);">Additive
m </span><span class="Apple-style-span" style="color:
rgb(31, 73, 125);">and LeftModule Whole m.</span></div>
<div style="color: rgb(0, 0, 0);"><span
class="Apple-style-span" style="color: rgb(31, 73, 125);"><br>
</span></div>
<div style="color: rgb(0, 0, 0);"><span
class="Apple-style-span" style="color: rgb(31, 73, 125);">LeftModule
Integer m => LeftModule Whole m <=> Additive m.</span></div>
</div>
</div>
</blockquote>
<br>
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).<br>
<br>
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.<br>
<br>
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.<br>
<br>
Here is another way to look at it: when you say<br>
class LeftModule Whole m => Additive m<br>
you are closer to specifying an *instance* relation than a *class
constraint* relation. <br>
<br>
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].<br>
<br>
Jacques<br>
</body>
</html>