Pierce's TAPL book gives in exercise 30.3.17 the setting where $T_1 \to T_2 \equiv T_2 \to T_1$ (the function type are assumed to be equivalent). In the solutions, he claims that this assumption breaks the progress property.

It is easy to see that preservation fails. How can progress:

$\vdash t:T \implies t \text{ is a value } \lor \exists t'. t \to t'$

be wrong in this setting?

  • $\begingroup$ I do not have a copy of the text. Can you please provide with some more details about the question? $\endgroup$
    – Apoorv
    Jan 10, 2020 at 15:43


Your Answer

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