Mercurial > cpdt > repo

annotate src/DataStruct.v @ 214:768889c969e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish porting MoreDep
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 12:21:28 -0500
parents f05514cc6c0d
children f8bcd33bdd91
rev   line source
adamc@105 1 (* Copyright (c) 2008, 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
adamc@106 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 [index], where [index n] is isomorphic to [{m : nat | m < n}]. Such a type family is also often called [Fin] or similar, standing 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@105 40 Inductive index : nat -> Set :=
adamc@105 41 | First : forall n, index (S n)
adamc@105 42 | Next : forall n, index n -> index (S n).
adamc@105 43
adamc@106 44 (** [index] 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.
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@106 49 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 50 match ls in ilist n return index n -> A 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@106 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 [index] 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@106 64 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 65 match ls in ilist n return index n -> A with
adamc@106 66 | Nil => fun idx =>
adamc@106 67 match idx in index 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
adamc@106 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']. 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 a trick that we will call "the convoy pattern," introducing a new function and applying it immediately, to satisfy the type checker.
adamc@106 84
adamc@106 85 [[
adamc@106 86 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 87 match ls in ilist n return index n -> A with
adamc@106 88 | Nil => fun idx =>
adamc@106 89 match idx in index n' return (match n' with
adamc@106 90 | O => A
adamc@106 91 | S _ => unit
adamc@106 92 end) with
adamc@106 93 | First _ => tt
adamc@106 94 | Next _ _ => tt
adamc@106 95 end
adamc@106 96 | Cons _ x ls' => fun idx =>
adamc@106 97 match idx in index n' return ilist (pred n') -> A with
adamc@106 98 | First _ => fun _ => x
adamc@106 99 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 100 end ls'
adamc@106 101 end.
adamc@106 102
adamc@205 103 ]]
adamc@205 104
adamc@106 105 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 106
adamc@105 107 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@105 108 match ls in ilist n return index n -> A with
adamc@105 109 | Nil => fun idx =>
adamc@105 110 match idx in index n' return (match n' with
adamc@105 111 | O => A
adamc@105 112 | S _ => unit
adamc@105 113 end) with
adamc@105 114 | First _ => tt
adamc@105 115 | Next _ _ => tt
adamc@105 116 end
adamc@105 117 | Cons _ x ls' => fun idx =>
adamc@105 118 match idx in index n' return (index (pred n') -> A) -> A with
adamc@105 119 | First _ => fun _ => x
adamc@105 120 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 121 end (get ls')
adamc@105 122 end.
adamc@113 123 (* end thide *)
adamc@105 124 End ilist.
adamc@105 125
adamc@105 126 Implicit Arguments Nil [A].
adamc@113 127 (* begin thide *)
adamc@108 128 Implicit Arguments First [n].
adamc@113 129 (* end thide *)
adamc@105 130
adamc@108 131 (** A few examples show how to make use of these definitions. *)
adamc@108 132
adamc@108 133 Check Cons 0 (Cons 1 (Cons 2 Nil)).
adamc@108 134 (** [[
adamc@108 135
adamc@108 136 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 137 : ilist nat 3
adamc@108 138 ]] *)
adamc@113 139 (* begin thide *)
adamc@108 140 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@108 141 (** [[
adamc@108 142
adamc@108 143 = 0
adamc@108 144 : nat
adamc@108 145 ]] *)
adamc@108 146 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@108 147 (** [[
adamc@108 148
adamc@108 149 = 1
adamc@108 150 : nat
adamc@108 151 ]] *)
adamc@108 152 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@108 153 (** [[
adamc@108 154
adamc@108 155 = 2
adamc@108 156 : nat
adamc@108 157 ]] *)
adamc@113 158 (* end thide *)
adamc@108 159
adamc@108 160 (** 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 161
adamc@105 162 Section ilist_map.
adamc@105 163 Variables A B : Set.
adamc@105 164 Variable f : A -> B.
adamc@105 165
adamc@105 166 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
adamc@105 167 match ls in ilist _ n return ilist B n with
adamc@105 168 | Nil => Nil
adamc@105 169 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 170 end.
adamc@105 171
adamc@107 172 (** It is easy to prove that [get] "distributes over" [imap] calls. The only tricky bit is remembering to use the [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *)
adamc@107 173
adamc@107 174 Theorem get_imap : forall n (idx : index n) (ls : ilist A n),
adamc@105 175 get (imap ls) idx = f (get ls idx).
adamc@113 176 (* begin thide *)
adamc@107 177 induction ls; dep_destruct idx; crush.
adamc@105 178 Qed.
adamc@113 179 (* end thide *)
adamc@105 180 End ilist_map.
adamc@107 181
adamc@107 182
adamc@107 183 (** * Heterogeneous Lists *)
adamc@107 184
adamc@107 185 (** 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 it we can do it much more cleanly and directly in Coq. *)
adamc@107 186
adamc@107 187 Section hlist.
adamc@107 188 Variable A : Type.
adamc@107 189 Variable B : A -> Type.
adamc@107 190
adamc@113 191 (* 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 192
adamc@107 193 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
adamc@107 194
adamc@113 195 (* begin thide *)
adamc@107 196 Inductive hlist : list A -> Type :=
adamc@107 197 | MNil : hlist nil
adamc@107 198 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 199
adamc@107 200 (** 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 201
adamc@113 202 (* end thide *)
adamc@113 203 (* EX: Define an analogue to [get] for [hlist]s. *)
adamc@113 204
adamc@113 205 (* begin thide *)
adamc@107 206 Variable elm : A.
adamc@107 207
adamc@107 208 Inductive member : list A -> Type :=
adamc@107 209 | MFirst : forall ls, member (elm :: ls)
adamc@107 210 | MNext : forall x ls, member ls -> member (x :: ls).
adamc@107 211
adamc@107 212 (** 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 213
adamc@107 214 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 215
adamc@107 216 Fixpoint hget ls (mls : hlist ls) {struct mls} : member ls -> B elm :=
adamc@107 217 match mls in hlist ls return member ls -> B elm with
adamc@107 218 | MNil => fun mem =>
adamc@107 219 match mem in member ls' return (match ls' with
adamc@107 220 | nil => B elm
adamc@107 221 | _ :: _ => unit
adamc@107 222 end) with
adamc@107 223 | MFirst _ => tt
adamc@107 224 | MNext _ _ _ => tt
adamc@107 225 end
adamc@107 226 | MCons _ _ x mls' => fun mem =>
adamc@107 227 match mem in member ls' return (match ls' with
adamc@107 228 | nil => Empty_set
adamc@107 229 | x' :: ls'' =>
adamc@107 230 B x' -> (member ls'' -> B elm) -> B elm
adamc@107 231 end) with
adamc@107 232 | MFirst _ => fun x _ => x
adamc@107 233 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@107 234 end x (hget mls')
adamc@107 235 end.
adamc@113 236 (* end thide *)
adamc@107 237 End hlist.
adamc@108 238
adamc@113 239 (* begin thide *)
adamc@108 240 Implicit Arguments MNil [A B].
adamc@108 241 Implicit Arguments MCons [A B x ls].
adamc@108 242
adamc@108 243 Implicit Arguments MFirst [A elm ls].
adamc@108 244 Implicit Arguments MNext [A elm x ls].
adamc@113 245 (* end thide *)
adamc@108 246
adamc@108 247 (** 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 248
adamc@108 249 Definition someTypes : list Set := nat :: bool :: nil.
adamc@108 250
adamc@113 251 (* begin thide *)
adamc@113 252
adamc@108 253 Example someValues : hlist (fun T : Set => T) someTypes :=
adamc@108 254 MCons 5 (MCons true MNil).
adamc@108 255
adamc@108 256 Eval simpl in hget someValues MFirst.
adamc@108 257 (** [[
adamc@108 258
adamc@108 259 = 5
adamc@108 260 : (fun T : Set => T) nat
adamc@108 261 ]] *)
adamc@108 262 Eval simpl in hget someValues (MNext MFirst).
adamc@108 263 (** [[
adamc@108 264
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
adamc@108 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. 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@108 291
adamc@113 292 (* begin thide *)
adamc@108 293 | Var : forall ts t, member t ts -> exp ts t
adamc@108 294 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 295 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@113 296 (* end thide *)
adamc@108 297
adamc@108 298 Implicit Arguments Const [ts].
adamc@108 299
adamc@108 300 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 301
adamc@108 302 Fixpoint typeDenote (t : type) : Set :=
adamc@108 303 match t with
adamc@108 304 | Unit => unit
adamc@108 305 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 306 end.
adamc@108 307
adamc@108 308 (** 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 309
adamc@113 310 (* EX: Define an interpreter for [exp]s. *)
adamc@113 311
adamc@113 312 (* begin thide *)
adamc@108 313 Fixpoint expDenote ts t (e : exp ts t) {struct e} : hlist typeDenote ts -> typeDenote t :=
adamc@108 314 match e in exp ts t return hlist typeDenote ts -> typeDenote t with
adamc@108 315 | Const _ => fun _ => tt
adamc@108 316
adamc@108 317 | Var _ _ mem => fun s => hget s mem
adamc@108 318 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@108 319 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
adamc@108 320 end.
adamc@108 321
adamc@108 322 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 323
adamc@108 324 Eval simpl in expDenote Const MNil.
adamc@108 325 (** [[
adamc@108 326
adamc@108 327 = tt
adamc@108 328 : typeDenote Unit
adamc@108 329 ]] *)
adamc@108 330 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
adamc@108 331 (** [[
adamc@108 332
adamc@108 333 = fun x : unit => x
adamc@108 334 : typeDenote (Arrow Unit Unit)
adamc@108 335 ]] *)
adamc@108 336 Eval simpl in expDenote (Abs (dom := Unit)
adamc@108 337 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
adamc@108 338 (** [[
adamc@108 339
adamc@108 340 = fun x _ : unit => x
adamc@108 341 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 342 ]] *)
adamc@108 343 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
adamc@108 344 (** [[
adamc@108 345
adamc@108 346 = fun _ x0 : unit => x0
adamc@108 347 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 348 ]] *)
adamc@108 349 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
adamc@108 350 (** [[
adamc@108 351
adamc@108 352 = tt
adamc@108 353 : typeDenote Unit
adamc@108 354 ]] *)
adamc@108 355
adamc@113 356 (* end thide *)
adamc@113 357
adamc@108 358 (** 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 359
adamc@108 360
adamc@109 361 (** * Recursive Type Definitions *)
adamc@109 362
adamc@109 363 (** 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 364
adamc@113 365 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
adamc@113 366
adamc@109 367 Section filist.
adamc@109 368 Variable A : Set.
adamc@109 369
adamc@113 370 (* begin thide *)
adamc@109 371 Fixpoint filist (n : nat) : Set :=
adamc@109 372 match n with
adamc@109 373 | O => unit
adamc@109 374 | S n' => A * filist n'
adamc@109 375 end%type.
adamc@109 376
adamc@109 377 (** 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 378
adamc@109 379 Fixpoint findex (n : nat) : Set :=
adamc@109 380 match n with
adamc@109 381 | O => Empty_set
adamc@109 382 | S n' => option (findex n')
adamc@109 383 end.
adamc@109 384
adamc@109 385 (** 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). *)
adamc@109 386
adamc@109 387 Fixpoint fget (n : nat) : filist n -> findex n -> A :=
adamc@109 388 match n return filist n -> findex n -> A with
adamc@109 389 | O => fun _ idx => match idx with end
adamc@109 390 | S n' => fun ls idx =>
adamc@109 391 match idx with
adamc@109 392 | None => fst ls
adamc@109 393 | Some idx' => fget n' (snd ls) idx'
adamc@109 394 end
adamc@109 395 end.
adamc@109 396
adamc@109 397 (** Our new [get] implementation needs only one dependent [match], which just copies the stated return type of the function. Our choices of data structure implementations lead to just the right typing behavior for this new definition to work out. *)
adamc@113 398 (* end thide *)
adamc@109 399 End filist.
adamc@109 400
adamc@109 401 (** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)
adamc@109 402
adamc@113 403 (* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)
adamc@113 404
adamc@109 405 Section fhlist.
adamc@109 406 Variable A : Type.
adamc@109 407 Variable B : A -> Type.
adamc@109 408
adamc@113 409 (* begin thide *)
adamc@109 410 Fixpoint fhlist (ls : list A) : Type :=
adamc@109 411 match ls with
adamc@109 412 | nil => unit
adamc@109 413 | x :: ls' => B x * fhlist ls'
adamc@109 414 end%type.
adamc@109 415
adamc@109 416 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently-typed data elements. *)
adamc@109 417
adamc@109 418 Variable elm : A.
adamc@109 419
adamc@109 420 Fixpoint fmember (ls : list A) : Type :=
adamc@109 421 match ls with
adamc@109 422 | nil => Empty_set
adamc@109 423 | x :: ls' => (x = elm) + fmember ls'
adamc@109 424 end%type.
adamc@109 425
adamc@109 426 (** The definition of [fmember] follows the definition of [findex]. 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 427
adamc@109 428 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
adamc@109 429
adamc@109 430 [[
adamc@109 431
adamc@109 432 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@109 433 match ls return fhlist ls -> fmember ls -> B elm with
adamc@109 434 | nil => fun _ idx => match idx with end
adamc@109 435 | _ :: ls' => fun mls idx =>
adamc@109 436 match idx with
adamc@109 437 | inl _ => fst mls
adamc@109 438 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 439 end
adamc@109 440 end.
adamc@109 441
adamc@205 442 ]]
adamc@205 443
adamc@109 444 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 445
adamc@109 446 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@109 447 match ls return fhlist ls -> fmember ls -> B elm with
adamc@109 448 | nil => fun _ idx => match idx with end
adamc@109 449 | _ :: ls' => fun mls idx =>
adamc@109 450 match idx with
adamc@109 451 | inl pf => match pf with
adamc@109 452 | refl_equal => fst mls
adamc@109 453 end
adamc@109 454 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 455 end
adamc@109 456 end.
adamc@109 457
adamc@109 458 (** 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 459
adamc@109 460 Print eq.
adamc@109 461 (** [[
adamc@109 462
adamc@109 463 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x
adamc@109 464 ]]
adamc@109 465
adamc@109 466 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. All examples of similar dependent pattern matching that we have seen before require explicit annotations, but Coq implements a special case of annotation inference for matches on equality proofs. *)
adamc@113 467 (* end thide *)
adamc@109 468 End fhlist.
adamc@110 469
adamc@111 470 Implicit Arguments fhget [A B elm ls].
adamc@111 471
adamc@110 472
adamc@110 473 (** * Data Structures as Index Functions *)
adamc@110 474
adamc@110 475 (** 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 476
adamc@110 477 Section tree.
adamc@110 478 Variable A : Set.
adamc@110 479
adamc@110 480 Inductive tree : Set :=
adamc@110 481 | Leaf : A -> tree
adamc@110 482 | Node : forall n, ilist tree n -> tree.
adamc@110 483 End tree.
adamc@110 484
adamc@110 485 (** 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 486
adamc@110 487 Section ifoldr.
adamc@110 488 Variables A B : Set.
adamc@110 489 Variable f : A -> B -> B.
adamc@110 490 Variable i : B.
adamc@110 491
adamc@110 492 Fixpoint ifoldr n (ls : ilist A n) {struct ls} : B :=
adamc@110 493 match ls with
adamc@110 494 | Nil => i
adamc@110 495 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 496 end.
adamc@110 497 End ifoldr.
adamc@110 498
adamc@110 499 Fixpoint sum (t : tree nat) : nat :=
adamc@110 500 match t with
adamc@110 501 | Leaf n => n
adamc@110 502 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 503 end.
adamc@110 504
adamc@110 505 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 506 match t with
adamc@110 507 | Leaf n => Leaf (S n)
adamc@110 508 | Node _ ls => Node (imap inc ls)
adamc@110 509 end.
adamc@110 510
adamc@110 511 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 512
adamc@110 513 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@113 514 (* begin thide *)
adamc@110 515 induction t; crush.
adamc@110 516 (** [[
adamc@110 517
adamc@110 518 n : nat
adamc@110 519 i : ilist (tree nat) n
adamc@110 520 ============================
adamc@110 521 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 522 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@110 523 ]]
adamc@110 524
adamc@110 525 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 526
adamc@110 527 Check tree_ind.
adamc@110 528 (** [[
adamc@110 529
adamc@110 530 tree_ind
adamc@110 531 : forall (A : Set) (P : tree A -> Prop),
adamc@110 532 (forall a : A, P (Leaf a)) ->
adamc@110 533 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 534 forall t : tree A, P t
adamc@110 535 ]]
adamc@110 536
adamc@110 537 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@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@110 547 (** [[
adamc@110 548
adamc@110 549 Inductive tree : Set :=
adamc@110 550 | Leaf : A -> tree
adamc@110 551 | Node : forall n, filist tree n -> tree.
adamc@110 552
adamc@205 553 ]]
adamc@205 554
adamc@110 555 [[
adamc@110 556
adamc@110 557 Error: Non strictly positive occurrence of "tree" in
adamc@110 558 "forall n : nat, filist tree n -> tree"
adamc@110 559 ]]
adamc@110 560
adamc@110 561 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 562
adamc@110 563 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, reflexive types. Instead of merely using [index] to get elements out of [ilist], we can %\textit{%#<i>#define#</i>#%}% [ilist] in terms of [index]. For the reasons outlined above, it turns out to be easier to work with [findex] in place of [index]. *)
adamc@110 564
adamc@110 565 Inductive tree : Set :=
adamc@110 566 | Leaf : A -> tree
adamc@110 567 | Node : forall n, (findex n -> tree) -> tree.
adamc@110 568
adamc@110 569 (** A [Node] is indexed by a natural number [n], and the node's [n] children are represented as a function from [findex n] to trees, which is isomorphic to the [ilist]-based representation that we used above. *)
adamc@110 570 End tree.
adamc@110 571
adamc@110 572 Implicit Arguments Node [A n].
adamc@110 573
adamc@110 574 (** 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 [findex] type, and it folds another function over the results of calling the first function at every possible [findex] value. *)
adamc@110 575
adamc@110 576 Section rifoldr.
adamc@110 577 Variables A B : Set.
adamc@110 578 Variable f : A -> B -> B.
adamc@110 579 Variable i : B.
adamc@110 580
adamc@110 581 Fixpoint rifoldr (n : nat) : (findex n -> A) -> B :=
adamc@110 582 match n return (findex n -> A) -> B with
adamc@110 583 | O => fun _ => i
adamc@110 584 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 585 end.
adamc@110 586 End rifoldr.
adamc@110 587
adamc@110 588 Implicit Arguments rifoldr [A B n].
adamc@110 589
adamc@110 590 Fixpoint sum (t : tree nat) : nat :=
adamc@110 591 match t with
adamc@110 592 | Leaf n => n
adamc@110 593 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 594 end.
adamc@110 595
adamc@110 596 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 597 match t with
adamc@110 598 | Leaf n => Leaf (S n)
adamc@110 599 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 600 end.
adamc@110 601
adamc@110 602 (** 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 603
adamc@110 604 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 605 x1 >= x2
adamc@110 606 -> y1 >= y2
adamc@110 607 -> x1 + y1 >= x2 + y2.
adamc@110 608 crush.
adamc@110 609 Qed.
adamc@110 610
adamc@110 611 Lemma sum_inc' : forall n (f1 f2 : findex n -> nat),
adamc@110 612 (forall idx, f1 idx >= f2 idx)
adamc@110 613 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 614 Hint Resolve plus_ge.
adamc@110 615
adamc@110 616 induction n; crush.
adamc@110 617 Qed.
adamc@110 618
adamc@110 619 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 620 Hint Resolve sum_inc'.
adamc@110 621
adamc@110 622 induction t; crush.
adamc@110 623 Qed.
adamc@110 624
adamc@113 625 (* end thide *)
adamc@113 626
adamc@110 627 (** 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 628
adamc@111 629 (** ** Another Interpreter Example *)
adamc@111 630
adamc@112 631 (** 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 632
adamc@112 633 Inductive type' : Type := Nat | Bool.
adamc@111 634
adamc@111 635 Inductive exp' : type' -> Type :=
adamc@112 636 | NConst : nat -> exp' Nat
adamc@112 637 | Plus : exp' Nat -> exp' Nat -> exp' Nat
adamc@112 638 | Eq : exp' Nat -> exp' Nat -> exp' Bool
adamc@111 639
adamc@112 640 | BConst : bool -> exp' Bool
adamc@113 641 (* begin thide *)
adamc@112 642 | Cond : forall n t, (findex n -> exp' Bool)
adamc@111 643 -> (findex n -> exp' t) -> exp' t -> exp' t.
adamc@113 644 (* end thide *)
adamc@111 645
adamc@112 646 (** 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 [findex n -> exp' Bool], and the bodies are represented with a function of type [findex n -> exp' t], where [t] is the overall type. The final [exp' t] argument is the default case.
adamc@112 647
adamc@112 648 We start implementing our interpreter with a standard type denotation function. *)
adamc@112 649
adamc@111 650 Definition type'Denote (t : type') : Set :=
adamc@111 651 match t with
adamc@112 652 | Nat => nat
adamc@112 653 | Bool => bool
adamc@111 654 end.
adamc@111 655
adamc@112 656 (** 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 657
adamc@113 658 (* begin thide *)
adamc@111 659 Section cond.
adamc@111 660 Variable A : Set.
adamc@111 661 Variable default : A.
adamc@111 662
adamc@111 663 Fixpoint cond (n : nat) : (findex n -> bool) -> (findex n -> A) -> A :=
adamc@111 664 match n return (findex n -> bool) -> (findex n -> A) -> A with
adamc@111 665 | O => fun _ _ => default
adamc@111 666 | S n' => fun tests bodies =>
adamc@111 667 if tests None
adamc@111 668 then bodies None
adamc@111 669 else cond n'
adamc@111 670 (fun idx => tests (Some idx))
adamc@111 671 (fun idx => bodies (Some idx))
adamc@111 672 end.
adamc@111 673 End cond.
adamc@111 674
adamc@111 675 Implicit Arguments cond [A n].
adamc@113 676 (* end thide *)
adamc@111 677
adamc@112 678 (** Now the expression interpreter is straightforward to write. *)
adamc@112 679
adamc@111 680 Fixpoint exp'Denote t (e : exp' t) {struct e} : type'Denote t :=
adamc@111 681 match e in exp' t return type'Denote t with
adamc@111 682 | NConst n =>
adamc@111 683 n
adamc@111 684 | Plus e1 e2 =>
adamc@111 685 exp'Denote e1 + exp'Denote e2
adamc@111 686 | Eq e1 e2 =>
adamc@111 687 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adamc@111 688
adamc@111 689 | BConst b =>
adamc@111 690 b
adamc@111 691 | Cond _ _ tests bodies default =>
adamc@113 692 (* begin thide *)
adamc@111 693 cond
adamc@111 694 (exp'Denote default)
adamc@111 695 (fun idx => exp'Denote (tests idx))
adamc@111 696 (fun idx => exp'Denote (bodies idx))
adamc@113 697 (* end thide *)
adamc@111 698 end.
adamc@111 699
adamc@112 700 (** 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 701
adamc@113 702 (* begin thide *)
adamc@111 703 Section cfoldCond.
adamc@111 704 Variable t : type'.
adamc@111 705 Variable default : exp' t.
adamc@111 706
adamc@112 707 Fixpoint cfoldCond (n : nat)
adamc@112 708 : (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t :=
adamc@112 709 match n return (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t with
adamc@111 710 | O => fun _ _ => default
adamc@111 711 | S n' => fun tests bodies =>
adamc@204 712 match tests None return _ with
adamc@111 713 | BConst true => bodies None
adamc@111 714 | BConst false => cfoldCond n'
adamc@111 715 (fun idx => tests (Some idx))
adamc@111 716 (fun idx => bodies (Some idx))
adamc@111 717 | _ =>
adamc@111 718 let e := cfoldCond n'
adamc@111 719 (fun idx => tests (Some idx))
adamc@111 720 (fun idx => bodies (Some idx)) in
adamc@112 721 match e in exp' t return exp' t -> exp' t with
adamc@112 722 | Cond n _ tests' bodies' default' => fun body =>
adamc@111 723 Cond
adamc@111 724 (S n)
adamc@111 725 (fun idx => match idx with
adamc@112 726 | None => tests None
adamc@111 727 | Some idx => tests' idx
adamc@111 728 end)
adamc@111 729 (fun idx => match idx with
adamc@111 730 | None => body
adamc@111 731 | Some idx => bodies' idx
adamc@111 732 end)
adamc@111 733 default'
adamc@112 734 | e => fun body =>
adamc@111 735 Cond
adamc@111 736 1
adamc@112 737 (fun _ => tests None)
adamc@111 738 (fun _ => body)
adamc@111 739 e
adamc@112 740 end (bodies None)
adamc@111 741 end
adamc@111 742 end.
adamc@111 743 End cfoldCond.
adamc@111 744
adamc@111 745 Implicit Arguments cfoldCond [t n].
adamc@113 746 (* end thide *)
adamc@111 747
adamc@112 748 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
adamc@112 749
adamc@111 750 Fixpoint cfold t (e : exp' t) {struct e} : exp' t :=
adamc@111 751 match e in exp' t return exp' t with
adamc@111 752 | NConst n => NConst n
adamc@111 753 | Plus e1 e2 =>
adamc@111 754 let e1' := cfold e1 in
adamc@111 755 let e2' := cfold e2 in
adamc@204 756 match e1', e2' return _ with
adamc@111 757 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@111 758 | _, _ => Plus e1' e2'
adamc@111 759 end
adamc@111 760 | Eq 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 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@111 765 | _, _ => Eq e1' e2'
adamc@111 766 end
adamc@111 767
adamc@111 768 | BConst b => BConst b
adamc@111 769 | Cond _ _ tests bodies default =>
adamc@113 770 (* begin thide *)
adamc@111 771 cfoldCond
adamc@111 772 (cfold default)
adamc@111 773 (fun idx => cfold (tests idx))
adamc@111 774 (fun idx => cfold (bodies idx))
adamc@113 775 (* end thide *)
adamc@111 776 end.
adamc@111 777
adamc@113 778 (* begin thide *)
adamc@112 779 (** 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 780
adamc@111 781 Lemma cfoldCond_correct : forall t (default : exp' t)
adamc@112 782 n (tests : findex n -> exp' Bool) (bodies : findex n -> exp' t),
adamc@111 783 exp'Denote (cfoldCond default tests bodies)
adamc@111 784 = exp'Denote (Cond n tests bodies default).
adamc@111 785 induction n; crush;
adamc@111 786 match goal with
adamc@111 787 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
adamc@111 788 generalize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)));
adamc@111 789 clear IHn; intro IHn
adamc@111 790 end;
adamc@111 791 repeat (match goal with
adamc@111 792 | [ |- context[match ?E with
adamc@111 793 | NConst _ => _
adamc@111 794 | Plus _ _ => _
adamc@111 795 | Eq _ _ => _
adamc@111 796 | BConst _ => _
adamc@111 797 | Cond _ _ _ _ _ => _
adamc@111 798 end] ] => dep_destruct E
adamc@111 799 | [ |- context[if ?B then _ else _] ] => destruct B
adamc@111 800 end; crush).
adamc@111 801 Qed.
adamc@111 802
adamc@112 803 (** 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 804
adamc@111 805 Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : findex n -> bool)
adamc@111 806 (bodies bodies' : findex n -> A),
adamc@111 807 (forall idx, tests idx = tests' idx)
adamc@111 808 -> (forall idx, bodies idx = bodies' idx)
adamc@111 809 -> cond default tests bodies
adamc@111 810 = cond default tests' bodies'.
adamc@111 811 induction n; crush;
adamc@111 812 match goal with
adamc@111 813 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@111 814 end; crush.
adamc@111 815 Qed.
adamc@111 816
adamc@112 817 (** 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 818 (* end thide *)
adamc@112 819
adamc@111 820 Theorem cfold_correct : forall t (e : exp' t),
adamc@111 821 exp'Denote (cfold e) = exp'Denote e.
adamc@113 822 (* begin thide *)
adamc@111 823 Hint Rewrite cfoldCond_correct : cpdt.
adamc@111 824 Hint Resolve cond_ext.
adamc@111 825
adamc@111 826 induction e; crush;
adamc@111 827 repeat (match goal with
adamc@111 828 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@111 829 end; crush).
adamc@111 830 Qed.
adamc@113 831 (* end thide *)
adamc@115 832
adamc@115 833
adamc@115 834 (** * Exercises *)
adamc@115 835
adamc@116 836 (** remove printing * *)
adamc@116 837
adamc@115 838 (** Some of the type family definitions from this chapter are duplicated in the [DepList] module of the book source. Only the recursive versions of length-indexed and heterogeneous lists are included, and they are renamed without the [f] prefixes, e.g., [ilist] in place of [filist].
adamc@115 839
adamc@115 840 %\begin{enumerate}%#<ol>#
adamc@115 841
adamc@128 842 %\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 843
adamc@129 844 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 845
adamc@130 846 %\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 847
adamc@116 848 [[
adamc@116 849 t ::= bool | t + t
adamc@116 850 p ::= x | b | inl p | inr p
adamc@116 851 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e
adamc@116 852 ]]
adamc@116 853
adamc@116 854 [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 855
adamc@117 856 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 857
adamc@115 858 #</ol>#%\end{enumerate}% *)