[TYPES/announce] Contextual Isomorphisms

[Paul B Levy]

Dear colleagues,

I hope this paper will be of interest.  It might be somewhat controversial.

Regards,
Paul

--

Contextual Isomorphisms
http://www.cs.bham.ac.uk/~pbl/papers/contextiso.pdf
(To appear at POPL 2017)

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 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.



-- 
Paul Blain Levy
School of Computer Science, University of Birmingham
http://www.cs.bham.ac.uk/~pbl