Are there recursive types in the theory of simple types? If not, how do I prove it? 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?
 A: We can inductively define a function $n \colon \mathbb T \to \mathbb N$ counting the number of arrows of a simple type as follows:


*

*If $\alpha \in \mathbb V$, then $n(\alpha) = 0$.

*If $\sigma, \tau \in \mathbb T$, then $n(\sigma \to \tau) = n(\sigma) + n(\tau) + 1$.


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$.
