Mercurial > cpdt > repo

comparison src/Generic.v @ 286:540a09187193

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PC changes to Equality and Generic
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 13:16:12 -0500
parents dbac52f5bce1
children 7b38729be069
comparison
equal deleted inserted replaced
285:bd7f8720a691 286:540a09187193
1 (* Copyright (c) 2008-2009, Adam Chlipala 1 (* Copyright (c) 2008-2010, 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 (** %\textit{%#<i>#Generic programming#</i>#%}% makes it possible to write functions that operate over different types of data. Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style module systems and Haskell type classes are more flexible cases. These language features are often not as powerful so 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 [deriving] clause, 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 datatype-generic programming much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support. 21 (** %\textit{%#<i>#Generic programming#</i>#%}% makes it possible to write functions that operate over different types of data. Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style module systems and Haskell type classes 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 [deriving] clause, 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 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
36 Record constructor : Type := Con { 36 Record constructor : Type := Con {
37 nonrecursive : Type; 37 nonrecursive : Type;
38 recursive : nat 38 recursive : nat
39 }. 39 }.
40 40
41 (** The idea is that a constructor represented as [Con T n] has [n] arguments of the type that we are defining. Additionally, all of the other, non-recursive arguments can be encoded in the type [T]. When there are no non-recursive arguments, [T] can be [unit]. When there are two non-recursive arguments, of types [A] and [B], [T] can be [A * B]. We can generalizer to any number of arguments via tupling. 41 (** The idea is that a constructor represented as [Con T n] has [n] arguments of the type that we are defining. Additionally, all of the other, non-recursive arguments can be encoded in the type [T]. When there are no non-recursive arguments, [T] can be [unit]. When there are two non-recursive arguments, of types [A] and [B], [T] can be [A * B]. We can generalize to any number of arguments via tupling.
42 42
43 With this definition, it as easy to define a datatype representation in terms of lists of constructors. *) 43 With this definition, it as easy to define a datatype representation in terms of lists of constructors. *)
44 44
45 Definition datatype := list constructor. 45 Definition datatype := list constructor.
46 46
78 Definition constructorDenote (c : constructor) := 78 Definition constructorDenote (c : constructor) :=
79 nonrecursive c -> ilist T (recursive c) -> T. 79 nonrecursive c -> ilist T (recursive c) -> T.
80 (** We write that a constructor is represented as a function returning a [T]. Such a function takes two arguments, which pack together the non-recursive and recursive arguments of the constructor. We represent a tuple of all recursive arguments using the length-indexed list type [ilist] that we met in Chapter 7. *) 80 (** We write that a constructor is represented as a function returning a [T]. Such a function takes two arguments, which pack together the non-recursive and recursive arguments of the constructor. We represent a tuple of all recursive arguments using the length-indexed list type [ilist] that we met in Chapter 7. *)
81 81
82 Definition datatypeDenote := hlist constructorDenote. 82 Definition datatypeDenote := hlist constructorDenote.
83 (** Finally, the evidence for type [T] is a hetergeneous list, including a constructor denotation for every constructor encoding in a datatype encoding. Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *) 83 (** Finally, the evidence for type [T] is a heterogeneous list, including a constructor denotation for every constructor encoding in a datatype encoding. Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *)
84 84
85 End denote. 85 End denote.
86 (* end thide *) 86 (* end thide *)
87 87
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$.% *) 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$.% *)