nLab coercion

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

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:

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:

e:AABe:B\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 ee satisfies the property AA, and AA entails BB, then ee also satisfies the property BB. 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 AA to BB. 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 ABA \le B, we would like to know that all of these result in equivalent coercions from AA to BB, 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:AP(x):PropA: Type, x:A \vdash P(x):Prop. Then the dependent sum, x:AP(x)\sum_{x:A} P(x), may be thought of as ‘AAs which are PP’. Sometimes it is convenient to identify a term of this dependent sum as though it were a term of the full type AA. 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 WomanWoman, and then wish to form a type Relatives(Eve)Relatives(Eve), when Relatives(x)Relatives(x) had been introduced as a type depending on x:Humanx: Human. If WomanWoman had been defined as x:HumanFemale(x)\sum_{x:Human} Female(x), then EveEve has projections to the underlying human and to a warrant for Eve’s being female. It would be clumsy to insist on Relatives(π 1(Eve))Relatives(\pi_1(Eve)). Coercion along this projection allows us to form Relatives(Eve)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:

Γ,x:Bf(x):C(x)Γa:AΓA< cB:TypeΓf(a)=f(c(a)):C(c(a)) \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 AA and BB is denoted A< cBA \lt_{c} B, for c:(AB)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 UU), and then establishing a “bracketing theorem” which says that for any domain [[A]][[A]] in the image of the intrinsic semantics, there are a pair of functions ϕ A:[[A]]U\phi_A : [[A]] \to U and ψ A:U[[A]]\psi_A : U \to [[A]] such that

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

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

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

and hence in particular that any two derivations α 1,α 2\alpha_1,\alpha_2 of ABA \le B result in the same coercion [[α 1]]=[[α 2]]=(ϕ A;ψ B):[[A]][[B]][[\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,

e:AABe:B\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 ee satisfies the property AA, and AA is logically equivalent to BB, then ee also satisfies the property BB. 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 AA to BB. 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 ABA \equiv B, we would like to know that all of these result in equivalent coercions from AA to BB, so that the meaning of a well-typed term is independent of its typing derivation.

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)

Last revised on January 13, 2024 at 17:14:57. See the history of this page for a list of all contributions to it.