In the book I am reading, the set of simple types $\mathbb{T}$ is defined by:
- If $\alpha \in \mathbb{V}$, then $\alpha \in \mathbb{T}$
- If $\sigma, \tau \in \mathbb{T}$ then $(\sigma \to \tau) \in \mathbb{T}$
Later one of the exercises asked to "investigate whether or not $xyx$ could be typed with a simple type".
My derivation for $xyx$ reasoned that, in order for this to be well typed $x$ must have type $\delta \to (\sigma \to \tau)$ and it must also have type $\sigma$. Clearly this is a contradiction...
or is it??
If $xyx$ was well typed, this would mean that $x$ would have a type $\sigma$ such that $\sigma = \delta \to (\sigma \to \tau)$ due to the uniqueness of types.
This doesn't seem to be okay, but I tried to think of a way to prove that there were no recursive types.
However, as far as I know, there is nothing stopping $\sigma$ from being in the set $\mathbb{V}$, in which case, $\sigma$ is a perfectly valid type.
Is there some flaw in my reasoning, or is there something that doesn't allow simple types to be recursive?
We can inductively define a function $n \colon \mathbb T \to \mathbb N$ counting the number of arrows of a simple type as follows:
The function $n$ is well-defined, because each type can either be an element of $\mathbb V$ or have the form $\sigma \to \tau$ for some types $\sigma, \tau$, but it can't be both: this is implicitly assumed by the fact that $\mathbb T$ is inductively defined by the rules 1 and 2 above.
You have already shown that in order for $x y x$ to be well-typed, there would have to be a type $\sigma$ such that $\sigma = \delta \to (\sigma \to \tau)$ for some types $\delta, \tau$. But this implies that
$$n(\sigma) = n(\delta \to (\sigma \to \tau)) = n(\delta) + n(\sigma) + n(\tau) + 2 > n(\sigma)$$
which is a contradiction, therefore there can be no such $\sigma$. Notice in particular that the contradiction holds even if we assume that $\sigma \in \mathbb V$.