Certified Programming with Dependent Types: src/Hoas.v comparison

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

-:3c4ed57c9907
+:0d77577e5ac0
 (** 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. *)
 (** * Parametric HOAS *)
+(** 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.
+The first step is to change the weak HOAS type so that [var] is a variable inside a section, rather than a global parameter. *)
+Reset uexp.
+Section uexp.
+Variable var : Set.
+Inductive uexp : Set :=
+| UVar : var -> uexp
+| UApp : uexp -> uexp -> uexp
+| UAbs : (var -> uexp) -> uexp.
+End uexp.
+(** Next, we can encapsulate choices of [var] inside a polymorphic function type. *)
+Definition Uexp := forall var, uexp var.
+(** 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.
+Our running example $\lambda x. \; x \; x$#<tt>\x. x x</tt># is easily expressed: *)
+Example self_app : Uexp := fun var => UAbs (var := var)
+(fun x : var => UApp (var := var) (UVar (var := var) x) (UVar (var := var) x)).
+(** 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. *)
+Example self_app' : Uexp := fun _ => UAbs (fun x => UApp (UVar x) (UVar x)).
+(** 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. *)
 Inductive type : Type :=
 | Nat : type
 | Arrow : type -> type -> type.
 Infix "-->" := Arrow (right associativity, at level 60).
+(** 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. *)
 Section exp.
 Variable var : type -> Type.
 Inductive exp : type -> Type :=
 Implicit Arguments Const' [var].
 Implicit Arguments Var [var t].
 Implicit Arguments Abs' [var dom ran].
+(** Our final representation type wraps [exp] as before. *)
 Definition Exp t := forall var, exp var t.
 (* begin thide *)
-Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
+(** We can define some smart constructors to make it easier to build [Exp]s without using polymorphism explicitly. *)
 Definition Const (n : nat) : Exp Nat :=
 fun _ => Const' n.
 Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
 fun _ => Plus' (E1 _) (E2 _).
 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
 fun _ => App' (F _) (X _).
+(** 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]. *)
+Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
 fun _ => Abs' (B _).
 (* end thide *)
 (* EX: Define appropriate shorthands, so that these definitions type-check. *)
-Definition zero := Const 0.
+(** Now it is easy to encode a number of example programs. *)
-Definition one := Const 1.
-Definition one_again := Plus zero one.
+Example zero := Const 0.
-Definition ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X).
+Example one := Const 1.
-Definition app_ident := App ident one_again.
+Example one_again := Plus zero one.
-Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
+Example ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X).
+Example app_ident := App ident one_again.
+Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))).
-Definition app_ident' := App (App app ident) one_again.
+Example app_ident' := App (App app ident) one_again.
 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *)
+(** 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. *)
 (* begin thide *)
 Fixpoint countVars t (e : exp (fun _ => unit) t) : nat :=
 match e with
 | Const' _ => 0
 | Var _ _ => 1
 | App' _ _ e1 e2 => countVars e1 + countVars e2
 | Abs' _ _ e' => countVars (e' tt)
 end.
+(** 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. *)
 Definition CountVars t (E : Exp t) : nat := countVars (E _).
 (* end thide *)
+(** A few evaluations establish that [CountVars] behaves plausibly. *)
 Eval compute in CountVars zero.
+(** %\vspace{-.15in}% [[
+= 0
+: nat
+]] *)
 Eval compute in CountVars one.
+(** %\vspace{-.15in}% [[
+= 0
+: nat
+]] *)
 Eval compute in CountVars one_again.
+(** %\vspace{-.15in}% [[
+= 0
+: nat
+]] *)
 Eval compute in CountVars ident.
+(** %\vspace{-.15in}% [[
+= 1
+: nat
+]] *)
 Eval compute in CountVars app_ident.
+(** %\vspace{-.15in}% [[
+= 1
+: nat
+]] *)
 Eval compute in CountVars app.
+(** %\vspace{-.15in}% [[
+= 2
+: nat
+]] *)
 Eval compute in CountVars app_ident'.
+(** %\vspace{-.15in}% [[
+= 3
+: nat
+]] *)
 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *)
+(** 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]. *)
 (* begin thide *)
 Fixpoint countOne t (e : exp (fun _ => bool) t) : nat :=
 match e with
 | Const' _ => 0
 | Var _ false => 0
 | App' _ _ e1 e2 => countOne e1 + countOne e2
 | Abs' _ _ e' => countOne (e' false)
 end.
+(** 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]. *)
 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat :=
 countOne (E _ true).
 (* end thide *)
-Definition ident1 : Exp1 Nat Nat := fun _ X => Var X.
+(** We can check the behavior of [CountOne] on a few examples. *)
-Definition add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X).
-Definition app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0).
+Example ident1 : Exp1 Nat Nat := fun _ X => Var X.
-Definition app_ident1 : Exp1 Nat Nat := fun _ X => App' (Abs' (fun Y => Var Y)) (Var X).
+Example add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X).
+Example app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0).
+Example app_ident1 : Exp1 Nat Nat := fun _ X =>
+App' (Abs' (fun Y => Var Y)) (Var X).
 Eval compute in CountOne ident1.
+(** %\vspace{-.15in}% [[
+= 1
+: nat
+]] *)
 Eval compute in CountOne add_self.
+(** %\vspace{-.15in}% [[
+= 2
+: nat
+]] *)
 Eval compute in CountOne app_zero.
+(** %\vspace{-.15in}% [[
+= 1
+: nat
+]] *)
 Eval compute in CountOne app_ident1.
+(** %\vspace{-.15in}% [[
+= 1
+: nat
+]] *)
 (* EX: Define a function to pretty-print [Exp]s as strings. *)
+(** 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. *)
 (* begin thide *)
 Section ToString.
 Open Scope string_scope.
 Fixpoint natToString (n : nat) : string :=
 match n with
 | O => "O"
 | S n' => "S(" ++ natToString n' ++ ")"
 end.
+(** 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. *)
 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string :=
 match e with
 | Const' n => (cur, natToString n)
 | Plus' e1 e2 =>
 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x").
 End ToString.
 (* end thide *)
 Eval compute in ToString zero.
+(** %\vspace{-.15in}% [[
+= "O"%string
+: string
+]] *)
 Eval compute in ToString one.
+(** %\vspace{-.15in}% [[
+= "S(O)"%string
+: string
+]] *)
 Eval compute in ToString one_again.
+(** %\vspace{-.15in}% [[
+= "(O) + (S(O))"%string
+: string
+]] *)
 Eval compute in ToString ident.
+(** %\vspace{-.15in}% [[
+= "(\x, x)"%string
+: string
+]] *)
 Eval compute in ToString app_ident.
+(** %\vspace{-.15in}% [[
+= "((\x, x)) ((O) + (S(O)))"%string
+: string
+]] *)
 Eval compute in ToString app.
+(** %\vspace{-.15in}% [[
+= "(\x, (\x', (x) (x')))"%string
+: string
+]] *)
 Eval compute in ToString app_ident'.
+(** %\vspace{-.15in}% [[
+= "(((\x, (\x', (x) (x')))) ((\x'', x''))) ((O) + (S(O)))"%string
+: string
+]] *)
 (* EX: Define a substitution function. *)
+(** 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]. *)
 (* begin thide *)
 Section flatten.
 Variable var : type -> Type.
 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
 end.
 End flatten.
+(** 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. *)
 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
 flatten (E2 _ (E1 _)).
 (* end thide *)
 Eval compute in Subst one ident1.
+(** %\vspace{-.15in}% [[
+= fun var : type -> Type => Const' 1
+: Exp Nat
+]] *)
 Eval compute in Subst one add_self.
+(** %\vspace{-.15in}% [[
+= fun var : type -> Type => Plus' (Const' 1) (Const' 1)
+: Exp Nat
+]] *)
 Eval compute in Subst ident app_zero.
+(** %\vspace{-.15in}% [[
+= fun var : type -> Type =>
+App' (Abs' (fun X : var Nat => Var X)) (Const' 0)
+: Exp Nat
+]] *)
 Eval compute in Subst one app_ident1.
+(** %\vspace{-.15in}% [[
+= fun var : type -> Type =>
+App' (Abs' (fun x : var Nat => Var x)) (Const' 1)
+: Exp Nat
+]] *)
 (** * A Type Soundness Proof *)
 Reserved Notation "E1 ==> E2" (no associativity, at level 90).

Mercurial > cpdt > repo

comparison src/Hoas.v @ 253:0d77577e5ac0