Mercurial > cpdt > repo

comparison src/Universes.v @ 233:f15f7c4eebfe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mention fake universe polymorphism
author Adam Chlipala <adamc@hcoop.net>
date Mon, 30 Nov 2009 14:21:34 -0500
parents bc0f515a929f
children be571572c088
comparison
equal deleted inserted replaced
232:d1e0a6d8eef1 233:f15f7c4eebfe
289 289
290 Error: Universe inconsistency (cannot enforce Top.51 < Top.51). 290 Error: Universe inconsistency (cannot enforce Top.51 < Top.51).
291 291
292 ]] 292 ]]
293 293
294 The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors. Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints. *) 294 The key benefit parameters bring us is the ability to avoid quantifying over types in the types of constructors. Such quantification induces less-than constraints, while parameters only introduce less-than-or-equal-to constraints.
295
296 Coq includes one more (potentially confusing) feature related to parameters. While Gallina does not support real universe polymorphism, there is a convenience facility that mimics universe polymorphism in some cases. We can illustrate what this means with a simple example. *)
297
298 Inductive foo (A : Type) : Type :=
299 | Foo : A -> foo A.
295 300
296 (* begin hide *) 301 (* begin hide *)
297 Unset Printing Universes. 302 Unset Printing Universes.
298 (* end hide *) 303 (* end hide *)
304
305 Check foo nat.
306 (** %\vspace{-.15in}% [[
307 foo nat
308 : Set
309 ]] *)
310
311 Check foo Set.
312 (** %\vspace{-.15in}% [[
313 foo Set
314 : Type
315 ]] *)
316
317 Check foo True.
318 (** %\vspace{-.15in}% [[
319 foo True
320 : Prop
321
322 ]]
323
324 The basic pattern here is that Coq is willing to automatically build a "copied-and-pasted" version of an inductive definition, where some occurrences of [Type] have been replaced by [Set] or [Prop]. In each context, the type-checker tries to find the valid replacements that are lowest in the type hierarchy. Automatic cloning of definitions can be much more convenient than manual cloning. We have already taken advantage of the fact that we may re-use the same families of tuple and list types to form values in [Set] and [Type].
325
326 Imitation polymorphism can be confusing in some contexts. For instance, it is what is responsible for this weird behavior. *)
327
328 Inductive bar : Type := Bar : bar.
329
330 Check bar.
331 (** %\vspace{-.15in}% [[
332 bar
333 : Prop
334
335 ]]
336
337 The type that Coq comes up with may be used in strictly more contexts than the type one might have expected. *)
299 338
300 339
301 (** * The [Prop] Universe *) 340 (** * The [Prop] Universe *)
302 341
303 (** In Chapter 4, we saw parallel versions of useful datatypes for "programs" and "proofs." The convention was that programs live in [Set], and proofs live in [Prop]. We gave little explanation for why it is useful to maintain this distinction. There is certainly documentation value from separating programs from proofs; in practice, different concerns apply to building the two types of objects. It turns out, however, that these concerns motivate formal differences between the two universes in Coq. 342 (** In Chapter 4, we saw parallel versions of useful datatypes for "programs" and "proofs." The convention was that programs live in [Set], and proofs live in [Prop]. We gave little explanation for why it is useful to maintain this distinction. There is certainly documentation value from separating programs from proofs; in practice, different concerns apply to building the two types of objects. It turns out, however, that these concerns motivate formal differences between the two universes in Coq.