Contextual isomorphisms

Contextual Isomorphisms
Paul Blain Levy

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 paper is based on a very simple idea that everyone familiar with type-systems can enjoy. It then applies it in a technical setting in which it brings a useful contribution. I suspect that many readers will find that second part too technical, but they may still enjoy the idea itself. To facilitate this, I will rephrase the abstract above in a way that I hope makes it accessible to a larger audience.

The problem that the paper solves is: how do we know what it means for two types to be equivalent? For many languages they are reasonable definitions of equivalence (such that: there exists a bijection between these two types in the language), but for more advanced languages these definitions break down. For example, in presence of hidden mutable state, one can build a pair of functions from the one-element type unit to the two-element type bool and back that are the identity when composed together -- the usual definition of bijection -- while these two types should probably not be considered "the same". Those two functions share some hidden state, so they "cheat". Other, more complex notions of type equivalence have been given in the literature, but how do we know whether they are the "right" notions, or whether they may disappoint us in the same way?

To define what it means for two program fragments to be equivalent, we have a "gold standard", which is contextual equivalence: two program fragments are contextually equivalent if we can replace one for the other in any complete program without changing its behavior. This is simple to state, it is usually clear how to instantiate this definition for a new system, and it gives you a satisfying notion of equivalent. It may not be the most convenient one to work with, so people define others, more specific notions of equivalence (typically beta-eta-equivalence or logical relations); it is fine if they are more sophisticated, and their definiton harder to justify or understand, because they can always be compared to this simple definition to gain confidence.

The simple idea in the paper above is to use this exact same trick to define what it means for two types to be equivalent. Naively, one could say that two types are equivalent if, in any well-typed program, one can replace some occurrences of the first type by occurrences of the second type, all other things being unchanged. This does not quite work, as changing the types that appear in a program without changing its terms would create ill-typed terms. So instead, the paper proposes that two types are equivalent when we are told how to transform any program using the first type into a program using the second type, in a way that is bijective (invertible) and compositional -- see the paper for details.

Then, the author can validate this definition by showing that, when instantiated to languages (simple or complex) where existing notions of equivalence have been proposed, this new notion of equivalence corresponds to the previous notions.

(Readers may find that even the warmup part of the paper, namely the sections 1 to 4, pages 1 to 6, are rather dense, with a compactly exposed general idea and arguably a lack of concrete examples that would help understanding. Surely this terseness is in large part a consequence of strict page limits -- conference articles are the tweets of computer science research. A nice side-effect (no pun intended) is that you can observe a carefully chosen formal language at work, designed to expose the setting and perform relevant proofs in minimal space: category theory, and in particular the concept of naturality, is the killer space-saving measure here.)

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Aside: can a value type be isomorphic to a computation type?

The second part of the paper uses Call-By-Push-Value to reason about programming languages with effects in a general setting. It recovers known notions of isomorphisms between value types, and of isomorphism between computation types. One may ask if there is a sensible notion of isomorphism between a value type and a computation type; this is not readily expressed in this setting as "replacing" a value type by a computational type would break syntactic invariants, but it can be asked at the semantic level. My understanding of the sections IV.5.3 and IV.6.5 of Guillaume Munch-Maccagnoni's thesis is that, in many similar systems, one can prove that such isomorphisms across the two categories of types do not exist.

I see undecidability everywhere

I don't think a lot of math is that precise. I don't even like domain theory.^1

^1. [EDIT] I looked that up. Guess I should say I don't like how people interpret domain theory. The bottom from there looks to be something different than the bottom assumed for, say, a Haskell.

Is the answer to your question really “probably not”?

Hi, thanks for the plug. This notion of isomorphism indeed arises very naturally as those pairs of inverse morphisms A→B and B→A that are both at the same time linear and thunkable. When A and B are homogeneous this is equivalent to either A and B are both positive and both morphisms are thunkable, or they are both negative and both morphisms are linear (in fact, it suffices that one morphism be thunkable or linear for the other one to be likewise).

However when, say, A is positive and B is negative, such an isomorphism decomposes into a (linear) isomorphism between FA and B and the equality ηGFA=GFηA:GFA→GFGFA (or equivalently a (thunkable) isomorphism between A and GB together with the equality εFGB=FGεB:FGFGB→FGB). In fact, whenever two types are isomorphic in the above sense then they share the same polarities, for a relaxed notion of polarities in which an object can be both positive and negative. This is related to the notion of fixed point of an adjunction for which there are plenty of examples outside of PL, but it is interesting that polarisation arose from an example (classical logic) where this fixed point is void, as you recall.