Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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 that can be used to coerce?
I don’t think it’s anything about itself; you just want the collection of all coercions to form a commutative diagram, so there is no ambiguity.
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).
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?
What do you mean by “coercion in universes in HoTT”?
I just meant the appearance of coercion in the HoTT book, e.g.,
coercion, universe-raising, 54
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.
Do people also think of and within as a coercion?
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:
One potential reading is that the types and denote properties of terms, in which case the rule is read as applying an entailment between properties to go from the fact that satisfies to the fact that also satisfies . 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 of , by composing a generalized element of with a map . Since both of these actually come from interpreting derivations of the premises and , 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.
Great! By all means, paste this into the entry.
I went ahead and inserted this (slightly augmented) material into the Idea section, and also added a sketch of Reynolds’ proof of coherence.
Thanks!
I was wondering over here about something like:
In general, with a , there would be a type . With coercion, I’m allowed to rewrite this as ?
Then term elimination should allow me to pass from to , for some function ?
Then I could coerce from to , so call the simply ?
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.
1 to 14 of 14