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.
I have added the following paragraph to calculus of constructions, I’d be grateful if experts could briefly give me a sanity check that this is an accurate characterization:
More in detail, the Calculus of (co)Inductive Constructions is
a system of natural deduction with dependent types;
with the natural-deduction rules for dependent product types specified;
and with a rule for how to introduce new such natural-deduction rules for arbitrary (co)inductive types.
and with a type of types (hierarchy).
Number 4 should be more precise: An impredicative universe (type of types), Prop, and a cumulative hierarchy of predicative universes (types of types), Type$_i$, on top of Prop.
Otherwise it looks fine!
Thanks! (On both accounts.)
I have changed it now as suggested in the entry.
But: can’t we allow ourselves not to demand the Prop-universe and still speak of a “calculus of constructions”?
Great.
But: can’t we allow ourselves not to demand the Prop-universe and still speak of a “calculus of constructions”?
Quite possibly when you say a CoC as opposed to the CoC! But I’m not sure how I’d define a CoC. I think the version with only predicative universes goes by the name of predicative type theory, but that’s also not quite a definite phrase.
Okay, thanks.
I gather that one of the four (or so) “teams” at the IAS HoTT program is concerned with doing something like re-writing Coq to make it homotopy-native.
I assume that in the course of doing so, they will re-examine these notions. I assume they will come up with a Calculus of homotopy-inductive Constructions, which
refines inductive types to higher inductive types;
drops the Prop-universe.
Maybe in the near future there’ll be some preliminary notes on this, and then maybe I’ll be allowed to point to it as “another CoC” without Prop-universe :-)
Let’s not proliferate terminology! “The CoC” is a particular type theory, with impredicative quantification. “The predicative CoC” is another one, as is “the predicative CoiC” — the latter is roughly the one that Coq is based on. We already have general notions like “a pure type system” and “a type theory” and “a dependent type theory” — I don’t see any need for a general notion of “a calculus of constructions”.
I agree with Mike about not proliferating terminology.
I know the Coq manual refers to the “predicative calculus of constructions” (with one impredicative sort, Prop) to distinguish it from the “impredicative calculus of constructions” (with two impredicative sorts, Prop and Set). However, I think I’m not the only one who finds that terminology confusing!
What do we then call the base of Agda? (I know, that’s a moving target!) – Last I checked, Agda had a non-cumulative hierarchy of predicative universes, and type of universe levels, rather fancy indexed induction-recursion and induction-induction, and a monadic(?) way of treating coinduction with operators ♯ and♭.
@Ulrik, that’s sure a good point about “predicative CoC” including impredicative Prop! Maybe it would be better called “semipredicative”.
I don’t think I’ve heard anyone call the type theory underlying Agda anything but “the type theory underlying Agda”. (-:
What’s the technical definition of “cumulative hierarchy”. Can a hierarchy of universes not be cumulative?
Cumulativity means that $A:Type_i$ implies $A:Type_{i+1}$ (so $Type_i$ is a subtype of $Type_{i+1}$). In Agda, you have to use an explicit raise operator $Type_i\to Type_{i+1}$. It’s much easier not to worry about subtyping rules. With subtyping, you have to work a bit to get principal types. I think that was first worked out in Luo’s PhD thesis, An Extended Calculus of Constructions, and in Harper and Pollack’s Type Checking with Universes. However, I’m not an expert here, so perhaps Mike can ask someone at IAS about the precise history.
Where “easier” means “easier for the formal theory of the type system, but much more tedious for the actual user”. (-:
Absolutely! (-:
Also, concerning type checking with universes, we should mention Gérard Huet’s Extending the Calculus of Constructions with Type:Type, which is an unpublished manuscript from 1987 that’s often referred to. But I haven’t seen it.
Yes, probably. (-:
@heades in #13,
could you say more concretely what’s wrong with the entry, if anything? Where it gives that numberd item list it does refer to CiC and “with inductive types”. That seems to agree with your #13!?
I also have a general question: what is the difference between CoC and PTS? It seems to me that if I remove from CiC the inductive types I am left with just PTS. Well, and universes. Is that the difference?
PTS refers to a class of type theories, not to any particular one. CoC can be presented as a PTS.
Hmm, that’s interesting. I wasn’t aware that Set was considered part of CiC but not CoC.
added this pointer:
1 to 23 of 23