3
$\begingroup$

If $2$ is the Church numeral $\lambda fx. f(f(x))$, then is there a closed term $t$ of System F of type $\forall \alpha ((\alpha \to \alpha) \to (\alpha \to \alpha))$ such that the type-erasure of $t$ is the untyped term $2(2)$?

$\endgroup$
3
$\begingroup$

Consider the System F version of two:

$$ T = \Lambda \alpha.\lambda f:\alpha\to\alpha. \lambda x:\alpha. f(f(x))$$

We can then search for a term $M$ of the form

$$ M = \Lambda \alpha. T \tau_1 (T \tau_2) $$

and try to find types $\tau_1,\tau_2$, possibly depending on $\alpha$, such that $M : \forall \alpha. (\alpha\to\alpha)\to(\alpha\to\alpha)$. Surely $M$ becomes $2(2)$ after type erasure.

I'll leave finding $\tau_1,\tau_2$ as an exercise. Think about what is the type of $M$, and require it to be the wanted one: this provides $\tau_1$. After that, choose $\tau_2$ so that $M$ is well-typed.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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