What is the right notion of "isomorphism" between types, in a simple type theory? The traditional answer is: a pair of terms that are inverse, up to a specified congruence. We firstly argue that, in the presence of effects, this answer is too liberal and needs to be restricted, using Fuehrmann's notion of thunkability in the case of value types (as in call-by-value), or using Munch-Maccagnoni's notion of linearity in the case of computation types (as in call-by-name). Yet that leaves us with different notions of isomorphism for different kinds of type.

This situation is resolved by means of a new notion of ``contextual'' isomorphism (or morphism), analogous at the level of types to contextual equivalence of terms. A contextual morphism is a way of replacing one type with the other wherever it may occur in a judgement, in a way that is preserved by the action of any term with holes. For types of pure $\lambda$-calculus, we show that a contextual morphism corresponds to a traditional isomorphism. For value types, a contextual morphism corresponds to a thunkable isomorphism, and for computation types, to a linear isomorphism.

The results are most easily formulated in the setting of call-by-push-value, which we briefly introduce during the talk. This is a fine-grained effectful calculus that subsumes call-by-value and call-by-name and distinguishes values from computations and value types from computation types.