comparison src/DataStruct.v @ 342:25d60fed2e96

Pass through DataStruct
author Adam Chlipala <adam@chlipala.net>
date Sun, 16 Oct 2011 10:46:15 -0400
parents d5787b70cf48
children 549d604c3d16
comparison
equal deleted inserted replaced
341:e76aced46eb1 342:25d60fed2e96
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
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. *) 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. *)
22 22
23 23
24 (** * More Length-Indexed Lists *) 24 (** * More Length-Indexed Lists *)
25 25
26 (** We begin with a deeper look at the length-indexed lists that began the last chapter. *) 26 (** We begin with a deeper look at the length-indexed lists that began the last chapter.%\index{Gallina terms!ilist}% *)
27 27
28 Section ilist. 28 Section ilist.
29 Variable A : Set. 29 Variable A : Set.
30 30
31 Inductive ilist : nat -> Set := 31 Inductive ilist : nat -> Set :=
32 | Nil : ilist O 32 | Nil : ilist O
33 | Cons : forall n, A -> ilist n -> ilist (S n). 33 | Cons : forall n, A -> ilist n -> ilist (S n).
34 34
35 (** We might like to have a certified function for selecting an element of an [ilist] by position. We could do this using subset types and explicit manipulation of proofs, but dependent types let us do it more directly. It is helpful to define a type family [fin], where [fin n] is isomorphic to [{m : nat | m < n}]. The type family name stands for %``%#"#finite.#"#%''% *) 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{Gallina terms!fin}%[fin], where [fin n] is isomorphic to [{m : nat | m < n}]. The type family name stands for %``%#"#finite.#"#%''% *)
36 36
37 (* EX: Define a function [get] for extracting an [ilist] element by position. *) 37 (* EX: Define a function [get] for extracting an [ilist] element by position. *)
38 38
39 (* begin thide *) 39 (* begin thide *)
40 Inductive fin : nat -> Set := 40 Inductive fin : nat -> Set :=
41 | First : forall n, fin (S n) 41 | First : forall n, fin (S n)
42 | Next : forall n, fin n -> fin (S n). 42 | Next : forall n, fin n -> fin (S n).
43 43
44 (** [fin] essentially makes a more richly-typed copy of the natural numbers. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))]. 44 (** An instance of [fin] is essentially a more richly typed copy of the natural numbers. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected. For instance, the three values of type [fin 3] are [First 2], [Next (][First 1)], and [Next (][Next (][First 0))].
45 45
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. 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.
47 47
48 [[ 48 [[
49 Fixpoint get n (ls : ilist n) : fin n -> A := 49 Fixpoint get n (ls : ilist n) : fin n -> A :=
124 end. 124 end.
125 (* end thide *) 125 (* end thide *)
126 End ilist. 126 End ilist.
127 127
128 Implicit Arguments Nil [A]. 128 Implicit Arguments Nil [A].
129 (* begin thide *)
130 Implicit Arguments First [n]. 129 Implicit Arguments First [n].
131 (* end thide *)
132 130
133 (** A few examples show how to make use of these definitions. *) 131 (** A few examples show how to make use of these definitions. *)
134 132
135 Check Cons 0 (Cons 1 (Cons 2 Nil)). 133 Check Cons 0 (Cons 1 (Cons 2 Nil)).
136 (** %\vspace{-.15in}% [[ 134 (** %\vspace{-.15in}% [[
174 | Cons _ x ls' => Cons (f x) (imap ls') 172 | Cons _ x ls' => Cons (f x) (imap ls')
175 end. 173 end.
176 174
177 (** It is easy to prove that [get] %``%#"#distributes over#"#%''% [imap] calls. The only tricky bit is remembering to use our [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *) 175 (** It is easy to prove that [get] %``%#"#distributes over#"#%''% [imap] calls. The only tricky bit is remembering to use our [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *)
178 176
177 (* EX: Prove that [get] distributes over [imap]. *)
178
179 (* begin thide *)
179 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n), 180 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n),
180 get (imap ls) idx = f (get ls idx). 181 get (imap ls) idx = f (get ls idx).
181 (* begin thide *)
182 induction ls; dep_destruct idx; crush. 182 induction ls; dep_destruct idx; crush.
183 Qed. 183 Qed.
184 (* end thide *) 184 (* end thide *)
185 End ilist_map. 185 End ilist_map.
186 186
187 187
188 (** * Heterogeneous Lists *) 188 (** * Heterogeneous Lists *)
189 189
190 (** 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. *) 190 (** 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. *)
191 191
192 Section hlist. 192 Section hlist.
193 Variable A : Type. 193 Variable A : Type.
194 Variable B : A -> Type. 194 Variable B : A -> Type.
195 195
196 (* 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. *) 196 (* 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. *)
197 197
198 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *) 198 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B].%\index{Gallina terms!hlist}% *)
199 199
200 (* begin thide *) 200 (* begin thide *)
201 Inductive hlist : list A -> Type := 201 Inductive hlist : list A -> Type :=
202 | MNil : hlist nil 202 | MNil : hlist nil
203 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). 203 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
204 204
205 (** 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. *) 205 (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to.%\index{Gallina terms!member}% *)
206 206
207 (* end thide *) 207 (* end thide *)
208 (* EX: Define an analogue to [get] for [hlist]s. *) 208 (* EX: Define an analogue to [get] for [hlist]s. *)
209 209
210 (* begin thide *) 210 (* begin thide *)
214 | MFirst : forall ls, member (elm :: ls) 214 | MFirst : forall ls, member (elm :: ls)
215 | MNext : forall x ls, member ls -> member (x :: ls). 215 | MNext : forall x ls, member ls -> member (x :: ls).
216 216
217 (** 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. 217 (** 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.
218 218
219 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. *) 219 We can use [member] to adapt our definition of [get] to [hlist]s. The same basic [match] tricks apply. In the [MCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match]. We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
220 220
221 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm := 221 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
222 match mls with 222 match mls with
223 | MNil => fun mem => 223 | MNil => fun mem =>
224 match mem in member ls' return (match ls' with 224 match mem in member ls' return (match ls' with
280 (* end thide *) 280 (* end thide *)
281 281
282 282
283 (** ** A Lambda Calculus Interpreter *) 283 (** ** A Lambda Calculus Interpreter *)
284 284
285 (** 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. 285 (** Heterogeneous lists are very useful in implementing %\index{interpreters}%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%\index{lambda calculus}%. Our interpreter can alternatively be thought of as a denotational semantics.
286 286
287 We start with an algebraic datatype for types. *) 287 We start with an algebraic datatype for types. *)
288 288
289 Inductive type : Set := 289 Inductive type : Set :=
290 | Unit : type 290 | Unit : type
291 | Arrow : type -> type -> type. 291 | Arrow : type -> type -> type.
292 292
293 (** Now we can define a type family for expressions. An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts]. We effectively use the de Bruijn variable representation, which we will discuss in more detail in later chapters, including a case study in Chapter 16. Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *) 293 (** 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 index variable representation%~\cite{DeBruijn}%. 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. *)
294 294
295 Inductive exp : list type -> type -> Set := 295 Inductive exp : list type -> type -> Set :=
296 | Const : forall ts, exp ts Unit 296 | Const : forall ts, exp ts Unit
297 (* begin thide *) 297 (* begin thide *)
298 | Var : forall ts t, member t ts -> exp ts t 298 | Var : forall ts t, member t ts -> exp ts t
308 match t with 308 match t with
309 | Unit => unit 309 | Unit => unit
310 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 310 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
311 end. 311 end.
312 312
313 (** 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. *) 313 (** 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. *)
314 314
315 (* EX: Define an interpreter for [exp]s. *) 315 (* EX: Define an interpreter for [exp]s. *)
316 316
317 (* begin thide *) 317 (* begin thide *)
318 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t := 318 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
362 ]] 362 ]]
363 *) 363 *)
364 364
365 (* end thide *) 365 (* end thide *)
366 366
367 (** 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. *) 367 (** 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. Other, more common approaches to language formalization 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. *)
368 368
369 369
370 (** * Recursive Type Definitions *) 370 (** * Recursive Type Definitions *)
371 371
372 (** 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. *) 372 (** %\index{recursive type definition}%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. *)
373 373
374 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *) 374 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
375 375
376 Section filist. 376 Section filist.
377 Variable A : Set. 377 Variable A : Set.
389 match n with 389 match n with
390 | O => Empty_set 390 | O => Empty_set
391 | S n' => option (ffin n') 391 | S n' => option (ffin n')
392 end. 392 end.
393 393
394 (** We express that there are no index values when [n = O], by defining such indices as type [Empty_set]; and we express that, at [n = S n'], there is a choice between picking the first element of the list (represented as [None]) or choosing a later element (represented by [Some idx], where [idx] is an index into the list tail). For instance, the three values of type [ffin 3] are [None], [Some None], and [Some (Some None)]. *) 394 (** We express that there are no index values when [n = O], by defining such indices as type [Empty_set]; and we express that, at [n = S n'], there is a choice between picking the first element of the list (represented as [None]) or choosing a later element (represented by [Some idx], where [idx] is an index into the list tail). For instance, the three values of type [ffin 3] are [None], [Some None], and [Some (][Some None)]. *)
395 395
396 Fixpoint fget (n : nat) : filist n -> ffin n -> A := 396 Fixpoint fget (n : nat) : filist n -> ffin n -> A :=
397 match n with 397 match n with
398 | O => fun _ idx => match idx with end 398 | O => fun _ idx => match idx with end
399 | S n' => fun ls idx => 399 | S n' => fun ls idx =>
421 match ls with 421 match ls with
422 | nil => unit 422 | nil => unit
423 | x :: ls' => B x * fhlist ls' 423 | x :: ls' => B x * fhlist ls'
424 end%type. 424 end%type.
425 425
426 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently-typed data elements. *) 426 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently typed data elements. *)
427 427
428 Variable elm : A. 428 Variable elm : A.
429 429
430 Fixpoint fmember (ls : list A) : Type := 430 Fixpoint fmember (ls : list A) : Type :=
431 match ls with 431 match ls with
480 Implicit Arguments fhget [A B elm ls]. 480 Implicit Arguments fhget [A B elm ls].
481 481
482 482
483 (** * Data Structures as Index Functions *) 483 (** * Data Structures as Index Functions *)
484 484
485 (** 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. *) 485 (** %\index{index function}%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. *)
486 486
487 Section tree. 487 Section tree.
488 Variable A : Set. 488 Variable A : Set.
489 489
490 Inductive tree : Set := 490 Inductive tree : Set :=
530 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >= 530 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
531 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i 531 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
532 532
533 ]] 533 ]]
534 534
535 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. *) 535 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 %\index{nested inductive type}%nested inductive types. *)
536 536
537 Check tree_ind. 537 Check tree_ind.
538 (** %\vspace{-.15in}% [[ 538 (** %\vspace{-.15in}% [[
539 tree_ind 539 tree_ind
540 : forall (A : Set) (P : tree A -> Prop), 540 : forall (A : Set) (P : tree A -> Prop),
542 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) -> 542 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
543 forall t : tree A, P t 543 forall t : tree A, P t
544 544
545 ]] 545 ]]
546 546
547 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]. *) 547 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]. *)
548 548
549 Abort. 549 Abort.
550 550
551 Reset tree. 551 Reset tree.
552 552
557 557
558 (** %\vspace{-.15in}% [[ 558 (** %\vspace{-.15in}% [[
559 Inductive tree : Set := 559 Inductive tree : Set :=
560 | Leaf : A -> tree 560 | Leaf : A -> tree
561 | Node : forall n, filist tree n -> tree. 561 | Node : forall n, filist tree n -> tree.
562 562 ]]
563
564 <<
563 Error: Non strictly positive occurrence of "tree" in 565 Error: Non strictly positive occurrence of "tree" in
564 "forall n : nat, filist tree n -> tree" 566 "forall n : nat, filist tree n -> tree"
565 567 >>
566 ]] 568
567 569 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.
568 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. 570
569 571 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, %\index{reflexive inductive type}%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]. *)
570 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]. *)
571 572
572 Inductive tree : Set := 573 Inductive tree : Set :=
573 | Leaf : A -> tree 574 | Leaf : A -> tree
574 | Node : forall n, (ffin n -> tree) -> tree. 575 | Node : forall n, (ffin n -> tree) -> tree.
575 576
634 635
635 (** 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. *) 636 (** 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. *)
636 637
637 (** ** Another Interpreter Example *) 638 (** ** Another Interpreter Example *)
638 639
639 (** 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. *) 640 (** 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 %\index{interpreters}%interpreter we will write, we force each conditional to include a final, default case. *)
640 641
641 Inductive type' : Type := Nat | Bool. 642 Inductive type' : Type := Nat | Bool.
642 643
643 Inductive exp' : type' -> Type := 644 Inductive exp' : type' -> Type :=
644 | NConst : nat -> exp' Nat 645 | NConst : nat -> exp' Nat
792 (fun idx => cfold (bodies idx)) 793 (fun idx => cfold (bodies idx))
793 (* end thide *) 794 (* end thide *)
794 end. 795 end.
795 796
796 (* begin thide *) 797 (* begin thide *)
797 (** 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 instantiation of the quantifiers in the induction hypothesis. *) 798 (** 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 instantiation of the quantifiers in the induction hypothesis. *)
798 799
799 Lemma cfoldCond_correct : forall t (default : exp' t) 800 Lemma cfoldCond_correct : forall t (default : exp' t)
800 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t), 801 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
801 exp'Denote (cfoldCond default tests bodies) 802 exp'Denote (cfoldCond default tests bodies)
802 = exp'Denote (Cond n tests bodies default). 803 = exp'Denote (Cond n tests bodies default).
852 853
853 (** 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. 854 (** 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.
854 855
855 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. 856 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.
856 857
857 Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation. For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types. Consider a call [get l f], where variable [l] has type [filist A (S n)]. The type of [l] would be simplified to an explicit pair type. In a proof involving many recursive types, this kind of unhelpful %``%#"#simplification#"#%''% can lead to rapid bloat in the sizes of subgoals. Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the %``%#"#simplified#"#%''% version. 858 Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation. For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types. Consider a call [get l f], where variable [l] has type [filist A (][S n)]. The type of [l] would be simplified to an explicit pair type. In a proof involving many recursive types, this kind of unhelpful %``%#"#simplification#"#%''% can lead to rapid bloat in the sizes of subgoals. Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the %``%#"#simplified#"#%''% version. The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may %``%#"#simplify#"#%''% when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value.
858 859
859 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. 860 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.
860 861
861 Reflexive encodings of data types are seen relatively rarely. As our examples demonstrated, manipulating index values manually can lead to hard-to-read code. A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3. For small developments, avoiding that kind of coding can justify the use of reflexive data structures. There are also some useful instances of co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *) 862 Finally, Coq type inference can be more helpful in constructing values in inductive types. Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type. This downside can be mitigated to an extent by writing %``%#"#constructor#"#%''% functions for a recursive type, mirroring the definition of the corresponding inductive type.
863
864 Reflexive encodings of data types are seen relatively rarely. As our examples demonstrated, manipulating index values manually can lead to hard-to-read code. A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3. For small developments, avoiding that kind of coding can justify the use of reflexive data structures. There are also some useful instances of %\index{co-inductive types}%co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *)
862 865
863 866
864 (** * Exercises *) 867 (** * Exercises *)
865 868
866 (** remove printing * *) 869 (** remove printing * *)
871 874
872 %\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. 875 %\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.
873 876
874 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># 877 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>#
875 878
876 %\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: 879 %\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:
877
878 [[ 880 [[
879 t ::= bool | t + t 881 t ::= bool | t + t
880 p ::= x | b | inl p | inr p 882 p ::= x | b | inl p | inr p
881 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e 883 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e
882 884 ]]
883 ]] 885
884 886 The non-terminal [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.
885 [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.
886 887
887 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># 888 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>#
888 889
889 #</ol>#%\end{enumerate}% *) 890 #</ol>#%\end{enumerate}% *)