New answers tagged

2 votes

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

I claim that $T \cong \mathbb 1+\mathbb2+\mathbb3\,+\,…$. I will prove the type equivalence and then show what terms of type $T$ correspond to values of type $\mathbb 1+\mathbb2+\mathbb3\,+\,…$ The ...
winitzki's user avatar
  • 294
0 votes

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

They are inequivalent. Let's number the three $\phi$ you listed as $\phi_1, \phi_2, \phi_3$. Then $\phi_1 \mathbb N (\lambda f. f(0)+1) = 1$, while $\phi_2, \phi_3$ both give the result $2$. Therefore ...
Trebor's user avatar
  • 335

Top 50 recent answers are included