The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Hello,

As already pointed out by Yanni, the example s = Prop, s'=Set, s''=Set 
is indeed treated in chap. 4:
Sections 4.3.2.4 (page 94), 4.3.3.5 (page 97, study the type of 
False_rec), and 4.3.4 (page 98, study the type of eq_rec).  However, in 
this chapter you won't find out how False_rec and eq_rec are defined.

Thinking in terms of practical use, you may consider a library of arrays 
of natural numbers, where you can read an array of size n only at an 
index i such that i < n.  You would represent the family of types of
arrays with array : nat -> Type, and the read function would have the 
following type:

forall n, array n -> forall i, i < n -> nat

This is a function with 4 arguments (in ML there would only be 3 
arguments), so there are
4 uses of the prod rule to verify that this type is well-typed.

first use : n : nat : Set,   s is Set
second use :  "anonymous variable" : array n : Set, s is Set
third use : i : nat : Set, s is Set
fourth use : "anonymous variable" : i < n : Prop, s is Prop
In all these uses, s' is Set and s'' is Set.

The fact that we can give this type to the read function is the 
distinguishing asset of dependently typed programming: this type imposes 
that the programmer will have to show that all reading accesses in 
arrays are legitimate.  For each reading access, this means either that 
this access will have to be encapsulated inside a proper conditional 
statement (thus entailing a run-time test) or that the legitimacy 
information will be inherited from known properties of the context (thus 
avoiding run-time overhead).  This means that the discipline of 
verifying all you array bounds is enforced by the type verifier, thus at 
compile time.  By comparison, in the Java language, all reading accesses 
in arrays are protected but most of these reading accesses (if not all 
of them) are protected by run-time tests.

Now, there actually are two questions: question one is "how do you write 
a meaningful type that contains both Prop and Set?", and this question 
was answered to by Edsko and Yanni; question two is
"how do you construct a meaningful term that has such a meaningful 
type?", and to have an answer
to this question you need to read on.  I believe that reading until the 
end of chapter 9 will give enough examples.

Yves