3
$\begingroup$

Is $\Gamma \vdash x x : T$ possible?

This problem appears on page 104 of Benjamin Pierce's "Types and Programming Languages".

My conclusion is that it is was the case then we would get $x: T_1 \to T_2$ and $x: T_1$ and by some axiom, these types are not equal.

The problem is identifying this axiom but I fear it might be possible to have this equality...

Any hints?

$\endgroup$
1
  • $\begingroup$ There's no way to unify $T_1 \to T_2$ and $T_1$ which means (by the typing rule for variables) we would have $x:\tau \in \Gamma \wedge x:\sigma \in \Gamma$ with $\tau \neq \sigma$, which would mean $x$ is not well-typed. $\endgroup$
    – siracusa
    Oct 1, 2019 at 20:46

1 Answer 1

2
$\begingroup$

You are on the right track. The argument you would use is on the lines of size of types defined below: (I am assuming you are in the world of simply typed $\lambda$-calculus)

$size(T) = 1$

$size(T \to T') = size(T) + size(T')$

Unification will only work if the size of types is equal, and in this case $size(T \to T') > size(T)$ hence there cannot be such a term.

However, if you add recursion/non-termination in the type system. You can indeed have such a term. $ \vdash (\lambda x. x x) (\lambda x. x x):\bot$

$\bot$ is the type that represents non-termination.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.