nLab coercion

Idea

A question that is traditionally of some debate in type theory is,

What does it mean for a term to have more than one type?

This question is relevant in a number of situations:

• the interpretation of polymorphism

• subtyping

• judgmental equality of types

Subtyping

One place where the above question is relevant is for type systems with a non-trivial subtyping relation, in which case it becomes pertinent to consider the meaning of the subsumption rule:

$$\frac{e:A \qquad A \le B}{e:B}$$

One possibility (sometimes called the inclusion interpretation of subtyping) is based on the idea of interpreting types as properties of terms (what is also sometimes called “types à la Curry”, or the extrinsic view of typing). Under this interpretation, the subsumption rule can be read more or less literally, as asserting that if $e$ satisfies the property $A$, and $A$ entails $B$, then $e$ also satisfies the property $B$. One potential drawback of this interpretation, though, is that it seems to commit you to giving a meaning to “untyped” terms (although these terms may of course intrinsically have some more coarse-grained type structure, as in models of pure lambda calculus by reflexive objects).

A different possibility (sometimes called the coercion interpretation of subtyping) is to read the subsumption rule as introducing an implicit coercion from $A$ to $B$. Under this interpretation, subtyping can be seen as simply providing a convenient shorthand notation, when having to write out these coercions explicitly would be too burdensome. This interpretation allows one to maintain an intrinsic (“à la Church”) view of typing, but on the other hand it introduces a subtle issue of coherence: if there is more than one way of deriving the subtyping judgment $A \le B$, we would like to know that all of these result in equivalent coercions from $A$ to $B$, so that the meaning of a well-typed term is independent of its typing derivation.

In dependent type theory

Consider a dependent proposition $A: Type, x:A \vdash P(x):Prop$. Then the dependent sum, $\sum_{x:A} P(x)$, may be thought of as ‘$A$s which are $P$’. Sometimes it is convenient to identify a term of this dependent sum as though it were a term of the full type $A$. Here we can use the first projection of the dependent sum to coerce the identification.

For example, we might have introduced ‘Eve’ as a term of type $Woman$, and then wish to form a type $Relatives(Eve)$, when $Relatives(x)$ had been introduced as a type depending on $x: Human$. If $Woman$ had been defined as $\sum_{x:Human} Female(x)$, then $Eve$ has projections to the underlying human and to a warrant for Eve’s being female. It would be clumsy to insist on $Relatives(\pi_1(Eve))$. Coercion along this projection allows us to form $Relatives(Eve)$.

Luo (1999) proposed a way of formalizing coercions in dependent type theory, through what he calls the coercive definition rule, which when generalized to allow dependency on the coerced term is:

$$\frac{\Gamma, x: B \vdash f(x) : C(x) \; \; \; \Gamma \vdash a : A \;\;\;\Gamma \vdash A \lt_{c} B : Type}{\Gamma \vdash f(a) = f(c(a)) : C(c(a))}$$

In this notation, a coercion between two types $A$ and $B$ is denoted $A \lt_{c} B$, for $c: (A \to B)$.

In HoTT

In homotopy type theory, the inclusion of a smaller universe in type theory in a larger one is often considered as a coercion.

Coherence

Reynolds (2000) gave an interesting proof of coherence for a coercion interpretation of a language with subtyping. The proof works by first building a logical relation between this “intrinsic semantics” and a separate untyped semantics of the language (the latter based on interpreting programs as elements of a universal domain $U$), and then establishing a “bracketing theorem” which says that for any domain $[[A]]$ in the image of the intrinsic semantics, there are a pair of functions $\phi_A : [[A]] \to U$ and $\psi_A : U \to [[A]]$ such that

• for any $a\in [[A]]$, $a$ is logically related to $\phi_A(a)$
• if $a$ is logically related to $x$, then $a = \psi_A(x)$

Combined, the logical relations theorem and the bracketing theorem imply that the coercion $[[\alpha]] : [[A]] \to [[B]]$ associated to any derivation $\alpha$ of a subtyping judgment $A \le B$ can be factored as

$$\begin{matrix} [[A]] &\overset{\phi_A}{\to} & U & \overset{\psi_B}{\to} & [[B]] \end{matrix}$$

and hence in particular that any two derivations $\alpha_1,\alpha_2$ of $A \le B$ result in the same coercion $[[\alpha_1]] = [[\alpha_2]] = (\phi_A;\psi_B) : [[A]] \to [[B]]$.

Judgmental equality of types

Another place where the above question is relevant in any dependent type theory which uses a separate type judgment and judgmental equality of types: if two types are judgmentally equal, then every term of the first type is also a term of the second type. This is given from the element conversion rule of judgmental equality,

$$\frac{e:A \qquad A \equiv B}{e:B}$$

which is provable from the structural rules of judgmental equality (cf. section 1.1 & exercise 1.1 of Rijke22).

Judgmental equality of types is the symmetric version of subtyping, since subtyping forms a preorder on types while judgmental equality forms an equivalence relation on types, which is a symmetric preorder. Thus, the same interpretations of subtyping also apply to judgmental equality:

One possibility (sometimes called the inclusion interpretation of judgmental equality) is based on the idea of interpreting types as properties of terms (what is also sometimes called “types à la Curry”, or the extrinsic view of typing). Under this interpretation, the element conversion rule can be read more or less literally, as asserting that if $e$ satisfies the property $A$, and $A$ is logically equivalent to $B$, then $e$ also satisfies the property $B$. One potential drawback of this interpretation, though, is that it seems to commit you to giving a meaning to “untyped” terms (although these terms may of course intrinsically have some more coarse-grained type structure, as in models of pure lambda calculus by reflexive objects).

A different possibility (sometimes called the coercion interpretation of judgmental equality) is to read the subsumption rule as introducing an implicit coercion from $A$ to $B$. Under this interpretation, judgmental equality can be seen as simply providing a convenient shorthand notation, when having to write out these coercions explicitly would be too burdensome. This interpretation allows one to maintain an intrinsic (“à la Church”) view of typing, but on the other hand it introduces a subtle issue of coherence: if there is more than one way of deriving the judgmental equality $A \equiv B$, we would like to know that all of these result in equivalent coercions from $A$ to $B$, so that the meaning of a well-typed term is independent of its typing derivation.

Related concepts

• subtype

• judgmental equality

References

• John C. Reynolds, Using Category Theory to Design Implicit Conversions and Generic Operators, In Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation (January 14-18, 1980), Springer-Verlag. (pdf)

• John C. Reynolds, The Coherence of Languages with Intersection Types. TACS 1991. (ps)

• John C. Reynolds, The Meaning of Types: from Intrinsic to Extrinsic Semantics. BRICS Report RS-00-32, Aarhus University, December 2000. (pdf)

• Zhaohui Luo, Coercive subtyping. Journal of Logic and Computation, 9(1):105–130, 1999. ps file.

• Zhaohui Luo, Type-Theoretical Semantics with Coercive Subtyping, pdf

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)