Abstract
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.
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 language | English |
---|---|
Title of host publication | POPL 2017 |
Subtitle of host publication | Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages |
Editors | Giuseppe Castagna, Andrew D. Gordon |
Publisher | Association for Computing Machinery |
Pages | 400-414 |
ISBN (Print) | 9781450346603 |
DOIs | |
Publication status | Published - 21 Jan 2017 |
Event | the 44th ACM SIGPLAN Symposium - Paris, France Duration: 15 Jan 2017 → 21 Jan 2017 |
Conference
Conference | the 44th ACM SIGPLAN Symposium |
---|---|
Country/Territory | France |
City | Paris |
Period | 15/01/17 → 21/01/17 |