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]. *)