Are type variables really only used in mathematical conversation about types?

Question

Are type variables really only used in mathematical conversation about types? i.e. are type variables (meta-variables that only contain the type classification label) only exist in proofs for types but not in real programming languages? At least is this true for monomorphic types? i.e. I can't actually define:

$$ \texttt{ let id x = x }: \tau$$

unless the type $\tau$ has already been defined or is built in? i.e. type variables only exist for symbolic manipulation of type proofs for humans (at least for monomorphism).

---

Extra thoughts:

I am trying to understand how one defines the identity function $\texttt{let id x = x}$ in monomorphic type systems. I believe the motivation for polymorphism is to allow to apply the same syntactic definition of a function to different data types that are NOT the same, like: $\texttt{id 2}$ and $\texttt{id true}$ without the type checker freaking out at us when it tries to run those (if the language is dynamically typed...I guess in static the compiler would complain at the first instance of the identity function being applied to the wrong type when we try to compile it to usable code).

So to my understanding, if we define types as a set of possible data values, so say $\texttt{int}$ defines the set of all integers. Then the set $Set_{int \to int}$ is the set of all functions that can map integers to integers. But if we have $Set_{\forall \alpha . \alpha \to \alpha}$ and we consider the identity function corresponding to both sets so $id_{\forall \alpha . \alpha \to \alpha} \in Set_{\forall \alpha . \alpha \to \alpha}$ and $id_{int} \in Set_{int \to int}$ then when both identity functions are applied to integers they will behave exactly the same BUT they are not the same function (because they are not the same data value, the data value for one is identity on only integers while the other is give me any type and I will act like its corresponding identity. So in particular $Set_{\alpha \to \alpha} = Set_{int \to int} \cup \dots \cup Set_{string \to string}$ (i.e. the identity $id_{\alpha \to \alpha}$ is just the identity function for a specific type but not actually a function that is able to process ANY type, its one and in this case this is why the for all is important).

So my question is, is $id_{\forall \alpha . \alpha \to \alpha} \in Set_{\alpha \to \alpha}$? I guess I am trying to clarify the dots ... What does it cover? Perhaps it depends on the context of how the types are formally defined? If the $\alpha$ stands for type variables, but type variables are only allowed to be monomorphic by definition (i.e. say the type constructor for the meta-langauge is recursive but only in the monomorphism where we can't introduce the forall quantifier) then the $id_{\forall \alpha . \alpha \to \alpha} \not\in Set_{\alpha \to \alpha}$. But if the recursive definition for polymorphic types is recursive at the polymorphic step then perhaps $id_{\forall \alpha . \alpha \to \alpha} \in Set_{\alpha \to \alpha}$ is true? Actually I don't think so...

---

Context: CS 421

---

Related:

• What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?

• What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?

Answer 1

I am not sure I understand your question, but I believe the answer is "yes". When describing monomorphic languages, an expression such as

let id x = x : τ

(where τ is understood as a type meta-variable) does not mean that you can write τ in the program text. Rather, it means an arbitrary expression of that shape, where the meta-variable is replaced by any type of the language:

let id x = x : int

let id x = x : string

etc. The "meta" in "meta-variable" means that the "variable" in question is not part of the syntax of programs, but a device we use to talk about types abstractly -- or, as you put it, in "mathematical conversation about types."

Answer 2

If you interpret a type $\tau$ as a set of values $Set_\tau$, then a natural definition for the interpretation of a polymorphic type would be the following: $$Set_{\forall \alpha.\tau} = \bigcap_{\kappa \in Types} Set_{\tau[\alpha := \kappa]}$$ You need an intersection because intuitively a polymorphic type should work for all its instantiations.

Of course, written like this, the definition of $Set_\tau$ would be cyclic, so you actually need to quantify over the semantic set of types (i.e., sets of values in your case). So you get: $$Set_{\forall \alpha.\tau} = \bigcap_{\kappa \subseteq \Lambda} Set_{\tau[\alpha := \kappa]}$$ Note that by doing this, we actually inject the semantic domain into the syntax (which is a common trick), so any any set of values $\kappa \in \Lambda$ can be directly seen as a "type". And so we take $Set_\kappa = \kappa$.

To answer your question in that setting, it is obvious that: $$Set_{\forall \alpha.\alpha \to \alpha} \subseteq Set_{\tau \to \tau}$$ for all type $\tau$. And so, if $id \in Set_{\forall \alpha.\alpha \to \alpha}$ then obviously $id \in Set_{\tau \to \tau}$. And here, $id = \lambda x.x$ is a pure (untyped) term, no particular annotation is required. If on the other hand you had a syntax with type abstraction and type application, then this approach would not directly work, and the above implication regarding $id$ would not be true.