Mercurial > cpdt > repo

annotate src/DataStruct.v @ 108:7abf5535baab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
STLC interp
author Adam Chlipala <adamc@hcoop.net>
date Mon, 13 Oct 2008 13:20:57 -0400
parents 924d77a177e8
children fe6cfbae86b9
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@105 11 Require Import 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@105 37 Inductive index : nat -> Set :=
adamc@105 38 | First : forall n, index (S n)
adamc@105 39 | Next : forall n, index n -> index (S n).
adamc@105 40
adamc@106 41 (** [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 42
adamc@106 43 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 44
adamc@106 45 [[
adamc@106 46 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 47 match ls in ilist n return index n -> A with
adamc@106 48 | Nil => fun idx => ?
adamc@106 49 | Cons _ x ls' => fun idx =>
adamc@106 50 match idx with
adamc@106 51 | First _ => x
adamc@106 52 | Next _ idx' => get ls' idx'
adamc@106 53 end
adamc@106 54 end.
adamc@106 55
adamc@106 56 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 57
adamc@106 58 [[
adamc@106 59 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 60 match ls in ilist n return index n -> A with
adamc@106 61 | Nil => fun idx =>
adamc@106 62 match idx in index n' return (match n' with
adamc@106 63 | O => A
adamc@106 64 | S _ => unit
adamc@106 65 end) with
adamc@106 66 | First _ => tt
adamc@106 67 | Next _ _ => tt
adamc@106 68 end
adamc@106 69 | Cons _ x ls' => fun idx =>
adamc@106 70 match idx with
adamc@106 71 | First _ => x
adamc@106 72 | Next _ idx' => get ls' idx'
adamc@106 73 end
adamc@106 74 end.
adamc@106 75
adamc@106 76 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 77
adamc@106 78 [[
adamc@106 79 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 80 match ls in ilist n return index n -> A with
adamc@106 81 | Nil => fun idx =>
adamc@106 82 match idx in index n' return (match n' with
adamc@106 83 | O => A
adamc@106 84 | S _ => unit
adamc@106 85 end) with
adamc@106 86 | First _ => tt
adamc@106 87 | Next _ _ => tt
adamc@106 88 end
adamc@106 89 | Cons _ x ls' => fun idx =>
adamc@106 90 match idx in index n' return ilist (pred n') -> A with
adamc@106 91 | First _ => fun _ => x
adamc@106 92 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 93 end ls'
adamc@106 94 end.
adamc@106 95
adamc@106 96 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 97
adamc@105 98 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@105 99 match ls in ilist n return index n -> A with
adamc@105 100 | Nil => fun idx =>
adamc@105 101 match idx in index n' return (match n' with
adamc@105 102 | O => A
adamc@105 103 | S _ => unit
adamc@105 104 end) with
adamc@105 105 | First _ => tt
adamc@105 106 | Next _ _ => tt
adamc@105 107 end
adamc@105 108 | Cons _ x ls' => fun idx =>
adamc@105 109 match idx in index n' return (index (pred n') -> A) -> A with
adamc@105 110 | First _ => fun _ => x
adamc@105 111 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 112 end (get ls')
adamc@105 113 end.
adamc@105 114 End ilist.
adamc@105 115
adamc@105 116 Implicit Arguments Nil [A].
adamc@108 117 Implicit Arguments First [n].
adamc@105 118
adamc@108 119 (** A few examples show how to make use of these definitions. *)
adamc@108 120
adamc@108 121 Check Cons 0 (Cons 1 (Cons 2 Nil)).
adamc@108 122 (** [[
adamc@108 123
adamc@108 124 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 125 : ilist nat 3
adamc@108 126 ]] *)
adamc@108 127 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@108 128 (** [[
adamc@108 129
adamc@108 130 = 0
adamc@108 131 : nat
adamc@108 132 ]] *)
adamc@108 133 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@108 134 (** [[
adamc@108 135
adamc@108 136 = 1
adamc@108 137 : nat
adamc@108 138 ]] *)
adamc@108 139 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@108 140 (** [[
adamc@108 141
adamc@108 142 = 2
adamc@108 143 : nat
adamc@108 144 ]] *)
adamc@108 145
adamc@108 146 (** 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 147
adamc@105 148 Section ilist_map.
adamc@105 149 Variables A B : Set.
adamc@105 150 Variable f : A -> B.
adamc@105 151
adamc@105 152 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
adamc@105 153 match ls in ilist _ n return ilist B n with
adamc@105 154 | Nil => Nil
adamc@105 155 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 156 end.
adamc@105 157
adamc@107 158 (** 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 159
adamc@107 160 Theorem get_imap : forall n (idx : index n) (ls : ilist A n),
adamc@105 161 get (imap ls) idx = f (get ls idx).
adamc@107 162 induction ls; dep_destruct idx; crush.
adamc@105 163 Qed.
adamc@105 164 End ilist_map.
adamc@107 165
adamc@107 166
adamc@107 167 (** * Heterogeneous Lists *)
adamc@107 168
adamc@107 169 (** 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 170
adamc@107 171 Section hlist.
adamc@107 172 Variable A : Type.
adamc@107 173 Variable B : A -> Type.
adamc@107 174
adamc@107 175 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
adamc@107 176
adamc@107 177 Inductive hlist : list A -> Type :=
adamc@107 178 | MNil : hlist nil
adamc@107 179 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 180
adamc@107 181 (** 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 182
adamc@107 183 Variable elm : A.
adamc@107 184
adamc@107 185 Inductive member : list A -> Type :=
adamc@107 186 | MFirst : forall ls, member (elm :: ls)
adamc@107 187 | MNext : forall x ls, member ls -> member (x :: ls).
adamc@107 188
adamc@107 189 (** 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 190
adamc@107 191 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 192
adamc@107 193 Fixpoint hget ls (mls : hlist ls) {struct mls} : member ls -> B elm :=
adamc@107 194 match mls in hlist ls return member ls -> B elm with
adamc@107 195 | MNil => fun mem =>
adamc@107 196 match mem in member ls' return (match ls' with
adamc@107 197 | nil => B elm
adamc@107 198 | _ :: _ => unit
adamc@107 199 end) with
adamc@107 200 | MFirst _ => tt
adamc@107 201 | MNext _ _ _ => tt
adamc@107 202 end
adamc@107 203 | MCons _ _ x mls' => fun mem =>
adamc@107 204 match mem in member ls' return (match ls' with
adamc@107 205 | nil => Empty_set
adamc@107 206 | x' :: ls'' =>
adamc@107 207 B x' -> (member ls'' -> B elm) -> B elm
adamc@107 208 end) with
adamc@107 209 | MFirst _ => fun x _ => x
adamc@107 210 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@107 211 end x (hget mls')
adamc@107 212 end.
adamc@107 213 End hlist.
adamc@108 214
adamc@108 215 Implicit Arguments MNil [A B].
adamc@108 216 Implicit Arguments MCons [A B x ls].
adamc@108 217
adamc@108 218 Implicit Arguments MFirst [A elm ls].
adamc@108 219 Implicit Arguments MNext [A elm x ls].
adamc@108 220
adamc@108 221 (** 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 222
adamc@108 223 Definition someTypes : list Set := nat :: bool :: nil.
adamc@108 224
adamc@108 225 Example someValues : hlist (fun T : Set => T) someTypes :=
adamc@108 226 MCons 5 (MCons true MNil).
adamc@108 227
adamc@108 228 Eval simpl in hget someValues MFirst.
adamc@108 229 (** [[
adamc@108 230
adamc@108 231 = 5
adamc@108 232 : (fun T : Set => T) nat
adamc@108 233 ]] *)
adamc@108 234 Eval simpl in hget someValues (MNext MFirst).
adamc@108 235 (** [[
adamc@108 236
adamc@108 237 = true
adamc@108 238 : (fun T : Set => T) bool
adamc@108 239 ]] *)
adamc@108 240
adamc@108 241 (** We can also build indexed lists of pairs in this way. *)
adamc@108 242
adamc@108 243 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
adamc@108 244 MCons (1, 2) (MCons (true, false) MNil).
adamc@108 245
adamc@108 246 (** ** A Lambda Calculus Interpreter *)
adamc@108 247
adamc@108 248 (** 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 249
adamc@108 250 We start with an algebraic datatype for types. *)
adamc@108 251
adamc@108 252 Inductive type : Set :=
adamc@108 253 | Unit : type
adamc@108 254 | Arrow : type -> type -> type.
adamc@108 255
adamc@108 256 (** 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 257
adamc@108 258 Inductive exp : list type -> type -> Set :=
adamc@108 259 | Const : forall ts, exp ts Unit
adamc@108 260
adamc@108 261 | Var : forall ts t, member t ts -> exp ts t
adamc@108 262 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 263 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@108 264
adamc@108 265 Implicit Arguments Const [ts].
adamc@108 266
adamc@108 267 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 268
adamc@108 269 Fixpoint typeDenote (t : type) : Set :=
adamc@108 270 match t with
adamc@108 271 | Unit => unit
adamc@108 272 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 273 end.
adamc@108 274
adamc@108 275 (** 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 276
adamc@108 277 Fixpoint expDenote ts t (e : exp ts t) {struct e} : hlist typeDenote ts -> typeDenote t :=
adamc@108 278 match e in exp ts t return hlist typeDenote ts -> typeDenote t with
adamc@108 279 | Const _ => fun _ => tt
adamc@108 280
adamc@108 281 | Var _ _ mem => fun s => hget s mem
adamc@108 282 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@108 283 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
adamc@108 284 end.
adamc@108 285
adamc@108 286 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 287
adamc@108 288 Eval simpl in expDenote Const MNil.
adamc@108 289 (** [[
adamc@108 290
adamc@108 291 = tt
adamc@108 292 : typeDenote Unit
adamc@108 293 ]] *)
adamc@108 294 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
adamc@108 295 (** [[
adamc@108 296
adamc@108 297 = fun x : unit => x
adamc@108 298 : typeDenote (Arrow Unit Unit)
adamc@108 299 ]] *)
adamc@108 300 Eval simpl in expDenote (Abs (dom := Unit)
adamc@108 301 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
adamc@108 302 (** [[
adamc@108 303
adamc@108 304 = fun x _ : unit => x
adamc@108 305 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 306 ]] *)
adamc@108 307 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
adamc@108 308 (** [[
adamc@108 309
adamc@108 310 = fun _ x0 : unit => x0
adamc@108 311 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 312 ]] *)
adamc@108 313 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
adamc@108 314 (** [[
adamc@108 315
adamc@108 316 = tt
adamc@108 317 : typeDenote Unit
adamc@108 318 ]] *)
adamc@108 319
adamc@108 320 (** 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 321
adamc@108 322