comparison src/Generic.v @ 398:05efde66559d

Get it working in Coq 8.4beta1; use nice coqdoc notation for italics
author Adam Chlipala <adam@chlipala.net>
date Wed, 06 Jun 2012 11:25:13 -0400
parents 3c941750c347
children 7c2167c3fbb2
comparison
equal deleted inserted replaced
397:d62ed7381a0b 398:05efde66559d
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2010, 2012, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\chapter{Generic Programming}% *) 19 (** %\chapter{Generic Programming}% *)
20 20
21 (** %\index{generic programming}\textit{%#<i>#Generic programming#</i>#%}% 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}\emph{%#<i>#datatype-generic programming#</i>#%}% much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support. 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.
22 22
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. *) 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. *)
24 24
25 (** * Reflecting Datatype Definitions *) 25 (** * Reflecting Datatype Definitions *)
26 26
27 (** The key to generic programming with dependent types is %\index{universe types}\textit{%#<i>#universe types#</i>#%}%. This concept should not be confused with the idea of %\textit{%#<i>#universes#</i>#%}% from the metatheory of CIC and related languages. Rather, the idea of universe types is to define inductive types that provide %\textit{%#<i>#syntactic representations#</i>#%}% of Coq types. We cannot directly write CIC programs that do case analysis on types, but we %\textit{%#<i>#can#</i>#%}% case analyze on reflected syntactic versions of those types. 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.
28 28
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. 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.
30 30
31 The first step is to define a representation for constructors of our datatypes. *) 31 The first step is to define a representation for constructors of our datatypes. *)
32 32
67 End tree. 67 End tree.
68 68
69 (* begin thide *) 69 (* begin thide *)
70 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil. 70 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
71 71
72 (** Each datatype representation stands for a family of inductive types. For a specific real datatype and a reputed representation for it, it is useful to define a type of %\textit{%#<i>#evidence#</i>#%}% that the datatype is compatible with the encoding. *) 72 (** Each datatype representation stands for a family of inductive types. For a specific real datatype and a reputed representation for it, it is useful to define a type of _evidence_ that the datatype is compatible with the encoding. *)
73 73
74 Section denote. 74 Section denote.
75 Variable T : Type. 75 Variable T : Type.
76 (** This variable stands for the concrete datatype that we are interested in. *) 76 (** This variable stands for the concrete datatype that we are interested in. *)
77 77
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}\textit{%#<i>#recursion scheme#</i>#%}% 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