This 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 |
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 (Abs(x,f)) -> begin match eval env e2 with | Some v -> eval (Cons((x,v), env)) f | None -> None end | Some (Tup _) -> None (* Type error *) | None -> None (* error propagation *) | Some _ -> fail () (* Not a value ?! *) end | Tup(e) -> begin match eval env e with | Some v -> Some (Tup v) | None -> None end | Proj(e) -> begin match eval env e with | Some (Tup v) -> Some v | Some (Abs _) -> None (* Type error *) | None -> None (* error propagation *) | 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.
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 | * <- 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, #35, 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 | #35 <- 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 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 | #51 <- Right env |
We get the following output:
| let rec eval' env e = match e with | Var' x -> assoc x env | (Abs'(x, e) | Closure'(x, _, e)) -> Some (Closure'(x, env, e)) | App'(e1, e2) -> begin match eval' env e1 with | (None | Some (Tup' _)) -> None | ((Some (Var' _) | Some (App'(_, _))) | Some (Proj' _)) -> 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, _, 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 (Tup' e) end | Proj' e -> begin match eval' env e with | ((None | Some (Abs'(_, _))) | Some (Closure'(_, _, _))) -> None | ((Some (Var' _) | Some (App'(_, _))) | Some (Proj' _)) -> fail () | Some (Tup' e) -> Some e 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 |