A sample revised prelude for numeric classes
William Lee Irwin III
wli@holomorphy.com
Sun, 11 Feb 2001 18:48:42 -0800
On Sun, Feb 11, 2001 at 05:42:15PM -0500, Dylan Thurston wrote:
> I've started writing up a more concrete proposal for what I'd like the
> Prelude to look like in terms of numeric classes. Please find it
> attached below. It's still a draft and rather incomplete, but please
> let me know any comments, questions, or suggestions.
This is great, it gets something concrete out there to comment on, which
is probably quite a bit of what needs to happen.
For brevity's sake, I'll have to chop up your message a bit.
> (1) The current Prelude defines no semantics for the fundamental
> operations. For instance, presumably addition should be
> associative (or come as close as feasible), but this is not
> mentioned anywhere.
This is something serious, as I sort of took for granted the various
properties of operations etc. I'm glad you pointed it out.
> (2) There are some superfluous superclasses. For instance, Eq and
> Show are superclasses of Num. Consider the data type
>
> > data IntegerFunction a = IF (a -> Integer)
>
> One can reasonably define all the methods of Num for
> IntegerFunction a (satisfying good semantics), but it is
> impossible to define non-bottom instances of Eq and Show.
>
> In general, superclass relationship should indicate some semantic
> connection between the two classes.
It's possible to define non-bottom instances, for instance:
instance Eq (a->b) where
_ == _ = False
instance Show (a->b) where
show = const "<<function>>"
I suspect you're aware of this and had in mind the constraint that
they should also respect the invariants and laws of the classes.
> > class (Additive a) => Num a where
> > (*) :: a -> a -> a
> > one :: a
> > fromInteger :: Integer -> a
> Num encapsulates the mathematical structure of a (not necessarily
> commutative) ring, with the laws
>
> a * (b * c) === (a * b) * c
> one * a === a
> a * one === a
> a * (b + c) === a * b + a * c
>
> Typical examples include integers, matrices, and quaternions.
There is an additional property of zero being neglected here, namely
that it is an annihilator. That is,
zero * x === zero
x * zero === 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.
> "reduceRepeat op a n" is an auxiliary function that, for an
> associative operation "op", computes the same value as
>
> reduceRepeat op a n = foldr1 op (repeat n a)
>
> but applies "op" O(log n) times. A sample implementation is below.
This is a terrific idea, and I'm glad someone has at last proposed
using it.
> > 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.
> 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.
> > class (Num a, Additive b) => Powerful a b where
> > ...
> I don't know interesting examples of this structure besides the
> instances above defined above and the Floating class below.
> "Positive" is a type constructor that asserts that its argument is >=
> 0; "positive" makes this assertion. I am not sure how this will
> interact with defaulting arguments so that one can write
>
> x ^ 5
>
> without constraining x to be of Fractional type.
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:
(1) in an arbitary commutative ring (or multiplicative semigroup),
the function can (at best) be defined as
(^) :: ring -> NaturalNumbers -> ring
That is, only the natural numbers can act on ring to produce
an exponentiation-like operation.
(2) if you have at least a division ring (or multiplicative group),
you can extend it to
(^) :: ring -> Integer -> ring
so that all of Z acts on ring to produce an exponentiation
operation.
(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.)
> > -- Note: I think "Analytic" would be a better name than "Floating".
> > class (Fractional a, Powerful a a) => Floating a where
> > ...
> The semantics of these operations are rather ill-defined because of
> branch cuts, etc.
A useful semantics can be recovered by assuming that the library-defined
functions are all the Cauchy principal values. Even now:
Complex> (0 :+ 1)**(0 :+ 1)
0.20788 :+ 0.0
> > 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.
> > module Lattice where
> > class Lattice a where
> > meet, join :: a -> a -> a
>
> Mathematically, a lattice (more properly, a semilattice) is a space
> with operations "meet" and "join" which are idempotent, commutative,
> associative, and (usually) distribute over each other. Examples
> include real-valued function with (pointwise) max and min and sets
> with union and intersection. It would be reasonable to make Ord a
> subclass of this, but it would probably complicate the class heirarchy
> too much for the gain. The advantage of Lattice over Ord is that it
> is better defined. Thus we can define a class
>
> > class (Lattice a, Num a) => NumLattice a where
> > abs :: a -> a -> a
> > abs x = meet x (negate x)
>
> and real-valued functions and computable reals can both be declared as
> instances of this class.
I'd be careful here, a meet (join) semilattices are partial orders in
which finite meets (joins) exist, and they only distribute over each
other in distributive lattices. Boolean lattices also have
complementation (e.g. not on type Bool) and Heyting lattices have
implications (x <= y ==> z iff x `meet` y <= z). My suggestion
(for simplicity) is:
class Ord a => MeetSemiLattice a where
meet :: a -> a -> a
class MeetSemiLattice a => CompleteMeetSemiLattice a where
bottom :: a
class Ord a => JoinSemiLattice a where
join :: a -> a -> a
class JoinSemiLattice a => CompleteJoinSemiLattice a where
top :: a
and Ord defines a partial order (and hence induces Eq) on a type.
(e.g.
instance Ord a => Eq a where
x == y = x <= y && y <= x
)
I don't really think bottoms and tops really get bundled in with
the strict mathematical definition, e.g. natural numbers have all
finite joins but no top, Integer has no bottom or top but all finite
joins and meets, etc. Again, your design seems to incorporate the
kind of simplicity that language implementors might want for a
Standard Prelude, so your judgment on how much generality is
appropriate here would probably be good.
Cheers,
Bill