Mercurial > cpdt > repo

annotate src/DataStruct.v @ 290:758778c0468c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PC comments for FirstOrder
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 15:37:01 -0500
parents 693897f8e0cb
children 1b6c81e51799
rev   line source
adam@284 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@105 2 *
adamc@105 3 * This work is licensed under a
adamc@105 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@105 5 * Unported License.
adamc@105 6 * The license text is available at:
adamc@105 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@105 8 *)
adamc@105 9
adamc@105 10 (* begin hide *)
adamc@111 11 Require Import Arith List.
adamc@105 12
adamc@105 13 Require Import Tactics.
adamc@105 14
adamc@105 15 Set Implicit Arguments.
adamc@105 16 (* end hide *)
adamc@105 17
adamc@105 18
adamc@105 19 (** %\chapter{Dependent Data Structures}% *)
adamc@105 20
adamc@106 21 (** Our red-black tree example from the last chapter illustrated how dependent types enable static enforcement of data structure invariants. To find interesting uses of dependent data structures, however, we need not look to the favorite examples of data structures and algorithms textbooks. More basic examples like length-indexed and heterogeneous lists come up again and again as the building blocks of dependent programs. There is a surprisingly large design space for this class of data structure, and we will spend this chapter exploring it. *)
adamc@105 22
adamc@105 23
adamc@106 24 (** * More Length-Indexed Lists *)
adamc@106 25
adamc@106 26 (** We begin with a deeper look at the length-indexed lists that began the last chapter. *)
adamc@105 27
adamc@105 28 Section ilist.
adamc@105 29 Variable A : Set.
adamc@105 30
adamc@105 31 Inductive ilist : nat -> Set :=
adamc@105 32 | Nil : ilist O
adamc@105 33 | Cons : forall n, A -> ilist n -> ilist (S n).
adamc@105 34
adam@284 35 (** We might like to have a certified function for selecting an element of an [ilist] by position. We could do this using subset types and explicit manipulation of proofs, but dependent types let us do it more directly. It is helpful to define a type family [fin], where [fin n] is isomorphic to [{m : nat | m < n}]. The type family name stands for %``%#"#finite.#"#%''% *)
adamc@106 36
adamc@113 37 (* EX: Define a function [get] for extracting an [ilist] element by position. *)
adamc@113 38
adamc@113 39 (* begin thide *)
adamc@215 40 Inductive fin : nat -> Set :=
adamc@215 41 | First : forall n, fin (S n)
adamc@215 42 | Next : forall n, fin n -> fin (S n).
adamc@105 43
adam@284 44 (** [fin] essentially makes a more richly-typed copy of the natural numbers. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
adamc@106 45
adamc@106 46 Now it is easy to pick a [Prop]-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
adamc@106 47
adamc@106 48 [[
adamc@215 49 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 50 match ls with
adamc@106 51 | Nil => fun idx => ?
adamc@106 52 | Cons _ x ls' => fun idx =>
adamc@106 53 match idx with
adamc@106 54 | First _ => x
adamc@106 55 | Next _ idx' => get ls' idx'
adamc@106 56 end
adamc@106 57 end.
adamc@106 58
adamc@205 59 ]]
adamc@205 60
adamc@215 61 We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return].
adamc@106 62
adamc@106 63 [[
adamc@215 64 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 65 match ls with
adamc@106 66 | Nil => fun idx =>
adamc@215 67 match idx in fin n' return (match n' with
adamc@106 68 | O => A
adamc@106 69 | S _ => unit
adamc@106 70 end) with
adamc@106 71 | First _ => tt
adamc@106 72 | Next _ _ => tt
adamc@106 73 end
adamc@106 74 | Cons _ x ls' => fun idx =>
adamc@106 75 match idx with
adamc@106 76 | First _ => x
adamc@106 77 | Next _ idx' => get ls' idx'
adamc@106 78 end
adamc@106 79 end.
adamc@106 80
adamc@205 81 ]]
adamc@205 82
adam@284 83 Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A]. We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
adam@284 84
adam@284 85 We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply the convoy pattern that we met last chapter. This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables.
adamc@106 86
adamc@106 87 [[
adamc@215 88 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 89 match ls with
adamc@106 90 | Nil => fun idx =>
adamc@215 91 match idx in fin n' return (match n' with
adamc@106 92 | O => A
adamc@106 93 | S _ => unit
adamc@106 94 end) with
adamc@106 95 | First _ => tt
adamc@106 96 | Next _ _ => tt
adamc@106 97 end
adamc@106 98 | Cons _ x ls' => fun idx =>
adamc@215 99 match idx in fin n' return ilist (pred n') -> A with
adamc@106 100 | First _ => fun _ => x
adamc@106 101 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 102 end ls'
adamc@106 103 end.
adamc@106 104
adamc@205 105 ]]
adamc@205 106
adamc@106 107 There is just one problem left with this implementation. Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination. We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
adamc@106 108
adamc@215 109 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 110 match ls with
adamc@105 111 | Nil => fun idx =>
adamc@215 112 match idx in fin n' return (match n' with
adamc@105 113 | O => A
adamc@105 114 | S _ => unit
adamc@105 115 end) with
adamc@105 116 | First _ => tt
adamc@105 117 | Next _ _ => tt
adamc@105 118 end
adamc@105 119 | Cons _ x ls' => fun idx =>
adamc@215 120 match idx in fin n' return (fin (pred n') -> A) -> A with
adamc@105 121 | First _ => fun _ => x
adamc@105 122 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 123 end (get ls')
adamc@105 124 end.
adamc@113 125 (* end thide *)
adamc@105 126 End ilist.
adamc@105 127
adamc@105 128 Implicit Arguments Nil [A].
adamc@113 129 (* begin thide *)
adamc@108 130 Implicit Arguments First [n].
adamc@113 131 (* end thide *)
adamc@105 132
adamc@108 133 (** A few examples show how to make use of these definitions. *)
adamc@108 134
adamc@108 135 Check Cons 0 (Cons 1 (Cons 2 Nil)).
adamc@215 136 (** %\vspace{-.15in}% [[
adamc@215 137 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 138 : ilist nat 3
adamc@108 139 ]] *)
adamc@215 140
adamc@113 141 (* begin thide *)
adamc@108 142 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@215 143 (** %\vspace{-.15in}% [[
adamc@108 144 = 0
adamc@108 145 : nat
adamc@108 146 ]] *)
adamc@215 147
adamc@108 148 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@215 149 (** %\vspace{-.15in}% [[
adamc@108 150 = 1
adamc@108 151 : nat
adamc@108 152 ]] *)
adamc@215 153
adamc@108 154 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@215 155 (** %\vspace{-.15in}% [[
adamc@108 156 = 2
adamc@108 157 : nat
adamc@108 158 ]] *)
adamc@113 159 (* end thide *)
adamc@108 160
adamc@108 161 (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *)
adamc@107 162
adamc@105 163 Section ilist_map.
adamc@105 164 Variables A B : Set.
adamc@105 165 Variable f : A -> B.
adamc@105 166
adamc@215 167 Fixpoint imap n (ls : ilist A n) : ilist B n :=
adamc@215 168 match ls with
adamc@105 169 | Nil => Nil
adamc@105 170 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 171 end.
adamc@105 172
adam@284 173 (** It is easy to prove that [get] %``%#"#distributes over#"#%''% [imap] calls. The only tricky bit is remembering to use our [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *)
adamc@107 174
adamc@215 175 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n),
adamc@105 176 get (imap ls) idx = f (get ls idx).
adamc@113 177 (* begin thide *)
adamc@107 178 induction ls; dep_destruct idx; crush.
adamc@105 179 Qed.
adamc@113 180 (* end thide *)
adamc@105 181 End ilist_map.
adamc@107 182
adamc@107 183
adamc@107 184 (** * Heterogeneous Lists *)
adamc@107 185
adam@284 186 (** Programmers who move to statically-typed functional languages from %``%#"#scripting languages#"#%''% often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a %``%#"#type-level#"#%''% list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Coq. *)
adamc@107 187
adamc@107 188 Section hlist.
adamc@107 189 Variable A : Type.
adamc@107 190 Variable B : A -> Type.
adamc@107 191
adamc@113 192 (* EX: Define a type [hlist] indexed by a [list A], where the type of each element is determined by running [B] on the corresponding element of the index list. *)
adamc@113 193
adamc@107 194 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
adamc@107 195
adamc@113 196 (* begin thide *)
adamc@107 197 Inductive hlist : list A -> Type :=
adamc@107 198 | MNil : hlist nil
adamc@107 199 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 200
adamc@107 201 (** 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. *)
adamc@107 202
adamc@113 203 (* end thide *)
adamc@113 204 (* EX: Define an analogue to [get] for [hlist]s. *)
adamc@113 205
adamc@113 206 (* begin thide *)
adamc@107 207 Variable elm : A.
adamc@107 208
adamc@107 209 Inductive member : list A -> Type :=
adamc@107 210 | MFirst : forall ls, member (elm :: ls)
adamc@107 211 | MNext : forall x ls, member ls -> member (x :: ls).
adamc@107 212
adam@284 213 (** 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.
adamc@107 214
adamc@107 215 We can use [member] to adapt our definition of [get] to [hlists]. 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. *)
adamc@107 216
adamc@215 217 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
adamc@215 218 match mls with
adamc@107 219 | MNil => fun mem =>
adamc@107 220 match mem in member ls' return (match ls' with
adamc@107 221 | nil => B elm
adamc@107 222 | _ :: _ => unit
adamc@107 223 end) with
adamc@107 224 | MFirst _ => tt
adamc@107 225 | MNext _ _ _ => tt
adamc@107 226 end
adamc@107 227 | MCons _ _ x mls' => fun mem =>
adamc@107 228 match mem in member ls' return (match ls' with
adamc@107 229 | nil => Empty_set
adamc@107 230 | x' :: ls'' =>
adamc@107 231 B x' -> (member ls'' -> B elm) -> B elm
adamc@107 232 end) with
adamc@107 233 | MFirst _ => fun x _ => x
adamc@107 234 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@107 235 end x (hget mls')
adamc@107 236 end.
adamc@113 237 (* end thide *)
adamc@107 238 End hlist.
adamc@108 239
adamc@113 240 (* begin thide *)
adamc@108 241 Implicit Arguments MNil [A B].
adamc@108 242 Implicit Arguments MCons [A B x ls].
adamc@108 243
adamc@108 244 Implicit Arguments MFirst [A elm ls].
adamc@108 245 Implicit Arguments MNext [A elm x ls].
adamc@113 246 (* end thide *)
adamc@108 247
adamc@108 248 (** By putting the parameters [A] and [B] in [Type], we allow some very higher-order uses. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
adamc@108 249
adamc@108 250 Definition someTypes : list Set := nat :: bool :: nil.
adamc@108 251
adamc@113 252 (* begin thide *)
adamc@113 253
adamc@108 254 Example someValues : hlist (fun T : Set => T) someTypes :=
adamc@108 255 MCons 5 (MCons true MNil).
adamc@108 256
adamc@108 257 Eval simpl in hget someValues MFirst.
adamc@215 258 (** %\vspace{-.15in}% [[
adamc@108 259 = 5
adamc@108 260 : (fun T : Set => T) nat
adamc@108 261 ]] *)
adamc@215 262
adamc@108 263 Eval simpl in hget someValues (MNext MFirst).
adamc@215 264 (** %\vspace{-.15in}% [[
adamc@108 265 = true
adamc@108 266 : (fun T : Set => T) bool
adamc@108 267 ]] *)
adamc@108 268
adamc@108 269 (** We can also build indexed lists of pairs in this way. *)
adamc@108 270
adamc@108 271 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
adamc@108 272 MCons (1, 2) (MCons (true, false) MNil).
adamc@108 273
adamc@113 274 (* end thide *)
adamc@113 275
adamc@113 276
adamc@108 277 (** ** A Lambda Calculus Interpreter *)
adamc@108 278
adamc@108 279 (** Heterogeneous lists are very useful in implementing interpreters for functional programming languages. Using the types and operations we have already defined, it is trivial to write an interpreter for simply-typed lambda calculus. Our interpreter can alternatively be thought of as a denotational semantics.
adamc@108 280
adamc@108 281 We start with an algebraic datatype for types. *)
adamc@108 282
adamc@108 283 Inductive type : Set :=
adamc@108 284 | Unit : type
adamc@108 285 | Arrow : type -> type -> type.
adamc@108 286
adam@284 287 (** Now we can define a type family for expressions. An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts]. We effectively use the de Bruijn variable representation, which we will discuss in more detail in later chapters, including a case study in Chapter 16. Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *)
adamc@108 288
adamc@108 289 Inductive exp : list type -> type -> Set :=
adamc@108 290 | Const : forall ts, exp ts Unit
adamc@113 291 (* begin thide *)
adamc@108 292 | Var : forall ts t, member t ts -> exp ts t
adamc@108 293 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 294 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@113 295 (* end thide *)
adamc@108 296
adamc@108 297 Implicit Arguments Const [ts].
adamc@108 298
adamc@108 299 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 300
adamc@108 301 Fixpoint typeDenote (t : type) : Set :=
adamc@108 302 match t with
adamc@108 303 | Unit => unit
adamc@108 304 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 305 end.
adamc@108 306
adamc@108 307 (** 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. *)
adamc@108 308
adamc@113 309 (* EX: Define an interpreter for [exp]s. *)
adamc@113 310
adamc@113 311 (* begin thide *)
adamc@215 312 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
adamc@215 313 match e with
adamc@108 314 | Const _ => fun _ => tt
adamc@108 315
adamc@108 316 | Var _ _ mem => fun s => hget s mem
adamc@108 317 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@108 318 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
adamc@108 319 end.
adamc@108 320
adamc@108 321 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 322
adamc@108 323 Eval simpl in expDenote Const MNil.
adamc@215 324 (** %\vspace{-.15in}% [[
adamc@108 325 = tt
adamc@108 326 : typeDenote Unit
adamc@108 327 ]] *)
adamc@215 328
adamc@108 329 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
adamc@215 330 (** %\vspace{-.15in}% [[
adamc@108 331 = fun x : unit => x
adamc@108 332 : typeDenote (Arrow Unit Unit)
adamc@108 333 ]] *)
adamc@215 334
adamc@108 335 Eval simpl in expDenote (Abs (dom := Unit)
adamc@108 336 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
adamc@215 337 (** %\vspace{-.15in}% [[
adamc@108 338 = fun x _ : unit => x
adamc@108 339 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 340 ]] *)
adamc@215 341
adamc@108 342 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
adamc@215 343 (** %\vspace{-.15in}% [[
adamc@108 344 = fun _ x0 : unit => x0
adamc@108 345 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 346 ]] *)
adamc@215 347
adamc@108 348 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
adamc@215 349 (** %\vspace{-.15in}% [[
adamc@108 350 = tt
adamc@108 351 : typeDenote Unit
adamc@108 352 ]] *)
adamc@108 353
adamc@113 354 (* end thide *)
adamc@113 355
adamc@108 356 (** We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas. Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply-typed lambda calculus without even needing to define a syntactic substitution operation. We did it all without a single line of proof, and our implementation is manifestly executable. In a later chapter, we will meet other, more common approaches to language formalization. Such approaches often state and prove explicit theorems about type safety of languages. In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties. *)
adamc@108 357
adamc@108 358
adamc@109 359 (** * Recursive Type Definitions *)
adamc@109 360
adam@284 361 (** There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above. Because Coq supports %``%#"#type-level computation,#"#%''% we can redo our inductive definitions as %\textit{%#<i>#recursive#</i>#%}% definitions. *)
adamc@109 362
adamc@113 363 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
adamc@113 364
adamc@109 365 Section filist.
adamc@109 366 Variable A : Set.
adamc@109 367
adamc@113 368 (* begin thide *)
adamc@109 369 Fixpoint filist (n : nat) : Set :=
adamc@109 370 match n with
adamc@109 371 | O => unit
adamc@109 372 | S n' => A * filist n'
adamc@109 373 end%type.
adamc@109 374
adamc@109 375 (** We say that a list of length 0 has no contents, and a list of length [S n'] is a pair of a data value and a list of length [n']. *)
adamc@109 376
adamc@215 377 Fixpoint ffin (n : nat) : Set :=
adamc@109 378 match n with
adamc@109 379 | O => Empty_set
adamc@215 380 | S n' => option (ffin n')
adamc@109 381 end.
adamc@109 382
adam@284 383 (** We express that there are no index values when [n = O], by defining such indices as type [Empty_set]; and we express that, at [n = S n'], there is a choice between picking the first element of the list (represented as [None]) or choosing a later element (represented by [Some idx], where [idx] is an index into the list tail). For instance, the three values of type [ffin 3] are [None], [Some None], and [Some (Some None)]. *)
adamc@109 384
adamc@215 385 Fixpoint fget (n : nat) : filist n -> ffin n -> A :=
adamc@215 386 match n with
adamc@109 387 | O => fun _ idx => match idx with end
adamc@109 388 | S n' => fun ls idx =>
adamc@109 389 match idx with
adamc@109 390 | None => fst ls
adamc@109 391 | Some idx' => fget n' (snd ls) idx'
adamc@109 392 end
adamc@109 393 end.
adamc@109 394
adamc@215 395 (** Our new [get] implementation needs only one dependent [match], and its annotation is inferred for us. Our choices of data structure implementations lead to just the right typing behavior for this new definition to work out. *)
adamc@113 396 (* end thide *)
adamc@215 397
adamc@109 398 End filist.
adamc@109 399
adamc@109 400 (** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)
adamc@109 401
adamc@113 402 (* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)
adamc@113 403
adamc@109 404 Section fhlist.
adamc@109 405 Variable A : Type.
adamc@109 406 Variable B : A -> Type.
adamc@109 407
adamc@113 408 (* begin thide *)
adamc@109 409 Fixpoint fhlist (ls : list A) : Type :=
adamc@109 410 match ls with
adamc@109 411 | nil => unit
adamc@109 412 | x :: ls' => B x * fhlist ls'
adamc@109 413 end%type.
adamc@109 414
adamc@109 415 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently-typed data elements. *)
adamc@109 416
adamc@109 417 Variable elm : A.
adamc@109 418
adamc@109 419 Fixpoint fmember (ls : list A) : Type :=
adamc@109 420 match ls with
adamc@109 421 | nil => Empty_set
adamc@109 422 | x :: ls' => (x = elm) + fmember ls'
adamc@109 423 end%type.
adamc@109 424
adamc@215 425 (** The definition of [fmember] follows the definition of [ffin]. Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail. While for [index] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for. We express that with a sum type whose left branch is the appropriate equality proposition. Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
adamc@109 426
adamc@109 427 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
adamc@109 428
adamc@109 429 [[
adamc@109 430 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 431 match ls with
adamc@109 432 | nil => fun _ idx => match idx with end
adamc@109 433 | _ :: ls' => fun mls idx =>
adamc@109 434 match idx with
adamc@109 435 | inl _ => fst mls
adamc@109 436 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 437 end
adamc@109 438 end.
adamc@109 439
adamc@205 440 ]]
adamc@205 441
adamc@109 442 Only one problem remains. The expression [fst mls] is not known to have the proper type. To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
adamc@109 443
adamc@109 444 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 445 match ls with
adamc@109 446 | nil => fun _ idx => match idx with end
adamc@109 447 | _ :: ls' => fun mls idx =>
adamc@109 448 match idx with
adamc@109 449 | inl pf => match pf with
adamc@109 450 | refl_equal => fst mls
adamc@109 451 end
adamc@109 452 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 453 end
adamc@109 454 end.
adamc@109 455
adamc@109 456 (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker. Exactly why this works can be seen by studying the definition of equality. *)
adamc@109 457
adamc@109 458 Print eq.
adamc@215 459 (** %\vspace{-.15in}% [[
adamc@109 460 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x
adamc@215 461
adamc@109 462 ]]
adamc@109 463
adamc@215 464 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument. The type of the constructor [refl_equal] shows that [y] can only ever be instantiated to [x]. Thus, within a pattern-match with [refl_equal], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
adamc@113 465 (* end thide *)
adamc@215 466
adamc@109 467 End fhlist.
adamc@110 468
adamc@111 469 Implicit Arguments fhget [A B elm ls].
adamc@111 470
adamc@110 471
adamc@110 472 (** * Data Structures as Index Functions *)
adamc@110 473
adamc@110 474 (** Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments. In this section, we consider parameterized trees with arbitrary branching factor. *)
adamc@110 475
adamc@110 476 Section tree.
adamc@110 477 Variable A : Set.
adamc@110 478
adamc@110 479 Inductive tree : Set :=
adamc@110 480 | Leaf : A -> tree
adamc@110 481 | Node : forall n, ilist tree n -> tree.
adamc@110 482 End tree.
adamc@110 483
adamc@110 484 (** Every [Node] of a [tree] has a natural number argument, which gives the number of child trees in the second argument, typed with [ilist]. We can define two operations on trees of naturals: summing their elements and incrementing their elements. It is useful to define a generic fold function on [ilist]s first. *)
adamc@110 485
adamc@110 486 Section ifoldr.
adamc@110 487 Variables A B : Set.
adamc@110 488 Variable f : A -> B -> B.
adamc@110 489 Variable i : B.
adamc@110 490
adamc@215 491 Fixpoint ifoldr n (ls : ilist A n) : B :=
adamc@110 492 match ls with
adamc@110 493 | Nil => i
adamc@110 494 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 495 end.
adamc@110 496 End ifoldr.
adamc@110 497
adamc@110 498 Fixpoint sum (t : tree nat) : nat :=
adamc@110 499 match t with
adamc@110 500 | Leaf n => n
adamc@110 501 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 502 end.
adamc@110 503
adamc@110 504 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 505 match t with
adamc@110 506 | Leaf n => Leaf (S n)
adamc@110 507 | Node _ ls => Node (imap inc ls)
adamc@110 508 end.
adamc@110 509
adamc@110 510 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 511
adamc@110 512 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@113 513 (* begin thide *)
adamc@110 514 induction t; crush.
adamc@110 515 (** [[
adamc@110 516 n : nat
adamc@110 517 i : ilist (tree nat) n
adamc@110 518 ============================
adamc@110 519 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 520 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@215 521
adamc@110 522 ]]
adamc@110 523
adamc@110 524 We are left with a single subgoal which does not seem provable directly. This is the same problem that we met in Chapter 3 with other nested inductive types. *)
adamc@110 525
adamc@110 526 Check tree_ind.
adamc@215 527 (** %\vspace{-.15in}% [[
adamc@215 528 tree_ind
adamc@110 529 : forall (A : Set) (P : tree A -> Prop),
adamc@110 530 (forall a : A, P (Leaf a)) ->
adamc@110 531 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 532 forall t : tree A, P t
adamc@215 533
adamc@110 534 ]]
adamc@110 535
adamc@110 536 The automatically-generated induction principle is too weak. For the [Node] case, it gives us no inductive hypothesis. We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *)
adamc@215 537
adamc@110 538 Abort.
adamc@110 539
adamc@110 540 Reset tree.
adamc@110 541
adamc@110 542 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
adamc@110 543
adamc@110 544 Section tree.
adamc@110 545 Variable A : Set.
adamc@110 546
adamc@215 547 (** %\vspace{-.15in}% [[
adamc@110 548 Inductive tree : Set :=
adamc@110 549 | Leaf : A -> tree
adamc@110 550 | Node : forall n, filist tree n -> tree.
adamc@110 551
adamc@110 552 Error: Non strictly positive occurrence of "tree" in
adamc@110 553 "forall n : nat, filist tree n -> tree"
adamc@215 554
adamc@110 555 ]]
adamc@110 556
adamc@110 557 The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually-inductive types. We defined [filist] recursively, so it may not be used for nested recursion.
adamc@110 558
adamc@215 559 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, reflexive types. Instead of merely using [fin] to get elements out of [ilist], we can %\textit{%#<i>#define#</i>#%}% [ilist] in terms of [fin]. For the reasons outlined above, it turns out to be easier to work with [ffin] in place of [fin]. *)
adamc@110 560
adamc@110 561 Inductive tree : Set :=
adamc@110 562 | Leaf : A -> tree
adamc@215 563 | Node : forall n, (ffin n -> tree) -> tree.
adamc@110 564
adamc@215 565 (** A [Node] is indexed by a natural number [n], and the node's [n] children are represented as a function from [ffin n] to trees, which is isomorphic to the [ilist]-based representation that we used above. *)
adamc@215 566
adamc@110 567 End tree.
adamc@110 568
adamc@110 569 Implicit Arguments Node [A n].
adamc@110 570
adamc@215 571 (** We can redefine [sum] and [inc] for our new [tree] type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose range is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
adamc@110 572
adamc@110 573 Section rifoldr.
adamc@110 574 Variables A B : Set.
adamc@110 575 Variable f : A -> B -> B.
adamc@110 576 Variable i : B.
adamc@110 577
adamc@215 578 Fixpoint rifoldr (n : nat) : (ffin n -> A) -> B :=
adamc@215 579 match n with
adamc@110 580 | O => fun _ => i
adamc@110 581 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 582 end.
adamc@110 583 End rifoldr.
adamc@110 584
adamc@110 585 Implicit Arguments rifoldr [A B n].
adamc@110 586
adamc@110 587 Fixpoint sum (t : tree nat) : nat :=
adamc@110 588 match t with
adamc@110 589 | Leaf n => n
adamc@110 590 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 591 end.
adamc@110 592
adamc@110 593 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 594 match t with
adamc@110 595 | Leaf n => Leaf (S n)
adamc@110 596 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 597 end.
adamc@110 598
adamc@110 599 (** Now we are ready to prove the theorem where we got stuck before. We will not need to define any new induction principle, but it %\textit{%#<i>#will#</i>#%}% be helpful to prove some lemmas. *)
adamc@110 600
adamc@110 601 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 602 x1 >= x2
adamc@110 603 -> y1 >= y2
adamc@110 604 -> x1 + y1 >= x2 + y2.
adamc@110 605 crush.
adamc@110 606 Qed.
adamc@110 607
adamc@215 608 Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat),
adamc@110 609 (forall idx, f1 idx >= f2 idx)
adamc@110 610 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 611 Hint Resolve plus_ge.
adamc@110 612
adamc@110 613 induction n; crush.
adamc@110 614 Qed.
adamc@110 615
adamc@110 616 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 617 Hint Resolve sum_inc'.
adamc@110 618
adamc@110 619 induction t; crush.
adamc@110 620 Qed.
adamc@110 621
adamc@113 622 (* end thide *)
adamc@113 623
adamc@110 624 (** Even if Coq would generate complete induction principles automatically for nested inductive definitions like the one we started with, there would still be advantages to using this style of reflexive encoding. We see one of those advantages in the definition of [inc], where we did not need to use any kind of auxiliary function. In general, reflexive encodings often admit direct implementations of operations that would require recursion if performed with more traditional inductive data structures. *)
adamc@111 625
adamc@111 626 (** ** Another Interpreter Example *)
adamc@111 627
adamc@112 628 (** We develop another example of variable-arity constructors, in the form of optimization of a small expression language with a construct like Scheme's %\texttt{%#<tt>#cond#</tt>#%}%. Each of our conditional expressions takes a list of pairs of boolean tests and bodies. The value of the conditional comes from the body of the first test in the list to evaluate to [true]. To simplify the interpreter we will write, we force each conditional to include a final, default case. *)
adamc@112 629
adamc@112 630 Inductive type' : Type := Nat | Bool.
adamc@111 631
adamc@111 632 Inductive exp' : type' -> Type :=
adamc@112 633 | NConst : nat -> exp' Nat
adamc@112 634 | Plus : exp' Nat -> exp' Nat -> exp' Nat
adamc@112 635 | Eq : exp' Nat -> exp' Nat -> exp' Bool
adamc@111 636
adamc@112 637 | BConst : bool -> exp' Bool
adamc@113 638 (* begin thide *)
adamc@215 639 | Cond : forall n t, (ffin n -> exp' Bool)
adamc@215 640 -> (ffin n -> exp' t) -> exp' t -> exp' t.
adamc@113 641 (* end thide *)
adamc@111 642
adam@284 643 (** A [Cond] is parameterized by a natural [n], which tells us how many cases this conditional has. The test expressions are represented with a function of type [ffin n -> exp' Bool], and the bodies are represented with a function of type [ffin n -> exp' t], where [t] is the overall type. The final [exp' t] argument is the default case. For example, here is an expression that successively checks whether [2 + 2 = 5] (returning 0 if so) or if [1 + 1 = 2] (returning 1 if so), returning 2 otherwise. *)
adamc@112 644
adam@284 645 Example ex1 := Cond 2
adam@284 646 (fun f => match f with
adam@284 647 | None => Eq (Plus (NConst 2) (NConst 2)) (NConst 5)
adam@284 648 | Some None => Eq (Plus (NConst 1) (NConst 1)) (NConst 2)
adam@284 649 | Some (Some v) => match v with end
adam@284 650 end)
adam@284 651 (fun f => match f with
adam@284 652 | None => NConst 0
adam@284 653 | Some None => NConst 1
adam@284 654 | Some (Some v) => match v with end
adam@284 655 end)
adam@284 656 (NConst 2).
adam@284 657
adam@284 658 (** We start implementing our interpreter with a standard type denotation function. *)
adamc@112 659
adamc@111 660 Definition type'Denote (t : type') : Set :=
adamc@111 661 match t with
adamc@112 662 | Nat => nat
adamc@112 663 | Bool => bool
adamc@111 664 end.
adamc@111 665
adamc@112 666 (** To implement the expression interpreter, it is useful to have the following function that implements the functionality of [Cond] without involving any syntax. *)
adamc@112 667
adamc@113 668 (* begin thide *)
adamc@111 669 Section cond.
adamc@111 670 Variable A : Set.
adamc@111 671 Variable default : A.
adamc@111 672
adamc@215 673 Fixpoint cond (n : nat) : (ffin n -> bool) -> (ffin n -> A) -> A :=
adamc@215 674 match n with
adamc@111 675 | O => fun _ _ => default
adamc@111 676 | S n' => fun tests bodies =>
adamc@111 677 if tests None
adamc@111 678 then bodies None
adamc@111 679 else cond n'
adamc@111 680 (fun idx => tests (Some idx))
adamc@111 681 (fun idx => bodies (Some idx))
adamc@111 682 end.
adamc@111 683 End cond.
adamc@111 684
adamc@111 685 Implicit Arguments cond [A n].
adamc@113 686 (* end thide *)
adamc@111 687
adamc@112 688 (** Now the expression interpreter is straightforward to write. *)
adamc@112 689
adamc@215 690 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
adamc@215 691 match e with
adamc@215 692 | NConst n => n
adamc@215 693 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
adamc@111 694 | Eq e1 e2 =>
adamc@111 695 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adamc@111 696
adamc@215 697 | BConst b => b
adamc@111 698 | Cond _ _ tests bodies default =>
adamc@113 699 (* begin thide *)
adamc@111 700 cond
adamc@111 701 (exp'Denote default)
adamc@111 702 (fun idx => exp'Denote (tests idx))
adamc@111 703 (fun idx => exp'Denote (bodies idx))
adamc@113 704 (* end thide *)
adamc@111 705 end.
adamc@111 706
adamc@112 707 (** We will implement a constant-folding function that optimizes conditionals, removing cases with known-[false] tests and cases that come after known-[true] tests. A function [cfoldCond] implements the heart of this logic. The convoy pattern is used again near the end of the implementation. *)
adamc@112 708
adamc@113 709 (* begin thide *)
adamc@111 710 Section cfoldCond.
adamc@111 711 Variable t : type'.
adamc@111 712 Variable default : exp' t.
adamc@111 713
adamc@112 714 Fixpoint cfoldCond (n : nat)
adamc@215 715 : (ffin n -> exp' Bool) -> (ffin n -> exp' t) -> exp' t :=
adamc@215 716 match n with
adamc@111 717 | O => fun _ _ => default
adamc@111 718 | S n' => fun tests bodies =>
adamc@204 719 match tests None return _ with
adamc@111 720 | BConst true => bodies None
adamc@111 721 | BConst false => cfoldCond n'
adamc@111 722 (fun idx => tests (Some idx))
adamc@111 723 (fun idx => bodies (Some idx))
adamc@111 724 | _ =>
adamc@111 725 let e := cfoldCond n'
adamc@111 726 (fun idx => tests (Some idx))
adamc@111 727 (fun idx => bodies (Some idx)) in
adamc@112 728 match e in exp' t return exp' t -> exp' t with
adamc@112 729 | Cond n _ tests' bodies' default' => fun body =>
adamc@111 730 Cond
adamc@111 731 (S n)
adamc@111 732 (fun idx => match idx with
adamc@112 733 | None => tests None
adamc@111 734 | Some idx => tests' idx
adamc@111 735 end)
adamc@111 736 (fun idx => match idx with
adamc@111 737 | None => body
adamc@111 738 | Some idx => bodies' idx
adamc@111 739 end)
adamc@111 740 default'
adamc@112 741 | e => fun body =>
adamc@111 742 Cond
adamc@111 743 1
adamc@112 744 (fun _ => tests None)
adamc@111 745 (fun _ => body)
adamc@111 746 e
adamc@112 747 end (bodies None)
adamc@111 748 end
adamc@111 749 end.
adamc@111 750 End cfoldCond.
adamc@111 751
adamc@111 752 Implicit Arguments cfoldCond [t n].
adamc@113 753 (* end thide *)
adamc@111 754
adamc@112 755 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
adamc@112 756
adamc@215 757 Fixpoint cfold t (e : exp' t) : exp' t :=
adamc@215 758 match e with
adamc@111 759 | NConst n => NConst n
adamc@111 760 | Plus e1 e2 =>
adamc@111 761 let e1' := cfold e1 in
adamc@111 762 let e2' := cfold e2 in
adamc@204 763 match e1', e2' return _ with
adamc@111 764 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@111 765 | _, _ => Plus e1' e2'
adamc@111 766 end
adamc@111 767 | Eq e1 e2 =>
adamc@111 768 let e1' := cfold e1 in
adamc@111 769 let e2' := cfold e2 in
adamc@204 770 match e1', e2' return _ with
adamc@111 771 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@111 772 | _, _ => Eq e1' e2'
adamc@111 773 end
adamc@111 774
adamc@111 775 | BConst b => BConst b
adamc@111 776 | Cond _ _ tests bodies default =>
adamc@113 777 (* begin thide *)
adamc@111 778 cfoldCond
adamc@111 779 (cfold default)
adamc@111 780 (fun idx => cfold (tests idx))
adamc@111 781 (fun idx => cfold (bodies idx))
adamc@113 782 (* end thide *)
adamc@111 783 end.
adamc@111 784
adamc@113 785 (* begin thide *)
adamc@112 786 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. This lemma formalizes that property. The proof is a standard mostly-automated one, with the only wrinkle being a guided instantation of the quantifiers in the induction hypothesis. *)
adamc@112 787
adamc@111 788 Lemma cfoldCond_correct : forall t (default : exp' t)
adamc@215 789 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
adamc@111 790 exp'Denote (cfoldCond default tests bodies)
adamc@111 791 = exp'Denote (Cond n tests bodies default).
adamc@111 792 induction n; crush;
adamc@111 793 match goal with
adamc@111 794 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
adamc@111 795 generalize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)));
adamc@111 796 clear IHn; intro IHn
adamc@111 797 end;
adamc@111 798 repeat (match goal with
adamc@111 799 | [ |- context[match ?E with
adamc@111 800 | NConst _ => _
adamc@111 801 | Plus _ _ => _
adamc@111 802 | Eq _ _ => _
adamc@111 803 | BConst _ => _
adamc@111 804 | Cond _ _ _ _ _ => _
adamc@111 805 end] ] => dep_destruct E
adamc@111 806 | [ |- context[if ?B then _ else _] ] => destruct B
adamc@111 807 end; crush).
adamc@111 808 Qed.
adamc@111 809
adamc@112 810 (** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old. It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal. We treat this issue with our discussion of axioms in a later chapter. For now, it suffices to prove that the particular function [cond] is %\textit{%#<i>#extensional#</i>#%}%; that is, it is unaffected by substitution of functions with input-output equivalents. *)
adamc@112 811
adamc@215 812 Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : ffin n -> bool)
adamc@215 813 (bodies bodies' : ffin n -> A),
adamc@111 814 (forall idx, tests idx = tests' idx)
adamc@111 815 -> (forall idx, bodies idx = bodies' idx)
adamc@111 816 -> cond default tests bodies
adamc@111 817 = cond default tests' bodies'.
adamc@111 818 induction n; crush;
adamc@111 819 match goal with
adamc@111 820 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@111 821 end; crush.
adamc@111 822 Qed.
adamc@111 823
adamc@112 824 (** Now the final theorem is easy to prove. We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct. *)
adamc@113 825 (* end thide *)
adamc@112 826
adamc@111 827 Theorem cfold_correct : forall t (e : exp' t),
adamc@111 828 exp'Denote (cfold e) = exp'Denote e.
adamc@113 829 (* begin thide *)
adamc@111 830 Hint Rewrite cfoldCond_correct : cpdt.
adamc@111 831 Hint Resolve cond_ext.
adamc@111 832
adamc@111 833 induction e; crush;
adamc@111 834 repeat (match goal with
adamc@111 835 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@111 836 end; crush).
adamc@111 837 Qed.
adamc@113 838 (* end thide *)
adamc@115 839
adamc@115 840
adamc@215 841 (** * Choosing Between Representations *)
adamc@215 842
adamc@215 843 (** It is not always clear which of these representation techniques to apply in a particular situation, but I will try to summarize the pros and cons of each.
adamc@215 844
adamc@215 845 Inductive types are often the most pleasant to work with, after someone has spent the time implementing some basic library functions for them, using fancy [match] annotations. Many aspects of Coq's logic and tactic support are specialized to deal with inductive types, and you may miss out if you use alternate encodings.
adamc@215 846
adam@284 847 Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation. For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types. Consider a call [get l f], where variable [l] has type [filist A (S n)]. The type of [l] would be simplified to an explicit pair type. In a proof involving many recursive types, this kind of unhelpful %``%#"#simplification#"#%''% can lead to rapid bloat in the sizes of subgoals.
adamc@215 848
adam@284 849 Another disadvantage of recursive types is that they only apply to type families whose indices determine their %``%#"#skeletons.#"#%''% This is not true for all data structures; a good counterexample comes from the richly-typed programming language syntax types we have used several times so far. The fact that a piece of syntax has type [Nat] tells us nothing about the tree structure of that syntax.
adamc@215 850
adamc@227 851 Reflexive encodings of data types are seen relatively rarely. As our examples demonstrated, manipulating index values manually can lead to hard-to-read code. A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3. For small developments, avoiding that kind of coding can justify the use of reflexive data structures. There are also some useful instances of co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *)
adamc@215 852
adamc@215 853
adamc@115 854 (** * Exercises *)
adamc@115 855
adamc@116 856 (** remove printing * *)
adamc@116 857
adamc@216 858 (** Some of the type family definitions and associated functions from this chapter are duplicated in the [DepList] module of the book source. Some of their names have been changed to be more sensible in a general context.
adamc@115 859
adamc@115 860 %\begin{enumerate}%#<ol>#
adamc@115 861
adam@284 862 %\item%#<li># Define a tree analogue of [hlist]. That is, define a parameterized type of binary trees with data at their leaves, and define a type family [htree] indexed by trees. The structure of an [htree] mirrors its index tree, with the type of each data element (which only occur at leaves) determined by applying a type function to the corresponding element of the index tree. Define a type standing for all possible paths from the root of a tree to leaves and use it to implement a function [tget] for extracting an element of an [htree] by path. Define a function [htmap2] for %``%#"#mapping over two trees in parallel.#"#%''% That is, [htmap2] takes in two [htree]s with the same index tree, and it forms a new [htree] with the same index by applying a binary function pointwise.
adamc@115 863
adamc@129 864 Repeat this process so that you implement each definition for each of the three definition styles covered in this chapter: inductive, recursive, and index function.#</li>#
adamc@116 865
adamc@130 866 %\item%#<li># Write a dependently-typed interpreter for a simple programming language with ML-style pattern-matching, using one of the encodings of heterogeneous lists to represent the different branches of a [case] expression. (There are other ways to represent the same thing, but the point of this exercise is to practice using those heterogeneous list types.) The object language is defined informally by this grammar:
adamc@116 867
adamc@116 868 [[
adamc@116 869 t ::= bool | t + t
adamc@116 870 p ::= x | b | inl p | inr p
adamc@116 871 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e
adamc@215 872
adamc@116 873 ]]
adamc@116 874
adamc@116 875 [x] stands for a variable, and [b] stands for a boolean constant. The production for [case] expressions means that a pattern-match includes zero or more pairs of patterns and expressions, along with a default case.
adamc@116 876
adamc@117 877 Your interpreter should be implemented in the style demonstrated in this chapter. That is, your definition of expressions should use dependent types and de Bruijn indices to combine syntax and typing rules, such that the type of an expression tells the types of variables that are in scope. You should implement a simple recursive function translating types [t] to [Set], and your interpreter should produce values in the image of this translation.#</li>#
adamc@116 878
adamc@115 879 #</ol>#%\end{enumerate}% *)