Mercurial > cpdt > repo
comparison src/Hoas.v @ 253:0d77577e5ac0
PHOAS intro section
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 16 Dec 2009 11:33:53 -0500 |
parents | 3c4ed57c9907 |
children | e3c3b7ef5901 |
comparison
equal
deleted
inserted
replaced
252:3c4ed57c9907 | 253:0d77577e5ac0 |
---|---|
116 (** However, it is still impossible to write a function to compute the size of an expression. We would still need to manufacture a value of type [var] to peer under a binder, and that is impossible, because [var] is an abstract type. *) | 116 (** However, it is still impossible to write a function to compute the size of an expression. We would still need to manufacture a value of type [var] to peer under a binder, and that is impossible, because [var] is an abstract type. *) |
117 | 117 |
118 | 118 |
119 (** * Parametric HOAS *) | 119 (** * Parametric HOAS *) |
120 | 120 |
121 (** In the context of Haskell, Washburn and Weirich introduced a technique called %\emph{%#<i>#parametric HOAS#</i>#%}%, or PHOAS. By making a slight alteration in the spirit of weak HOAS, we arrive at an encoding that addresses all three of the complaints above: the encoding is legal in Coq, exotic terms are impossible, and it is possible to write any syntax-deconstructing function that we can write with first-order encodings. The last of these advantages is not even present with HOAS in Twelf. In a sense, we receive it in exchange for giving up a free implementation of capture-avoiding substitution. | |
122 | |
123 The first step is to change the weak HOAS type so that [var] is a variable inside a section, rather than a global parameter. *) | |
124 | |
125 Reset uexp. | |
126 | |
127 Section uexp. | |
128 Variable var : Set. | |
129 | |
130 Inductive uexp : Set := | |
131 | UVar : var -> uexp | |
132 | UApp : uexp -> uexp -> uexp | |
133 | UAbs : (var -> uexp) -> uexp. | |
134 End uexp. | |
135 | |
136 (** Next, we can encapsulate choices of [var] inside a polymorphic function type. *) | |
137 | |
138 Definition Uexp := forall var, uexp var. | |
139 | |
140 (** This type [Uexp] is our final, exotic-term-free representation of lambda terms. Inside the body of a [Uexp] function, [var] values may not be deconstructed illegaly, for much the same reason as with weak HOAS. We simply trade an abstract type for parametric polymorphism. | |
141 | |
142 Our running example $\lambda x. \; x \; x$#<tt>\x. x x</tt># is easily expressed: *) | |
143 | |
144 Example self_app : Uexp := fun var => UAbs (var := var) | |
145 (fun x : var => UApp (var := var) (UVar (var := var) x) (UVar (var := var) x)). | |
146 | |
147 (** Including all mentions of [var] explicitly helps clarify what is happening here, but it is convenient to let Coq's local type inference fill in these occurrences for us. *) | |
148 | |
149 Example self_app' : Uexp := fun _ => UAbs (fun x => UApp (UVar x) (UVar x)). | |
150 | |
151 (** We can go further and apply the PHOAS technique to dependently-typed ASTs, where Gallina typing guarantees that only well-typed terms can be represented. For the rest of this chapter, we consider the example of simply-typed lambda calculus with natural numbers and addition. We start with a conventional definition of the type language. *) | |
152 | |
121 Inductive type : Type := | 153 Inductive type : Type := |
122 | Nat : type | 154 | Nat : type |
123 | Arrow : type -> type -> type. | 155 | Arrow : type -> type -> type. |
124 | 156 |
125 Infix "-->" := Arrow (right associativity, at level 60). | 157 Infix "-->" := Arrow (right associativity, at level 60). |
158 | |
159 (** Our definition of the expression type follows the definition for untyped lambda calculus, with one important change. Now our section variable [var] is not just a type. Rather, it is a %\textit{%#<i>#function#</i>#%}% returning types. The idea is that a variable of object language type [t] is represented by a [var t]. Note how this enables us to avoid indexing the [exp] type with a representation of typing contexts. *) | |
126 | 160 |
127 Section exp. | 161 Section exp. |
128 Variable var : type -> Type. | 162 Variable var : type -> Type. |
129 | 163 |
130 Inductive exp : type -> Type := | 164 Inductive exp : type -> Type := |
138 | 172 |
139 Implicit Arguments Const' [var]. | 173 Implicit Arguments Const' [var]. |
140 Implicit Arguments Var [var t]. | 174 Implicit Arguments Var [var t]. |
141 Implicit Arguments Abs' [var dom ran]. | 175 Implicit Arguments Abs' [var dom ran]. |
142 | 176 |
177 (** Our final representation type wraps [exp] as before. *) | |
178 | |
143 Definition Exp t := forall var, exp var t. | 179 Definition Exp t := forall var, exp var t. |
180 | |
144 (* begin thide *) | 181 (* begin thide *) |
145 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2. | 182 |
183 (** We can define some smart constructors to make it easier to build [Exp]s without using polymorphism explicitly. *) | |
146 | 184 |
147 Definition Const (n : nat) : Exp Nat := | 185 Definition Const (n : nat) : Exp Nat := |
148 fun _ => Const' n. | 186 fun _ => Const' n. |
149 Definition Plus (E1 E2 : Exp Nat) : Exp Nat := | 187 Definition Plus (E1 E2 : Exp Nat) : Exp Nat := |
150 fun _ => Plus' (E1 _) (E2 _). | 188 fun _ => Plus' (E1 _) (E2 _). |
151 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran := | 189 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran := |
152 fun _ => App' (F _) (X _). | 190 fun _ => App' (F _) (X _). |
191 | |
192 (** A case for function abstraction is not as natural, but we can implement one candidate in terms of a type family [Exp1], such that [Exp1 free result] represents an expression of type [result] with one free variable of type [free]. *) | |
193 | |
194 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2. | |
153 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) := | 195 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) := |
154 fun _ => Abs' (B _). | 196 fun _ => Abs' (B _). |
155 (* end thide *) | 197 (* end thide *) |
156 | 198 |
157 (* EX: Define appropriate shorthands, so that these definitions type-check. *) | 199 (* EX: Define appropriate shorthands, so that these definitions type-check. *) |
158 | 200 |
159 Definition zero := Const 0. | 201 (** Now it is easy to encode a number of example programs. *) |
160 Definition one := Const 1. | 202 |
161 Definition one_again := Plus zero one. | 203 Example zero := Const 0. |
162 Definition ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X). | 204 Example one := Const 1. |
163 Definition app_ident := App ident one_again. | 205 Example one_again := Plus zero one. |
164 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => | 206 Example ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X). |
207 Example app_ident := App ident one_again. | |
208 Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => | |
165 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))). | 209 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))). |
166 Definition app_ident' := App (App app ident) one_again. | 210 Example app_ident' := App (App app ident) one_again. |
167 | 211 |
168 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *) | 212 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *) |
213 | |
214 (** We can write syntax-deconstructing functions, such as [CountVars], which counts how many [Var] nodes appear in an [Exp]. First, we write a version [countVars] for [exp]s. The main trick is to specialize [countVars] to work over expressions where [var] is instantiated as [fun _ => unit]. That is, every variable is just a value of type [unit], such that variables carry no information. The important thing is that we have a value [tt] of type [unit] available, to use in descending into binders. *) | |
169 | 215 |
170 (* begin thide *) | 216 (* begin thide *) |
171 Fixpoint countVars t (e : exp (fun _ => unit) t) : nat := | 217 Fixpoint countVars t (e : exp (fun _ => unit) t) : nat := |
172 match e with | 218 match e with |
173 | Const' _ => 0 | 219 | Const' _ => 0 |
175 | Var _ _ => 1 | 221 | Var _ _ => 1 |
176 | App' _ _ e1 e2 => countVars e1 + countVars e2 | 222 | App' _ _ e1 e2 => countVars e1 + countVars e2 |
177 | Abs' _ _ e' => countVars (e' tt) | 223 | Abs' _ _ e' => countVars (e' tt) |
178 end. | 224 end. |
179 | 225 |
226 (** We turn [countVars] into [CountVars] with explicit instantiation of a polymorphic [Exp] value [E]. We can write an underscore for the paramter to [E], because local type inference is able to infer the proper value. *) | |
227 | |
180 Definition CountVars t (E : Exp t) : nat := countVars (E _). | 228 Definition CountVars t (E : Exp t) : nat := countVars (E _). |
181 (* end thide *) | 229 (* end thide *) |
182 | 230 |
231 (** A few evaluations establish that [CountVars] behaves plausibly. *) | |
232 | |
183 Eval compute in CountVars zero. | 233 Eval compute in CountVars zero. |
234 (** %\vspace{-.15in}% [[ | |
235 = 0 | |
236 : nat | |
237 ]] *) | |
238 | |
184 Eval compute in CountVars one. | 239 Eval compute in CountVars one. |
240 (** %\vspace{-.15in}% [[ | |
241 = 0 | |
242 : nat | |
243 ]] *) | |
244 | |
185 Eval compute in CountVars one_again. | 245 Eval compute in CountVars one_again. |
246 (** %\vspace{-.15in}% [[ | |
247 = 0 | |
248 : nat | |
249 ]] *) | |
250 | |
186 Eval compute in CountVars ident. | 251 Eval compute in CountVars ident. |
252 (** %\vspace{-.15in}% [[ | |
253 = 1 | |
254 : nat | |
255 ]] *) | |
256 | |
187 Eval compute in CountVars app_ident. | 257 Eval compute in CountVars app_ident. |
258 (** %\vspace{-.15in}% [[ | |
259 = 1 | |
260 : nat | |
261 ]] *) | |
262 | |
188 Eval compute in CountVars app. | 263 Eval compute in CountVars app. |
264 (** %\vspace{-.15in}% [[ | |
265 = 2 | |
266 : nat | |
267 ]] *) | |
268 | |
189 Eval compute in CountVars app_ident'. | 269 Eval compute in CountVars app_ident'. |
270 (** %\vspace{-.15in}% [[ | |
271 = 3 | |
272 : nat | |
273 ]] *) | |
274 | |
190 | 275 |
191 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *) | 276 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *) |
277 | |
278 (** We might want to go further and count occurrences of a single distinguished free variable in an expression. In this case, it is useful to instantiate [var] as [fun _ => bool]. We will represent the distinguished variable with [true] and all other variables with [false]. *) | |
192 | 279 |
193 (* begin thide *) | 280 (* begin thide *) |
194 Fixpoint countOne t (e : exp (fun _ => bool) t) : nat := | 281 Fixpoint countOne t (e : exp (fun _ => bool) t) : nat := |
195 match e with | 282 match e with |
196 | Const' _ => 0 | 283 | Const' _ => 0 |
199 | Var _ false => 0 | 286 | Var _ false => 0 |
200 | App' _ _ e1 e2 => countOne e1 + countOne e2 | 287 | App' _ _ e1 e2 => countOne e1 + countOne e2 |
201 | Abs' _ _ e' => countOne (e' false) | 288 | Abs' _ _ e' => countOne (e' false) |
202 end. | 289 end. |
203 | 290 |
291 (** We wrap [countOne] into [CountOne], which we type using the [Exp1] definition from before. [CountOne] operates on an expression [E] with a single free variable. We apply an instantiated [E] to [true] to mark this variable as the one [countOne] should look for. [countOne] itself is careful to instantiate all other variables with [false]. *) | |
292 | |
204 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat := | 293 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat := |
205 countOne (E _ true). | 294 countOne (E _ true). |
206 (* end thide *) | 295 (* end thide *) |
207 | 296 |
208 Definition ident1 : Exp1 Nat Nat := fun _ X => Var X. | 297 (** We can check the behavior of [CountOne] on a few examples. *) |
209 Definition add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X). | 298 |
210 Definition app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0). | 299 Example ident1 : Exp1 Nat Nat := fun _ X => Var X. |
211 Definition app_ident1 : Exp1 Nat Nat := fun _ X => App' (Abs' (fun Y => Var Y)) (Var X). | 300 Example add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X). |
301 Example app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0). | |
302 Example app_ident1 : Exp1 Nat Nat := fun _ X => | |
303 App' (Abs' (fun Y => Var Y)) (Var X). | |
212 | 304 |
213 Eval compute in CountOne ident1. | 305 Eval compute in CountOne ident1. |
306 (** %\vspace{-.15in}% [[ | |
307 = 1 | |
308 : nat | |
309 ]] *) | |
310 | |
214 Eval compute in CountOne add_self. | 311 Eval compute in CountOne add_self. |
312 (** %\vspace{-.15in}% [[ | |
313 = 2 | |
314 : nat | |
315 ]] *) | |
316 | |
215 Eval compute in CountOne app_zero. | 317 Eval compute in CountOne app_zero. |
318 (** %\vspace{-.15in}% [[ | |
319 = 1 | |
320 : nat | |
321 ]] *) | |
322 | |
216 Eval compute in CountOne app_ident1. | 323 Eval compute in CountOne app_ident1. |
324 (** %\vspace{-.15in}% [[ | |
325 = 1 | |
326 : nat | |
327 ]] *) | |
328 | |
217 | 329 |
218 (* EX: Define a function to pretty-print [Exp]s as strings. *) | 330 (* EX: Define a function to pretty-print [Exp]s as strings. *) |
331 | |
332 (** The PHOAS encoding turns out to be just as general as the first-order encodings we saw previously. To provide a taste of that generality, we implement a translation into concrete syntax, rendered in human-readable strings. This is as easy as representing variables as strings. *) | |
219 | 333 |
220 (* begin thide *) | 334 (* begin thide *) |
221 Section ToString. | 335 Section ToString. |
222 Open Scope string_scope. | 336 Open Scope string_scope. |
223 | 337 |
224 Fixpoint natToString (n : nat) : string := | 338 Fixpoint natToString (n : nat) : string := |
225 match n with | 339 match n with |
226 | O => "O" | 340 | O => "O" |
227 | S n' => "S(" ++ natToString n' ++ ")" | 341 | S n' => "S(" ++ natToString n' ++ ")" |
228 end. | 342 end. |
343 | |
344 (** Function [toString] takes an extra argument [cur], which holds the last variable name assigned to a binder. We build new variable names by extending [cur] with primes. The function returns a pair of the next available variable name and of the actual expression rendering. *) | |
229 | 345 |
230 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string := | 346 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string := |
231 match e with | 347 match e with |
232 | Const' n => (cur, natToString n) | 348 | Const' n => (cur, natToString n) |
233 | Plus' e1 e2 => | 349 | Plus' e1 e2 => |
247 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x"). | 363 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x"). |
248 End ToString. | 364 End ToString. |
249 (* end thide *) | 365 (* end thide *) |
250 | 366 |
251 Eval compute in ToString zero. | 367 Eval compute in ToString zero. |
368 (** %\vspace{-.15in}% [[ | |
369 = "O"%string | |
370 : string | |
371 ]] *) | |
372 | |
252 Eval compute in ToString one. | 373 Eval compute in ToString one. |
374 (** %\vspace{-.15in}% [[ | |
375 = "S(O)"%string | |
376 : string | |
377 ]] *) | |
378 | |
253 Eval compute in ToString one_again. | 379 Eval compute in ToString one_again. |
380 (** %\vspace{-.15in}% [[ | |
381 = "(O) + (S(O))"%string | |
382 : string | |
383 ]] *) | |
384 | |
254 Eval compute in ToString ident. | 385 Eval compute in ToString ident. |
386 (** %\vspace{-.15in}% [[ | |
387 = "(\x, x)"%string | |
388 : string | |
389 ]] *) | |
390 | |
255 Eval compute in ToString app_ident. | 391 Eval compute in ToString app_ident. |
392 (** %\vspace{-.15in}% [[ | |
393 = "((\x, x)) ((O) + (S(O)))"%string | |
394 : string | |
395 ]] *) | |
396 | |
256 Eval compute in ToString app. | 397 Eval compute in ToString app. |
398 (** %\vspace{-.15in}% [[ | |
399 = "(\x, (\x', (x) (x')))"%string | |
400 : string | |
401 ]] *) | |
402 | |
257 Eval compute in ToString app_ident'. | 403 Eval compute in ToString app_ident'. |
404 (** %\vspace{-.15in}% [[ | |
405 = "(((\x, (\x', (x) (x')))) ((\x'', x''))) ((O) + (S(O)))"%string | |
406 : string | |
407 ]] *) | |
408 | |
258 | 409 |
259 (* EX: Define a substitution function. *) | 410 (* EX: Define a substitution function. *) |
411 | |
412 (** Our final example is crucial to using PHOAS to encode standard operational semantics. We define capture-avoiding substitution, in terms of a function [flatten] which takes in an expression that represents variables as expressions. [flatten] replaces every node [Var e] with [e]. *) | |
260 | 413 |
261 (* begin thide *) | 414 (* begin thide *) |
262 Section flatten. | 415 Section flatten. |
263 Variable var : type -> Type. | 416 Variable var : type -> Type. |
264 | 417 |
270 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2) | 423 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2) |
271 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x))) | 424 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x))) |
272 end. | 425 end. |
273 End flatten. | 426 End flatten. |
274 | 427 |
428 (** Flattening turns out to implement the heart of substitution. We apply [E2], which has one free variable, to [E1], replacing the occurrences of the free variable by copies of [E1]. [flatten] takes care of removing the extra [Var] applications around these copies. *) | |
429 | |
275 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ => | 430 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ => |
276 flatten (E2 _ (E1 _)). | 431 flatten (E2 _ (E1 _)). |
277 (* end thide *) | 432 (* end thide *) |
278 | 433 |
279 Eval compute in Subst one ident1. | 434 Eval compute in Subst one ident1. |
435 (** %\vspace{-.15in}% [[ | |
436 = fun var : type -> Type => Const' 1 | |
437 : Exp Nat | |
438 ]] *) | |
439 | |
280 Eval compute in Subst one add_self. | 440 Eval compute in Subst one add_self. |
441 (** %\vspace{-.15in}% [[ | |
442 = fun var : type -> Type => Plus' (Const' 1) (Const' 1) | |
443 : Exp Nat | |
444 ]] *) | |
445 | |
281 Eval compute in Subst ident app_zero. | 446 Eval compute in Subst ident app_zero. |
447 (** %\vspace{-.15in}% [[ | |
448 = fun var : type -> Type => | |
449 App' (Abs' (fun X : var Nat => Var X)) (Const' 0) | |
450 : Exp Nat | |
451 ]] *) | |
452 | |
282 Eval compute in Subst one app_ident1. | 453 Eval compute in Subst one app_ident1. |
454 (** %\vspace{-.15in}% [[ | |
455 = fun var : type -> Type => | |
456 App' (Abs' (fun x : var Nat => Var x)) (Const' 1) | |
457 : Exp Nat | |
458 ]] *) | |
283 | 459 |
284 | 460 |
285 (** * A Type Soundness Proof *) | 461 (** * A Type Soundness Proof *) |
286 | 462 |
287 Reserved Notation "E1 ==> E2" (no associativity, at level 90). | 463 Reserved Notation "E1 ==> E2" (no associativity, at level 90). |