Mercurial > cpdt > repo
comparison src/Generic.v @ 408:7c2167c3fbb2
Typesetting pass over Generic
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 08 Jun 2012 14:49:56 -0400 |
parents | 05efde66559d |
children | b027b39606ed |
comparison
equal
deleted
inserted
replaced
407:ff0aef0f33a5 | 408:7c2167c3fbb2 |
---|---|
13 Require Import CpdtTactics DepList. | 13 Require Import CpdtTactics DepList. |
14 | 14 |
15 Set Implicit Arguments. | 15 Set Implicit Arguments. |
16 (* end hide *) | 16 (* end hide *) |
17 | 17 |
18 (** printing ~> $\leadsto$ *) | |
19 | |
18 | 20 |
19 (** %\chapter{Generic Programming}% *) | 21 (** %\chapter{Generic Programming}% *) |
20 | 22 |
21 (** %\index{generic programming}%_Generic programming_ makes it possible to write functions that operate over different types of data. %\index{parametric polymorphism}%Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style %\index{module systems}%module systems%~\cite{modules}% and Haskell %\index{type classes}%type classes%~\cite{typeclasses}% are more flexible cases. These language features are often not as powerful as we would like. For instance, while Haskell includes a type class classifying those types whose values can be pretty-printed, per-type pretty-printing is usually either implemented manually or implemented via a %\index{deriving clauses}%[deriving] clause%~\cite{deriving}%, which triggers ad-hoc code generation. Some clever encoding tricks have been used to achieve better within Haskell and other languages, but we can do %\index{datatype-generic programming}%_datatype-generic programming_ much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support. | 23 (** %\index{generic programming}% _Generic programming_ makes it possible to write functions that operate over different types of data. %\index{parametric polymorphism}%Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style %\index{module systems}%module systems%~\cite{modules}% and Haskell %\index{type classes}%type classes%~\cite{typeclasses}% are more flexible cases. These language features are often not as powerful as we would like. For instance, while Haskell includes a type class classifying those types whose values can be pretty-printed, per-type pretty-printing is usually either implemented manually or implemented via a %\index{deriving clauses}%[deriving] clause%~\cite{deriving}%, which triggers ad-hoc code generation. Some clever encoding tricks have been used to achieve better within Haskell and other languages, but we can do%\index{datatype-generic programming}% _datatype-generic programming_ much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support. |
22 | 24 |
23 Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it. In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *) | 25 Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it. In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *) |
24 | 26 |
25 (** * Reflecting Datatype Definitions *) | 27 (** * Reflecting Datatype Definitions *) |
26 | 28 |
27 (** The key to generic programming with dependent types is %\index{universe types}%_universe types_. This concept should not be confused with the idea of _universes_ from the metatheory of CIC and related languages. Rather, the idea of universe types is to define inductive types that provide _syntactic representations_ of Coq types. We cannot directly write CIC programs that do case analysis on types, but we _can_ case analyze on reflected syntactic versions of those types. | 29 (** The key to generic programming with dependent types is%\index{universe types}% _universe types_. This concept should not be confused with the idea of _universes_ from the metatheory of CIC and related languages. Rather, the idea of universe types is to define inductive types that provide _syntactic representations_ of Coq types. We cannot directly write CIC programs that do case analysis on types, but we _can_ case analyze on reflected syntactic versions of those types. |
28 | 30 |
29 Thus, to begin, we must define a syntactic representation of some class of datatypes. In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions. | 31 Thus, to begin, we must define a syntactic representation of some class of datatypes. In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions. |
30 | 32 |
31 The first step is to define a representation for constructors of our datatypes. *) | 33 The first step is to define a representation for constructors of our datatypes. *) |
32 | 34 |
84 | 86 |
85 End denote. | 87 End denote. |
86 (* end thide *) | 88 (* end thide *) |
87 | 89 |
88 (** Some example pieces of evidence should help clarify the convention. First, we define some helpful notations, providing different ways of writing constructor denotations. There is really just one notation, but we need several versions of it to cover different choices of which variables will be used in the body of a definition. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *) | 90 (** Some example pieces of evidence should help clarify the convention. First, we define some helpful notations, providing different ways of writing constructor denotations. There is really just one notation, but we need several versions of it to cover different choices of which variables will be used in the body of a definition. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *) |
89 | |
90 (** printing ~> $\leadsto$ *) | |
91 | 91 |
92 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)). | 92 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)). |
93 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)). | 93 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)). |
94 Notation "[ ! , r ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ _)). | 94 Notation "[ ! , r ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ _)). |
95 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)). | 95 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)). |
114 | 114 |
115 (** * Recursive Definitions *) | 115 (** * Recursive Definitions *) |
116 | 116 |
117 (* EX: Define a generic [size] function. *) | 117 (* EX: Define a generic [size] function. *) |
118 | 118 |
119 (** We built these encodings of datatypes to help us write datatype-generic recursive functions. To do so, we will want a reflected representation of a %\index{recursion schemes}%_recursion scheme_ for each type, similar to the [T_rect] principle generated automatically for an inductive definition of [T]. A clever reuse of [datatypeDenote] yields a short definition. *) | 119 (** We built these encodings of datatypes to help us write datatype-generic recursive functions. To do so, we will want a reflected representation of a%\index{recursion schemes}% _recursion scheme_ for each type, similar to the [T_rect] principle generated automatically for an inductive definition of [T]. A clever reuse of [datatypeDenote] yields a short definition. *) |
120 | 120 |
121 (* begin thide *) | 121 (* begin thide *) |
122 Definition fixDenote (T : Type) (dt : datatype) := | 122 Definition fixDenote (T : Type) (dt : datatype) := |
123 forall (R : Type), datatypeDenote R dt -> (T -> R). | 123 forall (R : Type), datatypeDenote R dt -> (T -> R). |
124 | 124 |
476 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)), | 476 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)), |
477 (forall i : fin (recursive c), P (get r i)) | 477 (forall i : fin (recursive c), P (get r i)) |
478 -> P ((hget dd m) x r)) | 478 -> P ((hget dd m) x r)) |
479 -> forall v, P v. | 479 -> forall v, P v. |
480 | 480 |
481 (** This definition can take a while to digest. The quantifier over [m : member c dt] is considering each constructor in turn; like in normal induction principles, each constructor has an associated proof case. The expression [hget dd m] then names the constructor we have selected. After binding [m], we quantify over all possible arguments (encoded with [x] and [r]) to the constructor that [m] selects. Within each specific case, we quantify further over [i : fin (][recursive c)] to consider all of our induction hypotheses, one for each recursive argument of the current constructor. | 481 (** This definition can take a while to digest. The quantifier over [m : member c dt] is considering each constructor in turn; like in normal induction principles, each constructor has an associated proof case. The expression [hget dd m] then names the constructor we have selected. After binding [m], we quantify over all possible arguments (encoded with [x] and [r]) to the constructor that [m] selects. Within each specific case, we quantify further over [i : fin (recursive c)] to consider all of our induction hypotheses, one for each recursive argument of the current constructor. |
482 | 482 |
483 We have completed half the burden of defining side conditions. The other half comes in characterizing when a recursion scheme [fx] is valid. The natural condition is that [fx] behaves appropriately when applied to any constructor application. *) | 483 We have completed half the burden of defining side conditions. The other half comes in characterizing when a recursion scheme [fx] is valid. The natural condition is that [fx] behaves appropriately when applied to any constructor application. *) |
484 | 484 |
485 Definition fixDenoteOk := | 485 Definition fixDenoteOk := |
486 forall (R : Type) (cases : datatypeDenote R dt) | 486 forall (R : Type) (cases : datatypeDenote R dt) |