annotate src/DataStruct.v @ 107:924d77a177e8

hlist and hget
author Adam Chlipala <adamc@hcoop.net>
date Mon, 13 Oct 2008 12:35:48 -0400
parents 1d2746eae1a6
children 7abf5535baab
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@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.