The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

On Wednesday 16 September 2009 17:13:01 Adam Chlipala wrote:
> 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.

One would like the virtual machine to make use of the Prop/Type distinction too. Russell O'Connor has argued, convincingly IMO, that the vm should be eager on Set/Type and lazy on Prop. However, I don't think this has ever been implemented yet.

Bas