[Agda] Re: Data.Nat.Primality.Prime and irreducibility

[N. Raghavendra]

At 2015-03-07T13:10:56+08:00, Dr. ERDI Gergo wrote:

> Yeah, I've been struggling with this point as well. I ended up just
> looking up irreducibility in Wikipedia where it is defined for
> integral domains, so I didn't want to push it too far from that.

Right, I don't know why Wikipedia defines it only for integral domains.
Anyway, ...

> In more practical terms however, since 0 is not a unit of the
> multiplicative monoid of Nat, so wouldn't your definition allow for 0
> being irreducible?

The definition I quoted makes sense for any monoid, which may not even
be commutative, but for the basic theory to work, we need to assume that
the monoid is cancellative and commutative.  The multiplicative monoid
of Nat is not cancellative, so we actually need to apply the general
theory to the multiplicative monoid of non-zero nats.

> I like naming things. Let's suppose you're writing Haskell code (just
> to stay in the realm of practicality; also because I am approaching
> Agda as a programmer and not as a mathematician). Would you ever write
>
> type Foo = Either (Int, Bool) (Either (Either () String) Double)
>
> instead of
>
> data Foo = Bar Int Bool
>          | Baz (Maybe String)
>          | Quux Double
>
> ? The first is more of an encoding of the latter than a proper
> definition that people would want to use. And I firmly believe
> programs are to be written first and foremost for other humans.

I agree.  I am learning from your comments.  Many thanks for them.

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/