## Mercurial > cpdt > repo

### comparison src/Universes.v @ 505:2036ef0bc891

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Pass through Chapter 12

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Sun, 10 Feb 2013 15:40:28 -0500 |

parents | 31258618ef73 |

children | fd6ec9b2dccb |

comparison

equal
deleted
inserted
replaced

504:04177dd1b133 | 505:2036ef0bc891 |
---|---|

173 %\index{universe inconsistency}%This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is _predicative_, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, when an object is defined using some sort of quantifier, none of the quantifiers may ever be instantiated with the object itself. %\index{impredicativity}%Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like "the set of all sets that do not contain themselves" (%\index{Russell's paradox}%Russell's paradox). Similar paradoxes would result from uncontrolled impredicativity in Coq. *) | 173 %\index{universe inconsistency}%This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is _predicative_, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, when an object is defined using some sort of quantifier, none of the quantifiers may ever be instantiated with the object itself. %\index{impredicativity}%Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like "the set of all sets that do not contain themselves" (%\index{Russell's paradox}%Russell's paradox). Similar paradoxes would result from uncontrolled impredicativity in Coq. *) |

174 | 174 |

175 | 175 |

176 (** ** Inductive Definitions *) | 176 (** ** Inductive Definitions *) |

177 | 177 |

178 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T]. | 178 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for an encoded expression of type [T]. |

179 [[ | 179 [[ |

180 Inductive exp : Set -> Set := | 180 Inductive exp : Set -> Set := |

181 | Const : forall T : Set, T -> exp T | 181 | Const : forall T : Set, T -> exp T |

182 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) | 182 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) |

183 | Eq : forall T, exp T -> exp T -> exp bool. | 183 | Eq : forall T, exp T -> exp T -> exp bool. |

192 Inductive exp : Type -> Type := | 192 Inductive exp : Type -> Type := |

193 | Const : forall T, T -> exp T | 193 | Const : forall T, T -> exp T |

194 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) | 194 | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2) |

195 | Eq : forall T, exp T -> exp T -> exp bool. | 195 | Eq : forall T, exp T -> exp T -> exp bool. |

196 | 196 |

197 (** Note that before we had to include an annotation [: Set] for the variable [T] in [Const]'s type, but we need no annotation now. When the type of a variable is not known, and when that variable is used in a context where only types are allowed, Coq infers that the variable is of type [Type]. That is the right behavior here, but it was wrong for the [Set] version of [exp]. | 197 (** Note that before we had to include an annotation [: Set] for the variable [T] in [Const]'s type, but we need no annotation now. When the type of a variable is not known, and when that variable is used in a context where only types are allowed, Coq infers that the variable is of type [Type], the right behavior here, though it was wrong for the [Set] version of [exp]. |

198 | 198 |

199 Our new definition is accepted. We can build some sample expressions. *) | 199 Our new definition is accepted. We can build some sample expressions. *) |

200 | 200 |

201 Check Const 0. | 201 Check Const 0. |

202 (** %\vspace{-.15in}% [[ | 202 (** %\vspace{-.15in}% [[ |

240 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ), | 240 | Pair : forall (T1 : Type $ Top.14 ^ ) (T2 : Type $ Top.15 ^ ), |

241 exp T1 -> exp T2 -> exp (T1 * T2) | 241 exp T1 -> exp T2 -> exp (T1 * T2) |

242 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool | 242 | Eq : forall T : Type $ Top.19 ^ , exp T -> exp T -> exp bool |

243 ]] | 243 ]] |

244 | 244 |

245 We see that the index type of [exp] has been assigned to universe level [Top.8]. In addition, each of the four occurrences of [Type] in the types of the constructors gets its own universe variable. Each of these variables appears explicitly in the type of [exp]. In particular, any type [exp T] lives at a universe level found by incrementing by one the maximum of the four argument variables. A consequence of this is that [exp] _must_ live at a higher universe level than any type which may be passed to one of its constructors. This consequence led to the universe inconsistency. | 245 We see that the index type of [exp] has been assigned to universe level [Top.8]. In addition, each of the four occurrences of [Type] in the types of the constructors gets its own universe variable. Each of these variables appears explicitly in the type of [exp]. In particular, any type [exp T] lives at a universe level found by incrementing by one the maximum of the four argument variables. Therefore, [exp] _must_ live at a higher universe level than any type which may be passed to one of its constructors. This consequence led to the universe inconsistency. |

246 | 246 |

247 Strangely, the universe variable [Top.8] only appears in one place. Is there no restriction imposed on which types are valid arguments to [exp]? In fact, there is a restriction, but it only appears in a global set of universe constraints that are maintained "off to the side," not appearing explicitly in types. We can print the current database.%\index{Vernacular commands!Print Universes}% *) | 247 Strangely, the universe variable [Top.8] only appears in one place. Is there no restriction imposed on which types are valid arguments to [exp]? In fact, there is a restriction, but it only appears in a global set of universe constraints that are maintained "off to the side," not appearing explicitly in types. We can print the current database.%\index{Vernacular commands!Print Universes}% *) |

248 | 248 |

249 Print Universes. | 249 Print Universes. |

250 (** %\vspace{-.15in}% [[ | 250 (** %\vspace{-.15in}% [[ |

279 | 279 |

280 Thus it is apparent that Coq maintains a tortuous set of universe variable inequalities behind the scenes. It may look like some functions are polymorphic in the universe levels of their arguments, but what is really happening is imperative updating of a system of constraints, such that all uses of a function are consistent with a global set of universe levels. When the constraint system may not be evolved soundly, we get a universe inconsistency error. | 280 Thus it is apparent that Coq maintains a tortuous set of universe variable inequalities behind the scenes. It may look like some functions are polymorphic in the universe levels of their arguments, but what is really happening is imperative updating of a system of constraints, such that all uses of a function are consistent with a global set of universe levels. When the constraint system may not be evolved soundly, we get a universe inconsistency error. |

281 | 281 |

282 %\medskip% | 282 %\medskip% |

283 | 283 |

284 Something interesting is revealed in the annotated definition of [prod]. A type [prod A B] lives at a universe that is the maximum of the universes of [A] and [B]. From our earlier experiments, we might expect that [prod]'s universe would in fact need to be _one higher_ than the maximum. The critical difference is that, in the definition of [prod], [A] and [B] are defined as _parameters_; that is, they appear named to the left of the main colon, rather than appearing (possibly unnamed) to the right. | 284 The annotated definition of [prod] reveals something interesting. A type [prod A B] lives at a universe that is the maximum of the universes of [A] and [B]. From our earlier experiments, we might expect that [prod]'s universe would in fact need to be _one higher_ than the maximum. The critical difference is that, in the definition of [prod], [A] and [B] are defined as _parameters_; that is, they appear named to the left of the main colon, rather than appearing (possibly unnamed) to the right. |

285 | 285 |

286 Parameters are not as flexible as normal inductive type arguments. The range types of all of the constructors of a parameterized type must share the same parameters. Nonetheless, when it is possible to define a polymorphic type in this way, we gain the ability to use the new type family in more ways, without triggering universe inconsistencies. For instance, nested pairs of types are perfectly legal. *) | 286 Parameters are not as flexible as normal inductive type arguments. The range types of all of the constructors of a parameterized type must share the same parameters. Nonetheless, when it is possible to define a polymorphic type in this way, we gain the ability to use the new type family in more ways, without triggering universe inconsistencies. For instance, nested pairs of types are perfectly legal. *) |

287 | 287 |

288 Check (nat, (Type, Set)). | 288 Check (nat, (Type, Set)). |

289 (** %\vspace{-.15in}% [[ | 289 (** %\vspace{-.15in}% [[ |

809 (** %\vspace{-.15in}% [[ | 809 (** %\vspace{-.15in}% [[ |

810 constructive_definite_description | 810 constructive_definite_description |

811 : forall (A : Set) (f : A -> nat) (g : nat -> A), | 811 : forall (A : Set) (f : A -> nat) (g : nat -> A), |

812 (forall x : A, g (f x) = x) -> | 812 (forall x : A, g (f x) = x) -> |

813 forall P : A -> Prop, | 813 forall P : A -> Prop, |

814 (forall x : A, {P x} + {~ P x}) -> | 814 (forall x : A, {P x} + { ~ P x}) -> |

815 (exists! x : A, P x) -> {x : A | P x} | 815 (exists! x : A, P x) -> {x : A | P x} |

816 ]] | 816 ]] |

817 *) | 817 *) |

818 | 818 |

819 Print Assumptions constructive_definite_description. | 819 Print Assumptions constructive_definite_description. |

861 exist (fun f => forall x : A, R x (f x)) | 861 exist (fun f => forall x : A, R x (f x)) |

862 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)). | 862 (fun x => proj1_sig (H x)) (fun x => proj2_sig (H x)). |

863 | 863 |

864 (** %\smallskip{}%Via the Curry-Howard correspondence, this "axiom" can be taken to have the same meaning as the original. It is implemented trivially as a transformation not much deeper than uncurrying. Thus, we see that the utility of the axioms that we mentioned earlier comes in their usage to build programs from proofs. Normal set theory has no explicit proofs, so the meaning of the usual axiom of choice is subtly different. In Gallina, the axioms implement a controlled relaxation of the restrictions on information flow from proofs to programs. | 864 (** %\smallskip{}%Via the Curry-Howard correspondence, this "axiom" can be taken to have the same meaning as the original. It is implemented trivially as a transformation not much deeper than uncurrying. Thus, we see that the utility of the axioms that we mentioned earlier comes in their usage to build programs from proofs. Normal set theory has no explicit proofs, so the meaning of the usual axiom of choice is subtly different. In Gallina, the axioms implement a controlled relaxation of the restrictions on information flow from proofs to programs. |

865 | 865 |

866 However, when we combine an axiom of choice with the law of the excluded middle, the idea of "choice" becomes more interesting. Excluded middle gives us a highly non-computational way of constructing proofs, but it does not change the computational nature of programs. Thus, the axiom of choice is still giving us a way of translating between two different sorts of "programs," but the input programs (which are proofs) may be written in a rich language that goes beyond normal computability. This truly is more than repackaging a function with a different type. | 866 However, when we combine an axiom of choice with the law of the excluded middle, the idea of "choice" becomes more interesting. Excluded middle gives us a highly non-computational way of constructing proofs, but it does not change the computational nature of programs. Thus, the axiom of choice is still giving us a way of translating between two different sorts of "programs," but the input programs (which are proofs) may be written in a rich language that goes beyond normal computability. This combination truly is more than repackaging a function with a different type. |

867 | 867 |

868 %\bigskip% | 868 %\bigskip% |

869 | 869 |

870 The Coq tools support a command-line flag %\index{impredicative Set}%<<-impredicative-set>>, which modifies Gallina in a more fundamental way by making [Set] impredicative. A term like [forall T : Set, T] has type [Set], and inductive definitions in [Set] may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for [Prop]. The restriction only applies to large inductive types, where some constructor quantifies over a type of type [Type]. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is [Set] or [Prop]. This contrasts with [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop]. | 870 The Coq tools support a command-line flag %\index{impredicative Set}%<<-impredicative-set>>, which modifies Gallina in a more fundamental way by making [Set] impredicative. A term like [forall T : Set, T] has type [Set], and inductive definitions in [Set] may have constructors that quantify over arguments of any types. To maintain consistency, an elimination restriction must be imposed, similarly to the restriction for [Prop]. The restriction only applies to large inductive types, where some constructor quantifies over a type of type [Type]. In such cases, a value in this inductive type may only be pattern-matched over to yield a result type whose type is [Set] or [Prop]. This rule contrasts with the rule for [Prop], where the restriction applies even to non-large inductive types, and where the result type may only have type [Prop]. |

871 | 871 |

872 In old versions of Coq, [Set] was impredicative by default. Later versions make [Set] predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative [Set] with axioms of choice. In combination with excluded middle or predicate extensionality, this can lead to inconsistency. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *) | 872 In old versions of Coq, [Set] was impredicative by default. Later versions make [Set] predicative to avoid inconsistency with some classical axioms. In particular, one should watch out when using impredicative [Set] with axioms of choice. In combination with excluded middle or predicate extensionality, inconsistency can result. Impredicative [Set] can be useful for modeling inherently impredicative mathematical concepts, but almost all Coq developments get by fine without it. *) |

873 | 873 |

874 (** ** Axioms and Computation *) | 874 (** ** Axioms and Computation *) |

875 | 875 |

876 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of _computational equivalence_ is central to the definition of the formal system. Axioms tend not to play well with computation. Consider this example. We start by implementing a function that uses a type equality proof to perform a safe type-cast. *) | 876 (** One additional axiom-related wrinkle arises from an aspect of Gallina that is very different from set theory: a notion of _computational equivalence_ is central to the definition of the formal system. Axioms tend not to play well with computation. Consider this example. We start by implementing a function that uses a type equality proof to perform a safe type-cast. *) |

877 | 877 |