Mercurial > cpdt > repo

annotate src/ProgLang.v @ 381:d5112c099fbf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New chapter: ProgLang
author Adam Chlipala <adam@chlipala.net>
date Sun, 01 Apr 2012 15:02:32 -0400
parents
children 05efde66559d
rev   line source
adam@381 1 (* Copyright (c) 2011-2012, 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@381 13 Require Import CpdtTactics DepList.
adam@381 14
adam@381 15 Set Implicit Arguments.
adam@381 16 (* end hide *)
adam@381 17
adam@381 18 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *)
adam@381 19
adam@381 20 (** 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{%#<a href="http://www.cis.upenn.edu/~bcpierce/sf/"><i>#Software Foundations#</i></a>#%}\footnote{\url{http://www.cis.upenn.edu/~bcpierce/sf/}}% by Pierce et al.
adam@381 21
adam@381 22 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 23
adam@381 24 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 25
adam@381 26 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. *)
adam@381 27
adam@381 28 Ltac ext := let x := fresh "x" in extensionality x.
adam@381 29 Ltac t := crush; repeat (ext || f_equal; crush).
adam@381 30
adam@381 31 (** At this point in the book source, some auxiliary proofs also appear. *)
adam@381 32
adam@381 33 (* begin hide *)
adam@381 34 Section hmap.
adam@381 35 Variable A : Type.
adam@381 36 Variables B1 B2 B3 : A -> Type.
adam@381 37
adam@381 38 Variable f1 : forall x, B1 x -> B2 x.
adam@381 39 Variable f2 : forall x, B2 x -> B3 x.
adam@381 40
adam@381 41 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 42 induction hl; crush.
adam@381 43 Qed.
adam@381 44 End hmap.
adam@381 45
adam@381 46 Section Forall.
adam@381 47 Variable A : Type.
adam@381 48 Variable P : A -> Prop.
adam@381 49
adam@381 50 Theorem Forall_In : forall ls, Forall P ls -> forall x, In x ls -> P x.
adam@381 51 induction 1; crush.
adam@381 52 Qed.
adam@381 53
adam@381 54 Theorem Forall_In' : forall ls, (forall x, In x ls -> P x) -> Forall P ls.
adam@381 55 induction ls; crush.
adam@381 56 Qed.
adam@381 57
adam@381 58 Variable P' : A -> Prop.
adam@381 59
adam@381 60 Theorem Forall_weaken : forall ls, Forall P ls
adam@381 61 -> (forall x, P x -> P' x)
adam@381 62 -> Forall P' ls.
adam@381 63 induction 1; crush.
adam@381 64 Qed.
adam@381 65 End Forall.
adam@381 66 (* end hide *)
adam@381 67
adam@381 68 (** 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 69
adam@381 70 Inductive type : Type :=
adam@381 71 | Nat : type
adam@381 72 | Func : type -> type -> type.
adam@381 73
adam@381 74 Fixpoint typeDenote (t : type) : Type :=
adam@381 75 match t with
adam@381 76 | Nat => nat
adam@381 77 | Func t1 t2 => typeDenote t1 -> typeDenote t2
adam@381 78 end.
adam@381 79
adam@381 80 (** 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 81
adam@381 82
adam@381 83 (** * Dependent de Bruijn Indices *)
adam@381 84
adam@381 85 (** The first encoding is one we met first in Chapter 9, the %\emph{%#<i>#dependent de Bruijn index#</i>#%}% encoding. We represent program syntax terms in a type familiy parametrized by a list of types, representing the %\emph{%#<i>#typing context#</i>#%}%, 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 86
adam@381 87 Module FirstOrder.
adam@381 88
adam@381 89 (** Here is the definition of the [term] type, including variables, constants, addition, function abstraction and application, and let binding of local variables. *)
adam@381 90
adam@381 91 Inductive term : list type -> type -> Type :=
adam@381 92 | Var : forall G t, member t G -> term G t
adam@381 93
adam@381 94 | Const : forall G, nat -> term G Nat
adam@381 95 | Plus : forall G, term G Nat -> term G Nat -> term G Nat
adam@381 96
adam@381 97 | Abs : forall G dom ran, term (dom :: G) ran -> term G (Func dom ran)
adam@381 98 | App : forall G dom ran, term G (Func dom ran) -> term G dom -> term G ran
adam@381 99
adam@381 100 | Let : forall G t1 t2, term G t1 -> term (t1 :: G) t2 -> term G t2.
adam@381 101
adam@381 102 Implicit Arguments Const [G].
adam@381 103
adam@381 104 (** 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 105
adam@381 106 Example add : term nil (Func Nat (Func Nat Nat)) :=
adam@381 107 Abs (Abs (Plus (Var (HNext HFirst)) (Var HFirst))).
adam@381 108
adam@381 109 Example three_the_hard_way : term nil Nat :=
adam@381 110 App (App add (Const 1)) (Const 2).
adam@381 111
adam@381 112 (** 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 113
adam@381 114 Fixpoint termDenote G t (e : term G t) : hlist typeDenote G -> typeDenote t :=
adam@381 115 match e with
adam@381 116 | Var _ _ x => fun s => hget s x
adam@381 117
adam@381 118 | Const _ n => fun _ => n
adam@381 119 | Plus _ e1 e2 => fun s => termDenote e1 s + termDenote e2 s
adam@381 120
adam@381 121 | Abs _ _ _ e1 => fun s => fun x => termDenote e1 (x ::: s)
adam@381 122 | App _ _ _ e1 e2 => fun s => (termDenote e1 s) (termDenote e2 s)
adam@381 123
adam@381 124 | Let _ _ _ e1 e2 => fun s => termDenote e2 (termDenote e1 s ::: s)
adam@381 125 end.
adam@381 126
adam@381 127 (** 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 %\emph{%#<i>#identity#</i>#%}% transformation, which takes a term apart and reassembles it. *)
adam@381 128
adam@381 129 Fixpoint ident G t (e : term G t) : term G t :=
adam@381 130 match e with
adam@381 131 | Var _ _ x => Var x
adam@381 132
adam@381 133 | Const _ n => Const n
adam@381 134 | Plus _ e1 e2 => Plus (ident e1) (ident e2)
adam@381 135
adam@381 136 | Abs _ _ _ e1 => Abs (ident e1)
adam@381 137 | App _ _ _ e1 e2 => App (ident e1) (ident e2)
adam@381 138
adam@381 139 | Let _ _ _ e1 e2 => Let (ident e1) (ident e2)
adam@381 140 end.
adam@381 141
adam@381 142 Theorem identSound : forall G t (e : term G t) s,
adam@381 143 termDenote (ident e) s = termDenote e s.
adam@381 144 induction e; t.
adam@381 145 Qed.
adam@381 146
adam@381 147 (** A slightly more ambitious transformation belongs to the family of %\emph{%#<i>#constant folding#</i>#%}% optimizations we have used as examples in other chapters. *)
adam@381 148
adam@381 149 Fixpoint cfold G t (e : term G t) : term G t :=
adam@381 150 match e with
adam@381 151 | Plus G e1 e2 =>
adam@381 152 let e1' := cfold e1 in
adam@381 153 let e2' := cfold e2 in
adam@381 154 match e1', e2' return _ with
adam@381 155 | Const _ n1, Const _ n2 => Const (n1 + n2)
adam@381 156 | _, _ => Plus e1' e2'
adam@381 157 end
adam@381 158
adam@381 159 | Abs _ _ _ e1 => Abs (cfold e1)
adam@381 160 | App _ _ _ e1 e2 => App (cfold e1) (cfold e2)
adam@381 161
adam@381 162 | Let _ _ _ e1 e2 => Let (cfold e1) (cfold e2)
adam@381 163
adam@381 164 | e => e
adam@381 165 end.
adam@381 166
adam@381 167 (** The correctness proof is more complex, but only slightly so. *)
adam@381 168
adam@381 169 Theorem cfoldSound : forall G t (e : term G t) s,
adam@381 170 termDenote (cfold e) s = termDenote e s.
adam@381 171 induction e; t;
adam@381 172 repeat (match goal with
adam@381 173 | [ |- context[match ?E with
adam@381 174 | Var _ _ _ => _ | Const _ _ => _ | Plus _ _ _ => _
adam@381 175 | Abs _ _ _ _ => _ | App _ _ _ _ _ => _
adam@381 176 | Let _ _ _ _ _ => _
adam@381 177 end] ] => dep_destruct E
adam@381 178 end; t).
adam@381 179 Qed.
adam@381 180
adam@381 181 (** 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}\emph{%#<i>#first-order#</i>#%}% because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure.
adam@381 182
adam@381 183 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 %\emph{%#<i>#substitution#</i>#%}%, 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 %\emph{%#<i>#lifting#</i>#%}%, a standard de Bruijn indices operation. With dependent typing, lifting corresponds to weakening for typing judgments.
adam@381 184
adam@381 185 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 186
adam@381 187 Fixpoint insertAt (t : type) (G : list type) (n : nat) {struct n} : list type :=
adam@381 188 match n with
adam@381 189 | O => t :: G
adam@381 190 | S n' => match G with
adam@381 191 | nil => t :: G
adam@381 192 | t' :: G' => t' :: insertAt t G' n'
adam@381 193 end
adam@381 194 end.
adam@381 195
adam@381 196 (** Another function lifts bound variable instances, which we represent with [member] values. *)
adam@381 197
adam@381 198 Fixpoint liftVar t G (x : member t G) t' n : member t (insertAt t' G n) :=
adam@381 199 match x with
adam@381 200 | HFirst G' => match n return member t (insertAt t' (t :: G') n) with
adam@381 201 | O => HNext HFirst
adam@381 202 | _ => HFirst
adam@381 203 end
adam@381 204 | HNext t'' G' x' => match n return member t (insertAt t' (t'' :: G') n) with
adam@381 205 | O => HNext (HNext x')
adam@381 206 | S n' => HNext (liftVar x' t' n')
adam@381 207 end
adam@381 208 end.
adam@381 209
adam@381 210 (** The final helper function for lifting allows us to insert a new variable anywhere in a typing context. *)
adam@381 211
adam@381 212 Fixpoint lift' G t' n t (e : term G t) : term (insertAt t' G n) t :=
adam@381 213 match e with
adam@381 214 | Var _ _ x => Var (liftVar x t' n)
adam@381 215
adam@381 216 | Const _ n => Const n
adam@381 217 | Plus _ e1 e2 => Plus (lift' t' n e1) (lift' t' n e2)
adam@381 218
adam@381 219 | Abs _ _ _ e1 => Abs (lift' t' (S n) e1)
adam@381 220 | App _ _ _ e1 e2 => App (lift' t' n e1) (lift' t' n e2)
adam@381 221
adam@381 222 | Let _ _ _ e1 e2 => Let (lift' t' n e1) (lift' t' (S n) e2)
adam@381 223 end.
adam@381 224
adam@381 225 (** In the [Let] removal transformation, we only need to apply lifting to add a new variable at the %\emph{%#<i>#beginning#</i>#%}% of a typing context, so we package lifting into this final, simplified form. *)
adam@381 226
adam@381 227 Definition lift G t' t (e : term G t) : term (t' :: G) t :=
adam@381 228 lift' t' O e.
adam@381 229
adam@381 230 (** 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 231
adam@381 232 Fixpoint unlet G t (e : term G t) G' : hlist (term G') G -> term G' t :=
adam@381 233 match e with
adam@381 234 | Var _ _ x => fun s => hget s x
adam@381 235
adam@381 236 | Const _ n => fun _ => Const n
adam@381 237 | Plus _ e1 e2 => fun s => Plus (unlet e1 s) (unlet e2 s)
adam@381 238
adam@381 239 | Abs _ _ _ e1 => fun s => Abs (unlet e1 (Var HFirst ::: hmap (lift _) s))
adam@381 240 | App _ _ _ e1 e2 => fun s => App (unlet e1 s) (unlet e2 s)
adam@381 241
adam@381 242 | Let _ t1 _ e1 e2 => fun s => unlet e2 (unlet e1 s ::: s)
adam@381 243 end.
adam@381 244
adam@381 245 (** 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 246
adam@381 247 Fixpoint insertAtS (t : type) (x : typeDenote t) (G : list type) (n : nat) {struct n}
adam@381 248 : hlist typeDenote G -> hlist typeDenote (insertAt t G n) :=
adam@381 249 match n with
adam@381 250 | O => fun s => x ::: s
adam@381 251 | S n' => match G return hlist typeDenote G
adam@381 252 -> hlist typeDenote (insertAt t G (S n')) with
adam@381 253 | nil => fun s => x ::: s
adam@381 254 | t' :: G' => fun s => hhd s ::: insertAtS t x n' (htl s)
adam@381 255 end
adam@381 256 end.
adam@381 257
adam@381 258 Implicit Arguments insertAtS [t G].
adam@381 259
adam@381 260 (** 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 261
adam@381 262 Lemma liftVarSound : forall t' (x : typeDenote t') t G (m : member t G) s n,
adam@381 263 hget s m = hget (insertAtS x n s) (liftVar m t' n).
adam@381 264 induction m; destruct n; dep_destruct s; t.
adam@381 265 Qed.
adam@381 266
adam@381 267 Hint Resolve liftVarSound.
adam@381 268
adam@381 269 (** An analogous lemma establishes correctness of [lift']. *)
adam@381 270
adam@381 271 Lemma lift'Sound : forall G t' (x : typeDenote t') t (e : term G t) n s,
adam@381 272 termDenote e s = termDenote (lift' t' n e) (insertAtS x n s).
adam@381 273 induction e; t;
adam@381 274 repeat match goal with
adam@381 275 | [ IH : forall n s, _ = termDenote (lift' _ n ?E) _
adam@381 276 |- context[lift' _ (S ?N) ?E] ] => specialize (IH (S N))
adam@381 277 end; t.
adam@381 278 Qed.
adam@381 279
adam@381 280 (** Correctness of [lift] itself is an easy corollary. *)
adam@381 281
adam@381 282 Lemma liftSound : forall G t' (x : typeDenote t') t (e : term G t) s,
adam@381 283 termDenote (lift t' e) (x ::: s) = termDenote e s.
adam@381 284 unfold lift; intros; rewrite (lift'Sound _ x e O); trivial.
adam@381 285 Qed.
adam@381 286
adam@381 287 Hint Rewrite hget_hmap hmap_hmap liftSound.
adam@381 288
adam@381 289 (** Finally, we can prove correctness of [unletSound] for terms in arbitrary typing environments. *)
adam@381 290
adam@381 291 Lemma unletSound' : forall G t (e : term G t) G' (s : hlist (term G') G) s1,
adam@381 292 termDenote (unlet e s) s1
adam@381 293 = termDenote e (hmap (fun t' (e' : term G' t') => termDenote e' s1) s).
adam@381 294 induction e; t.
adam@381 295 Qed.
adam@381 296
adam@381 297 (** 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. *)
adam@381 298
adam@381 299 Theorem unletSound : forall t (e : term nil t),
adam@381 300 termDenote (unlet e HNil) HNil = termDenote e HNil.
adam@381 301 intros; apply unletSound'.
adam@381 302 Qed.
adam@381 303
adam@381 304 End FirstOrder.
adam@381 305
adam@381 306 (** 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 307
adam@381 308
adam@381 309 (** * Parametric Higher-Order Abstract Syntax *)
adam@381 310
adam@381 311 (** In contrast to first-order encodings, %\index{higher-order syntax}\emph{%#<i>#higher-order#</i>#%}% encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an %\index{object language}\emph{%#<i>#object language#</i>#%}% (the language being formalized) can be represented using the binding constructs of the %\index{meta language}\emph{%#<i>#meta language#</i>#%}% (the language in which the formalization is done). The best known higher-order encoding is called %\index{higher-order abstract syntax}\index{HOAS}\emph{%#<i>#higher-order abstract syntax (HOAS)#</i>#%}~\cite{HOAS}%, and we can start by attempting to apply it directly in Coq. *)
adam@381 312
adam@381 313 Module HigherOrder.
adam@381 314
adam@381 315 (** With HOAS, each object language binding construct is represented with a %\emph{%#<i>#function#</i>#%}% of the meta language. Here is what we get if we apply that idea within an inductive definition of term syntax. *)
adam@381 316
adam@381 317 (** %\vspace{-.15in}%[[
adam@381 318 Inductive term : type -> Type :=
adam@381 319 | Const : nat -> term Nat
adam@381 320 | Plus : term Nat -> term Nat -> term Nat
adam@381 321
adam@381 322 | Abs : forall dom ran, (term dom -> term ran) -> term (Func dom ran)
adam@381 323 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
adam@381 324
adam@381 325 | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2.
adam@381 326 ]]
adam@381 327
adam@381 328 However, Coq rejects this definition for failing to meet the %\index{strict positivity restriction}%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 329
adam@381 330 An alternate higher-order encoding is %\index{parametric higher-order abstract syntax}\index{PHOAS}\emph{%#<i>#parametric HOAS#</i>#%}%, 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 parametrize the syntax type by a type family standing for a %\emph{%#<i>#representation of variables#</i>#%}%. *)
adam@381 331
adam@381 332 Section var.
adam@381 333 Variable var : type -> Type.
adam@381 334
adam@381 335 Inductive term : type -> Type :=
adam@381 336 | Var : forall t, var t -> term t
adam@381 337
adam@381 338 | Const : nat -> term Nat
adam@381 339 | Plus : term Nat -> term Nat -> term Nat
adam@381 340
adam@381 341 | Abs : forall dom ran, (var dom -> term ran) -> term (Func dom ran)
adam@381 342 | App : forall dom ran, term (Func dom ran) -> term dom -> term ran
adam@381 343
adam@381 344 | Let : forall t1 t2, term t1 -> (var t1 -> term t2) -> term t2.
adam@381 345 End var.
adam@381 346
adam@381 347 Implicit Arguments Var [var t].
adam@381 348 Implicit Arguments Const [var].
adam@381 349 Implicit Arguments Abs [var dom ran].
adam@381 350
adam@381 351 (** Coq accepts this definition because our embedded functions now merely take %\emph{%#<i>#variables#</i>#%}% 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 352
adam@381 353 We write the final type of a closed term using polymorphic quantification over all possible choices of [var] type family. *)
adam@381 354
adam@381 355 Definition Term t := forall var, term var t.
adam@381 356
adam@381 357 (** 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 %\emph{%#<i>#structure#</i>#%}% of the term. *)
adam@381 358
adam@381 359 Example add : Term (Func Nat (Func Nat Nat)) := fun var =>
adam@381 360 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))).
adam@381 361
adam@381 362 Example three_the_hard_way : Term Nat := fun var =>
adam@381 363 App (App (add var) (Const 1)) (Const 2).
adam@381 364
adam@381 365 (** 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 %\emph{%#<i>#are#</i>#%}% mentioned in the function bodies that type inference calculates. *)
adam@381 366
adam@381 367 Example add' : Term (Func Nat (Func Nat Nat)) := fun _ =>
adam@381 368 Abs (fun x => Abs (fun y => Plus (Var x) (Var y))).
adam@381 369
adam@381 370 Example three_the_hard_way' : Term Nat := fun _ =>
adam@381 371 App (App (add' _) (Const 1)) (Const 2).
adam@381 372
adam@381 373
adam@381 374 (** ** Functional Programming with PHOAS *)
adam@381 375
adam@381 376 (** 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 %\emph{%#<i>#which data should be annotated on each variable#</i>#%}%. 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 377
adam@381 378 Fixpoint countVars t (e : term (fun _ => unit) t) : nat :=
adam@381 379 match e with
adam@381 380 | Var _ _ => 1
adam@381 381
adam@381 382 | Const _ => 0
adam@381 383 | Plus e1 e2 => countVars e1 + countVars e2
adam@381 384
adam@381 385 | Abs _ _ e1 => countVars (e1 tt)
adam@381 386 | App _ _ e1 e2 => countVars e1 + countVars e2
adam@381 387
adam@381 388 | Let _ _ e1 e2 => countVars e1 + countVars (e2 tt)
adam@381 389 end.
adam@381 390
adam@381 391 (** 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 392
adam@381 393 Definition CountVars t (E : Term t) := countVars (E (fun _ => unit)).
adam@381 394
adam@381 395 (** It is easy to test that [CountVars] operates properly. *)
adam@381 396
adam@381 397 Eval compute in CountVars three_the_hard_way.
adam@381 398 (** %\vspace{-.15in}%[[
adam@381 399 = 2
adam@381 400 ]]
adam@381 401 *)
adam@381 402
adam@381 403 (** 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 404
adam@381 405 Require Import String.
adam@381 406 Open Scope string_scope.
adam@381 407
adam@381 408 Fixpoint pretty t (e : term (fun _ => string) t) (x : string) : string :=
adam@381 409 match e with
adam@381 410 | Var _ s => s
adam@381 411
adam@381 412 | Const _ => "N"
adam@381 413 | Plus e1 e2 => "(" ++ pretty e1 x ++ " + " ++ pretty e2 x ++ ")"
adam@381 414
adam@381 415 | Abs _ _ e1 => "(fun " ++ x ++ " => " ++ pretty (e1 x) (x ++ "'") ++ ")"
adam@381 416 | App _ _ e1 e2 => "(" ++ pretty e1 x ++ " " ++ pretty e2 x ++ ")"
adam@381 417
adam@381 418 | Let _ _ e1 e2 => "(let " ++ x ++ " = " ++ pretty e1 x ++ " in "
adam@381 419 ++ pretty (e2 x) (x ++ "'") ++ ")"
adam@381 420 end.
adam@381 421
adam@381 422 Definition Pretty t (E : Term t) := pretty (E (fun _ => string)) "x".
adam@381 423
adam@381 424 Eval compute in Pretty three_the_hard_way.
adam@381 425 (** %\vspace{-.15in}%[[
adam@381 426 = "(((fun x => (fun x' => (x + x'))) N) N)"
adam@381 427 ]]
adam@381 428 *)
adam@381 429
adam@381 430 (** 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 one term in another. The key insight here is to %\emph{%#<i>#tag variables with terms#</i>#%}%, 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 parametrized over a specific [var] choice. *)
adam@381 431
adam@381 432 Fixpoint squash var t (e : term (term var) t) : term var t :=
adam@381 433 match e with
adam@381 434 | Var _ e1 => e1
adam@381 435
adam@381 436 | Const n => Const n
adam@381 437 | Plus e1 e2 => Plus (squash e1) (squash e2)
adam@381 438
adam@381 439 | Abs _ _ e1 => Abs (fun x => squash (e1 (Var x)))
adam@381 440 | App _ _ e1 e2 => App (squash e1) (squash e2)
adam@381 441
adam@381 442 | Let _ _ e1 e2 => Let (squash e1) (fun x => squash (e2 (Var x)))
adam@381 443 end.
adam@381 444
adam@381 445 (** 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 446
adam@381 447 Definition Term1 (t1 t2 : type) := forall var, var t1 -> term var t2.
adam@381 448
adam@381 449 (** 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 450
adam@381 451 Definition Subst (t1 t2 : type) (E : Term1 t1 t2) (E' : Term t1) : Term t2 :=
adam@381 452 fun var => squash (E (term var) (E' var)).
adam@381 453
adam@381 454 Eval compute in Subst (fun _ x => Plus (Var x) (Const 3)) three_the_hard_way.
adam@381 455 (** %\vspace{-.15in}%[[
adam@381 456 = fun var : type -> Type =>
adam@381 457 Plus
adam@381 458 (App
adam@381 459 (App
adam@381 460 (Abs
adam@381 461 (fun x : var Nat =>
adam@381 462 Abs (fun y : var Nat => Plus (Var x) (Var y))))
adam@381 463 (Const 1)) (Const 2)) (Const 3)
adam@381 464 ]]
adam@381 465
adam@381 466 One further development, which may seem surprising at first, is that we can also implement a usual term denotation function, when we %\emph{%#<i>#tag variables with their denotations#</i>#%}%. *)
adam@381 467
adam@381 468 Fixpoint termDenote t (e : term typeDenote t) : typeDenote t :=
adam@381 469 match e with
adam@381 470 | Var _ v => v
adam@381 471
adam@381 472 | Const n => n
adam@381 473 | Plus e1 e2 => termDenote e1 + termDenote e2
adam@381 474
adam@381 475 | Abs _ _ e1 => fun x => termDenote (e1 x)
adam@381 476 | App _ _ e1 e2 => (termDenote e1) (termDenote e2)
adam@381 477
adam@381 478 | Let _ _ e1 e2 => termDenote (e2 (termDenote e1))
adam@381 479 end.
adam@381 480
adam@381 481 Definition TermDenote t (E : Term t) : typeDenote t :=
adam@381 482 termDenote (E typeDenote).
adam@381 483
adam@381 484 Eval compute in TermDenote three_the_hard_way.
adam@381 485 (** %\vspace{-.15in}%[[
adam@381 486 = 3
adam@381 487 ]]
adam@381 488
adam@381 489 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 490
adam@381 491
adam@381 492 (** ** Verifying Program Transformations *)
adam@381 493
adam@381 494 (** 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 495
adam@381 496 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 497
adam@381 498 Fixpoint ident var t (e : term var t) : term var t :=
adam@381 499 match e with
adam@381 500 | Var _ x => Var x
adam@381 501
adam@381 502 | Const n => Const n
adam@381 503 | Plus e1 e2 => Plus (ident e1) (ident e2)
adam@381 504
adam@381 505 | Abs _ _ e1 => Abs (fun x => ident (e1 x))
adam@381 506 | App _ _ e1 e2 => App (ident e1) (ident e2)
adam@381 507
adam@381 508 | Let _ _ e1 e2 => Let (ident e1) (fun x => ident (e2 x))
adam@381 509 end.
adam@381 510
adam@381 511 Definition Ident t (E : Term t) : Term t := fun var =>
adam@381 512 ident (E var).
adam@381 513
adam@381 514 (** 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 515
adam@381 516 Lemma identSound : forall t (e : term typeDenote t),
adam@381 517 termDenote (ident e) = termDenote e.
adam@381 518 induction e; t.
adam@381 519 Qed.
adam@381 520
adam@381 521 Theorem IdentSound : forall t (E : Term t),
adam@381 522 TermDenote (Ident E) = TermDenote E.
adam@381 523 intros; apply identSound.
adam@381 524 Qed.
adam@381 525
adam@381 526 (** The translation of the constant-folding function and its proof work more or less the same way. *)
adam@381 527
adam@381 528 Fixpoint cfold var t (e : term var t) : term var t :=
adam@381 529 match e with
adam@381 530 | Plus e1 e2 =>
adam@381 531 let e1' := cfold e1 in
adam@381 532 let e2' := cfold e2 in
adam@381 533 match e1', e2' with
adam@381 534 | Const n1, Const n2 => Const (n1 + n2)
adam@381 535 | _, _ => Plus e1' e2'
adam@381 536 end
adam@381 537
adam@381 538 | Abs _ _ e1 => Abs (fun x => cfold (e1 x))
adam@381 539 | App _ _ e1 e2 => App (cfold e1) (cfold e2)
adam@381 540
adam@381 541 | Let _ _ e1 e2 => Let (cfold e1) (fun x => cfold (e2 x))
adam@381 542
adam@381 543 | e => e
adam@381 544 end.
adam@381 545
adam@381 546 Definition Cfold t (E : Term t) : Term t := fun var =>
adam@381 547 cfold (E var).
adam@381 548
adam@381 549 Lemma cfoldSound : forall t (e : term typeDenote t),
adam@381 550 termDenote (cfold e) = termDenote e.
adam@381 551 induction e; t;
adam@381 552 repeat (match goal with
adam@381 553 | [ |- context[match ?E with
adam@381 554 | Var _ _ => _ | Const _ => _ | Plus _ _ => _
adam@381 555 | Abs _ _ _ => _ | App _ _ _ _ => _
adam@381 556 | Let _ _ _ _ => _
adam@381 557 end] ] => dep_destruct E
adam@381 558 end; t).
adam@381 559 Qed.
adam@381 560
adam@381 561 Theorem CfoldSound : forall t (E : Term t),
adam@381 562 TermDenote (Cfold E) = TermDenote E.
adam@381 563 intros; apply cfoldSound.
adam@381 564 Qed.
adam@381 565
adam@381 566 (** 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 567
adam@381 568 Fixpoint unlet var t (e : term (term var) t) : term var t :=
adam@381 569 match e with
adam@381 570 | Var _ e1 => e1
adam@381 571
adam@381 572 | Const n => Const n
adam@381 573 | Plus e1 e2 => Plus (unlet e1) (unlet e2)
adam@381 574
adam@381 575 | Abs _ _ e1 => Abs (fun x => unlet (e1 (Var x)))
adam@381 576 | App _ _ e1 e2 => App (unlet e1) (unlet e2)
adam@381 577
adam@381 578 | Let _ _ e1 e2 => unlet (e2 (unlet e1))
adam@381 579 end.
adam@381 580
adam@381 581 Definition Unlet t (E : Term t) : Term t := fun var =>
adam@381 582 unlet (E (term var)).
adam@381 583
adam@381 584 (** We can test [Unlet] first on an uninteresting example, [three_the_hard_way], which does not use [Let]. *)
adam@381 585
adam@381 586 Eval compute in Unlet three_the_hard_way.
adam@381 587 (** %\vspace{-.15in}%[[
adam@381 588 = fun var : type -> Type =>
adam@381 589 App
adam@381 590 (App
adam@381 591 (Abs
adam@381 592 (fun x : var Nat =>
adam@381 593 Abs (fun x0 : var Nat => Plus (Var x) (Var x0))))
adam@381 594 (Const 1)) (Const 2)
adam@381 595 ]]
adam@381 596
adam@381 597 Next, we try a more interesting example, with some extra [Let]s introduced in [three_the_hard_way]. *)
adam@381 598
adam@381 599 Definition three_a_harder_way : Term Nat := fun _ =>
adam@381 600 Let (Const 1) (fun x => Let (Const 2) (fun y => App (App (add _) (Var x)) (Var y))).
adam@381 601
adam@381 602 Eval compute in Unlet three_a_harder_way.
adam@381 603 (** %\vspace{-.15in}%[[
adam@381 604 = fun var : type -> Type =>
adam@381 605 App
adam@381 606 (App
adam@381 607 (Abs
adam@381 608 (fun x : var Nat =>
adam@381 609 Abs (fun x0 : var Nat => Plus (Var x) (Var x0))))
adam@381 610 (Const 1)) (Const 2)
adam@381 611 ]]
adam@381 612
adam@381 613 The output is the same as in the previous test, confirming that [Unlet] operates properly here.
adam@381 614
adam@381 615 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 616
adam@381 617 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 618
adam@381 619 Section wf.
adam@381 620 Variables var1 var2 : type -> Type.
adam@381 621
adam@381 622 (** 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 623
adam@381 624 Record varEntry := {
adam@381 625 Ty : type;
adam@381 626 First : var1 Ty;
adam@381 627 Second : var2 Ty
adam@381 628 }.
adam@381 629
adam@381 630 (** 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 631
adam@381 632 Inductive wf : list varEntry -> forall t, term var1 t -> term var2 t -> Prop :=
adam@381 633 | WfVar : forall G t x x', In {| Ty := t; First := x; Second := x' |} G
adam@381 634 -> wf G (Var x) (Var x')
adam@381 635
adam@381 636 | WfConst : forall G n, wf G (Const n) (Const n)
adam@381 637
adam@381 638 | WfPlus : forall G e1 e2 e1' e2', wf G e1 e1'
adam@381 639 -> wf G e2 e2'
adam@381 640 -> wf G (Plus e1 e2) (Plus e1' e2')
adam@381 641
adam@381 642 | WfAbs : forall G dom ran (e1 : _ dom -> term _ ran) e1',
adam@381 643 (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e1 x1) (e1' x2))
adam@381 644 -> wf G (Abs e1) (Abs e1')
adam@381 645
adam@381 646 | WfApp : forall G dom ran (e1 : term _ (Func dom ran)) (e2 : term _ dom) e1' e2',
adam@381 647 wf G e1 e1'
adam@381 648 -> wf G e2 e2'
adam@381 649 -> wf G (App e1 e2) (App e1' e2')
adam@381 650
adam@381 651 | WfLet : forall G t1 t2 e1 e1' (e2 : _ t1 -> term _ t2) e2', wf G e1 e1'
adam@381 652 -> (forall x1 x2, wf ({| First := x1; Second := x2 |} :: G) (e2 x1) (e2' x2))
adam@381 653 -> wf G (Let e1 e2) (Let e1' e2').
adam@381 654 End wf.
adam@381 655
adam@381 656 (** 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 657
adam@381 658 Definition Wf t (E : Term t) := forall var1 var2, wf nil (E var1) (E var2).
adam@381 659
adam@381 660 (** After digesting the syntactic details of [Wf], it is probably not hard to see that reasonable term encodings will satsify it. For example: *)
adam@381 661
adam@381 662 Theorem three_the_hard_way_Wf : Wf three_the_hard_way.
adam@381 663 red; intros; repeat match goal with
adam@381 664 | [ |- wf _ _ _ ] => constructor; intros
adam@381 665 end; intuition.
adam@381 666 Qed.
adam@381 667
adam@381 668 (** Now we are ready to give a nice simple proof of correctness for [unlet]. First, we add one hint to apply 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 669
adam@381 670 Hint Extern 1 => match goal with
adam@381 671 | [ H1 : Forall _ _, H2 : In _ _ |- _ ] => apply (Forall_In H1 _ H2)
adam@381 672 end.
adam@381 673
adam@381 674 (** The rest of the proof is about as automated as we could hope for. *)
adam@381 675
adam@381 676 Lemma unletSound : forall G t (e1 : term _ t) e2,
adam@381 677 wf G e1 e2
adam@381 678 -> Forall (fun ve => termDenote (First ve) = Second ve) G
adam@381 679 -> termDenote (unlet e1) = termDenote e2.
adam@381 680 induction 1; t.
adam@381 681 Qed.
adam@381 682
adam@381 683 Theorem UnletSound : forall t (E : Term t), Wf E
adam@381 684 -> TermDenote (Unlet E) = TermDenote E.
adam@381 685 intros; eapply unletSound; eauto.
adam@381 686 Qed.
adam@381 687
adam@381 688 (** 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 689
adam@381 690 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 691
adam@381 692 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 693
adam@381 694
adam@381 695 (** ** Establishing Term Well-Formedness *)
adam@381 696
adam@381 697 (** Can there be values of type [Term t] that are not well-formed according to [Wf]? We expect that Gallina satisfies key %\index{parametricity}\emph{%#<i>#parametricity#</i>#%}~\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 698
adam@381 699 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 700
adam@381 701 First, we prove that [wf] is %\emph{%#<i>#monotone#</i>#%}%, in that a given instance continues to hold as we add new variable pairs to the variable isomorphism. *)
adam@381 702
adam@381 703 Hint Constructors wf.
adam@381 704 Hint Extern 1 (In _ _) => simpl; tauto.
adam@381 705 Hint Extern 1 (Forall _ _) => eapply Forall_weaken; [ eassumption | simpl ].
adam@381 706
adam@381 707 Lemma wf_monotone : forall var1 var2 G t (e1 : term var1 t) (e2 : term var2 t),
adam@381 708 wf G e1 e2
adam@381 709 -> forall G', Forall (fun x => In x G') G
adam@381 710 -> wf G' e1 e2.
adam@381 711 induction 1; t; auto 6.
adam@381 712 Qed.
adam@381 713
adam@381 714 Hint Resolve wf_monotone Forall_In'.
adam@381 715
adam@381 716 (** 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 717
adam@381 718 Hint Extern 1 (wf _ _ _) => progress simpl.
adam@381 719
adam@381 720 Lemma unletWf : forall var1 var2 G t (e1 : term (term var1) t) (e2 : term (term var2) t),
adam@381 721 wf G e1 e2
adam@381 722 -> forall G', Forall (fun ve => wf G' (First ve) (Second ve)) G
adam@381 723 -> wf G' (unlet e1) (unlet e2).
adam@381 724 induction 1; t; eauto 9.
adam@381 725 Qed.
adam@381 726
adam@381 727 (** Repackaging [unletWf] into a theorem about [Wf] and [Unlet] is straightforward. *)
adam@381 728
adam@381 729 Theorem UnletWf : forall t (E : Term t), Wf E
adam@381 730 -> Wf (Unlet E).
adam@381 731 red; intros; apply unletWf with nil; auto.
adam@381 732 Qed.
adam@381 733
adam@381 734 (** 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 735
adam@381 736
adam@381 737 (** ** A Few More Remarks *)
adam@381 738
adam@381 739 (** 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 740
adam@381 741 Infix "-->" := Func (right associativity, at level 52).
adam@381 742
adam@381 743 Notation "^" := Var.
adam@381 744 Notation "#" := Const.
adam@381 745 Infix "@" := App (left associativity, at level 50).
adam@381 746 Infix "@+" := Plus (left associativity, at level 50).
adam@381 747 Notation "\ x : t , e" := (Abs (dom := t) (fun x => e))
adam@381 748 (no associativity, at level 51, x at level 0).
adam@381 749 Notation "[ e ]" := (fun _ => e).
adam@381 750
adam@381 751 Example Add : Term (Nat --> Nat --> Nat) :=
adam@381 752 [\x : Nat, \y : Nat, ^x @+ ^y].
adam@381 753
adam@381 754 Example Three_the_hard_way : Term Nat :=
adam@381 755 [Add _ @ #1 @ #2].
adam@381 756
adam@381 757 Eval compute in TermDenote Three_the_hard_way.
adam@381 758 (** %\vspace{-.15in}%[[
adam@381 759 = 3
adam@381 760 ]]
adam@381 761 *)
adam@381 762
adam@381 763 End HigherOrder.
adam@381 764
adam@381 765 (** 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. *)