A sample revised prelude for numeric classes

Dylan Thurston dpt@math.harvard.edu
Sun, 11 Feb 2001 22:56:29 -0500


On Sun, Feb 11, 2001 at 06:48:42PM -0800, William Lee Irwin III wrote:
> There is an additional property of zero being neglected here, namely
> that it is an annihilator. That is,
> 
> 	zero * x === zero
> 	x * zero === zero

It follows:

  zero * x === (one - one) * x === one * x - one * x === x - x === zero

> Again, it's probably a reasonable compromise not to accommodate
> nonassociative algebras, though an important application of them
> lies within graphics, namely 3-vectors with the cross product.

Agreed that non-associative algebras are useful, but I feel that they
should have a different symbol.

> > > class (Num a) => Integral a where
> > >     div, mod :: a -> a -> a
> > >     divMod :: a -> a -> (a,a)
> > >     gcd, lcm :: a -> a -> a
> > >     extendedGCD :: a -> a -> (a,a,a)
> 
> While I'm wholeheartedly in favor of the Euclidean algorithm idea, I
> suspect that more structure (i.e. separating it out to another class)
> could be useful, for instance, formal power series' over Z are integral
> domains, but are not a Euclidean domain because their residue classes
> aren't computable by a finite process. Various esoteric rings like
> Z[sqrt(k)] for various positive and negative integer k can also make
> this dependence explode, though they're probably too rare to matter.

<technical math>
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.

What operations would you propose to encapsulate an integral domain
(rather than a UFD)?

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.
</technical math>

> > TODO: quot, rem partially defined.  Explain.
> > The default definition of extendedGCD above should not be taken as
> > canonical (unlike most default definitions); for some Integral
> > instances, the algorithm could diverge, might not satisfy the laws
> > above, etc.
> > TODO: (/) is only partially defined.  How to specify?  Add a member
> >       isInvertible :: a -> Bool?
> > Typical examples include rationals, the real numbers, and rational
> > functions (ratios of polynomials).
> 
> It's too easy to make it a partial function to really consider this,
> but if you wanted to go over the top (and you don't) you want the
> multiplicative group of units to be the type of the argument (and
> hence result) of recip.

Yes.  I considered and rejected that.  But it would be nice to let
callers check whether the division will blow up, and that's not
possible for classes that aren't members of Eq.

But I suppose that's the whole point.  For computable reals, the way I
would compute 1/(very small number) would be to look at (very small
number) more and more closely to figure out on which side of 0 it lay;
if it actually were zero, the program would loop.  I think programs
that want to avoid this have to take type-specific steps (in this
case, cutting off the evaluation at a certain point.)

> What you're really trying to capture here is the (right?) Z-module-like
> structure of the multiplicative monoid in a commutative ring. There are
> some weird things going on here I'm not sure about, namely:

Right.

> 	(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.)

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.

> > > class (Num a, Ord a) => Real a where
> > >     abs    :: x -> x
> > >     signum :: x -> x
> 
> 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.

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.

> <good stuff on lattices deleted> ...and Ord defines a partial order
> (and hence induces Eq) on a type.

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.

> (e.g.
> instance Ord a => Eq a where
> 	x == y = x <= y && y <= x
> )

But to define <= in terms of meet and join you already need Eq!

  x <= y === meet x y == y

Best,
	Dylan Thurston