Contextual isomorphisms

Contextual Isomorphisms
Paul Blain Levy
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 λ-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.

Contextual equivalence for dependent types

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.

I haven't read the paper, but I followed your translated abstract, and it turns out
I asked a related but harder question before (and got stuck). I've wondered about contextual equivalence for dependently-typed languages (in fact, for arbitrary PTSs, but dependent types were hard enough). That's related because you can't replace a term t1 by another one t2 and preserve types, unless t1 and t2 are beta-equivalent (or definitionally equivalent, if you're looking at Martin-Löf type theory). In particular, if you have a context C, C[t1] might well-typed while C[t2] might not.

If I took a wild guess and stick to Agda terminology, it seems that propositional equality eq : t1 ≡ t2 could imply a contextual equivalence (as in the paper) among them: you can transform C[t1] to C'[t2], since you can substitute t2 for t1 in types, and even viceversa, using subst everywhere needed. And you might want the converse: if t1 and t2 are equivalent, they're also propositionally equal — or heterogeneously equal?

What would you think of this conjecture? Do ideas of the paper make it approachable?

(The reason I got to this question is at some point Cai and I wondered about ILC for arbitrary PTSs, following your comments, and about how one would prove it correct, and it was unclear what program equivalence we could use to state correctness).

What about non-dependent contexts?

In the non-dependent cases, to define contextual equivalence between (t1, t2 : A), we ask that the context C[_] we consider be closed and of ground type, that is we expect a ground/data type G such that

x : A |- C[x] : G

with x not free in C.

I believe that you could keep the same criterion in a dependent type theory (or a PTS); that corresponds to looking only at the "non-dependent" contexts, those whose type do not depend on their hole.

I would be willing to conjecture that this is a good notion of equivalence. It is clearly maximal: if you pick a stronger notion of equivalence (that equate things that are distinguishable by some non-dependent context), you can prove (True = False). It might be "too large", in the sense that using more refined notions contexts that allow some dependencies as you suggest would distinguish terms that cannot be distinguished by non-dependent contexts alone.

I think you're right. What I

I think you're right. What I propose should end up being equivalent to propositional or heterogeneous equality, and weaker than contextual equivalence.

The only remaining point (if this hasn't been solved) is that given two equivalent terms t1 and t2 and a "dependent context" C such that C[t1] is well-typed, how do we adapt C[t2] (by inserting coercions) so that it's well-typed as well?

I can imagine that source-to-source program transformations on dependently typed languages might need a solution.

I believe that you could keep the same criterion in a dependent type theory (or a PTS); that corresponds to looking only at the "non-dependent" contexts, those whose type do not depend on their hole.

To make what you're saying more explicit, it's not just "their final type doesn't depend on the hole" — it's "no intermediate type can depend on the hole" or "the context is unconditionally well-typed".
Specifically, `A []` is only a valid context if A has a "degenerate" (non-dependent) Pi-type (A -> B rather than Pi(x: A). B).

It is clearly maximal: if you pick a stronger notion of equivalence (that equate things that are distinguishable by some non-dependent context), you can prove (True = False).

I agree with that, though HoTT can prove Bool = 1 + 1 without contradictions and I can't fully tell what's the difference, beyond "in HoTT you remove anything that proves that Bool != 1 + 1".

It might be "too large", in the sense that using more refined notions contexts that allow some dependencies as you suggest would distinguish terms that cannot be distinguished by non-dependent contexts alone.

Indeed, but that's probably unavoidable—in Agda, if x : Nat, dependent contexts distinguish x + 1 from 1 + x, because those two terms are only propositionally equal. In particular, you can't introduce a term of type Vec (x + 1) A, only Vec (1 + x) A.
But given a proof of propositional equality among the two, you can fix that using subst.

I'll speculate that if my sketch worked, *and* if all contextual equivalences with non-dependent contexts could be internalized (a separate problem*), the two relations would end up being equivalent. Since probably some equivalences can't be internalized, what I proposed might be only as strong as propositional/het. equality.

*Propositional equality, or even heterogeneous equality, are clearly incomplete as long as you don't internalize parametricity. If you do, I'd guess incompleteness might strike, though I don't quite have a proof.

BTW yours could be a good SO answer

I asked a related question on StackOverflow^H^HTheoretical Computer Science, in case you want to turn your suggestion into an answer...
http://cstheory.stackexchange.com/q/30712/989

Are nested types not a complication?

In a dependent context, you could have t1:*, x:t1 and v:x (or deeper). Wouldn't there be an analogous problem to solve for these deeper levels (a substitution for such v in addition to one for the x)?

I'm being very lazy with the amount of effort I'm putting into this comment, so don't put much effort into a reply if the answer is "no, that's dumb".

Edit: Since *_i is isomorphic to *_j only if i = j, this probably isn't an issue.

That's the sort of questions

That's the sort of questions I'm wondering about, but I'm not sure on the details of your example or on what's *_i.

HTT

Have you read Homotopy Type Theory: Univalent Foundations of Mathematics? There is quite a bit in it about things you can do with propositional equality in ML type theory, some of which may be of interest to your problem. It's a pretty accessible read given your familiarity with MLTT.

Extensional or Intentional

Type equality being a transformation between types seems relatively obvious to me. What is more interesting is whether this transformation is a mapping (so intentional, definitional and decidable) or requires a computation (so extensional, undecidable, may not terminate).

To me the value of a type system is that it is simpler than the language which it types, otherwise you may as well have the language as its own meta-language.

I think the interesting ground is in the computable but decidable area, so not necessarily restricted to definitions of a mapping, but guaranteed to terminate.

As for contextual equality, it seems an interesting concept, and somehow related to Monads, in that Monads provide an embedding of effects in a pure language, and hence remove the need for different contexts. There should be a mapping between the contextual equality of types with effects and monadic types with a non-contextual equality.