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

Question

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.

Answer 1

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 https://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, and so forth.

Answer 2

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.