Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A question concerning certain variant of the Prod rule

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A question concerning certain variant of the Prod rule


chronological Thread 
  • From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
  • To: Matej Kosik <kosik AT fiit.stuba.sk>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] A question concerning certain variant of the Prod rule
  • Date: Thu, 16 Apr 2009 08:51:49 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page