Mercurial > cpdt > repo

annotate src/ProgLang.v @ 564:5504235ea06d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Link to RIT CSCI 740
author Adam Chlipala <adam@chlipala.net>
date Sun, 25 Mar 2018 13:03:34 -0400
parents dac7a2705b00
children 81d63d9c1cc5
rev   line source
adam@534 1 (* Copyright (c) 2011-2012, 2015, Adam Chlipala
adam@381 2 *
adam@381 3 * This work is licensed under a
adam@381 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adam@381 5 * Unported License.
adam@381 6 * The license text is available at:
adam@381 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adam@381 8 *)
adam@381 9
adam@381 10 (* begin hide *)
adam@381 11 Require Import FunctionalExtensionality List.
adam@381 12
adam@534 13 Require Import Cpdt.CpdtTactics Cpdt.DepList.
adam@381 14
adam@381 15 Set Implicit Arguments.
adam@534 16 Set Asymmetric Patterns.
adam@381 17 (* end hide *)
adam@381 18
adam@381 19 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *)
adam@381 20
adam@434 21 (** Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants. Before proving the first theorem of this kind, it is necessary to choose a formal encoding of the informal notions of syntax, dealing with such issues as %\index{variable binding}%variable binding conventions. I believe the pragmatic questions in this domain are far from settled and remain as important open research problems. However, in this chapter, I will demonstrate two underused encoding approaches. Note that I am not recommending either approach as a silver bullet! Mileage will vary across concrete problems, and I expect there to be significant future advances in our knowledge of encoding techniques. For a broader introduction to programming language formalization, using more elementary techniques, see %\emph{%{{http://www.cis.upenn.edu/~bcpierce/sf/}Software Foundations}%}% by Pierce et al.
adam@381 22
adam@381 23 This chapter is also meant as a case study, bringing together what we have learned in the previous chapters. We will see a concrete example of the importance of representation choices; translating mathematics from paper to Coq is not a deterministic process, and different creative choices can have big impacts. We will also see dependent types and scripted proof automation in action, applied to solve a particular problem as well as possible, rather than to demonstrate new Coq concepts.
adam@381 24
adam@381 25 I apologize in advance to those readers not familiar with the theory of programming language semantics. I will make a few remarks intended to relate the material here with common ideas in semantics, but these remarks should be safe for others to skip.
adam@381 26
adam@534 27 We will define a small programming language and reason about its semantics, expressed as an interpreter into Coq terms, much as we have done in examples throughout the book. It will be helpful to build a slight extension of [crush] that tries to apply %\index{functional extensionality}%functional extensionality, an axiom we met in Chapter 12, which says that two functions are equal if they map equal inputs to equal outputs. We also use [f_equal] to simplify goals of a particular form that will come up with the term denotation function that we define shortly. *)
adam@381 28
adam@381 29 Ltac ext := let x := fresh "x" in extensionality x.
adam@534 30 Ltac pl := crush; repeat (match goal with
adam@534 31 | [ |- (fun x => _) = (fun y => _) ] => ext
adam@534 32 | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal
adam@535 33 | [ |- ?E ::: _ = ?E ::: _ ] => f_equal
adam@535 34 | [ |- hmap _ ?E = hmap _ ?E ] => f_equal
adam@534 35 end; crush).
adam@381 36
adam@381 37 (** At this point in the book source, some auxiliary proofs also appear. *)
adam@381 38
adam@381 39 (* begin hide *)
adam@381 40 Section hmap.
adam@381 41 Variable A : Type.
adam@381 42 Variables B1 B2 B3 : A -> Type.
adam@381 43
adam@381 44 Variable f1 : forall x, B1 x -> B2 x.
adam@381 45 Variable f2 : forall x, B2 x -> B3 x.
adam@381 46
adam@381 47 Theorem hmap_hmap : forall ls (hl : hlist B1 ls), hmap f2 (hmap f1 hl) = hmap (fun i (x : B1 i) => f2 (f1 x)) hl.
adam@381 48 induction hl; crush.
adam@381 49 Qed.
adam@381 50 End hmap.
adam@381 51
adam@381 52 Section Forall.
adam@381 53 Variable A : Type.
adam@381 54 Variable P : A -> Prop.
adam@381 55
adam@381 56 Theorem Forall_In : forall ls, Forall P ls -> forall x, In x ls -> P x.
adam@381 57 induction 1; crush.
adam@381 58 Qed.
adam@381 59
adam@381 60 Theorem Forall_In' : forall ls, (forall x, In x ls -> P x) -> Forall P ls.
adam@381 61 induction ls; crush.
adam@381 62 Qed.
adam@381 63
adam@381 64 Variable P' : A -> Prop.
adam@381 65
adam@381 66 Theorem Forall_weaken : forall ls, Forall P ls
adam@381 67 -> (forall x, P x -> P' x)
adam@381 68 -> Forall P' ls.
adam@381 69 induction 1; crush.
adam@381 70 Qed.
adam@381 71 End Forall.
adam@381 72 (* end hide *)
adam@381 73
adam@381 74 (** Here is a definition of the type system we will use throughout the chapter. It is for simply typed lambda calculus with natural numbers as the base type. *)
adam@381 75
adam@381 76 Inductive type : Type :=
adam@381 77 | Nat : type
adam@381 78 | Func : type -> type -> type.
adam@381 79
adam@381 80 Fixpoint typeDenote (t : type) : Type :=
adam@381 81 match t with
adam@381 82 | Nat => nat
adam@381 83 | Func t1 t2 => typeDenote t1 -> typeDenote t2
adam@381 84 end.
adam@381 85
adam@381 86 (** Now we have some choices as to how we represent the syntax of programs. The two sections of the chapter explore two such choices, demonstrating the effect the choice has on proof complexity. *)
adam@381 87
adam@381 88
adam@381 89 (** * Dependent de Bruijn Indices *)
adam@381 90
adam@465 91 (** The first encoding is one we met first in Chapter 9, the _dependent de Bruijn index_ encoding. We represent program syntax terms in a type family parameterized by a list of types, representing the _typing context_, or information on which free variables are in scope and what their types are. Variables are represented in a way isomorphic to the natural numbers, where number 0 represents the first element in the context, number 1 the second element, and so on. Actually, instead of numbers, we use the [member] dependent type family from Chapter 9. *)
adam@381 92
adam@381 93 Module FirstOrder.
adam@381 94
adam@381 95 (** Here is the definition of the [term] type, including variables, constants, addition, function abstraction and application, and let binding of local variables. *)
adam@381 96
adam@381 97 Inductive term : list type -> type -> Type :=
adam@381 98 | Var : forall G t, member t G -> term G t
adam@381 99
adam@381 100 | Const : forall G, nat -> term G Nat
adam@381 101 | Plus : forall G, term G Nat -> term G Nat -> term G Nat
adam@381 102
adam@381 103 | Abs : forall G dom ran, term (dom :: G) ran -> term G (Func dom ran)
adam@381 104 | App : forall G dom ran, term G (Func dom ran) -> term G dom -> term G ran
adam@381 105
adam@381 106 | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2.
adam@381 107
adam@381 108 Implicit Arguments Const [G].
adam@381 109
adam@381 110 (** Here are two example term encodings, the first of addition packaged as a two-argument curried function, and the second of a sample application of addition to constants. *)
adam@381 111
adam@381 112 Example add : term nil (Func Nat (Func Nat Nat)) :=
adam@381 113 Abs (Abs (Plus (Var (HNext HFirst)) (Var HFirst))).
adam@381 114
adam@381 115 Example three_the_hard_way : term nil Nat :=
adam@381 116 App (App add (Const 1)) (Const 2).
adam@381 117
adam@381 118 (** Since dependent typing ensures that any term is well-formed in its context and has a particular type, it is easy to translate syntactic terms into Coq values. *)
adam@381 119
adam@381 120 Fixpoint termDenote G t (e : term G t) : hlist typeDenote G -> typeDenote t :=
adam@381 121 match e with
adam@381 122 | Var _ _ x => fun s => hget s x
adam@381 123
adam@381 124 | Const _ n => fun _ => n
adam@381 125 | Plus _ e1 e2 => fun s => termDenote e1 s + termDenote e2 s
adam@381 126
adam@381 127 | Abs _ _ _ e1 => fun s => fun x => termDenote e1 (x ::: s)
adam@381 128 | App _ _ _ e1 e2 => fun s => (termDenote e1 s) (termDenote e2 s)
adam@381 129
adam@381 130 | Let _ _ _ e1 e2 => fun s => termDenote e2 (termDenote e1 s ::: s)
adam@381 131 end.
adam@381 132
adam@398 133 (** With this term representation, some program transformations are easy to implement and prove correct. Certainly we would be worried if this were not the the case for the _identity_ transformation, which takes a term apart and reassembles it. *)
adam@381 134
adam@381 135 Fixpoint ident G t (e : term G t) : term G t :=
adam@381 136 match e with
adam@381 137 | Var _ _ x => Var x
adam@381 138
adam@381 139 | Const _ n => Const n
adam@381 140 | Plus _ e1 e2 => Plus (ident e1) (ident e2)
adam@381 141
adam@381 142 | Abs _ _ _ e1 => Abs (ident e1)
adam@381 143 | App _ _ _ e1 e2 => App (ident e1) (ident e2)
adam@381 144
adam@381 145 | Let _ _ _ e1 e2 => Let (ident e1) (ident e2)
adam@381 146 end.
adam@381 147
adam@381 148 Theorem identSound : forall G t (e : term G t) s,
adam@381 149 termDenote (ident e) s = termDenote e s.
adam@497 150 induction e; pl.
adam@381 151 Qed.
adam@381 152
adam@398 153 (** A slightly more ambitious transformation belongs to the family of _constant folding_ optimizations we have used as examples in other chapters. *)
adam@398 154
adam@381 155 Fixpoint cfold G t (e : term G t) : term G t :=
adam@381 156 match e with
adam@381 157 | Plus G e1 e2 =>
adam@381 158 let e1' := cfold e1 in
adam@381 159 let e2' := cfold e2 in
adam@398 160 let maybeOpt := match e1' return _ with
adam@398 161 | Const _ n1 =>
adam@398 162 match e2' return _ with
adam@398 163 | Const _ n2 => Some (Const (n1 + n2))
adam@398 164 | _ => None
adam@398 165 end
adam@398 166 | _ => None
adam@398 167 end in
adam@398 168 match maybeOpt with
adam@398 169 | None => Plus e1' e2'
adam@398 170 | Some e' => e'
adam@398 171 end
adam@381 172
adam@381 173 | Abs _ _ _ e1 => Abs (cfold e1)
adam@381 174 | App _ _ _ e1 e2 => App (cfold e1) (cfold e2)
adam@381 175
adam@381 176 | Let _ _ _ e1 e2 => Let (cfold e1) (cfold e2)
adam@381 177
adam@381 178 | e => e
adam@381 179 end.
adam@381 180
adam@381 181 (** The correctness proof is more complex, but only slightly so. *)
adam@381 182
adam@381 183 Theorem cfoldSound : forall G t (e : term G t) s,
adam@381 184 termDenote (cfold e) s = termDenote e s.
adam@497 185 induction e; pl;
adam@381 186 repeat (match goal with
adam@414 187 | [ |- context[match ?E with Var _ _ _ => _ | _ => _ end] ] =>
adam@414 188 dep_destruct E
adam@497 189 end; pl).
adam@381 190 Qed.
adam@381 191
adam@414 192 (** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms. The dependent de Bruijn representation is called%\index{first-order syntax}% _first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure.
adam@381 193
adam@434 194 As an example of a tricky transformation, consider one that removes all uses of "[let x = e1 in e2]" by substituting [e1] for [x] in [e2]. We will implement the translation by pairing the "compile-time" typing environment with a "run-time" value environment or _substitution_, mapping each variable to a value to be substituted for it. Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen. To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation. With dependent typing, lifting corresponds to weakening for typing judgments.
adam@381 195
adam@381 196 The fundamental goal of lifting is to add a new variable to a typing context, maintaining the validity of a term in the expanded context. To express the operation of adding a type to a context, we use a helper function [insertAt]. *)
adam@381 197
adam@381 198 Fixpoint insertAt (t : type) (G : list type) (n : nat) {struct n} : list type :=
adam@381 199 match n with
adam@381 200 | O => t :: G
adam@381 201 | S n' => match G with
adam@381 202 | nil => t :: G
adam@381 203 | t' :: G' => t' :: insertAt t G' n'
adam@381 204 end
adam@381 205 end.
adam@381 206
adam@381 207 (** Another function lifts bound variable instances, which we represent with [member] values. *)
adam@381 208
adam@381 209 Fixpoint liftVar t G (x : member t G) t' n : member t (insertAt t' G n) :=
adam@381 210 match x with
adam@381 211 | HFirst G' => match n return member t (insertAt t' (t :: G') n) with
adam@381 212 | O => HNext HFirst
adam@381 213 | _ => HFirst
adam@381 214 end
adam@381 215 | HNext t'' G' x' => match n return member t (insertAt t' (t'' :: G') n) with
adam@381 216 | O => HNext (HNext x')
adam@381 217 | S n' => HNext (liftVar x' t' n')
adam@381 218 end
adam@381 219 end.
adam@381 220
adam@381 221 (** The final helper function for lifting allows us to insert a new variable anywhere in a typing context. *)
adam@381 222
adam@381 223 Fixpoint lift' G t' n t (e : term G t) : term (insertAt t' G n) t :=
adam@381 224 match e with
adam@381 225 | Var _ _ x => Var (liftVar x t' n)
adam@381 226
adam@381 227 | Const _ n => Const n
adam@381 228 | Plus _ e1 e2 => Plus (lift' t' n e1) (lift' t' n e2)
adam@381 229
adam@381 230 | Abs _ _ _ e1 => Abs (lift' t' (S n) e1)
adam@381 231 | App _ _ _ e1 e2 => App (lift' t' n e1) (lift' t' n e2)
adam@381 232
adam@381 233 | Let _ _ _ e1 e2 => Let (lift' t' n e1) (lift' t' (S n) e2)
adam@381 234 end.
adam@381 235
adam@398 236 (** In the [Let] removal transformation, we only need to apply lifting to add a new variable at the _beginning_ of a typing context, so we package lifting into this final, simplified form. *)
adam@381 237
adam@381 238 Definition lift G t' t (e : term G t) : term (t' :: G) t :=
adam@381 239 lift' t' O e.
adam@381 240
adam@381 241 (** Finally, we can implement [Let] removal. The argument of type [hlist (term G') G] represents a substitution mapping each variable from context [G] into a term that is valid in context [G']. Note how the [Abs] case (1) extends via lifting the substitution [s] to hold in the broader context of the abstraction body [e1] and (2) maps the new first variable to itself. It is only the [Let] case that maps a variable to any substitute beside itself. *)
adam@381 242
adam@381 243 Fixpoint unlet G t (e : term G t) G' : hlist (term G') G -> term G' t :=
adam@381 244 match e with
adam@381 245 | Var _ _ x => fun s => hget s x
adam@381 246
adam@381 247 | Const _ n => fun _ => Const n
adam@381 248 | Plus _ e1 e2 => fun s => Plus (unlet e1 s) (unlet e2 s)
adam@381 249
adam@381 250 | Abs _ _ _ e1 => fun s => Abs (unlet e1 (Var HFirst ::: hmap (lift _) s))
adam@381 251 | App _ _ _ e1 e2 => fun s => App (unlet e1 s) (unlet e2 s)
adam@381 252
adam@381 253 | Let _ t1 _ e1 e2 => fun s => unlet e2 (unlet e1 s ::: s)
adam@381 254 end.
adam@381 255
adam@381 256 (** We have finished defining the transformation, but the parade of helper functions is not over. To prove correctness, we will use one more helper function and a few lemmas. First, we need an operation to insert a new value into a substitution at a particular position. *)
adam@381 257
adam@381 258 Fixpoint insertAtS (t : type) (x : typeDenote t) (G : list type) (n : nat) {struct n}
adam@381 259 : hlist typeDenote G -> hlist typeDenote (insertAt t G n) :=
adam@381 260 match n with
adam@381 261 | O => fun s => x ::: s
adam@381 262 | S n' => match G return hlist typeDenote G
adam@381 263 -> hlist typeDenote (insertAt t G (S n')) with
adam@381 264 | nil => fun s => x ::: s
adam@381 265 | t' :: G' => fun s => hhd s ::: insertAtS t x n' (htl s)
adam@381 266 end
adam@381 267 end.
adam@381 268
adam@381 269 Implicit Arguments insertAtS [t G].
adam@381 270
adam@381 271 (** Next we prove that [liftVar] is correct. That is, a lifted variable retains its value with respect to a substitution when we perform an analogue to lifting by inserting a new mapping into the substitution. *)
adam@381 272
adam@381 273 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n,
adam@381 274 hget s m = hget (insertAtS x n s) (liftVar m t' n).
adam@497 275 induction m; destruct n; dep_destruct s; pl.
adam@381 276 Qed.
adam@381 277
adam@381 278 Hint Resolve liftVarSound.
adam@381 279
adam@381 280 (** An analogous lemma establishes correctness of [lift']. *)
adam@381 281
adam@381 282 Lemma lift'Sound : forall G t' (x : typeDenote t') t (e : term G t) n s,
adam@381 283 termDenote e s = termDenote (lift' t' n e) (insertAtS x n s).
adam@497 284 induction e; pl;
adam@381 285 repeat match goal with
adam@381 286 | [ IH : forall n s, _ = termDenote (lift' _ n ?E) _
adam@381 287 |- context[lift' _ (S ?N) ?E] ] => specialize (IH (S N))
adam@497 288 end; pl.
adam@381 289 Qed.
adam@381 290
adam@381 291 (** Correctness of [lift] itself is an easy corollary. *)
adam@381 292
adam@381 293 Lemma liftSound : forall G t' (x : typeDenote t') t (e : term G t) s,
adam@381 294 termDenote (lift t' e) (x ::: s) = termDenote e s.
adam@381 295 unfold lift; intros; rewrite (lift'Sound _ x e O); trivial.
adam@381 296 Qed.
adam@381 297
adam@381 298 Hint Rewrite hget_hmap hmap_hmap liftSound.
adam@381 299
adam@381 300 (** Finally, we can prove correctness of [unletSound] for terms in arbitrary typing environments. *)
adam@381 301
adam@381 302 Lemma unletSound' : forall G t (e : term G t) G' (s : hlist (term G') G) s1,
adam@381 303 termDenote (unlet e s) s1
adam@381 304 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s).
adam@497 305 induction e; pl.
adam@381 306 Qed.
adam@381 307
adam@510 308 (** 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. *)
adam@381 309
adam@381 310 Theorem unletSound : forall t (e : term nil t),
adam@381 311 termDenote (unlet e HNil) HNil = termDenote e HNil.
adam@381 312 intros; apply unletSound'.
adam@381 313 Qed.
adam@381 314
adam@381 315 End FirstOrder.
adam@381 316
adam@381 317 (** 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. *)
adam@381 318
adam@381 319
adam@381 320 (** * Parametric Higher-Order Abstract Syntax *)
adam@381 321
adam@510 322 (** 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. *)
adam@381 323
adam@381 324 Module HigherOrder.
adam@381 325
adam@398 326 (** 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. *)
adam@381 327
adam@381 328 (** %\vspace{-.15in}%[[
adam@381 329 Inductive term : type -> Type :=
adam@381 330 | Const : nat -> term Nat
adam@381 331 | Plus : term Nat -> term Nat -> term Nat
adam@381 332
adam@381 333 | Abs : forall dom ran, (term dom -> term ran) -> term (Func dom ran)
adam@381 334 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
adam@381 335
adam@381 336 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2.
adam@381 337 ]]
adam@381 338
adam@464 339 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.
adam@381 340
adam@510 341 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_. *)
adam@381 342
adam@381 343 Section var.
adam@381 344 Variable var : type -> Type.
adam@381 345
adam@381 346 Inductive term : type -> Type :=
adam@381 347 | Var : forall t, var t -> term t
adam@381 348
adam@381 349 | Const : nat -> term Nat
adam@381 350 | Plus : term Nat -> term Nat -> term Nat
adam@381 351
adam@381 352 | Abs : forall dom ran, (var dom -> term ran) -> term (Func dom ran)
adam@381 353 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
adam@381 354
adam@381 355 | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2.
adam@381 356 End var.
adam@381 357
adam@381 358 Implicit Arguments Var [var t].
adam@381 359 Implicit Arguments Const [var].
adam@381 360 Implicit Arguments Abs [var dom ran].
adam@381 361
adam@398 362 (** Coq accepts this definition because our embedded functions now merely take _variables_ as arguments, instead of arbitrary terms. One might wonder whether there is an easy loophole to exploit here, instantiating the parameter [var] as [term] itself. However, to do that, we would need to choose a variable representation for this nested mention of [term], and so on through an infinite descent into [term] arguments.
adam@381 363
adam@381 364 We write the final type of a closed term using polymorphic quantification over all possible choices of [var] type family. *)
adam@381 365
adam@381 366 Definition Term t := forall var, term var t.
adam@381 367
adam@398 368 (** Here are the new representations of the example terms from the last section. Note how each is written as a function over a [var] choice, such that the specific choice has no impact on the _structure_ of the term. *)
adam@381 369
adam@381 370 Example add : Term (Func Nat (Func Nat Nat)) := fun var =>
adam@381 371 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))).
adam@381 372
adam@381 373 Example three_the_hard_way : Term Nat := fun var =>
adam@381 374 App (App (add var) (Const 1)) (Const 2).
adam@381 375
adam@510 376 (** 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! *)
adam@381 377
adam@381 378 Example add' : Term (Func Nat (Func Nat Nat)) := fun _ =>
adam@381 379 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))).
adam@381 380
adam@381 381 Example three_the_hard_way' : Term Nat := fun _ =>
adam@381 382 App (App (add' _) (Const 1)) (Const 2).
adam@381 383
adam@510 384 (** Even though the [var] formal parameters appear as underscores, they _are_ mentioned in the function bodies that type inference calculates. *)
adam@510 385
adam@381 386
adam@381 387 (** ** Functional Programming with PHOAS *)
adam@381 388
adam@398 389 (** 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]. *)
adam@381 390
adam@381 391 Fixpoint countVars t (e : term (fun _ => unit) t) : nat :=
adam@381 392 match e with
adam@381 393 | Var _ _ => 1
adam@381 394
adam@381 395 | Const _ => 0
adam@381 396 | Plus e1 e2 => countVars e1 + countVars e2
adam@381 397
adam@381 398 | Abs _ _ e1 => countVars (e1 tt)
adam@381 399 | App _ _ e1 e2 => countVars e1 + countVars e2
adam@381 400
adam@381 401 | Let _ _ e1 e2 => countVars e1 + countVars (e2 tt)
adam@381 402 end.
adam@381 403
adam@381 404 (** The above definition may seem a bit peculiar. What gave us the right to represent variables as [unit] values? Recall that our final representation of closed terms is as polymorphic functions. We merely specialize a closed term to exactly the right variable representation for the transformation we wish to perform. *)
adam@381 405
adam@381 406 Definition CountVars t (E : Term t) := countVars (E (fun _ => unit)).
adam@381 407
adam@381 408 (** It is easy to test that [CountVars] operates properly. *)
adam@381 409
adam@381 410 Eval compute in CountVars three_the_hard_way.
adam@381 411 (** %\vspace{-.15in}%[[
adam@381 412 = 2
adam@381 413 ]]
adam@381 414 *)
adam@381 415
adam@381 416 (** In fact, PHOAS can be used anywhere that first-order representations can. We will not go into all the details here, but the intuition is that it is possible to interconvert between PHOAS and any reasonable first-order representation. Here is a suggestive example, translating PHOAS terms into strings giving a first-order rendering. To implement this translation, the key insight is to tag variables with strings, giving their names. The function takes as an additional input a string giving the name to be assigned to the next variable introduced. We evolve this name by adding a prime to its end. To avoid getting bogged down in orthogonal details, we render all constants as the string ["N"]. *)
adam@381 417
adam@381 418 Require Import String.
adam@381 419 Open Scope string_scope.
adam@381 420
adam@381 421 Fixpoint pretty t (e : term (fun _ => string) t) (x : string) : string :=
adam@381 422 match e with
adam@381 423 | Var _ s => s
adam@381 424
adam@381 425 | Const _ => "N"
adam@381 426 | Plus e1 e2 => "(" ++ pretty e1 x ++ " + " ++ pretty e2 x ++ ")"
adam@381 427
adam@381 428 | Abs _ _ e1 => "(fun " ++ x ++ " => " ++ pretty (e1 x) (x ++ "'") ++ ")"
adam@381 429 | App _ _ e1 e2 => "(" ++ pretty e1 x ++ " " ++ pretty e2 x ++ ")"
adam@381 430
adam@381 431 | Let _ _ e1 e2 => "(let " ++ x ++ " = " ++ pretty e1 x ++ " in "
adam@381 432 ++ pretty (e2 x) (x ++ "'") ++ ")"
adam@381 433 end.
adam@381 434
adam@381 435 Definition Pretty t (E : Term t) := pretty (E (fun _ => string)) "x".
adam@381 436
adam@381 437 Eval compute in Pretty three_the_hard_way.
adam@381 438 (** %\vspace{-.15in}%[[
adam@381 439 = "(((fun x => (fun x' => (x + x'))) N) N)"
adam@381 440 ]]
adam@381 441 *)
adam@381 442
adam@497 443 (** However, it is not necessary to convert to first-order form to support many common operations on terms. For instance, we can implement substitution of terms for variables. The key insight here is to _tag variables with terms_, so that, on encountering a variable, we can simply replace it by the term in its tag. We will call this function initially on a term with exactly one free variable, tagged with the appropriate substitute. During recursion, new variables are added, but they are only tagged with their own term equivalents. Note that this function [squash] is parameterized over a specific [var] choice. *)
adam@381 444
adam@381 445 Fixpoint squash var t (e : term (term var) t) : term var t :=
adam@381 446 match e with
adam@381 447 | Var _ e1 => e1
adam@381 448
adam@381 449 | Const n => Const n
adam@381 450 | Plus e1 e2 => Plus (squash e1) (squash e2)
adam@381 451
adam@381 452 | Abs _ _ e1 => Abs (fun x => squash (e1 (Var x)))
adam@381 453 | App _ _ e1 e2 => App (squash e1) (squash e2)
adam@381 454
adam@381 455 | Let _ _ e1 e2 => Let (squash e1) (fun x => squash (e2 (Var x)))
adam@381 456 end.
adam@381 457
adam@381 458 (** To define the final substitution function over terms with single free variables, we define [Term1], an analogue to [Term] that we defined before for closed terms. *)
adam@381 459
adam@381 460 Definition Term1 (t1 t2 : type) := forall var, var t1 -> term var t2.
adam@381 461
adam@381 462 (** Substitution is defined by (1) instantiating a [Term1] to tag variables with terms and (2) applying the result to a specific term to be substituted. Note how the parameter [var] of [squash] is instantiated: the body of [Subst] is itself a polymorphic quantification over [var], standing for a variable tag choice in the output term; and we use that input to compute a tag choice for the input term. *)
adam@381 463
adam@381 464 Definition Subst (t1 t2 : type) (E : Term1 t1 t2) (E' : Term t1) : Term t2 :=
adam@381 465 fun var => squash (E (term var) (E' var)).
adam@381 466
adam@381 467 Eval compute in Subst (fun _ x => Plus (Var x) (Const 3)) three_the_hard_way.
adam@381 468 (** %\vspace{-.15in}%[[
adam@381 469 = fun var : type -> Type =>
adam@381 470 Plus
adam@381 471 (App
adam@381 472 (App
adam@381 473 (Abs
adam@381 474 (fun x : var Nat =>
adam@381 475 Abs (fun y : var Nat => Plus (Var x) (Var y))))
adam@381 476 (Const 1)) (Const 2)) (Const 3)
adam@381 477 ]]
adam@381 478
adam@398 479 One further development, which may seem surprising at first, is that we can also implement a usual term denotation function, when we _tag variables with their denotations_. *)
adam@381 480
adam@381 481 Fixpoint termDenote t (e : term typeDenote t) : typeDenote t :=
adam@381 482 match e with
adam@381 483 | Var _ v => v
adam@381 484
adam@381 485 | Const n => n
adam@381 486 | Plus e1 e2 => termDenote e1 + termDenote e2
adam@381 487
adam@381 488 | Abs _ _ e1 => fun x => termDenote (e1 x)
adam@381 489 | App _ _ e1 e2 => (termDenote e1) (termDenote e2)
adam@381 490
adam@381 491 | Let _ _ e1 e2 => termDenote (e2 (termDenote e1))
adam@381 492 end.
adam@381 493
adam@381 494 Definition TermDenote t (E : Term t) : typeDenote t :=
adam@381 495 termDenote (E typeDenote).
adam@381 496
adam@381 497 Eval compute in TermDenote three_the_hard_way.
adam@381 498 (** %\vspace{-.15in}%[[
adam@381 499 = 3
adam@381 500 ]]
adam@381 501
adam@381 502 To summarize, the PHOAS representation has all the expressive power of more standard first-order encodings, and a variety of translations are actually much more pleasant to implement than usual, thanks to the novel ability to tag variables with data. *)
adam@381 503
adam@381 504
adam@381 505 (** ** Verifying Program Transformations *)
adam@381 506
adam@381 507 (** Let us now revisit the three example program transformations from the last section. Each is easy to implement with PHOAS, and the last is substantially easier than with first-order representations.
adam@381 508
adam@381 509 First, we have the recursive identity function, following the same pattern as in the previous subsection, with a helper function, polymorphic in a tag choice; and a final function that instantiates the choice appropriately. *)
adam@381 510
adam@381 511 Fixpoint ident var t (e : term var t) : term var t :=
adam@381 512 match e with
adam@381 513 | Var _ x => Var x
adam@381 514
adam@381 515 | Const n => Const n
adam@381 516 | Plus e1 e2 => Plus (ident e1) (ident e2)
adam@381 517
adam@381 518 | Abs _ _ e1 => Abs (fun x => ident (e1 x))
adam@381 519 | App _ _ e1 e2 => App (ident e1) (ident e2)
adam@381 520
adam@381 521 | Let _ _ e1 e2 => Let (ident e1) (fun x => ident (e2 x))
adam@381 522 end.
adam@381 523
adam@381 524 Definition Ident t (E : Term t) : Term t := fun var =>
adam@381 525 ident (E var).
adam@381 526
adam@381 527 (** Proving correctness is both easier and harder than in the last section, easier because we do not need to manipulate substitutions, and harder because we do the induction in an extra lemma about [ident], to establish the correctness theorem for [Ident]. *)
adam@381 528
adam@381 529 Lemma identSound : forall t (e : term typeDenote t),
adam@381 530 termDenote (ident e) = termDenote e.
adam@497 531 induction e; pl.
adam@381 532 Qed.
adam@381 533
adam@381 534 Theorem IdentSound : forall t (E : Term t),
adam@381 535 TermDenote (Ident E) = TermDenote E.
adam@381 536 intros; apply identSound.
adam@381 537 Qed.
adam@381 538
adam@381 539 (** The translation of the constant-folding function and its proof work more or less the same way. *)
adam@381 540
adam@381 541 Fixpoint cfold var t (e : term var t) : term var t :=
adam@381 542 match e with
adam@381 543 | Plus e1 e2 =>
adam@381 544 let e1' := cfold e1 in
adam@381 545 let e2' := cfold e2 in
adam@381 546 match e1', e2' with
adam@381 547 | Const n1, Const n2 => Const (n1 + n2)
adam@381 548 | _, _ => Plus e1' e2'
adam@381 549 end
adam@381 550
adam@381 551 | Abs _ _ e1 => Abs (fun x => cfold (e1 x))
adam@381 552 | App _ _ e1 e2 => App (cfold e1) (cfold e2)
adam@381 553
adam@381 554 | Let _ _ e1 e2 => Let (cfold e1) (fun x => cfold (e2 x))
adam@381 555
adam@381 556 | e => e
adam@381 557 end.
adam@381 558
adam@381 559 Definition Cfold t (E : Term t) : Term t := fun var =>
adam@381 560 cfold (E var).
adam@381 561
adam@381 562 Lemma cfoldSound : forall t (e : term typeDenote t),
adam@381 563 termDenote (cfold e) = termDenote e.
adam@497 564 induction e; pl;
adam@381 565 repeat (match goal with
adam@414 566 | [ |- context[match ?E with Var _ _ => _ | _ => _ end] ] =>
adam@414 567 dep_destruct E
adam@497 568 end; pl).
adam@381 569 Qed.
adam@381 570
adam@381 571 Theorem CfoldSound : forall t (E : Term t),
adam@381 572 TermDenote (Cfold E) = TermDenote E.
adam@381 573 intros; apply cfoldSound.
adam@381 574 Qed.
adam@381 575
adam@381 576 (** Things get more interesting in the [Let]-removal optimization. Our recursive helper function adapts the key idea from our earlier definitions of [squash] and [Subst]: tag variables with terms. We have a straightforward generalization of [squash], where only the [Let] case has changed, to tag the new variable with the term it is bound to, rather than just tagging the variable with itself as a term. *)
adam@381 577
adam@381 578 Fixpoint unlet var t (e : term (term var) t) : term var t :=
adam@381 579 match e with
adam@381 580 | Var _ e1 => e1
adam@381 581
adam@381 582 | Const n => Const n
adam@381 583 | Plus e1 e2 => Plus (unlet e1) (unlet e2)
adam@381 584
adam@381 585 | Abs _ _ e1 => Abs (fun x => unlet (e1 (Var x)))
adam@381 586 | App _ _ e1 e2 => App (unlet e1) (unlet e2)
adam@381 587
adam@381 588 | Let _ _ e1 e2 => unlet (e2 (unlet e1))
adam@381 589 end.
adam@381 590
adam@381 591 Definition Unlet t (E : Term t) : Term t := fun var =>
adam@381 592 unlet (E (term var)).
adam@381 593
adam@381 594 (** We can test [Unlet] first on an uninteresting example, [three_the_hard_way], which does not use [Let]. *)
adam@381 595
adam@381 596 Eval compute in Unlet three_the_hard_way.
adam@381 597 (** %\vspace{-.15in}%[[
adam@381 598 = fun var : type -> Type =>
adam@381 599 App
adam@381 600 (App
adam@381 601 (Abs
adam@381 602 (fun x : var Nat =>
adam@381 603 Abs (fun x0 : var Nat => Plus (Var x) (Var x0))))
adam@381 604 (Const 1)) (Const 2)
adam@381 605 ]]
adam@381 606
adam@381 607 Next, we try a more interesting example, with some extra [Let]s introduced in [three_the_hard_way]. *)
adam@381 608
adam@381 609 Definition three_a_harder_way : Term Nat := fun _ =>
adam@381 610 Let (Const 1) (fun x => Let (Const 2) (fun y => App (App (add _) (Var x)) (Var y))).
adam@381 611
adam@381 612 Eval compute in Unlet three_a_harder_way.
adam@381 613 (** %\vspace{-.15in}%[[
adam@381 614 = fun var : type -> Type =>
adam@381 615 App
adam@381 616 (App
adam@381 617 (Abs
adam@381 618 (fun x : var Nat =>
adam@381 619 Abs (fun x0 : var Nat => Plus (Var x) (Var x0))))
adam@381 620 (Const 1)) (Const 2)
adam@381 621 ]]
adam@381 622
adam@381 623 The output is the same as in the previous test, confirming that [Unlet] operates properly here.
adam@381 624
adam@381 625 Now we need to state a correctness theorem for [Unlet], based on an inductively proved lemma about [unlet]. It is not at all obvious how to arrive at a proper induction principle for the lemma. The problem is that we want to relate two instantiations of the same [Term], in a way where we know they share the same structure. Note that, while [Unlet] is defined to consider all possible [var] choices in the output term, the correctness proof conveniently only depends on the case of [var := typeDenote]. Thus, one parallel instantiation will set [var := typeDenote], to take the denotation of the original term. The other parallel instantiation will set [var := term typeDenote], to perform the [unlet] transformation in the original term.
adam@381 626
adam@381 627 Here is a relation formalizing the idea that two terms are structurally the same, differing only by replacing the variable data of one with another isomorphic set of variable data in some possibly different type family. *)
adam@381 628
adam@381 629 Section wf.
adam@381 630 Variables var1 var2 : type -> Type.
adam@381 631
adam@381 632 (** To formalize the tag isomorphism, we will use lists of values with the following record type. Each entry has an object language type and an appropriate tag for that type, in each of the two tag families [var1] and [var2]. *)
adam@381 633
adam@381 634 Record varEntry := {
adam@381 635 Ty : type;
adam@381 636 First : var1 Ty;
adam@381 637 Second : var2 Ty
adam@381 638 }.
adam@381 639
adam@381 640 (** Here is the inductive relation definition. An instance [wf G e1 e2] asserts that terms [e1] and [e2] are equivalent up to the variable tag isomorphism [G]. Note how the [Var] rule looks up an entry in [G], and the [Abs] and [Let] rules include recursive [wf] invocations inside the scopes of quantifiers to introduce parallel tag values to be considered as isomorphic. *)
adam@381 641
adam@381 642 Inductive wf : list varEntry -> forall t, term var1 t -> term var2 t -> Prop :=
adam@381 643 | WfVar : forall G t x x', In {| Ty := t; First := x; Second := x' |} G
adam@381 644 -> wf G (Var x) (Var x')
adam@381 645
adam@381 646 | WfConst : forall G n, wf G (Const n) (Const n)
adam@381 647
adam@381 648 | WfPlus : forall G e1 e2 e1' e2', wf G e1 e1'
adam@381 649 -> wf G e2 e2'
adam@381 650 -> wf G (Plus e1 e2) (Plus e1' e2')
adam@381 651
adam@381 652 | WfAbs : forall G dom ran (e1 : _ dom -> term _ ran) e1',
adam@381 653 (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e1 x1) (e1' x2))
adam@381 654 -> wf G (Abs e1) (Abs e1')
adam@381 655
adam@381 656 | WfApp : forall G dom ran (e1 : term _ (Func dom ran)) (e2 : term _ dom) e1' e2',
adam@381 657 wf G e1 e1'
adam@381 658 -> wf G e2 e2'
adam@381 659 -> wf G (App e1 e2) (App e1' e2')
adam@381 660
adam@381 661 | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> term _ t2) e2', wf G e1 e1'
adam@381 662 -> (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e2 x1) (e2' x2))
adam@381 663 -> wf G (Let e1 e2) (Let e1' e2').
adam@381 664 End wf.
adam@381 665
adam@381 666 (** We can state a well-formedness condition for closed terms: for any two choices of tag type families, the parallel instantiations belong to the [wf] relation, starting from an empty variable isomorphism. *)
adam@381 667
adam@381 668 Definition Wf t (E : Term t) := forall var1 var2, wf nil (E var1) (E var2).
adam@381 669
adam@465 670 (** After digesting the syntactic details of [Wf], it is probably not hard to see that reasonable term encodings will satisfy it. For example: *)
adam@381 671
adam@381 672 Theorem three_the_hard_way_Wf : Wf three_the_hard_way.
adam@381 673 red; intros; repeat match goal with
adam@381 674 | [ |- wf _ _ _ ] => constructor; intros
adam@381 675 end; intuition.
adam@381 676 Qed.
adam@381 677
adam@497 678 (** Now we are ready to give a nice simple proof of correctness for [unlet]. First, we add one hint to apply a small variant of a standard library theorem connecting [Forall], a higher-order predicate asserting that every element of a list satisfies some property; and [In], the list membership predicate. *)
adam@381 679
adam@381 680 Hint Extern 1 => match goal with
adam@381 681 | [ H1 : Forall _ _, H2 : In _ _ |- _ ] => apply (Forall_In H1 _ H2)
adam@381 682 end.
adam@381 683
adam@381 684 (** The rest of the proof is about as automated as we could hope for. *)
adam@381 685
adam@381 686 Lemma unletSound : forall G t (e1 : term _ t) e2,
adam@381 687 wf G e1 e2
adam@381 688 -> Forall (fun ve => termDenote (First ve) = Second ve) G
adam@381 689 -> termDenote (unlet e1) = termDenote e2.
adam@497 690 induction 1; pl.
adam@381 691 Qed.
adam@381 692
adam@381 693 Theorem UnletSound : forall t (E : Term t), Wf E
adam@381 694 -> TermDenote (Unlet E) = TermDenote E.
adam@381 695 intros; eapply unletSound; eauto.
adam@381 696 Qed.
adam@381 697
adam@381 698 (** With this example, it is not obvious that the PHOAS encoding is more tractable than dependent de Bruijn. Where the de Bruijn version had [lift] and its helper functions, here we have [Wf] and its auxiliary definitions. In practice, [Wf] is defined once per object language, while such operations as [lift] often need to operate differently for different examples, forcing new implementations for new transformations.
adam@381 699
adam@381 700 The reader may also have come up with another objection: via Curry-Howard, [wf] proofs may be thought of as first-order encodings of term syntax! For instance, the [In] hypothesis of rule [WfVar] is equivalent to a [member] value. There is some merit to this objection. However, as the proofs above show, we are able to reason about transformations using first-order representation only for their inputs, not their outputs. Furthermore, explicit numbering of variables remains absent from the proofs.
adam@381 701
adam@381 702 Have we really avoided first-order reasoning about the output terms of translations? The answer depends on some subtle issues, which deserve a subsection of their own. *)
adam@381 703
adam@381 704
adam@381 705 (** ** Establishing Term Well-Formedness *)
adam@381 706
adam@434 707 (** Can there be values of type [Term t] that are not well-formed according to [Wf]? We expect that Gallina satisfies key%\index{parametricity}% _parametricity_ %\cite{parametricity}% properties, which indicate how polymorphic types may only be inhabited by specific values. We omit details of parametricity theorems here, but [forall t (E : Term t), Wf E] follows the flavor of such theorems. One option would be to assert that fact as an axiom, "proving" that any output of any of our translations is well-formed. We could even prove the soundness of the theorem on paper meta-theoretically, say by considering some particular model of CIC.
adam@381 708
adam@381 709 To be more cautious, we could prove [Wf] for every term that interests us, threading such proofs through all transformations. Here is an example exercise of that kind, for [Unlet].
adam@381 710
adam@398 711 First, we prove that [wf] is _monotone_, in that a given instance continues to hold as we add new variable pairs to the variable isomorphism. *)
adam@381 712
adam@381 713 Hint Constructors wf.
adam@381 714 Hint Extern 1 (In _ _) => simpl; tauto.
adam@381 715 Hint Extern 1 (Forall _ _) => eapply Forall_weaken; [ eassumption | simpl ].
adam@381 716
adam@381 717 Lemma wf_monotone : forall var1 var2 G t (e1 : term var1 t) (e2 : term var2 t),
adam@381 718 wf G e1 e2
adam@381 719 -> forall G', Forall (fun x => In x G') G
adam@381 720 -> wf G' e1 e2.
adam@497 721 induction 1; pl; auto 6.
adam@381 722 Qed.
adam@381 723
adam@381 724 Hint Resolve wf_monotone Forall_In'.
adam@381 725
adam@381 726 (** Now we are ready to prove that [unlet] preserves any [wf] instance. The key invariant has to do with the parallel execution of [unlet] on two different [var] instantiations of a particular term. Since [unlet] uses [term] as the type of variable data, our variable isomorphism context [G] contains pairs of terms, which, conveniently enough, allows us to state the invariant that any pair of terms in the context is also related by [wf]. *)
adam@381 727
adam@381 728 Hint Extern 1 (wf _ _ _) => progress simpl.
adam@381 729
adam@381 730 Lemma unletWf : forall var1 var2 G t (e1 : term (term var1) t) (e2 : term (term var2) t),
adam@381 731 wf G e1 e2
adam@381 732 -> forall G', Forall (fun ve => wf G' (First ve) (Second ve)) G
adam@381 733 -> wf G' (unlet e1) (unlet e2).
adam@497 734 induction 1; pl; eauto 9.
adam@381 735 Qed.
adam@381 736
adam@381 737 (** Repackaging [unletWf] into a theorem about [Wf] and [Unlet] is straightforward. *)
adam@381 738
adam@381 739 Theorem UnletWf : forall t (E : Term t), Wf E
adam@381 740 -> Wf (Unlet E).
adam@381 741 red; intros; apply unletWf with nil; auto.
adam@381 742 Qed.
adam@381 743
adam@381 744 (** This example demonstrates how we may need to use reasoning reminiscent of that associated with first-order representations, though the bookkeeping details are generally easier to manage, and bookkeeping theorems may generally be proved separately from the independently interesting theorems about program transformations. *)
adam@381 745
adam@381 746
adam@381 747 (** ** A Few More Remarks *)
adam@381 748
adam@381 749 (** Higher-order encodings derive their strength from reuse of the meta language's binding constructs. As a result, we can write encoded terms so that they look very similar to their informal counterparts, without variable numbering schemes like for de Bruijn indices. The example encodings above have demonstrated this fact, but modulo the clunkiness of explicit use of the constructors of [term]. After defining a few new Coq syntax notations, we can work with terms in an even more standard form. *)
adam@381 750
adam@381 751 Infix "-->" := Func (right associativity, at level 52).
adam@381 752
adam@381 753 Notation "^" := Var.
adam@381 754 Notation "#" := Const.
adam@381 755 Infix "@" := App (left associativity, at level 50).
adam@381 756 Infix "@+" := Plus (left associativity, at level 50).
adam@381 757 Notation "\ x : t , e" := (Abs (dom := t) (fun x => e))
adam@381 758 (no associativity, at level 51, x at level 0).
adam@381 759 Notation "[ e ]" := (fun _ => e).
adam@381 760
adam@381 761 Example Add : Term (Nat --> Nat --> Nat) :=
adam@381 762 [\x : Nat, \y : Nat, ^x @+ ^y].
adam@381 763
adam@381 764 Example Three_the_hard_way : Term Nat :=
adam@381 765 [Add _ @ #1 @ #2].
adam@381 766
adam@381 767 Eval compute in TermDenote Three_the_hard_way.
adam@381 768 (** %\vspace{-.15in}%[[
adam@381 769 = 3
adam@381 770 ]]
adam@381 771 *)
adam@381 772
adam@381 773 End HigherOrder.
adam@381 774
adam@381 775 (** The PHOAS approach shines here because we are working with an object language that has an easy embedding into Coq. That is, there is a straightforward recursive function translating object terms into terms of Gallina. All Gallina programs terminate, so clearly we cannot hope to find such embeddings for Turing-complete languages; and non-Turing-complete languages may still require much more involved translations. I have some work%~\cite{CompilerPOPL10}% on modeling semantics of Turing-complete languages with PHOAS, but my impression is that there are many more advances left to be made in this field, possibly with completely new term representations that we have not yet been clever enough to think up. *)