Proofreading pass through Chapter 11

src/DataStruct.v

@@ -197,8 +197,8 @@ Section hlist.
 
 (* begin thide *)
   Inductive hlist : list A -> Type :=
-  | MNil : hlist nil
-  | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
+  | HNil : hlist nil
+  | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
 
   (** We can implement a variant of the last section's [get] function for [hlist]s.  To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to.%\index{Gallina terms!member}% *)
 
@@ -214,11 +214,11 @@ Section hlist.
 
   (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable.  In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too.  The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations.
 
-     We can use [member] to adapt our definition of [get] to [hlist]s.  The same basic [match] tricks apply.  In the [MCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match].  We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
+     We can use [member] to adapt our definition of [get] to [hlist]s.  The same basic [match] tricks apply.  In the [HCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match].  We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
 
   Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
     match mls with
-      | MNil => fun mem =>
+      | HNil => fun mem =>
         match mem in member ls' return (match ls' with
                                           | nil => B elm
                                           | _ :: _ => unit
@@ -226,7 +226,7 @@ Section hlist.
           | MFirst _ => tt
           | MNext _ _ _ => tt
         end
-      | MCons _ _ x mls' => fun mem =>
+      | HCons _ _ x mls' => fun mem =>
         match mem in member ls' return (match ls' with
                                           | nil => Empty_set
                                           | x' :: ls'' =>
@@ -241,8 +241,8 @@ Section hlist.
 End hlist.
 
 (* begin thide *)
-Implicit Arguments MNil [A B].
-Implicit Arguments MCons [A B x ls].
+Implicit Arguments HNil [A B].
+Implicit Arguments HCons [A B x ls].
 
 Implicit Arguments MFirst [A elm ls].
 Implicit Arguments MNext [A elm x ls].
@@ -255,7 +255,7 @@ Definition someTypes : list Set := nat :: bool :: nil.
 (* begin thide *)
 
 Example someValues : hlist (fun T : Set => T) someTypes :=
-  MCons 5 (MCons true MNil).
+  HCons 5 (HCons true HNil).
 
 Eval simpl in hget someValues MFirst.
 (** %\vspace{-.15in}% [[
@@ -274,7 +274,7 @@ Eval simpl in hget someValues (MNext MFirst).
 (** We can also build indexed lists of pairs in this way. *)
 
 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
-  MCons (1, 2) (MCons (true, false) MNil).
+  HCons (1, 2) (HCons (true, false) HNil).
 
 (** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)
 
@@ -311,7 +311,7 @@ Fixpoint typeDenote (t : type) : Set :=
     | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
   end.
 
-(** Now it is straightforward to write an expression interpreter.  The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values.  An environment for a free variable list [ts] is simply a [hlist typeDenote ts].  That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type.  We use [hget] to implement the [Var] case, and we use [MCons] to extend the environment in the [Abs] case. *)
+(** Now it is straightforward to write an expression interpreter.  The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values.  An environment for a free variable list [ts] is simply a [hlist typeDenote ts].  That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type.  We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *)
 
 (* EX: Define an interpreter for [exp]s. *)
 
@@ -322,19 +322,19 @@ Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
 
     | Var _ _ mem => fun s => hget s mem
     | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
-    | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
+    | Abs _ _ _ e' => fun s => fun x => expDenote e' (HCons x s)
   end.
 
 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
 
-Eval simpl in expDenote Const MNil.
+Eval simpl in expDenote Const HNil.
 (** %\vspace{-.15in}% [[
     = tt
      : typeDenote Unit
 ]]
 *)
 
-Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
+Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) HNil.
 (** %\vspace{-.15in}% [[
      = fun x : unit => x
      : typeDenote (Arrow Unit Unit)
@@ -342,21 +342,21 @@ Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
 *)
 
 Eval simpl in expDenote (Abs (dom := Unit)
-  (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
+  (Abs (dom := Unit) (Var (MNext MFirst)))) HNil.
 (** %\vspace{-.15in}% [[
      = fun x _ : unit => x
      : typeDenote (Arrow Unit (Arrow Unit Unit))
 ]]
 *)
 
-Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
+Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) HNil.
 (** %\vspace{-.15in}% [[
      = fun _ x0 : unit => x0
      : typeDenote (Arrow Unit (Arrow Unit Unit))
 ]]
 *)
 
-Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
+Eval simpl in expDenote (App (Abs (Var MFirst)) Const) HNil.
 (** %\vspace{-.15in}% [[
      = tt
      : typeDenote Unit

src/Generic.v

@@ -24,15 +24,15 @@ Set Implicit Arguments.
 
    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. *)
 
-(** * Reflecting Datatype Definitions *)
+(** * Reifying Datatype Definitions *)
 
-(** 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.
+(** 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.
 
    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.
 
    The first step is to define a representation for constructors of our datatypes. *)
 
-(* EX: Define a reflected representation of simple algebraic datatypes. *)
+(* EX: Define a reified representation of simple algebraic datatypes. *)
 
 (* begin thide *)
 Record constructor : Type := Con {
@@ -54,7 +54,7 @@ Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
 
-(** 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].
+(** 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].
 
    As a further example, we can do the same encoding for a generic binary tree type. *)
 
@@ -116,13 +116,13 @@ Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
 
 (* EX: Define a generic [size] function. *)
 
-(** 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. *)
+(** 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. *)
 
 (* begin thide *)
 Definition fixDenote (T : Type) (dt : datatype) :=
   forall (R : Type), datatypeDenote R dt -> (T -> R).
 
-(** 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.
+(** 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.
 
    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. *)
 
@@ -230,6 +230,8 @@ Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
 *)
 (* end thide *)
 
+(** As our examples show, even recursive datatypes are mapped to normal-looking size functions. *)
+
 
 (** ** Pretty-Printing *)