YAP (was Re: Proposal: Remove Show and Eq superclasses of Num)

[Ben Millwood]

On Thu, Nov 3, 2011 at 4:11 PM, Paterson, Ross <R.Paterson at city.ac.uk> wrote:
> Tyson Whitehead writes:
>> I see an integral domain is just a commutative ring with no zero divisors (and
>> every euclidean domain is also an integral domain)
>
>> http://en.wikipedia.org/wiki/Integral_domain
>
>> If I'm understanding you then this is sufficient structure to tell us that an
>> associate and unit decomposition exists, even if we can't compute it.
>
>> I spent sometime last night trying to figure out what about this structure
>> guarantees such a decomposition.  I didn't have much luck though.  Any hints?
>
> Units are invertible elements, and two elements are associates if they're
> factors of each other.  So association is an equivalence relation; in
> particular the associates of 1 are the units, and the only associate of
> 0 is itself.
>
> Now choose a member from each association equivalence class to be the
> canonical associate for all the members of that class, choosing 1 as
> the canonical associate for the unit class.  Because there are no zero
> divisors, that uniquely determines the canonical unit for each element.

Huh, that seems a bit arbitrary, but I can see how it would be useful.
The documentation and/or laws should probably be altered to prevent
the definitions 'unit = const 1' and 'associate = id' :)