## Mercurial > cpdt > repo

### comparison src/ProgLang.v @ 510:fd6ec9b2dccb

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Finished last pass through the book before beginning the MIT Press editorial process

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Wed, 13 Feb 2013 10:22:18 -0500 |

parents | 6252dd4540a9 |

children | ed829eaa91b2 |

comparison

equal
deleted
inserted
replaced

509:21079e42b773 | 510:fd6ec9b2dccb |
---|---|

297 termDenote (unlet e s) s1 | 297 termDenote (unlet e s) s1 |

298 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s). | 298 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s). |

299 induction e; pl. | 299 induction e; pl. |

300 Qed. | 300 Qed. |

301 | 301 |

302 (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions. It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect. We do that here for the simple case of terms with empty typing contexts. *) | 302 (** The lemma statement is a mouthful, with all its details of typing contexts and substitutions. It is usually prudent to state a final theorem in as simple a way as possible, to help your readers believe that you have proved what they expect. We follow that advice here for the simple case of terms with empty typing contexts. *) |

303 | 303 |

304 Theorem unletSound : forall t (e : term nil t), | 304 Theorem unletSound : forall t (e : term nil t), |

305 termDenote (unlet e HNil) HNil = termDenote e HNil. | 305 termDenote (unlet e HNil) HNil = termDenote e HNil. |

306 intros; apply unletSound'. | 306 intros; apply unletSound'. |

307 Qed. | 307 Qed. |

311 (** The [Let] removal optimization is a good case study of a simple transformation that may turn out to be much more work than expected, based on representation choices. In the second part of this chapter, we consider an alternate choice that produces a more pleasant experience. *) | 311 (** The [Let] removal optimization is a good case study of a simple transformation that may turn out to be much more work than expected, based on representation choices. In the second part of this chapter, we consider an alternate choice that produces a more pleasant experience. *) |

312 | 312 |

313 | 313 |

314 (** * Parametric Higher-Order Abstract Syntax *) | 314 (** * Parametric Higher-Order Abstract Syntax *) |

315 | 315 |

316 (** In contrast to first-order encodings,%\index{higher-order syntax}% _higher-order_ encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an%\index{object language}% _object language_ (the language being formalized) can be represented using the binding constructs of the%\index{meta language}% _meta language_ (the language in which the formalization is done). The best known higher-order encoding is called%\index{higher-order abstract syntax}\index{HOAS}% _higher-order abstract syntax_ (HOAS) %\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *) | 316 (** In contrast to first-order encodings,%\index{higher-order syntax}% _higher-order_ encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an%\index{object language}% _object language_ (the language being formalized) can be represented using the binding constructs of the%\index{meta language}% _meta language_ (the language in which the formalization is done). The best known higher-order encoding is called%\index{higher-order abstract syntax}% _higher-order abstract syntax_ (HOAS) %\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *) |

317 | 317 |

318 Module HigherOrder. | 318 Module HigherOrder. |

319 | 319 |

320 (** With HOAS, each object language binding construct is represented with a _function_ of the meta language. Here is what we get if we apply that idea within an inductive definition of term syntax. *) | 320 (** With HOAS, each object language binding construct is represented with a _function_ of the meta language. Here is what we get if we apply that idea within an inductive definition of term syntax. *) |

321 | 321 |

330 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2. | 330 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2. |

331 ]] | 331 ]] |

332 | 332 |

333 However, Coq rejects this definition for failing to meet the %\index{strict positivity requirement}%strict positivity restriction. For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining. Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic. | 333 However, Coq rejects this definition for failing to meet the %\index{strict positivity requirement}%strict positivity restriction. For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining. Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic. |

334 | 334 |

335 An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq. Here the idea is to parameterize the syntax type by a type family standing for a _representation of variables_. *) | 335 An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS|see{parametric higher-order abstract syntax}}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq. Here the idea is to parameterize the syntax type by a type family standing for a _representation of variables_. *) |

336 | 336 |

337 Section var. | 337 Section var. |

338 Variable var : type -> Type. | 338 Variable var : type -> Type. |

339 | 339 |

340 Inductive term : type -> Type := | 340 Inductive term : type -> Type := |

365 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))). | 365 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))). |

366 | 366 |

367 Example three_the_hard_way : Term Nat := fun var => | 367 Example three_the_hard_way : Term Nat := fun var => |

368 App (App (add var) (Const 1)) (Const 2). | 368 App (App (add var) (Const 1)) (Const 2). |

369 | 369 |

370 (** The argument [var] does not even appear in the function body for [add]. How can that be? By giving our terms expressive types, we allow Coq to infer many arguments for us. In fact, we do not even need to name the [var] argument! Even though these formal parameters appear as underscores, they _are_ mentioned in the function bodies that type inference calculates. *) | 370 (** The argument [var] does not even appear in the function body for [add]. How can that be? By giving our terms expressive types, we allow Coq to infer many arguments for us. In fact, we do not even need to name the [var] argument! *) |

371 | 371 |

372 Example add' : Term (Func Nat (Func Nat Nat)) := fun _ => | 372 Example add' : Term (Func Nat (Func Nat Nat)) := fun _ => |

373 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))). | 373 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))). |

374 | 374 |

375 Example three_the_hard_way' : Term Nat := fun _ => | 375 Example three_the_hard_way' : Term Nat := fun _ => |

376 App (App (add' _) (Const 1)) (Const 2). | 376 App (App (add' _) (Const 1)) (Const 2). |

377 | |

378 (** Even though the [var] formal parameters appear as underscores, they _are_ mentioned in the function bodies that type inference calculates. *) | |

377 | 379 |

378 | 380 |

379 (** ** Functional Programming with PHOAS *) | 381 (** ** Functional Programming with PHOAS *) |

380 | 382 |

381 (** It may not be at all obvious that the PHOAS representation admits the crucial computable operations. The key to effective deconstruction of PHOAS terms is one principle: treat the [var] parameter as an unconstrained choice of _which data should be annotated on each variable_. We will begin with a simple example, that of counting how many variable nodes appear in a PHOAS term. This operation requires no data annotated on variables, so we simply annotate variables with [unit] values. Note that, when we go under binders in the cases for [Abs] and [Let], we must provide the data value to annotate on the new variable we pass beneath. For our current choice of [unit] data, we always pass [tt]. *) | 383 (** It may not be at all obvious that the PHOAS representation admits the crucial computable operations. The key to effective deconstruction of PHOAS terms is one principle: treat the [var] parameter as an unconstrained choice of _which data should be annotated on each variable_. We will begin with a simple example, that of counting how many variable nodes appear in a PHOAS term. This operation requires no data annotated on variables, so we simply annotate variables with [unit] values. Note that, when we go under binders in the cases for [Abs] and [Let], we must provide the data value to annotate on the new variable we pass beneath. For our current choice of [unit] data, we always pass [tt]. *) |