How can I determine the cardinality of a set of polymorphic functions?

It seems obvious to me that the set of functions with the signature $\forall A. A \rightarrow A$ is "once-inhabited", i.e. there is only one such polymorphic function which "works" for any set $A$, which is the identity function. (I think perhaps mathematicians would consider this to be actually a whole family of functions; I'm coming from CS where we tend to talk about single polymorphic functions, but feel free to explain how a mathematician would phrase the problem). However I don't know how to prove it except in a very hand-wavy manner.

A slightly more complex example would be to show that $$\forall A B C. (A \rightarrow B) \rightarrow (B \rightarrow C) \rightarrow (A \rightarrow C)$$ is also once-inhabited, and that the only such function with this signature is the function composition operator.

-
What is a polymorphic function? The Wikipedia article is very unclear to someone without a background in functional programming (e.g. me). – Qiaochu Yuan May 20 '11 at 13:19
Please add the definition for a polymorphic function. Without understanding this concept it is very hard to answer your question properly, furthermore it seems that you are using lambda-calculus notations, if so please add the tag for lambda-calculus. If this is not the case, please add some clarification as per this notation. Either way, I'm not 100% certain that this question has anything to do with the [set-theory] tag. – Asaf Karagila May 23 '11 at 15:35
I'm specifically referring to the notion of parametric polymorphism from System F, which allows universal quantification over types within a formula. The reason I tagged this set-theory is because I wanted to understand how this sort of statement would be articulated and then proven in set theory... – pelotom May 23 '11 at 17:48

If you know about $\lambda$-calculus, you can make this precise by looking for normalized $\lambda$-terms that have type $\forall A. A \rightarrow A$ in the system F type system (which is described in details on http://fr.wikipedia.org/wiki/SystÃ¨me_F, the english page is not as complete, for example it doesn't have the rules for typing)

In this basic case, looking at the inference rules, you quickly get that $\Lambda A. \lambda x:A. x$ is the only normalized term having the type $\forall A. A \rightarrow A$.

The wikipedia page also explains how to make a Boolean type (A type inhabited by exactly 2 terms), a natural number type, product types etc.

-
 Thanks for the answer, this looks right but I was really hoping to understand how to state and prove these sorts of things in set theory. – pelotom May 23 '11 at 17:50 @pelotom : Well then you would need to define what exactly is a polymorphic function in set theory. The first idea would be that we quantify $A$ over a set $S$, and we would be looking for applications that take some set $A \in S$ and returns a function from $A$ to $A$, but then you have to explain which functions are not polymorphic. Personally I feel that $\lambda$-calculus does a good job at describing what exactly are polymorphic functions. – chandok May 23 '11 at 17:58 You're right, System F is the right framework in which to answer this sort of question, and specifically using the idea of Parametricity. Thanks! – pelotom Sep 15 '11 at 9:01

I'll try my best to answer your question, but we're on some shaky ground, with regards to foundations of what you call "sets".

However, I've found similar questions are framed better in terms of category theory, which has a much better notion of what you mean by polymorphisms and a "once-inhabited" function space. In the terminology of categories, polymorphic functions are called "natural transformations". There's a bit more going on, but the idea is essentially the same. Similarly, instead of saying "once-inhabited", you'd say that such a natural transformation is "unique up to isomorphism".

Regardless, the way I usually see things like that proved is to let $A$ have only on element. In such a case, there is only one function defined on $A \to A$. So that special case gives you the universal case. A similar technique will probably work for your composition example.

UPDATE:

Here's an example of how I'd prove this using the language of category theory.

Take the category $\textbf{Set}$ of all sets and functions between them. It is well known that the terminal object in $\textbf{Set}$ is the singleton set. In other words, for any set $|A| = 1, A = \{ a \}$, there is at most one function $f : X \to \{ a \}$, for any other set $X$. In other words, $f$ must be the constant function.

Some authors take the empty function ($\emptyset \to \emptyset$) to be a well defined concept (although I personally don't) to make sure that $\textbf{Set}$ is, in fact, a category.

Personally, I find the notion to be a bit silly. If you're coming from a CS background, it's probably closer to the intended semantics to work in $\textbf{Set}_{\bot}$, the category of pointed sets and partially defined functions, since most programs people write are not total functions. And $\bot$ is everywhere you'd want $\emptyset$ to be.

Now consider the function space $\forall A, B, C, (A \to B) \to (B \to C) \to (A \to C)$ where $A, B, C$ are objects in $\textbf{Set}$. To determine the cardinality of this space, as $A, B$ and $C$ vary on $\textbf{Set}$, consider the extreme case where $A, B$ and $C$ are all terminal objects. Then the individual function spaces $f : A \to B$, $g : B \to C$ and $h : A \to C$ all contain, at most, one element. Hence $\forall f, g, h, f \to g \to h$ can, at most, range over one element each: $f, g$, and $h$. Thus, this function space also only has one element.

Side-note

If you find questions like this interesting, and find yourself asking similar questions, I would take some time to read up on categories. They are a lot of fun and can make precise a lot of vague ideas that are not well defined in computer science, making many hard-to-define questions worth asking.

-
Why one element? Why not zero, since the intersection of all sets is $\emptyset$? And could you give a more specific answer, i.e. actually prove it (and especially the composition one, which was the real point of my question)? – pelotom May 20 '11 at 2:40
As far as I know, $\emptyset \to \emptyset$ is not well defined. Like I said, there are some tricky semantics going on here as far as what foundations you use. I'll update my answer with a proper proof of your question. – Robin Hoode May 20 '11 at 8:53
If $\emptyset \rightarrow \emptyset$ is not well-defined, then $\emptyset$ can't have an identity function, and ${\bf Set}$ is not a category... – pelotom May 20 '11 at 16:53
Well, some authors do believe in an empty function, just to make sure that $\textbf{Set}$ is a category. But what does this definition even look like? – Robin Hoode May 20 '11 at 23:38
@robinhoode - for each element of $\emptyset$ you give me, I can give you another element of $\emptyset$... try me :) – pelotom May 23 '11 at 21:14
show 1 more comment