This example is from Algebraic Subtyping, p. 14. Let's say we have a type system with just function types, $\bot$ and $\top$; propositions involving type variables are defined by quantification over ground types.

I understand why $$(\bot \rightarrow \top) \rightarrow \bot \leqslant (\alpha \rightarrow \bot) \sqcup \alpha$$ holds. But how do I convince myself that it no longer holds when the type system is extended with a more general function type $\tau_1 \xrightarrow{\circ} \tau_2$ (for example, a function with possible side effects)?

The specific counterexample given in the text is $\alpha = (\top \xrightarrow{\circ} \bot) \xrightarrow{\circ} \bot$. But I don't understand why it's so obvious that this is a counterexample.

Also, I don't understand how to check whether $\alpha = \bot \xrightarrow{\circ} \top$ is a (simpler) counterexample.

| cite | improve this question | | | | |

Your Answer

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

Browse other questions tagged or ask your own question.