The categories mailing list is a good one for this sort of discussion: it's hard to make sense of these issues without the abstract framework of categories to interpret statements about the difference if any between a function with no arguments and a function on the empty domain, as the following examples make clear. Steve Stevenson wrote:
All us Fortran II survivors know this issue well ... This is the "function" versus "routine" argument: (1) a routine can have no arguments but (2) can't return a value. This where CALL comes from.
In both Set and (bottomless) CPO a function (or routine) on the empty domain is typed as 0 --> X, one with no arguments as 1 --> X (1 being the empty product). Andrew, in discussing 0 --> X with your students in the context of ordinary sets and functions (the category Set) you might also want to clarify how it differs from 1 --> X. (Need 1 be identified with Y^0 for any particular Y? I would guess that a specific Y^0 should be different from the empty dependent product but is that the case? Any dependent product experts?) Robin Cockett wrote:
But now we have remembered that initial and final datatypes are supposed to coincide we have a blinding flash of inspiration: because ()=1 is the final type it must also be the initial object. So constant functions ARE the same as initial functions after all ....... so the student was not confused at all!
Or was he?
Haskell datatypes naively are pointed CPOs (CPPO), in which case one might expect the initial and final CPOs with bottom to coincide as the zero object (0 = 1). In that case the distinction between 0 --> X and 1 --> X would then vanish, in accordance with your story. Without (ultimately) contradicting this, Makoto Hamana's slides at http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf paint a more nuanced picture comparing (bottomless) CPO, CPPO (which *lacks* an initial object), and strict CPPO (all functions preserve bottom, unlike CPPO). Hamana argues for the order-enriched version of the last as the appropriate semantics for Haskell, where 0 = 1 remains the case, in agreement with the intuitions and prior semantics of Haskell. Other languages may vary. Thorsten Altenkirch wrote:
There really shouldn't be a difference between the functions in Mathematics and in Computer Science, especially functional programming.
1. There should be differences within Mathematics and within Computer Science, and therefore between them. Only in the narrow technical definition of "function" as a morphism of Set should everyone be in agreement as to what a function is. But perhaps what you meant is that mathematics and CS should recognize the same latitude in the conception of function, which is reasonable given the difficulty of defining the boundary between mathematics and CS. 2. One should not assume that mathematics has the answer to every practical problem. Scientists and engineers indeed benefit enormously from the tools of mathematics, in rough proportion to how many of them they have at their fingertips, but when mathematics comes up short the fault does not necessarily lie with the practitioners, who may from time to time be in need of genuinely new mathematical methods.
However, there may be some historic differences. Many Mathematicians still use classical set theory, where the set of functions is a derived concept (i.e. a relation which has certain properties) while in constructive theories (such as Type Theory) as in functional programming, functions are a primitive concepts and they are always computable (I like to say that a function which isn't computable doesn't really function :-).
You constructivists can be so judgmental at times. :)
Another potential confusion is that functional programming languages allow the definition of partial functions which may not be terminating. However, I think this is an unnecessary complication because non-termination is just a bug and we are really only interested in the total functions anyway.
Jimmy Treybig made a fortune from his company Tandem's line of NonStop servers, see http://en.wikipedia.org/wiki/NonStop . Computer scientists are confronted with Hobson's Choice of a programming language that includes some partial recursive functions that diverge on some inputs, and one that excludes some (total) recursive functions. No effectively compilable language can capture all and only the recursive functions. If you accept the former in order to avoid the latter, it is unkind to call all the partial ones buggy, especially when the language provides some means of getting useful work out of them. If those programs can't be analyzed as functions then how is functional programming relevant to systems programming? If they can, in what sense do they terminate?
A constant function in functional programming as in set theory is a function which always returns the same value. And clearly there is only one function from the empty set into any set, because any two functions are equal if they agree on all inputs and hence this statement is vaccously true here. The problem in understanding this is the usual trouble in understanding "ex falso quod libet".
I took Andrew's question to be more about existence of f: 0 --> X than its uniqueness. We could argue against its existence by noting that the empty function diverges on every input and also converges on every input. Hence it is clearly inconsistent and therefore cannot exist. It might seem like a bad joke, but some algebraists actually reason that way to argue that the empty algebra does not exist. We saw at UACT at MSRI in 1993 that the authors of "Algebras, Lattices, Varieties: Volume I" (Volume II still pending) forbid empty algebras because they were unable to come up with a consistent way of quantifying over the empty set. For signatures with no constants, this creates the difficulty that the subalgebras need not be closed under intersection because of the possibility of disjoint nonempty subalgebras. In order to make the set Sub A of subalgebras of an algebra A a lattice under inclusion, the authors of ALV created the notion of a subuniverse as a subalgebra that is allowed to be empty, and define Sub A to be the set of *subuniverses* of A. They spell out this arrangement with admirable clarity in Definition 1.3, and at least one of them insists to this day that maintaining separate notions of subalgebra and subuniverse in order to work around the paradoxes of the empty universe is just fine, with no explanation as to why the inconsistencies supposedly created by empty algebras do not arise for empty subuniverses. One side effect of this algebraic apartheid is that the initial lattice doesn't exist; more generally varieties without constants don't have initial algebras, only free algebras on nonempty sets. Vaughan Pratt