Top

This file has been processed with:

ocamlorn --library stdlib.mli \ --library expr_larger.in.ml --input expr_larger.in.ml --lifting expr_larger.lif.ml \ > expr_larger.out.ml

A small interpreter

We will write an interpreter for a small programming language.

We first assume a few definitions to manipulate identifiers and environments

type id = Identifier type 'a list = Nil | Cons of 'a * 'a list type 'a option = None | Some of 'a type bool = True | False val equal : 'a -> 'a -> bool val fail : 'a -> 'b let assoc x l = match l with | Nil -> None | Cons ((y, v), l) -> (match equal x y with True -> Some v | False -> None) (* val assoc : 'a -> ('a * 'b) list -> 'b option *)

We start by writing the type of expressions for a language with asbtractions and tuples. We only consider one element tuples, single field, but just to make the example and the code shorter, and changing them to pairs would not raise any difficulty.

type expr = | Var of id | Abs of id * expr | App of expr * expr | Tup of expr | Proj of expr

Then, we write an evaluator for this type, using environments:

let rec eval env e = match e with | Var x -> assoc x env | Abs(x, f) -> Some (Abs(x, f)) | App(e1,e2) -> begin match eval env e1 with | Some (Tup _) -> None (* Type error *) | None -> None (* error propagation *) | Some (Abs(x,f)) -> begin match eval env e2 with | None -> None | Some v -> eval (Cons((x,v), env)) f end | Some _ -> fail () (* Not a value ?! *) end | Tup(e) -> begin match eval env e with | None -> None | Some v -> Some (Tup v) end | Proj(e) -> begin match eval env e with | None -> None (* error propagation *) | Some (Tup v) -> Some v | Some (Abs _) -> None (* Type error *) | Some _ -> fail () (* Not a value ?! *) end (* eval : (id * expr) list -> expr -> expr option *)

The evaluator distinguishes type (or scope) errors in the program, where it returns None, and internal errors when the expression returned by the evaluator is not a value. In this case, the evaluator raises an exception by calling fail ().

We should soon realize that we mistakenly implemented dynamic scoping: the result of evaluating an abstraction should not be an abstraction but a closure that holds the lexical environment of the abstraction.

This examples show how ornaments can be used to fix this problem, and use automatic transformations of the code as much as possible, leaving to the programmer just a small manual transformation to eventually fix the bug. Notice that fixing a but will always require a manual step, since the semantics of the base program cannot be changed by ornamentation alone.

Undoing our mistakes

In the current implementation, the expressions taken by the evaluator and the values it returns are not separated. Before we can fix the problem, we first implement this separation. For that purpose, we write a new datatype value of values

type value = | VAbs of id * expr | VTup of value

and a partial ornament that lifts abstractions and tupples to values and is undefined on other cases:

type ornament expr_value : expr => value with | Abs(x, e) => VAbs(x, e) | Tup(e) => VTup(e) when e : expr_value | Var(x) => ~ | App(e1,e2) => ~ | Proj(e) => ~

This ornament can be used to transform the evaluator to make explicit the fact that it only returns values:

let eval' = lifting eval : (id * expr_value) list -> expr -> expr_value option

We get the following program.

let rec eval' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VAbs(x, e)) | App(e1, e2) -> begin match eval' env e1 with | (None | Some (VTup _)) -> None | Some (VAbs(x, e)) -> begin match eval' env e2 with | None -> None | Some v -> eval' (Cons((x, v), env)) e end end | Tup e -> begin match eval' env e with | None -> None | Some e -> Some (VTup e) end | Proj e -> begin match eval' env e with | (None | Some (VAbs(_, _))) -> None | Some (VTup e) -> Some e end

Note that all fail () have been removed, automatically! This works because we are just making explicit an invariant that what implicit. In particular, the semantics has not been changed.

The next step is to change abstractions appearing in values to closure: we define a new type val' of where functions are represented as closures.

type value' = | VClosure' of id * (id * value') list * expr | VTup' of value'

To apply this transformation in the code mecanically, we define an ornament that renames VAbs to VClosure' and adds an environment:

type ornament value_value' : value => value' with | VAbs(x, e) => VClosure'(x, _, e) | VTup(v) => VTup'(v) when v : value_value'

Since, adding closure has an extra field, we expect the lifting of eval to be partial. The advanced programmer would see that there should be only one source of partiality which is the replacement of VAbs(x, e) by Vclosure' (x, _, e) in which case, the current environment env should fill the hole. Hence she may directly write

let eval'' = lifting eval' with ornament * <- value_value', @id patch #[env]

where * stand for every patch occurrence.

let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClosure'(x, env, e)) | App(e1, e2) -> begin match eval'' env e1 with | (None | Some (VTup' _)) -> None | Some (VClosure'(x, _, e)) -> begin match eval'' env e2 with | None -> None | Some v -> eval'' (Cons((x, v), env)) e end end | Tup e -> begin match eval'' env e with | None -> None | Some v -> Some (VTup' v) end | Proj e -> begin match eval'' env e with | (None | Some (VClosure'(_, _, _))) -> None | Some (VTup' v) -> Some v end

A prudent programmer may first ask for a partial lifting to see the occurrences where patches are needed:

let eval'' = lifting eval' with ornament * <- value_value', @id

As expected

let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClosure'(x, #48, e)) | App(e1, e2) -> begin match eval'' env e1 with | (None |Some (VTup' _)) -> None | Some (VClosure'(x, _, e)) -> begin match eval'' env e2 with | None -> None | Some v -> eval'' (Cons((x, v), env)) e end end | Tup e -> begin match eval'' env e with | None -> None | Some v -> Some (VTup' v) end | Proj e -> begin match eval'' env e with | (None |Some (VClosure'(_, _, _))) -> None | Some (VTup' v) -> Some v end

She can then write the patch that will fix the single hole #35 with env as done below. At this point, it is easying to imagine an interactive tool that would point her to the occurrence of the hole in the partial lifing code which she would fill with env and then automatically adapt the partial patch into the following code:

let eval'' = lifting eval' with ornament * <- value_value', @id patch #48[env]

Notice that env in this case, env is the only variable in context of the expected type. It does not mean that env is the only possible patch, but the obvious choice. Hence, an interactive tool could make the suggestion for us, which we would just need to confirm—or if we are quite confident, we could request such obvious patched to be automatically filled for us

let eval'' = lifting eval' with ornament * <- value_value', @id | * <- try obvious (* not implemented yet *)

Another solution, possibly more robust to changes in the base code, would be to use example-based code inference and write the following patch:

let eval'' = lifting eval' : (id * value_value') list -> expr -> value_value' option with | * <- try eval env (VAbs (_, _)) = Some (Closure (_, env, _)) (* Not implemented *)

In all cases, we get the following code:

let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClosure'(x, env, e)) | App(e1, e2) -> begin match eval'' env e1 with | (None | Some (VTup' _)) -> None | Some (VClosure'(x, _, e)) -> begin match eval'' env e2 with | None -> None | Some v -> eval'' (Cons((x, v), env)) e end end | Tup e -> begin match eval'' env e with | None -> None | Some v -> Some (VTup' v) end | Proj e -> begin match eval'' env e with | (None | Some (VClosure'(_, _, _))) -> None | Some (VTup' v) -> Some v end

We only used ornamentation so far. Therefore, we know the behaviour of the code has been preserved (even though we adding a new field). The final step to fix the bug has to change the semantics and must be done manually: instead of passing the dynamic environment to the code of a function, we pass the environment closure_env stored in the closure (line 10).

let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClosure'(x, env, e)) | App(e1, e2) -> begin match eval'' env e1 with | (None | Some (VTup' _)) -> None | Some (VClosure'(x, closure_env, e)) -> begin match eval'' env e2 with | None -> None | Some v -> eval'' (Cons((x, v), closure_env (* was env *) )) e end end | Tup e -> begin match eval'' env e with | None -> None | Some v -> Some (VTup' v) end | Proj e -> begin match eval'' env e with | (None | Some (VClosure'(_, _, _))) -> None | Some (VTup' v) -> Some v end

Another path

Another path is possible: we first define an enriched type of expressions that contain both applications and closures.

type expr' = | Var' of id | Abs' of id * expr' | Closure' of id * (id * expr') list * expr' | App' of expr' * expr' | Tup' of expr' | Proj' of expr'
type ornament expr_expr' : expr => expr' with | Var(x) => Var'(x) | Abs(x, e) => (Abs'(x, e) | Closure'(x,_,e)) when e : expr_expr' | App(e1, e2) => App'(e1, e2) when e1 e2 : expr_expr' | Tup(e) => Tup'(e) when e : expr_expr' | Proj(e) => Proj'(e) when e : expr_expr'

Then, we lift the eval function. We evaluating an Abs we choose to always construct a closure.

let eval' = lifting eval : (id * expr_expr') list -> expr_expr' -> expr_expr' option with ornament * <- @id patch #66[Right env]

We get the following output:

let rec eval' env e = match e with | Var' x -> assoc x env | Abs'(x, e) -> Some (Closure'(x, env, e)) | Closure'(x, _, e) -> Some (Closure'(x, env, e)) | App'(e1, e2) -> begin match eval' env e1 with | (None | Some (Tup' _)) -> None | Some (Abs'(x, e)) -> begin match eval' env e2 with | None -> None | Some v -> eval' (Cons((x, v), env)) e end | Some (Closure'(x, _, e)) -> begin match eval' env e2 with | None -> None | Some v -> eval' (Cons((x, v), env)) e end | ((Some (Var' _) | Some (App'(_, _))) | Some (Proj' _)) -> fail () end | Tup' e -> begin match eval' env e with | None -> None | Some e -> Some (Tup' e) end | Proj' e -> begin match eval' env e with | ((None | Some (Abs'(_, _))) | Some (Closure'(_, _, _))) -> None | Some (Tup' e) -> Some e | ((Some (Var' _) | Some (App'(_, _))) | Some (Proj' _)) -> fail () end

We can then manually edit the relevant case (line 17):

let rec eval' env e = match e with | Var' x -> assoc x env | Abs'(x, e) -> Some (Closure'(x, env, e)) | Closure'(x, _, e) -> Some (Closure'(x, env, e)) | App'(e1, e2) -> begin match eval' env e1 with | (None | Some (Tup' _)) -> None | Some (Var' _) -> fail () | Some (Abs'(x, e)) -> begin match eval' env e2 with | None -> None | Some v -> eval' (Cons((x, v), env)) e end | Some (Closure'(x, closure_env, e)) -> begin match eval' env e2 with | None -> None | Some v -> eval' (Cons((x, v), closure_env (* was env *))) e end | Some (App'(_, _)) -> fail () | Some (Proj' _) -> fail () end | Tup' e -> begin match eval' env e with | None -> None | Some e -> Some (Tup' e) end | Proj' e -> begin match eval' env e with | ((None | Some (Abs'(_, _))) | Some (Closure'(_, _, _))) -> None | Some (Var' _) -> fail () | Some (App'(_, _)) -> fail () | Some (Tup' e) -> Some e | Some (Proj' _) -> fail () end

Finally, we can cleanup by separating expressions and values:

type ornament expr'_expr : expr' => expr with | Var'(x) => Var(x) | Abs'(x,e) => Abs(x,e) when e : expr'_expr | App'(e1,e2) => App(e1,e2) when e1 e2 : expr'_expr | Tup'(e) => Tup(e) when e : expr'_expr | Proj'(e) => Proj(e) when e : expr'_expr | Closure'(x,env,e) => ~ when e : expr'_expr type ornament expr'_value' : expr' => value' with | Abs'(x, e) => ~ when e : expr'_expr | Closure'(x,env,e) => VClosure'(x,env,e) when env : (id * expr'_value') list, e : expr'_expr | Tup'(e) => VTup'(e) when e : expr'_value' | Var'(x) => ~ | App'(e1,e2) => ~ | Proj'(e) => ~

And apply the refactoring:

let eval'' = lifting eval' : (id * expr'_value') list -> expr'_expr -> expr'_value' option

We again get the desired program:

let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClosure'(x, env, e)) | App(e1, e2) -> begin match eval'' env e1 with | (None | Some (VTup' _)) -> None | Some (VClosure'(x, env1, e)) -> begin match eval'' env e2 with | None -> None | Some v -> eval'' (Cons((x, v), env1)) e end end | Tup e -> begin match eval'' env e with | None -> None | Some e -> Some (VTup' e) end | Proj e -> begin match eval'' env e with | (None | Some (VClosure'(_, _, _))) -> None | Some (VTup' e) -> Some e end