Mercurial > cpdt > repo

comparison src/Generic.v @ 457:b1fead9f68f2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proofreading pass through Chapter 11
author Adam Chlipala <adam@chlipala.net>
date Tue, 28 Aug 2012 15:53:21 -0400
parents 8077352044b2
children 4320c1a967c2
comparison
equal deleted inserted replaced
456:848bf35f7f6c 457:b1fead9f68f2
22 22
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. 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.
24 24
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. *) 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. *)
26 26
27 (** * Reflecting Datatype Definitions *) 27 (** * Reifying Datatype Definitions *)
28 28
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. 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 reified syntactic versions of those types.
30 30
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. 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.
32 32
33 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. *)
34 34
35 (* EX: Define a reflected representation of simple algebraic datatypes. *) 35 (* EX: Define a reified representation of simple algebraic datatypes. *)
36 36
37 (* begin thide *) 37 (* begin thide *)
38 Record constructor : Type := Con { 38 Record constructor : Type := Con {
39 nonrecursive : Type; 39 nonrecursive : Type;
40 recursive : nat 40 recursive : nat
52 Definition unit_dt : datatype := Con unit 0 :: nil. 52 Definition unit_dt : datatype := Con unit 0 :: nil.
53 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil. 53 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
54 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil. 54 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
55 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil. 55 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
56 56
57 (** The type [Empty_set] has no constructors, so its representation is the empty list. The type [unit] has one constructor with no arguments, so its one reflected constructor indicates no non-recursive data and [0] recursive arguments. The representation for [bool] just duplicates this single argumentless constructor. We get from [bool] to [nat] by changing one of the constructors to indicate 1 recursive argument. We get from [nat] to [list] by adding a non-recursive argument of a parameter type [A]. 57 (** The type [Empty_set] has no constructors, so its representation is the empty list. The type [unit] has one constructor with no arguments, so its one reified constructor indicates no non-recursive data and [0] recursive arguments. The representation for [bool] just duplicates this single argumentless constructor. We get from [bool] to [nat] by changing one of the constructors to indicate 1 recursive argument. We get from [nat] to [list] by adding a non-recursive argument of a parameter type [A].
58 58
59 As a further example, we can do the same encoding for a generic binary tree type. *) 59 As a further example, we can do the same encoding for a generic binary tree type. *)
60 60
61 (* end thide *) 61 (* end thide *)
62 62
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 reified 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
125 (** The idea of a recursion scheme is parameterized by a type and a reputed encoding of it. The principle itself is polymorphic in a type [R], which is the return type of the recursive function that we mean to write. The next argument is a hetergeneous list of one case of the recursive function definition for each datatype constructor. The [datatypeDenote] function turns out to have just the right definition to express the type we need; a set of function cases is just like an alternate set of constructors where we replace the original type [T] with the function result type [R]. Given such a reflected definition, a [fixDenote] invocation returns a function from [T] to [R], which is just what we wanted. 125 (** The idea of a recursion scheme is parameterized by a type and a reputed encoding of it. The principle itself is polymorphic in a type [R], which is the return type of the recursive function that we mean to write. The next argument is a hetergeneous list of one case of the recursive function definition for each datatype constructor. The [datatypeDenote] function turns out to have just the right definition to express the type we need; a set of function cases is just like an alternate set of constructors where we replace the original type [T] with the function result type [R]. Given such a reified definition, a [fixDenote] invocation returns a function from [T] to [R], which is just what we wanted.
126 126
127 We are ready to write some example functions now. It will be useful to use one new function from the [DepList] library included in the book source. *) 127 We are ready to write some example functions now. It will be useful to use one new function from the [DepList] library included in the book source. *)
128 128
129 Check hmake. 129 Check hmake.
130 (** %\vspace{-.15in}% [[ 130 (** %\vspace{-.15in}% [[
227 end 227 end
228 : forall A : Type, tree A -> n 228 : forall A : Type, tree A -> n
229 ]] 229 ]]
230 *) 230 *)
231 (* end thide *) 231 (* end thide *)
232
233 (** As our examples show, even recursive datatypes are mapped to normal-looking size functions. *)
232 234
233 235
234 (** ** Pretty-Printing *) 236 (** ** Pretty-Printing *)
235 237
236 (** It is also useful to do generic pretty-printing of datatype values, rendering them as human-readable strings. To do so, we will need a bit of metadata for each constructor. Specifically, we need the name to print for the constructor and the function to use to render its non-recursive arguments. Everything else can be done generically. *) 238 (** It is also useful to do generic pretty-printing of datatype values, rendering them as human-readable strings. To do so, we will need a bit of metadata for each constructor. Specifically, we need the name to print for the constructor and the function to use to render its non-recursive arguments. Everything else can be done generically. *)