patternMinor
Term of System F whose type-erasure is $2(2)$
Viewed 0 times
whosesystemtermtypeerasure
Problem
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)$?
Solution
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.
$$ 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.
Context
StackExchange Computer Science Q#70900, answer score: 3
Revisions (0)
No revisions yet.