POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 11:20 - 11:45 at Auditorium - Type Systems 2 Chair(s): Andrew D. Gordon

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 contextual equivalence. 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. As a corollary, in all these cases, every contextual morphism is an isomorphism.

Thu 19 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: POPL - Type Systems 2 at Auditorium
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
POPL-2017-papers10:30 - 10:55
Gabriel SchererNortheastern University
POPL-2017-papers10:55 - 11:20
Danko IlikTrusted Labs
POPL-2017-papers11:20 - 11:45
POPL-2017-papers11:45 - 12:10
Matt BrownUCLA, Jens PalsbergUniversity of California, Los Angeles