Vaughan Pratt wrote:

The categories mailing list is a good one for this sort of discussion ... So here is some (gentle) push-back for Vaughan ...

BTW thank you everyone for pointing out that /everything/ I said was wrong/right! There really are underlying serious pedagogical and practical issue behind this ... typified by the comment.

Thorsten Altenkirch wrote:

...

There really shouldn't be a difference between the functions in Mathematics and in Computer Science, especially functional programming.

There should be differences within Mathematics and within Computer Science, and therefore between them. I confess -- in this context -- what springs (uncalled) to mind is the (modified) comment of Chairman Mao: Computer Science is the continuation of Mathematics by other means! ... and sometimes the balance between what /should/ be done and what /can/ be done is pushed too far. At what stage this becomes a "bug" -- as Thorsten bluntly puts it -- definitely should be up for debate. And there is no doubt in my mind that in making this judgment the clarity of the underlying (categorical) semantics adds an important perspective .... and even should be

The fact that nothing is quite what it "should be" in what has become the/a leading functional language is bothersome on the one hand for students struggling to develop a (unified) mathematical view and, simultaneously exciting for researchers who now have to find out which (!?!@!) category one is actually working in ... the fact that the answer is not an entirely simple (I do like Vaughan's "nuanced"!) is cause simultaneously for (pedagogical) concern and (researcher) delight. This reflects a general tension between semantics and implementation and the tussle over which is to be the cart and which is to be the horse. As it happens (I recall) one of the motivations behind Haskell was to produce a /lazy/ functional language and so a significant focus was actually on the implementation side ... perhaps at some semantical cost? Vaughan comments: prescriptive. Semantics does have some "real" effects: the semantics that a programmer has in mind and what is actually implemented by a language/API can be rather different ... and this can become particularly subtle as languages become more abstract (and peculiar) and are built on top of each other. Through these gaps can lie some very unexpected behaviors! Vaughan comments:

2. One should not assume that mathematics has the answer to every practical problem. Oft quoted John Arbuthnot commented (some time ago!): "There are very few things which we know, which are not capable of being reduced to a Mathematical Reasoning; and when they cannot it's a sign our knowledge of them is very small and confused; and when a Mathematical Reasoning can be had it's as great a folly to make use of any other, as to grope for a thing in the dark, when you have a Candle standing by you."

It really is hard to say more :-) ... but maybe "candle" should be replaced "compact florescent light bulb"? -robin

I am not sure whether you got a response to this ... here is my attempt. Bill Lawvere wrote:

Question: Do the various programming languages explicitly implement the indispensible ingredient of categorical semantics, that every map has a unique codomain?

SO (you are right) the first problem is that usually maps (as a category theorist is thinking of such) are not what is implemented. Functional programming languages, for example, originate from combinatory algebra and the \lambda-calculus ... typing is only really introduced retrospectively as useful sugar on this underlying structure ... what is implemented is application -- or at least a particular rewriting/reduction process of application. A function A -> B is then a just a term which can be typed to be of type A -> B which can be applied to a term of type A to reduce (maybe) to something of type B ... application (as rewriting) is definitely the primitive and typing is retrospective (although very nice and useful). However, at this stage it does /look/ deceptively categorical as one does define f :: A -> B! And, of course that has led people to look at how one might interpret this as actually categorical ... and, of course, thereby hangs a lot of excellent work! However, what emerges is something whose relation to standard mathematical settings is surprisingly remote. Lazy evaluation (mixed with non-termination/partiality) is definitely partly to blame for this ...

I don't know the technical meaning of "lazy"; was it an attempt to avoid the processing speed and ram needed to take account of the composition with inclusion maps, etcetera?

Lazy evaluation is basically a reduction strategy for the lambda calculus. It is a graph reduction strategy (you need a machine model with pointers) which does a "by-name"/"by need" evaluation with sharing of subexpressions which are duplicated in the rewriting process. Sharing arises as in the reduction S x y z => x z (y z) if z is a big structure you don't want to duplicate it so you "share" it ... and this means also you can share any rewriting you do on that structure. In terms of the rewriting steps required on the lambda calculus this reduction strategy is optimal ... however, in storage requirements it is often not optimal (so sometimes a "by-value" reduction will do better under this criterion). One feature of this rewriting technique is that it never looks at subterms which will be eliminated. E.g. in K x y => x the contents of y will never be inspected (as there is apparently no need). Of course, this is all well and good, except, when y had happened to be a term which did not terminate (i.e. had no support) , suddenly now one can produce something very definite from nothing! Of course this is what Miles Gould pointed out with a really simple Haskell program (lovely!). Even if you define the initial type "correctly" you can still write five :: Initial -> Int five _ = 5 and actually get 5 from nowhere! Of course, this really will not seem at all mysterious to a Haskell programmer who will mutter about strictness and bottoms. But it may be a bit of a shock to a mathematician! -robin P.S. Steve Vickers and Stevenson pointed out Chairman Mao plagiarized O:-) : According to the Penguin Dictionary of quotations: Karl von Clausewitz (1780-1831): "War is nothing more than the continuation of politics by other means".

Hi all, I am surprised that, in answer to one of Andrew Stacey's original questions (i.e., how are mathematical functions related to functions in computer programming), nobody has mentioned Moggi's work. I originally replied to Andrew privately, thinking that surely my reply would be one of dozens of more or less identical ones. Here is what I wrote:

Your wider question, on how functions in mathematics relate to functions in computing, is an interesting and well-studied question. In its simplest form, computer functions are the same as math functions, i.e., they input an argument from a set, and compute an output from another set. However, computer functions can have additional behaviors known as "side effects". Here are some examples of possible side-effects:

(a) non-termination (loops forever) (b) non-determinism (can output several possible values on the same input) (c) probability (can call a random number generator) (d) input/output (can write stuff to the screen or to a file) (e) state (can "remember" some information from the last time it was called) (f) exceptions (can indicate an error condition, to be handled elsewhere) ...

Interestingly, all of the above can be dealt with by using category theory. Each of these notions of side-effect corresponds to a particular strong monad on the category of sets. Each notion of function corresponds to a morphism in the corresponding Kleisli category. This was discovered by Moggi in the 1980's, see the following paper, and particularly Example 1.1:

Eugenio Moggi, "Notions of computation and monads". Information And Computation, 93(1), 1991. http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf

And I may further elaborate, in case it is not obvious, what the monad is in each of the 6 examples of side-effects mentioned above: (a) TX = X+1 (b) TX = powerset(X) (c) TX = probability distributions on X (d) For output: TX = X x Sigma^* For input: TX = X + Sigma->X + Sigma^2->X + ... (Here, Sigma is an alphabet, and Sigma^* the free monoid generated by it). (e) TX = S -> (X x S), where S is a fixed set of states. (f) TX = X + E, where E is a fixed set of exceptions. It is straightforward to equip each of these operations with the structure of a strong monad, and to convince yourself that the Kleisli category in each case is the desired category of side-effecting functions. Of course this is not the end of the story: much further work has been devoted to the question of how to combine several such monads (for example, probability and state, or probability and non-determinism). Also, in the presence of higher-order functions, Set is not always good enough as a base category, and one typically considers other base categories such as a suitable category of DCPOs. So the question is not, as some have put it, whether non-termination (or other side effects) are "good" or "bad" to have in a programming language, but rather, what monad you would like to work with. In response to Bill Lawvere's question: laziness refers to an evaluation strategy where subterms are evaluated only if they are actually needed. For example, an "eager" evaluation of the arithmetic expression 0*(2+3) would first compute 2+3=5, then multiply the result by 0. A "lazy" evaluation would recognize that computing 2+3 is unnecessary. The question is not only one of efficiency, but also one of termination: if instead of 2+3, we use a non-terminating expression, then the lazy evaluation will terminate, whereas the eager one will not. In a lazy language such as Haskell, you can implement a function that computes the first 5 prime numbers as follows: (1) compute the list L of all prime numbers, in increasing order, and (2) take the first 5 elements of L. Since Haskell is lazy, it will automatically only do as much work in step (1) as is actually needed in step (2), i.e., it will not attempt to compute an infinite list. This leads to a quite natural programming style, often reminiscent of mathematical notation. -- Peter Andrew Stacey wrote:

Here's a question for those who know about translating between category theory for mathematicians and category theory for computer programmers.

In class today I was discussing functions with domain the empty set. The students don't have much background in formal set theory (and none in category theory though I'm doing my best to sneak it in where I can) so they were trying to get to grips with the idea that the _are_ functions from the empty set, but just not very many of them.

Afterwards, one student asked about how this related to functions as used in computer programming. It seemed from what he said that he had some understanding of the formal relationship between functions in mathematics and functions in computer programs - beyond them having the same name. He said that a function that takes no input is known as a "constant function" and so wasn't sure how to fit the two notions together.

I, on the other hand, am at the level of "Ooo, look! Mathematicians and computer programmers both use the word 'function'. So do biologists and event organisers. Maybe we should organise a function whose function would be to investigate all these different uses.' so I didn't know what answer to give.

The best that I could think of was that program functions have a 'hidden' input: the fact that they have been called. So a function defined on the empty set corresponds to a function that can never be called.

Can anyone help me straighten this out?

Extra kudos for answers that I can just pass on to the student!

Thanks,

Andrew Stacey