Mercurial > cpdt > repo
comparison src/MoreDep.v @ 85:3746a2ded8da
Tagless interpreter & cfold
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 06 Oct 2008 13:07:24 -0400 |
parents | 522436ed6688 |
children | fd505bcb5632 |
comparison
equal
deleted
inserted
replaced
84:522436ed6688 | 85:3746a2ded8da |
---|---|
6 * The license text is available at: | 6 * The license text is available at: |
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ | 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ |
8 *) | 8 *) |
9 | 9 |
10 (* begin hide *) | 10 (* begin hide *) |
11 Require Import List. | 11 Require Import Arith Bool List. |
12 | 12 |
13 Require Import Tactics. | 13 Require Import Tactics. |
14 | 14 |
15 Set Implicit Arguments. | 15 Set Implicit Arguments. |
16 (* end hide *) | 16 (* end hide *) |
132 Definition hd n (ls : ilist (S n)) : A := hd' ls. | 132 Definition hd n (ls : ilist (S n)) : A := hd' ls. |
133 | 133 |
134 (** We annotate our main [match] with a type that is itself a [match]. We write that the function [hd'] returns [unit] when the list is empty and returns the carried type [A] in all other cases. In the definition of [hd], we just call [hd']. Because the index of [ls] is known to be nonzero, the type checker reduces the [match] in the type of [hd'] to [A]. *) | 134 (** We annotate our main [match] with a type that is itself a [match]. We write that the function [hd'] returns [unit] when the list is empty and returns the carried type [A] in all other cases. In the definition of [hd], we just call [hd']. Because the index of [ls] is known to be nonzero, the type checker reduces the [match] in the type of [hd'] to [A]. *) |
135 | 135 |
136 End ilist. | 136 End ilist. |
137 | |
138 | |
139 (** * A Tagless Interpreter *) | |
140 | |
141 (** A favorite example for motivating the power of functional programming is implementation of a simple expression language interpreter. In ML and Haskell, such interpreters are often implemented using an algebraic datatype of values, where at many points it is checked that a value was built with the right constructor of the value type. With dependent types, we can implement a %\textit{%#<i>#tagless#</i>#%}% interpreter that both removes this source of runtime ineffiency and gives us more confidence that our implementation is correct. *) | |
142 | |
143 Inductive type : Set := | |
144 | Nat : type | |
145 | Bool : type | |
146 | Prod : type -> type -> type. | |
147 | |
148 Inductive exp : type -> Set := | |
149 | NConst : nat -> exp Nat | |
150 | Plus : exp Nat -> exp Nat -> exp Nat | |
151 | Eq : exp Nat -> exp Nat -> exp Bool | |
152 | |
153 | BConst : bool -> exp Bool | |
154 | And : exp Bool -> exp Bool -> exp Bool | |
155 | If : forall t, exp Bool -> exp t -> exp t -> exp t | |
156 | |
157 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2) | |
158 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1 | |
159 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2. | |
160 | |
161 (** We have a standard algebraic datatype [type], defining a type language of naturals, booleans, and product (pair) types. Then we have the indexed inductive type [exp], where the argument to [exp] tells us the encoded type of an expression. In effect, we are defining the typing rules for expressions simultaneously with the syntax. | |
162 | |
163 We can give types and expressions semantics in a new style, based critically on the chance for %\textit{%#<i>#type-level computation#</i>#%}%. *) | |
164 | |
165 Fixpoint typeDenote (t : type) : Set := | |
166 match t with | |
167 | Nat => nat | |
168 | Bool => bool | |
169 | Prod t1 t2 => typeDenote t1 * typeDenote t2 | |
170 end%type. | |
171 | |
172 (** [typeDenote] compiles types of our object language into "native" Coq types. It is deceptively easy to implement. The only new thing we see is the [%type] annotation, which tells Coq to parse the [match] expression using the notations associated with types. Without this annotation, the [*] would be interpreted as multiplication on naturals, rather than as the product type constructor. [type] is one example of an identifer bound to a %\textit{%#<i>#notation scope#</i>#%}%. We will deal more explicitly with notations and notation scopes in later chapters. | |
173 | |
174 We can define a function [expDenote] that is typed in terms of [typeDenote]. *) | |
175 | |
176 Fixpoint expDenote t (e : exp t) {struct e} : typeDenote t := | |
177 match e in (exp t) return (typeDenote t) with | |
178 | NConst n => n | |
179 | Plus e1 e2 => expDenote e1 + expDenote e2 | |
180 | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false | |
181 | |
182 | BConst b => b | |
183 | And e1 e2 => expDenote e1 && expDenote e2 | |
184 | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2 | |
185 | |
186 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) | |
187 | Fst _ _ e' => fst (expDenote e') | |
188 | Snd _ _ e' => snd (expDenote e') | |
189 end. | |
190 | |
191 (** Again we find that an [in] annotation is essential for type-checking a function. Besides that, the definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns. | |
192 | |
193 We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error. | |
194 | |
195 [[ | |
196 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) := | |
197 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with | |
198 | Pair _ _ e1 e2 => Some (e1, e2) | |
199 | _ => None | |
200 end. | |
201 | |
202 [[ | |
203 Error: The reference t2 was not found in the current environment | |
204 ]] | |
205 | |
206 We run again into the problem of not being able to specify non-variable arguments in [in] clauses. The problem would just be hopeless without a use of an [in] clause, though, since the result type of the [match] depends on an argument to [exp]. Our solution will be to use a more general type, as we did for [hd]. First, we define a type-valued function to use in assigning a type to [pairOut]. *) | |
207 | |
208 Definition pairOutType (t : type) := | |
209 match t with | |
210 | Prod t1 t2 => option (exp t1 * exp t2) | |
211 | _ => unit | |
212 end. | |
213 | |
214 (** When passed a type that is a product, [pairOutType] returns our final desired type. On any other input type, [pairOutType] returns [unit], since we do not care about extracting components of non-pairs. Now we can write another helper function to provide the default behavior of [pairOut], which we will apply for inputs that are not literal pairs. *) | |
215 | |
216 Definition pairOutDefault (t : type) := | |
217 match t return (pairOutType t) with | |
218 | Prod _ _ => None | |
219 | _ => tt | |
220 end. | |
221 | |
222 (** Now [pairOut] is deceptively easy to write. *) | |
223 | |
224 Definition pairOut t (e : exp t) := | |
225 match e in (exp t) return (pairOutType t) with | |
226 | Pair _ _ e1 e2 => Some (e1, e2) | |
227 | _ => pairOutDefault _ | |
228 end. | |
229 | |
230 (** There is one important subtlety in this definition. Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time. Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case. From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages, but is similar to what goes on with Haskell type classes. | |
231 | |
232 With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. *) | |
233 | |
234 Fixpoint cfold t (e : exp t) {struct e} : exp t := | |
235 match e in (exp t) return (exp t) with | |
236 | NConst n => NConst n | |
237 | Plus e1 e2 => | |
238 let e1' := cfold e1 in | |
239 let e2' := cfold e2 in | |
240 match e1', e2' with | |
241 | NConst n1, NConst n2 => NConst (n1 + n2) | |
242 | _, _ => Plus e1' e2' | |
243 end | |
244 | Eq e1 e2 => | |
245 let e1' := cfold e1 in | |
246 let e2' := cfold e2 in | |
247 match e1', e2' with | |
248 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false) | |
249 | _, _ => Eq e1' e2' | |
250 end | |
251 | |
252 | BConst b => BConst b | |
253 | And e1 e2 => | |
254 let e1' := cfold e1 in | |
255 let e2' := cfold e2 in | |
256 match e1', e2' with | |
257 | BConst b1, BConst b2 => BConst (b1 && b2) | |
258 | _, _ => And e1' e2' | |
259 end | |
260 | If _ e e1 e2 => | |
261 let e' := cfold e in | |
262 match e' with | |
263 | BConst true => cfold e1 | |
264 | BConst false => cfold e2 | |
265 | _ => If e' (cfold e1) (cfold e2) | |
266 end | |
267 | |
268 | Pair _ _ e1 e2 => Pair (cfold e1) (cfold e2) | |
269 | Fst _ _ e => | |
270 let e' := cfold e in | |
271 match pairOut e' with | |
272 | Some p => fst p | |
273 | None => Fst e' | |
274 end | |
275 | Snd _ _ e => | |
276 let e' := cfold e in | |
277 match pairOut e' with | |
278 | Some p => snd p | |
279 | None => Snd e' | |
280 end | |
281 end. | |
282 | |
283 (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *) | |
284 | |
285 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e). | |
286 induction e; crush. | |
287 | |
288 (** The first remaining subgoal is: | |
289 | |
290 [[ | |
291 | |
292 expDenote (cfold e1) + expDenote (cfold e2) = | |
293 expDenote | |
294 match cfold e1 with | |
295 | NConst n1 => | |
296 match cfold e2 with | |
297 | NConst n2 => NConst (n1 + n2) | |
298 | Plus _ _ => Plus (cfold e1) (cfold e2) | |
299 | Eq _ _ => Plus (cfold e1) (cfold e2) | |
300 | BConst _ => Plus (cfold e1) (cfold e2) | |
301 | And _ _ => Plus (cfold e1) (cfold e2) | |
302 | If _ _ _ _ => Plus (cfold e1) (cfold e2) | |
303 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2) | |
304 | Fst _ _ _ => Plus (cfold e1) (cfold e2) | |
305 | Snd _ _ _ => Plus (cfold e1) (cfold e2) | |
306 end | |
307 | Plus _ _ => Plus (cfold e1) (cfold e2) | |
308 | Eq _ _ => Plus (cfold e1) (cfold e2) | |
309 | BConst _ => Plus (cfold e1) (cfold e2) | |
310 | And _ _ => Plus (cfold e1) (cfold e2) | |
311 | If _ _ _ _ => Plus (cfold e1) (cfold e2) | |
312 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2) | |
313 | Fst _ _ _ => Plus (cfold e1) (cfold e2) | |
314 | Snd _ _ _ => Plus (cfold e1) (cfold e2) | |
315 end | |
316 ]] | |
317 | |
318 We would like to do a case analysis on [cfold e1], and we attempt that in the way that has worked so far. | |
319 | |
320 [[ | |
321 destruct (cfold e1). | |
322 | |
323 [[ | |
324 User error: e1 is used in hypothesis e | |
325 ]] | |
326 | |
327 Coq gives us another cryptic error message. Like so many others, this one basically means that Coq is not able to build some proof about dependent types. It is hard to generate helpful and specific error messages for problems like this, since that would require some kind of understanding of the dependency structure of a piece of code. We will encounter many examples of case-specific tricks for recovering from errors like this one. | |
328 | |
329 For our current proof, we can use a tactic [dep_destruct] defined in the book [Tactics] module. General elimination/inversion of dependently-typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed. [dep_destruct] makes a best effort to handle some common cases. In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dep_destruct]'s implementation in Ltac, but for now, we treat it as a useful black box. *) | |
330 | |
331 dep_destruct (cfold e1). | |
332 | |
333 (** This successfully breaks the subgoal into 5 new subgoals, one for each constructor of [exp] that could produce an [exp Nat]. Note that [dep_destruct] is successful in ruling out the other cases automatically, in effect automating some of the work that we have done manually in implementing functions like [hd] and [pairOut]. | |
334 | |
335 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof. *) | |
336 | |
337 Restart. | |
338 | |
339 induction e; crush; | |
340 repeat (match goal with | |
341 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) | |
342 | [ |- (if ?E then _ else _) = _ ] => destruct E | |
343 end; crush). | |
344 Qed. |