Mercurial > cpdt > repo

annotate src/DataStruct.v @ 216:d1464997078d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch DepList to inductive, not recursive, types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:28:47 -0500
parents f8bcd33bdd91
children 6601384e7e14
rev   line source
adamc@215 1 (* Copyright (c) 2008-2009, 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@215 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 names 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
adamc@215 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.
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
adamc@215 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 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 84
adamc@106 85 [[
adamc@215 86 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 87 match ls with
adamc@106 88 | Nil => fun idx =>
adamc@215 89 match idx in fin 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@215 97 match idx in fin 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@215 107 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 108 match ls with
adamc@105 109 | Nil => fun idx =>
adamc@215 110 match idx in fin 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@215 118 match idx in fin n' return (fin (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@215 134 (** %\vspace{-.15in}% [[
adamc@215 135 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 136 : ilist nat 3
adamc@108 137 ]] *)
adamc@215 138
adamc@113 139 (* begin thide *)
adamc@108 140 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@215 141 (** %\vspace{-.15in}% [[
adamc@108 142 = 0
adamc@108 143 : nat
adamc@108 144 ]] *)
adamc@215 145
adamc@108 146 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@215 147 (** %\vspace{-.15in}% [[
adamc@108 148 = 1
adamc@108 149 : nat
adamc@108 150 ]] *)
adamc@215 151
adamc@108 152 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@215 153 (** %\vspace{-.15in}% [[
adamc@108 154 = 2
adamc@108 155 : nat
adamc@108 156 ]] *)
adamc@113 157 (* end thide *)
adamc@108 158
adamc@108 159 (** 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 160
adamc@105 161 Section ilist_map.
adamc@105 162 Variables A B : Set.
adamc@105 163 Variable f : A -> B.
adamc@105 164
adamc@215 165 Fixpoint imap n (ls : ilist A n) : ilist B n :=
adamc@215 166 match ls with
adamc@105 167 | Nil => Nil
adamc@105 168 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 169 end.
adamc@105 170
adamc@107 171 (** 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 172
adamc@215 173 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n),
adamc@105 174 get (imap ls) idx = f (get ls idx).
adamc@113 175 (* begin thide *)
adamc@107 176 induction ls; dep_destruct idx; crush.
adamc@105 177 Qed.
adamc@113 178 (* end thide *)
adamc@105 179 End ilist_map.
adamc@107 180
adamc@107 181
adamc@107 182 (** * Heterogeneous Lists *)
adamc@107 183
adamc@215 184 (** 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 185
adamc@107 186 Section hlist.
adamc@107 187 Variable A : Type.
adamc@107 188 Variable B : A -> Type.
adamc@107 189
adamc@113 190 (* 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 191
adamc@107 192 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
adamc@107 193
adamc@113 194 (* begin thide *)
adamc@107 195 Inductive hlist : list A -> Type :=
adamc@107 196 | MNil : hlist nil
adamc@107 197 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 198
adamc@107 199 (** 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 200
adamc@113 201 (* end thide *)
adamc@113 202 (* EX: Define an analogue to [get] for [hlist]s. *)
adamc@113 203
adamc@113 204 (* begin thide *)
adamc@107 205 Variable elm : A.
adamc@107 206
adamc@107 207 Inductive member : list A -> Type :=
adamc@107 208 | MFirst : forall ls, member (elm :: ls)
adamc@107 209 | MNext : forall x ls, member ls -> member (x :: ls).
adamc@107 210
adamc@107 211 (** 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 212
adamc@107 213 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 214
adamc@215 215 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
adamc@215 216 match mls with
adamc@107 217 | MNil => fun mem =>
adamc@107 218 match mem in member ls' return (match ls' with
adamc@107 219 | nil => B elm
adamc@107 220 | _ :: _ => unit
adamc@107 221 end) with
adamc@107 222 | MFirst _ => tt
adamc@107 223 | MNext _ _ _ => tt
adamc@107 224 end
adamc@107 225 | MCons _ _ x mls' => fun mem =>
adamc@107 226 match mem in member ls' return (match ls' with
adamc@107 227 | nil => Empty_set
adamc@107 228 | x' :: ls'' =>
adamc@107 229 B x' -> (member ls'' -> B elm) -> B elm
adamc@107 230 end) with
adamc@107 231 | MFirst _ => fun x _ => x
adamc@107 232 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@107 233 end x (hget mls')
adamc@107 234 end.
adamc@113 235 (* end thide *)
adamc@107 236 End hlist.
adamc@108 237
adamc@113 238 (* begin thide *)
adamc@108 239 Implicit Arguments MNil [A B].
adamc@108 240 Implicit Arguments MCons [A B x ls].
adamc@108 241
adamc@108 242 Implicit Arguments MFirst [A elm ls].
adamc@108 243 Implicit Arguments MNext [A elm x ls].
adamc@113 244 (* end thide *)
adamc@108 245
adamc@108 246 (** 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 247
adamc@108 248 Definition someTypes : list Set := nat :: bool :: nil.
adamc@108 249
adamc@113 250 (* begin thide *)
adamc@113 251
adamc@108 252 Example someValues : hlist (fun T : Set => T) someTypes :=
adamc@108 253 MCons 5 (MCons true MNil).
adamc@108 254
adamc@108 255 Eval simpl in hget someValues MFirst.
adamc@215 256 (** %\vspace{-.15in}% [[
adamc@108 257 = 5
adamc@108 258 : (fun T : Set => T) nat
adamc@108 259 ]] *)
adamc@215 260
adamc@108 261 Eval simpl in hget someValues (MNext MFirst).
adamc@215 262 (** %\vspace{-.15in}% [[
adamc@108 263 = true
adamc@108 264 : (fun T : Set => T) bool
adamc@108 265 ]] *)
adamc@108 266
adamc@108 267 (** We can also build indexed lists of pairs in this way. *)
adamc@108 268
adamc@108 269 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
adamc@108 270 MCons (1, 2) (MCons (true, false) MNil).
adamc@108 271
adamc@113 272 (* end thide *)
adamc@113 273
adamc@113 274
adamc@108 275 (** ** A Lambda Calculus Interpreter *)
adamc@108 276
adamc@108 277 (** 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 278
adamc@108 279 We start with an algebraic datatype for types. *)
adamc@108 280
adamc@108 281 Inductive type : Set :=
adamc@108 282 | Unit : type
adamc@108 283 | Arrow : type -> type -> type.
adamc@108 284
adamc@108 285 (** 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 286
adamc@108 287 Inductive exp : list type -> type -> Set :=
adamc@108 288 | Const : forall ts, exp ts Unit
adamc@113 289 (* begin thide *)
adamc@108 290 | Var : forall ts t, member t ts -> exp ts t
adamc@108 291 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 292 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@113 293 (* end thide *)
adamc@108 294
adamc@108 295 Implicit Arguments Const [ts].
adamc@108 296
adamc@108 297 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 298
adamc@108 299 Fixpoint typeDenote (t : type) : Set :=
adamc@108 300 match t with
adamc@108 301 | Unit => unit
adamc@108 302 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 303 end.
adamc@108 304
adamc@108 305 (** 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 306
adamc@113 307 (* EX: Define an interpreter for [exp]s. *)
adamc@113 308
adamc@113 309 (* begin thide *)
adamc@215 310 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
adamc@215 311 match e with
adamc@108 312 | Const _ => fun _ => tt
adamc@108 313
adamc@108 314 | Var _ _ mem => fun s => hget s mem
adamc@108 315 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@108 316 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
adamc@108 317 end.
adamc@108 318
adamc@108 319 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 320
adamc@108 321 Eval simpl in expDenote Const MNil.
adamc@215 322 (** %\vspace{-.15in}% [[
adamc@108 323 = tt
adamc@108 324 : typeDenote Unit
adamc@108 325 ]] *)
adamc@215 326
adamc@108 327 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
adamc@215 328 (** %\vspace{-.15in}% [[
adamc@108 329 = fun x : unit => x
adamc@108 330 : typeDenote (Arrow Unit Unit)
adamc@108 331 ]] *)
adamc@215 332
adamc@108 333 Eval simpl in expDenote (Abs (dom := Unit)
adamc@108 334 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
adamc@215 335 (** %\vspace{-.15in}% [[
adamc@108 336 = fun x _ : unit => x
adamc@108 337 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 338 ]] *)
adamc@215 339
adamc@108 340 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
adamc@215 341 (** %\vspace{-.15in}% [[
adamc@108 342 = fun _ x0 : unit => x0
adamc@108 343 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 344 ]] *)
adamc@215 345
adamc@108 346 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
adamc@215 347 (** %\vspace{-.15in}% [[
adamc@108 348 = tt
adamc@108 349 : typeDenote Unit
adamc@108 350 ]] *)
adamc@108 351
adamc@113 352 (* end thide *)
adamc@113 353
adamc@108 354 (** 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 355
adamc@108 356
adamc@109 357 (** * Recursive Type Definitions *)
adamc@109 358
adamc@109 359 (** 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 360
adamc@113 361 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
adamc@113 362
adamc@109 363 Section filist.
adamc@109 364 Variable A : Set.
adamc@109 365
adamc@113 366 (* begin thide *)
adamc@109 367 Fixpoint filist (n : nat) : Set :=
adamc@109 368 match n with
adamc@109 369 | O => unit
adamc@109 370 | S n' => A * filist n'
adamc@109 371 end%type.
adamc@109 372
adamc@109 373 (** 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 374
adamc@215 375 Fixpoint ffin (n : nat) : Set :=
adamc@109 376 match n with
adamc@109 377 | O => Empty_set
adamc@215 378 | S n' => option (ffin n')
adamc@109 379 end.
adamc@109 380
adamc@109 381 (** 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 382
adamc@215 383 Fixpoint fget (n : nat) : filist n -> ffin n -> A :=
adamc@215 384 match n with
adamc@109 385 | O => fun _ idx => match idx with end
adamc@109 386 | S n' => fun ls idx =>
adamc@109 387 match idx with
adamc@109 388 | None => fst ls
adamc@109 389 | Some idx' => fget n' (snd ls) idx'
adamc@109 390 end
adamc@109 391 end.
adamc@109 392
adamc@215 393 (** 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 394 (* end thide *)
adamc@215 395
adamc@109 396 End filist.
adamc@109 397
adamc@109 398 (** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)
adamc@109 399
adamc@113 400 (* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)
adamc@113 401
adamc@109 402 Section fhlist.
adamc@109 403 Variable A : Type.
adamc@109 404 Variable B : A -> Type.
adamc@109 405
adamc@113 406 (* begin thide *)
adamc@109 407 Fixpoint fhlist (ls : list A) : Type :=
adamc@109 408 match ls with
adamc@109 409 | nil => unit
adamc@109 410 | x :: ls' => B x * fhlist ls'
adamc@109 411 end%type.
adamc@109 412
adamc@109 413 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently-typed data elements. *)
adamc@109 414
adamc@109 415 Variable elm : A.
adamc@109 416
adamc@109 417 Fixpoint fmember (ls : list A) : Type :=
adamc@109 418 match ls with
adamc@109 419 | nil => Empty_set
adamc@109 420 | x :: ls' => (x = elm) + fmember ls'
adamc@109 421 end%type.
adamc@109 422
adamc@215 423 (** 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 424
adamc@109 425 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
adamc@109 426
adamc@109 427 [[
adamc@109 428 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 429 match ls with
adamc@109 430 | nil => fun _ idx => match idx with end
adamc@109 431 | _ :: ls' => fun mls idx =>
adamc@109 432 match idx with
adamc@109 433 | inl _ => fst mls
adamc@109 434 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 435 end
adamc@109 436 end.
adamc@109 437
adamc@205 438 ]]
adamc@205 439
adamc@109 440 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 441
adamc@109 442 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 443 match ls with
adamc@109 444 | nil => fun _ idx => match idx with end
adamc@109 445 | _ :: ls' => fun mls idx =>
adamc@109 446 match idx with
adamc@109 447 | inl pf => match pf with
adamc@109 448 | refl_equal => fst mls
adamc@109 449 end
adamc@109 450 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 451 end
adamc@109 452 end.
adamc@109 453
adamc@109 454 (** 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 455
adamc@109 456 Print eq.
adamc@215 457 (** %\vspace{-.15in}% [[
adamc@109 458 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x
adamc@215 459
adamc@109 460 ]]
adamc@109 461
adamc@215 462 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 463 (* end thide *)
adamc@215 464
adamc@109 465 End fhlist.
adamc@110 466
adamc@111 467 Implicit Arguments fhget [A B elm ls].
adamc@111 468
adamc@110 469
adamc@110 470 (** * Data Structures as Index Functions *)
adamc@110 471
adamc@110 472 (** 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 473
adamc@110 474 Section tree.
adamc@110 475 Variable A : Set.
adamc@110 476
adamc@110 477 Inductive tree : Set :=
adamc@110 478 | Leaf : A -> tree
adamc@110 479 | Node : forall n, ilist tree n -> tree.
adamc@110 480 End tree.
adamc@110 481
adamc@110 482 (** 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 483
adamc@110 484 Section ifoldr.
adamc@110 485 Variables A B : Set.
adamc@110 486 Variable f : A -> B -> B.
adamc@110 487 Variable i : B.
adamc@110 488
adamc@215 489 Fixpoint ifoldr n (ls : ilist A n) : B :=
adamc@110 490 match ls with
adamc@110 491 | Nil => i
adamc@110 492 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 493 end.
adamc@110 494 End ifoldr.
adamc@110 495
adamc@110 496 Fixpoint sum (t : tree nat) : nat :=
adamc@110 497 match t with
adamc@110 498 | Leaf n => n
adamc@110 499 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 500 end.
adamc@110 501
adamc@110 502 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 503 match t with
adamc@110 504 | Leaf n => Leaf (S n)
adamc@110 505 | Node _ ls => Node (imap inc ls)
adamc@110 506 end.
adamc@110 507
adamc@110 508 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 509
adamc@110 510 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@113 511 (* begin thide *)
adamc@110 512 induction t; crush.
adamc@110 513 (** [[
adamc@110 514
adamc@110 515 n : nat
adamc@110 516 i : ilist (tree nat) n
adamc@110 517 ============================
adamc@110 518 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 519 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@215 520
adamc@110 521 ]]
adamc@110 522
adamc@110 523 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 524
adamc@110 525 Check tree_ind.
adamc@215 526 (** %\vspace{-.15in}% [[
adamc@215 527 tree_ind
adamc@110 528 : forall (A : Set) (P : tree A -> Prop),
adamc@110 529 (forall a : A, P (Leaf a)) ->
adamc@110 530 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 531 forall t : tree A, P t
adamc@215 532
adamc@110 533 ]]
adamc@110 534
adamc@110 535 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 536
adamc@110 537 Abort.
adamc@110 538
adamc@110 539 Reset tree.
adamc@110 540
adamc@110 541 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
adamc@110 542
adamc@110 543 Section tree.
adamc@110 544 Variable A : Set.
adamc@110 545
adamc@215 546 (** %\vspace{-.15in}% [[
adamc@110 547 Inductive tree : Set :=
adamc@110 548 | Leaf : A -> tree
adamc@110 549 | Node : forall n, filist tree n -> tree.
adamc@110 550
adamc@110 551 Error: Non strictly positive occurrence of "tree" in
adamc@110 552 "forall n : nat, filist tree n -> tree"
adamc@215 553
adamc@110 554 ]]
adamc@110 555
adamc@110 556 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 557
adamc@215 558 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 559
adamc@110 560 Inductive tree : Set :=
adamc@110 561 | Leaf : A -> tree
adamc@215 562 | Node : forall n, (ffin n -> tree) -> tree.
adamc@110 563
adamc@215 564 (** 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 565
adamc@110 566 End tree.
adamc@110 567
adamc@110 568 Implicit Arguments Node [A n].
adamc@110 569
adamc@215 570 (** 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 571
adamc@110 572 Section rifoldr.
adamc@110 573 Variables A B : Set.
adamc@110 574 Variable f : A -> B -> B.
adamc@110 575 Variable i : B.
adamc@110 576
adamc@215 577 Fixpoint rifoldr (n : nat) : (ffin n -> A) -> B :=
adamc@215 578 match n with
adamc@110 579 | O => fun _ => i
adamc@110 580 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 581 end.
adamc@110 582 End rifoldr.
adamc@110 583
adamc@110 584 Implicit Arguments rifoldr [A B n].
adamc@110 585
adamc@110 586 Fixpoint sum (t : tree nat) : nat :=
adamc@110 587 match t with
adamc@110 588 | Leaf n => n
adamc@110 589 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 590 end.
adamc@110 591
adamc@110 592 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 593 match t with
adamc@110 594 | Leaf n => Leaf (S n)
adamc@110 595 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 596 end.
adamc@110 597
adamc@110 598 (** 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 599
adamc@110 600 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 601 x1 >= x2
adamc@110 602 -> y1 >= y2
adamc@110 603 -> x1 + y1 >= x2 + y2.
adamc@110 604 crush.
adamc@110 605 Qed.
adamc@110 606
adamc@215 607 Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat),
adamc@110 608 (forall idx, f1 idx >= f2 idx)
adamc@110 609 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 610 Hint Resolve plus_ge.
adamc@110 611
adamc@110 612 induction n; crush.
adamc@110 613 Qed.
adamc@110 614
adamc@110 615 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 616 Hint Resolve sum_inc'.
adamc@110 617
adamc@110 618 induction t; crush.
adamc@110 619 Qed.
adamc@110 620
adamc@113 621 (* end thide *)
adamc@113 622
adamc@110 623 (** 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 624
adamc@111 625 (** ** Another Interpreter Example *)
adamc@111 626
adamc@112 627 (** 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 628
adamc@112 629 Inductive type' : Type := Nat | Bool.
adamc@111 630
adamc@111 631 Inductive exp' : type' -> Type :=
adamc@112 632 | NConst : nat -> exp' Nat
adamc@112 633 | Plus : exp' Nat -> exp' Nat -> exp' Nat
adamc@112 634 | Eq : exp' Nat -> exp' Nat -> exp' Bool
adamc@111 635
adamc@112 636 | BConst : bool -> exp' Bool
adamc@113 637 (* begin thide *)
adamc@215 638 | Cond : forall n t, (ffin n -> exp' Bool)
adamc@215 639 -> (ffin n -> exp' t) -> exp' t -> exp' t.
adamc@113 640 (* end thide *)
adamc@111 641
adamc@215 642 (** 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.
adamc@112 643
adamc@112 644 We start implementing our interpreter with a standard type denotation function. *)
adamc@112 645
adamc@111 646 Definition type'Denote (t : type') : Set :=
adamc@111 647 match t with
adamc@112 648 | Nat => nat
adamc@112 649 | Bool => bool
adamc@111 650 end.
adamc@111 651
adamc@112 652 (** 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 653
adamc@113 654 (* begin thide *)
adamc@111 655 Section cond.
adamc@111 656 Variable A : Set.
adamc@111 657 Variable default : A.
adamc@111 658
adamc@215 659 Fixpoint cond (n : nat) : (ffin n -> bool) -> (ffin n -> A) -> A :=
adamc@215 660 match n with
adamc@111 661 | O => fun _ _ => default
adamc@111 662 | S n' => fun tests bodies =>
adamc@111 663 if tests None
adamc@111 664 then bodies None
adamc@111 665 else cond n'
adamc@111 666 (fun idx => tests (Some idx))
adamc@111 667 (fun idx => bodies (Some idx))
adamc@111 668 end.
adamc@111 669 End cond.
adamc@111 670
adamc@111 671 Implicit Arguments cond [A n].
adamc@113 672 (* end thide *)
adamc@111 673
adamc@112 674 (** Now the expression interpreter is straightforward to write. *)
adamc@112 675
adamc@215 676 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
adamc@215 677 match e with
adamc@215 678 | NConst n => n
adamc@215 679 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
adamc@111 680 | Eq e1 e2 =>
adamc@111 681 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adamc@111 682
adamc@215 683 | BConst b => b
adamc@111 684 | Cond _ _ tests bodies default =>
adamc@113 685 (* begin thide *)
adamc@111 686 cond
adamc@111 687 (exp'Denote default)
adamc@111 688 (fun idx => exp'Denote (tests idx))
adamc@111 689 (fun idx => exp'Denote (bodies idx))
adamc@113 690 (* end thide *)
adamc@111 691 end.
adamc@111 692
adamc@112 693 (** 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 694
adamc@113 695 (* begin thide *)
adamc@111 696 Section cfoldCond.
adamc@111 697 Variable t : type'.
adamc@111 698 Variable default : exp' t.
adamc@111 699
adamc@112 700 Fixpoint cfoldCond (n : nat)
adamc@215 701 : (ffin n -> exp' Bool) -> (ffin n -> exp' t) -> exp' t :=
adamc@215 702 match n with
adamc@111 703 | O => fun _ _ => default
adamc@111 704 | S n' => fun tests bodies =>
adamc@204 705 match tests None return _ with
adamc@111 706 | BConst true => bodies None
adamc@111 707 | BConst false => cfoldCond n'
adamc@111 708 (fun idx => tests (Some idx))
adamc@111 709 (fun idx => bodies (Some idx))
adamc@111 710 | _ =>
adamc@111 711 let e := cfoldCond n'
adamc@111 712 (fun idx => tests (Some idx))
adamc@111 713 (fun idx => bodies (Some idx)) in
adamc@112 714 match e in exp' t return exp' t -> exp' t with
adamc@112 715 | Cond n _ tests' bodies' default' => fun body =>
adamc@111 716 Cond
adamc@111 717 (S n)
adamc@111 718 (fun idx => match idx with
adamc@112 719 | None => tests None
adamc@111 720 | Some idx => tests' idx
adamc@111 721 end)
adamc@111 722 (fun idx => match idx with
adamc@111 723 | None => body
adamc@111 724 | Some idx => bodies' idx
adamc@111 725 end)
adamc@111 726 default'
adamc@112 727 | e => fun body =>
adamc@111 728 Cond
adamc@111 729 1
adamc@112 730 (fun _ => tests None)
adamc@111 731 (fun _ => body)
adamc@111 732 e
adamc@112 733 end (bodies None)
adamc@111 734 end
adamc@111 735 end.
adamc@111 736 End cfoldCond.
adamc@111 737
adamc@111 738 Implicit Arguments cfoldCond [t n].
adamc@113 739 (* end thide *)
adamc@111 740
adamc@112 741 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
adamc@112 742
adamc@215 743 Fixpoint cfold t (e : exp' t) : exp' t :=
adamc@215 744 match e with
adamc@111 745 | NConst n => NConst n
adamc@111 746 | Plus e1 e2 =>
adamc@111 747 let e1' := cfold e1 in
adamc@111 748 let e2' := cfold e2 in
adamc@204 749 match e1', e2' return _ with
adamc@111 750 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@111 751 | _, _ => Plus e1' e2'
adamc@111 752 end
adamc@111 753 | Eq 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 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@111 758 | _, _ => Eq e1' e2'
adamc@111 759 end
adamc@111 760
adamc@111 761 | BConst b => BConst b
adamc@111 762 | Cond _ _ tests bodies default =>
adamc@113 763 (* begin thide *)
adamc@111 764 cfoldCond
adamc@111 765 (cfold default)
adamc@111 766 (fun idx => cfold (tests idx))
adamc@111 767 (fun idx => cfold (bodies idx))
adamc@113 768 (* end thide *)
adamc@111 769 end.
adamc@111 770
adamc@113 771 (* begin thide *)
adamc@112 772 (** 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 773
adamc@111 774 Lemma cfoldCond_correct : forall t (default : exp' t)
adamc@215 775 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
adamc@111 776 exp'Denote (cfoldCond default tests bodies)
adamc@111 777 = exp'Denote (Cond n tests bodies default).
adamc@111 778 induction n; crush;
adamc@111 779 match goal with
adamc@111 780 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
adamc@111 781 generalize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)));
adamc@111 782 clear IHn; intro IHn
adamc@111 783 end;
adamc@111 784 repeat (match goal with
adamc@111 785 | [ |- context[match ?E with
adamc@111 786 | NConst _ => _
adamc@111 787 | Plus _ _ => _
adamc@111 788 | Eq _ _ => _
adamc@111 789 | BConst _ => _
adamc@111 790 | Cond _ _ _ _ _ => _
adamc@111 791 end] ] => dep_destruct E
adamc@111 792 | [ |- context[if ?B then _ else _] ] => destruct B
adamc@111 793 end; crush).
adamc@111 794 Qed.
adamc@111 795
adamc@112 796 (** 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 797
adamc@215 798 Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : ffin n -> bool)
adamc@215 799 (bodies bodies' : ffin n -> A),
adamc@111 800 (forall idx, tests idx = tests' idx)
adamc@111 801 -> (forall idx, bodies idx = bodies' idx)
adamc@111 802 -> cond default tests bodies
adamc@111 803 = cond default tests' bodies'.
adamc@111 804 induction n; crush;
adamc@111 805 match goal with
adamc@111 806 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@111 807 end; crush.
adamc@111 808 Qed.
adamc@111 809
adamc@112 810 (** 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 811 (* end thide *)
adamc@112 812
adamc@111 813 Theorem cfold_correct : forall t (e : exp' t),
adamc@111 814 exp'Denote (cfold e) = exp'Denote e.
adamc@113 815 (* begin thide *)
adamc@111 816 Hint Rewrite cfoldCond_correct : cpdt.
adamc@111 817 Hint Resolve cond_ext.
adamc@111 818
adamc@111 819 induction e; crush;
adamc@111 820 repeat (match goal with
adamc@111 821 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@111 822 end; crush).
adamc@111 823 Qed.
adamc@113 824 (* end thide *)
adamc@115 825
adamc@115 826
adamc@215 827 (** * Choosing Between Representations *)
adamc@215 828
adamc@215 829 (** 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 830
adamc@215 831 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 832
adamc@215 833 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 function [replace] of type [forall A, filist A n -> fin n -> A -> filist A n], such that [replace l f x] should substitute [x] for the element in position [f] of [l]. A call to [replace] on a variable [l] of type [filist A (S n)] would probably be simplified to an explicit pair, even though we know nothing about the structure of [l] beyond its 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 834
adamc@215 835 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 836
adamc@215 837 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. *)
adamc@215 838
adamc@215 839
adamc@115 840 (** * Exercises *)
adamc@115 841
adamc@116 842 (** remove printing * *)
adamc@116 843
adamc@216 844 (** 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 845
adamc@115 846 %\begin{enumerate}%#<ol>#
adamc@115 847
adamc@128 848 %\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 849
adamc@129 850 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 851
adamc@130 852 %\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 853
adamc@116 854 [[
adamc@116 855 t ::= bool | t + t
adamc@116 856 p ::= x | b | inl p | inr p
adamc@116 857 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e
adamc@215 858
adamc@116 859 ]]
adamc@116 860
adamc@116 861 [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 862
adamc@117 863 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 864
adamc@115 865 #</ol>#%\end{enumerate}% *)