Contextual isomorphisms

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Colleges, School and Institutes


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 Führmannâ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 λ-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.


Original languageEnglish
Title of host publicationPOPL 2017
Subtitle of host publicationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
EditorsGiuseppe Castagna, Andrew D. Gordon
Publication statusPublished - 21 Jan 2017
Eventthe 44th ACM SIGPLAN Symposium - Paris, France
Duration: 15 Jan 201721 Jan 2017


Conferencethe 44th ACM SIGPLAN Symposium