A sample revised prelude for numeric classes

[William Lee Irwin III]

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> It follows:
>   zero * x === (one - one) * x === one * x - one * x === x - x === zero

Heh, you've caught me sleeping. =)

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> I tried to write the definitions in a way that could be defined for
> any unique factorization domain, not necessarily Euclidean: just take
> the two numbers, write them as a unit times prime factors in canonical
> form, and take the product of the common factors and call that the
> GCD.  On reflection, extendedGCD probably isn't easy to write in
> general.

Well, factorizing things in various UFD's doesn't sound easy to me, but
at this point I'm already having to do some reaching for counterexamples
of practical programs where this matters. It could end up being a useless
class method in some instances, so I'm wary of it.

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> What operations would you propose to encapsulate an integral domain
> (rather than a UFD)?

I'm not necessarily proposing a different set of operations to
encapsulate them, but rather that gcd and cousins be split off into
another subclass. Your design decisions in general appear to be
striking a good chord, so I'll just bring up the idea and let you
decide whether it should be done that way and so on.

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> Formal power series over Z are an interesting example; I'll think
> about it.  On first blush, it seems like if you represented them as
> lazy lists you might be able to compute the remainder term by term.

Consider taking of the residue of a truly infinite member of Z[[x]]
mod an ideal generated by a polynomial, e.g. 1/(1-x) mod (1+x^2).
You can take the residue of each term of 1/(1-x), so x^(2n) -> (-1)^n
and x^(2n+1) -> (-1)^n x, but you end up with an infinite number of
(nonzero!) residues to add up and hence encounter the troubles with
processes not being finite that I mentioned.

On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
>> 	(3) Under some condition I don't seem to be able to formulate
>> 		offhand, one can do
>> 		(^) :: ring -> ring -> ring
>> 		Now the ring (or perhaps more generally some related ring)
>> 		acts on ring to produce an expontiation operation like what
>> 		is typically thought of for real numbers. Anyone with good
>> 		ideas as to what the appropriate conditions are here, please
>> 		speak up.
>> 		(Be careful, w ^ z = exp (z * log w) behaves badly for w < 0
>> 			on the reals.)

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> For complex numbers as well, this operation has problems because of
> branch cuts.  It does satisfy that identity I mentioned, but is not
> continuous in the first argument.
> It is more common to see functions like exp be well defined (for more
> general additive groups) than to see the full (^) be defined.

I think it's nice to have the Cauchy principal value versions of things
floating around.  I know at least that I've had call for using the CPV
of exponentiation (and it's not hard to contrive an implementation),
but I'm almost definitely an atypical user. (Note, (**) does this today.)

On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
>> I'm not convinced that Real is a great name for this, or that this
>> is really the right type for all this stuff. I'd still like to see
>> abs and signum generalized to vector spaces.

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> After thinking about this, I decided that I would be happy calling the
> comparable operation on vector spaces "norm":
> a) it's compatible with mathematical usage
> b) it keeps the Prelude itself simple.
> It's unfortunate that the operation for complex numbers can't be
> called "abs", but I think it's reasonable.

I'm not entirely sure, but I think part of the reason this hasn't been
done already is because it's perhaps painful to statically type
dimensionality in vector spaces. On the other hand, assuming that the
user has perhaps contrived a representation satisfactory to him or her,
defining a class on the necessary type constructor shouldn't be tough
at all.

In a side note, it seems conventional to use abs and signum on complex
numbers (and functions), and also perhaps the same symbol as abs for
the norm on vectors and vector functions. It seems the distinction
drawn is that abs is definitely pointwise and the norm more often does
some sort of shenanigan like L^p norms etc. How much of this convention
should be preserved seems like a design decision, but perhaps one that
should be made explicit.

On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
>> <good stuff on lattices deleted> ...and Ord defines a partial order
>> (and hence induces Eq) on a type.

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> I think that "Ord" should define a total ordering; it's certainly what
> naive users would expect.  I would define another class "Poset" with a
> partial ordering.

I neglected here to add in the assumption that (<=) was a total relation,
I had in mind antisymmetry of (<=) in posets so that element isomorphism
implies equality. Introducing a Poset class where elements may be
incomparable appears to butt against some of the bits where Bool is
hardwired into the language, at least where one might attempt to use a
trinary logical type in place of Bool to denote the result of an
attempted comparison.

On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
>> (e.g.
>> instance Ord a => Eq a where
>> 	x == y = x <= y && y <= x
>> )

On Sun, Feb 11, 2001 at 10:56:29PM -0500, Dylan Thurston wrote:
> But to define <= in terms of meet and join you already need Eq!
> 
>   x <= y === meet x y == y

I don't usually see this definition of (<=), and it doesn't seem like
the natural way to go about defining it on most machines. The notion
of the partial (possibly total) ordering (<=) seems to be logically
prior to that of the meet to me. The containment usually goes:

reflexive + transitive partial relation (preorder)
	=>
antisymmetric (partial order)
	[lattices possible here with additional structure,
		also equality decidable in terms of <= independently
		of the notion of lattices, for arbitrary partial orders]
	=>
total relation (well ordering)

Whether this matters for library design is fairly unclear.

Good work!


Cheers,
Bill