Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 6th 2015

Thought I should put some content into coercion. I’m sure it could be much better phrased. What should be said about the kind of $c:(A \to B)$ that can be used to coerce?

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeFeb 6th 2015

I don’t think it’s anything about $c$ itself; you just want the collection of all coercions to form a commutative diagram, so there is no ambiguity.

1. To put it a bit more abstractly, for a coercive semantics of a language with subtyping, the general property that you want is coherence: any two typing derivations of the same typing judgment have the same interpretation. A paper I highly recommend exploring these issues is John Reynolds’ The Meaning of Types: From Intrinsic to Extrinsic Semantics (see in particular his Definition 2.2).

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 7th 2015

Could we summarise what’s said in #2 and #3 as

All the coercions of a type system must be coherent in the sense that any two typing derivations of one type as a subtype of another must agree.

I’m sure you experts could say it properly.

Is it worth a mention of coercion in universes in HoTT?

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeFeb 7th 2015

What do you mean by “coercion in universes in HoTT”?

• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 7th 2015

I just meant the appearance of coercion in the HoTT book, e.g.,

coercion, universe-raising, 54

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeFeb 8th 2015

Ok – there’s nothing specific to HoTT about that, but we could certainly mention that the inclusion of a smaller universe in a larger one is often a coercion.

• CommentRowNumber8.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 8th 2015

Do people also think of $Prop$ and $Set$ within $Type$ as a coercion?

• CommentRowNumber9.
• CommentAuthorNoam_Zeilberger
• CommentTimeFeb 8th 2015
• (edited Feb 8th 2015)

Re: #4, I would put things a little differently, and I would actually delay speaking of dependent types and HoTT until after the Idea section.

First, coherence is something that can hold for a particular style of semantics of a type system, rather than for a type system itself. In particular, whenever you have a type system with a non-trivial subtyping relation, it is pertinent to consider the meaning of the subsumption rule:

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

One potential reading is that the types $A$ and $B$ denote properties of terms, in which case the rule is read as applying an entailment between properties $A \le B$ to go from the fact that $e$ satisfies $A$ to the fact that $e$ also satisfies $B$. This is what Reynolds calls an “extrinsic semantics” of the type system, since terms have a meaning independently of types. Under such a style of semantics the question of coherence does not arise, but it commits you to interpreting “untyped” terms, which might not be what you want to do (I put “untyped” in quotes because that’s the traditional way of putting things, but as usual, it can be taken to mean “uni-typed”, or better, “more coarsely-typed”).

On the other hand, in what Reynolds calls an “intrinsic semantics”, meanings are assigned to typing judgments rather than to untyped terms. Under this style of semantics, the subsumption rule is seen as introducing an implicit coercion — or more formally, the rule is interpreted as constructing a generalized element $[[e:B]]$ of $[[B]]$, by composing a generalized element $[[e:A]]$ of $[[A]]$ with a map $[[A\le B]] : [[A]]\to [[B]]$. Since both of these actually come from interpreting derivations of the premises $e:A$ and $A \le B$, this is where the question of coherence arises – if the type system allows for multiple derivations of the same judgment, we better make sure that their meanings are identified by the intrinsic semantics.

In the 2000 paper, Reynolds gave a very elegant proof of coherence for an intrinsic semantics of a language with subtyping, by showing how it can be factored by way of an extrinsic semantics (this is his “bracketing theorem”, Theorem 5.7 on p.28).

I believe that this perspective on the general problem of coherence should be compatible with the specific kind of system of coercions described by Luo in those references cited in the article, though I disagree strongly with some of the things written there (e.g., in the SALT 2010 paper, “subsumptive subtyping is incompatible with canonicity and cannot be employed in a modern type theory”). On the other hand, what makes this trickier to apply to dependent types is that as far as I know nothing like Reynolds’ bracketing theorem has been considered in that setting.

• CommentRowNumber10.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 8th 2015

Great! By all means, paste this into the entry.

2. I went ahead and inserted this (slightly augmented) material into the Idea section, and also added a sketch of Reynolds’ proof of coherence.

• CommentRowNumber12.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 9th 2015

Thanks!

• CommentRowNumber13.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 13th 2015
• (edited Feb 13th 2015)

I was wondering over here about something like:

$\frac {\vdash a, b: A \;\;\; \vdash p:Id_A(a,b) \;\;\; \vdash A \lt_{c} B : Type}{\vdash p: Id_B (a, b)}?$

In general, with a $c: A \to B$, there would be a type $Id_B(c(a), c(b))$. With coercion, I’m allowed to rewrite this as $Id_B(a, b))$?

Then term elimination should allow me to pass from $p:Id_A(a,b)$ to $J(p): Id_B(a, b)$, for some function $J$?

Then I could coerce from $Id_A(a,b)$ to $Id_B(a, b)$, so call the $J(p)$ simply $p$?

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeFeb 13th 2015

In general I think people do study this sort of rule; Noam can probably say more. It’s tricky because not all type formers are covariant, e.g. function types are contravariant in one argument. The way coercions are implemented in Coq, which is the one I’m most familiar with, this would not be allowed.