The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeffrey Harris wrote:
> I am aware that having the special rule that members of type Prop 
> can't be used for computation is useful for efficiency and for 
> extracting programs, but I was curious as to whether there was any 
> "purely mathematical" (sorry, I know that's not very precise) reason 
> for having this restriction. The same for Set. More specifically, if 
> the Calculus of Inductive Constructions were implemented solely with 
> sorts Type(0), Type(1), etc., what would be the differences between 
> that implementation and the implementation with Set and Prop?

The important difference of [Prop] vs. [Type] is that [Prop] is 
impredicative: you may define a [Prop] by quantifying over all [Prop]s.  
This is a natural thing to do, even in basic theorems about 
"propositional" logic, like this:
   forall P : Prop, P -> ~~P
This statement is itself a [Prop].  If you used [Type] instead of [Prop] 
everywhere (both in this statement and in the standard library), then 
the statement would exist at a higher universe level than the universe 
it quantifies over, so it wouldn't apply to itself.

To me, this justification is separate from the extraction restrictions 
that you asked about.  I think [Prop] (as opposed to impredicative 
[Set]) exists solely to enable extraction of efficient programs, so 
there's not so much detective work required about its justification as 
your question suggests.  Impredicativity in a type without [Prop]'s 
restrictions _is_ inconsistent with some popular classical axioms, so 
there's another reason.

> Also, do you know of any paper which describes the CIC system with the 
> only sorts being the Type(n)'s?

I think I've heard that Agda is purely predicative, but I might be wrong.