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

Question

I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a definition:

• Monomorphic Types ($\tau$):
  • Basic Types: $int,bool,float,string,unit, \dots$
  • Type types: $\alpha, \beta, \gamma, \delta, \epsilon$.
  • Compund Types: $\alpha \to \beta, int * string, bool list, \dots$
• Polymorphic Types:
  • Monomorphic types $\tau $
  • Universally quantified monomorphic types
  • $\forall \alpha_1, \dots, \alpha_n . \tau $ (Question: is this not just universally quantified monomophism? If not what's the difference?)
  • Can think of $\tau$ (I assume they mean monomorphic types) the same as $\forall . \tau$

I guess I find MANY things in this definition rather confusing. But was seems to be the core about my confusion is the difference between:

$$ expr: \alpha \to \beta$$

vs

$$ expr : \forall \alpha, \beta . \alpha \to \beta$$

I don't understand why they are not the same. What is the difference?

After writing this question I have some ideas of what might be going on and want to double check. Is what is going on that $\alpha \to \beta $ (the first one) saying that the expression $expr$ has a monomorphic type as its type (so it just has a real "fixed" type as a type)... Perhaps what's confusing me are type variables. Because nothing can be of a type "type variable". Type variables are just (meta) variables that can later be filled in with a real "basic type", right? So $\alpha \to \beta$ in my first example just stands for "some function type from one type to another but we have not decided which type to choose later, but the expression really just has a fixed basic type as a type once used in a real programming context". Is that right? So saying $fun x \to x$ has type $\alpha \to \alpha$ when reasoning in the meta-theory just means that the function really just has a fixed basic type except we have not specified it. While saying (in a more expressive type system) that $fun x \to x$ has type $\forall \alpha . \alpha \to \alpha$ means that that expression actually has the capability of encompassing all the monomorphic types at once. i.e. in the monomorphic version we actually have to define each identity function separately for each type (for the sake or argument) while in the polymorphic version we have only have 1 single programming construct for all of them...so the type variable basically just stands for a real monomorphic type (at least in the context of this definition).

I guess if we allowed type variables to be anything, then I'd be confused...I think my main worry is about type variables.

---

More rambling cuz I'm confused:

Lets look at this from FOL or as if we were trying to construct or define what an L-term is with an L-structure (see mathematical logic MATH 570). I think right now what confuses me is that this mapping between this vague definition of types (that seems to attempt to define an L-term) is not clear to me. Where is the recursion? What is the L-structure? This type definition is vague for me to really believe it. Something like this would be much better:

---

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

Answer 1

$$\newcommand{\expr}{\mathsf{expr}} \newcommand{\int}{\mathbf{Int}} \newcommand{\List}{\mathbf{List}} \newcommand{\let}{\mathbf{let}} \newcommand{\id}{\mathsf{id}} \newcommand{\in}{\mathbf{in}} \newcommand{\map}{\mathsf{map}} \newcommand{\string}{\mathbf{String}} $$

It's not really possible to answer this without being a little more precise about the status of some things. To this end, let's be clear about distinguishing 'meta' variables from variables that may be part of the syntax of the language. I'll use Greek letters for meta variables and English letters for object variables. Term names will be sans-serif, like $\expr$, keywords/constants will be bold, like $\int$.

So, the two things you ask about actually become at least three things: $$ \begin{align} \expr &: α → β \\ \expr &: a → b \\ \expr &: ∀ a\ b. a → b \end{align} $$

The first is something you might see when discussing the simply typed lambda calculus. It does not have type variables in its object language at all, but it would be inconvenient to talk about particular concrete types all the time. So instead, people tend to talk about things in a schematic way, where meta variables stand in for arbitrary particular simple types. So, something like:

$$\frac{}{λx. x : α → α}$$

is actually a schematic statement, saying that $λx.x$ could be shown to have any type of the form $α → α$. But in a concrete derivation, each occurrence of $λx.x$ can only have a particular concrete type, like $\int → \int$. There is no universal identity function in the language, each occurrence of $λx.x$ stands for an identity function that only works on one type. Perhaps it might help to require annotating the lambda bound variable in this scenario, like so:

$$λ(x : \int). x$$

since now the notations for different identity functions are actually syntactically distinct.

Now, the obvious problem with this is that the concrete system is awful to work in. You can tell, because people are routinely writing schemas rather than concrete stuff. It is basically the type system of C, and schemas are like macros that automatically copy and paste your code, which is one way that people work around this awfulness in actual C (the other way being unsafe casting, which prevents the types from guaranteeing that your code actually makes sense).

To remedy this, we can move to #2, which is to make type schemas a well-defined part of the language. This is the approach of things like Hindley-Milner (HM), and the many languages based on it (ML, Haskell, ...). One way of looking at HM is that you add named definitions to the language itself, and these definitions are allowed to have internalized type schemas, rather than particular simple types. Then, when those named definitions are referenced, the schema can be instantiated to any concrete type necessary, and the fact that the schematic definitions are uniform in the choice of type ensures that they will work. So for instance:

$$ \begin{align} \let\ &\id : a → a \\ &\id = λ x. x \\ \in\ &(\id\ 5, \id\ \texttt{"hello"}) \end{align} $$

This sort of system is a pretty strong sweet spot, because it is easy to implement and these sort of named schematic definitions cover a wide range of things that people want to write.

However, one deficiency is that these schematic objects are not first class. Expressions cannot be given a schematic type, only named definitions can, even though we somehow figure out that expressions are valid ways of implementing them. And we cannot take something with a schematic type as an argument to a function to be used at multiple instantiations. Even though:

$$λi. (i\ 5, i\ \texttt{"hello"})$$

seems similar to our term with $\let$ above, it is invalid, because $i$ is a lambda-bound variable, not a definition name.

So, the step to eliminating this discrepancy is to pass from type schemas: $$a → b$$ to quantified types: $$∀ a\ b. a → b$$.

The idea is that the quantifier can bind variables and produce something that is a type in its own right. Then we can ascribe these types to expressions (and variables), rather than only to named definitions. If we do keep named definitions around (which really we probably should, although many type theories aren't presented that way), they no longer have a special status with respect to typing.

All our previous schematic definitions can be translated to this new system by putting all the quantifiers at the beginning of the schema:

$$ \begin{align} \let\ &\id : ∀ a. a → a \\ &\id = λ x. x \\ \in\ &(\id\ 5, \id\ \texttt{"hello"}) \end{align} $$

But now we can write a corresponding lambda expressions and make sense of their types:

$$ \begin{align} (λi. (i\ 5, i\ \texttt{"hello"})) &: (∀ a. a → a) → (\int, \string) \\ λx. x &: ∀ a. a → a \\ (λi. (i\ 5, i\ \texttt{"hello"}))\ (λx.x) &: (\int, \string) \end{align} $$

There are subtleties/consequences to these steps that I haven't mentioned, but this is sort of the core idea. You might also make slightly different choices for notation. For instance, you might require writing the prefix $∀$ syntax for the schemas because it is clearer that it means the named definition works for every choice of instantiation of the variables, not for some unknown choice.

Answer 2

From a programmer's perspective, the real difference between $f : \forall \alpha. \alpha\to\alpha$ and $g : \beta\to\beta$ is that the function $f$ can be applied to an argument of an arbitrary type, because we can substitute $\alpha$ to any other type. But the function $g$ has a specific type $\beta\to\beta$, and can only be applied to an argument of type $\beta$. In a program, perhaps the type $\beta$ is defined somewhere in an outer scope, or perhaps it is a type parameter in some outer scope. But at the place where we are writing our code, we can't change what $\beta$ is.

In the language of computer science researchers, $\beta$ is a free type variable while $\alpha$ is a bound type variable. This is a confusing language, but we just need to remember that $\beta$ being a "free variable" means that it has no visible definition in the scope where we have written $g : \beta\to\beta$.