[Haskell-cafe] Re: Num instances for 2-dimensional types

[Felipe Lessa]

On Wed, Oct 07, 2009 at 08:44:27PM -0400, Jason McCarty wrote:
> Daniel Fischer wrote:
> > Am Mittwoch 07 Oktober 2009 23:51:54 schrieb Joe Fredette:
> > > I generally find semirings defined as a ring
> > > structure without additive inverse and with 0-annihilation (which one
> > > has to assume in the case of SRs, I included it in my previous
> > > definition because I wasn't sure if I could prove it via the axioms, I
> > > think it's possible, but I don't recall the proof).
> >
> > 0*x = (0+0)*x = 0*x + 0*x ==> 0*x = 0
>
> This proof only works if your additive monoid is cancellative, which
> need not be true in a semiring. The natural numbers extended with
> infinity is one example (if you don't take 0*x = 0 as an axiom, I think
> there are two possibilities for 0*∞).

Given that

x = 1*x = (0+1)*x = 0*x + 1*x = 0*x + x

we can show that

x = x + 0*x  (right)
x = 0*x + x  (left)

so, by definition of 'zero', we have that 0*x is a zero.  But we
can easily prove that there can be only one zero: suppose we have
two zeros z1 and z2; it follows that

z1 = z1 + z2 = z2

So 0*x = 0.  Any flaws?

--
Felipe.