Mercurial > cpdt > repo

comparison src/DataStruct.v @ 106:1d2746eae1a6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Commentary on ilist get
author Adam Chlipala <adamc@hcoop.net>
date Mon, 13 Oct 2008 11:59:20 -0400
parents ec0fb0f00f46
children 924d77a177e8
comparison
equal deleted inserted replaced
105:ec0fb0f00f46 106:1d2746eae1a6
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\chapter{Dependent Data Structures}% *) 19 (** %\chapter{Dependent Data Structures}% *)
20 20
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 known-length and heterogeneous lists prop 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 Known-Length Lists *) 24 (** * More Length-Indexed Lists *)
25
26 (** We begin with a deeper look at the length-indexed lists that began the last chapter. *)
25 27
26 Section ilist. 28 Section ilist.
27 Variable A : Set. 29 Variable A : Set.
28 30
29 Inductive ilist : nat -> Set := 31 Inductive ilist : nat -> Set :=
30 | Nil : ilist O 32 | Nil : ilist O
31 | Cons : forall n, A -> ilist n -> ilist (S n). 33 | Cons : forall n, A -> ilist n -> ilist (S n).
32 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 [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." *)
36
33 Inductive index : nat -> Set := 37 Inductive index : nat -> Set :=
34 | First : forall n, index (S n) 38 | First : forall n, index (S n)
35 | Next : forall n, index n -> index (S n). 39 | Next : forall n, index n -> index (S n).
40
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.
42
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.
44
45 [[
46 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
47 match ls in ilist n return index n -> A with
48 | Nil => fun idx => ?
49 | Cons _ x ls' => fun idx =>
50 match idx with
51 | First _ => x
52 | Next _ idx' => get ls' idx'
53 end
54 end.
55
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].
57
58 [[
59 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
60 match ls in ilist n return index n -> A with
61 | Nil => fun idx =>
62 match idx in index n' return (match n' with
63 | O => A
64 | S _ => unit
65 end) with
66 | First _ => tt
67 | Next _ _ => tt
68 end
69 | Cons _ x ls' => fun idx =>
70 match idx with
71 | First _ => x
72 | Next _ idx' => get ls' idx'
73 end
74 end.
75
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.
77
78 [[
79 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
80 match ls in ilist n return index n -> A with
81 | Nil => fun idx =>
82 match idx in index n' return (match n' with
83 | O => A
84 | S _ => unit
85 end) with
86 | First _ => tt
87 | Next _ _ => tt
88 end
89 | Cons _ x ls' => fun idx =>
90 match idx in index n' return ilist (pred n') -> A with
91 | First _ => fun _ => x
92 | Next _ idx' => fun ls' => get ls' idx'
93 end ls'
94 end.
95
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. *)
36 97
37 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A := 98 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
38 match ls in ilist n return index n -> A with 99 match ls in ilist n return index n -> A with
39 | Nil => fun idx => 100 | Nil => fun idx =>
40 match idx in index n' return (match n' with 101 match idx in index n' return (match n' with