|
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@105
|
117
|
|
adamc@107
|
118 (** Our [get] function is quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *)
|
|
adamc@107
|
119
|
|
adamc@105
|
120 Section ilist_map.
|
|
adamc@105
|
121 Variables A B : Set.
|
|
adamc@105
|
122 Variable f : A -> B.
|
|
adamc@105
|
123
|
|
adamc@105
|
124 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
|
|
adamc@105
|
125 match ls in ilist _ n return ilist B n with
|
|
adamc@105
|
126 | Nil => Nil
|
|
adamc@105
|
127 | Cons _ x ls' => Cons (f x) (imap ls')
|
|
adamc@105
|
128 end.
|
|
adamc@105
|
129
|
|
adamc@107
|
130 (** 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
|
131
|
|
adamc@107
|
132 Theorem get_imap : forall n (idx : index n) (ls : ilist A n),
|
|
adamc@105
|
133 get (imap ls) idx = f (get ls idx).
|
|
adamc@107
|
134 induction ls; dep_destruct idx; crush.
|
|
adamc@105
|
135 Qed.
|
|
adamc@105
|
136 End ilist_map.
|
|
adamc@107
|
137
|
|
adamc@107
|
138
|
|
adamc@107
|
139 (** * Heterogeneous Lists *)
|
|
adamc@107
|
140
|
|
adamc@107
|
141 (** 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
|
142
|
|
adamc@107
|
143 Section hlist.
|
|
adamc@107
|
144 Variable A : Type.
|
|
adamc@107
|
145 Variable B : A -> Type.
|
|
adamc@107
|
146
|
|
adamc@107
|
147 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
|
|
adamc@107
|
148
|
|
adamc@107
|
149 Inductive hlist : list A -> Type :=
|
|
adamc@107
|
150 | MNil : hlist nil
|
|
adamc@107
|
151 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
|
|
adamc@107
|
152
|
|
adamc@107
|
153 (** 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
|
154
|
|
adamc@107
|
155 Variable elm : A.
|
|
adamc@107
|
156
|
|
adamc@107
|
157 Inductive member : list A -> Type :=
|
|
adamc@107
|
158 | MFirst : forall ls, member (elm :: ls)
|
|
adamc@107
|
159 | MNext : forall x ls, member ls -> member (x :: ls).
|
|
adamc@107
|
160
|
|
adamc@107
|
161 (** 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
|
162
|
|
adamc@107
|
163 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
|
164
|
|
adamc@107
|
165 Fixpoint hget ls (mls : hlist ls) {struct mls} : member ls -> B elm :=
|
|
adamc@107
|
166 match mls in hlist ls return member ls -> B elm with
|
|
adamc@107
|
167 | MNil => fun mem =>
|
|
adamc@107
|
168 match mem in member ls' return (match ls' with
|
|
adamc@107
|
169 | nil => B elm
|
|
adamc@107
|
170 | _ :: _ => unit
|
|
adamc@107
|
171 end) with
|
|
adamc@107
|
172 | MFirst _ => tt
|
|
adamc@107
|
173 | MNext _ _ _ => tt
|
|
adamc@107
|
174 end
|
|
adamc@107
|
175 | MCons _ _ x mls' => fun mem =>
|
|
adamc@107
|
176 match mem in member ls' return (match ls' with
|
|
adamc@107
|
177 | nil => Empty_set
|
|
adamc@107
|
178 | x' :: ls'' =>
|
|
adamc@107
|
179 B x' -> (member ls'' -> B elm) -> B elm
|
|
adamc@107
|
180 end) with
|
|
adamc@107
|
181 | MFirst _ => fun x _ => x
|
|
adamc@107
|
182 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
|
|
adamc@107
|
183 end x (hget mls')
|
|
adamc@107
|
184 end.
|
|
adamc@107
|
185 End hlist.
|
