Draft Libraries Document

[Frank Atanassow]

Dylan Thurston wrote (on 31-05-01 18:50 -0400):
> On Thu, May 31, 2001 at 04:27:14PM -0600, Alastair David Reid wrote:
> > While pondering what else we'd put in mathematics other than numeric
> > stuff, I hit upon the crazy idea of adding:
> > 
> >    Mathematics.Monad
> > 
> > instead of putting Monad in Control (which is the current proposal, I
> > believe).
> 
> I'd vote against this. Monads are not terribly prominent in
> mathematics.  They're used in category theory, but the reason they're
> in Haskell is because of their usefulness as a control structure.

I would also oppose this, but for different reasons.

First, I think it is too early to put anything into Mathematics. There ought
to be some more formal standards for what goes in and what doesn't and how its
innards are arranged and named.

For example, I can imagine several different ways of encoding mathematical
constructs in Haskell: as in Monad, where you use a Curry-Howard-et al.-style
correspondence---so, you have sets/objects/propositions as types and
functions/arrows/proofs as terms; as in a metacircular interpreter or
symbolic manipulation package, where you collapse these two levels; as above,
but for a three-level structure with type classes or kinds encoding the third
level (say 2-categories). And then, as Jan pointed out, there are often many
algorithms, especially for the less foundational, continuous stuff.

Second, as everybody knows, there is nothing in Monad which forces
user-defined instances to be monads in the mathematical sense. Whether such
things belong in Mathematics may be open to argument. For example, you might want
to put the class definition outside Mathematics, but the standard instances in
(to `certify' them).

> Hmm.  Reading this list, categories don't seem to fit that well.  On
> reflection, "Mathematics" is extremely broad; perhaps too broad.
> Maybe "Algebra" is better?

I think it's too broad also; what parts of mathematics are "blessed" enough to
be put in Mathematics? By the C-H correspondence, every program is a piece of
mathematics in some sense. I have no better suggestion. Maybe someone can give
a list of examples of things that are intended to go into Mathematics...?

-- 
Frank Atanassow, Information & Computing Sciences, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-3261 Fax +31 (030) 251-379