What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?
$$\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 &amp;: α → β \\
\expr &amp;: a → b \\
\expr &amp;: ∀ 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\ &amp;\id : a → a \\
      &amp;\id = λ x. x \\
\in\ &amp;(\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\ &amp;\id : ∀ a. a → a \\
      &amp;\id = λ x. x \\
 \in\ &amp;(\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"})) &amp;: (∀ a. a → a) → (\int, \string) \\
λx. x &amp;: ∀ a. a → a \\
(λi. (i\ 5, i\ \texttt{"hello"}))\ (λx.x) &amp;: (\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.