This has been processed with:

ocamlorn --library stdlib.mli \ --library expr_smaller.in.ml --input expr_smaller.in.ml --lifting expr_smaller.lif.ml \ > expr_smaller.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 *)
let bind x f = match x with Some v -> f v | None -> None
(* val bind : 'a option -> ('a -> 'b option) -> 'b option *) |

Notice that `assoc`

returns an `'a option`

to avoid raising a
`Not_found`

exception. The fonction `bind`

is used to sequence
computations over a value of an "option" type. We also have a more verbose
version of this example where `bind`

has been
inlined.

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) ->
bind (eval env e1) (fun v -> match v with
| Abs(x,f) ->
bind (eval env e2) (fun v -> eval (Cons((x,v), env)) f)
| Tup _ -> None (* Type error *)
| _ -> fail () (* Not a value ?! *)
)
| Tup(e) ->
bind (eval env e) (fun v -> Some (Tup v))
| Proj(e) ->
bind (eval env e) (fun v -> match v with
| Tup v -> Some v
| Abs _ -> None (* Type error *)
| _ -> fail () (* Not a value ?! *)
)
(* val 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) => ~ |

Using this ornament, we can make apparent that the evaluator only returns values, instead of leaving the invariant implicit:

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) -> bind (eval' env e1) (fun v -> match v with | VAbs(x, e) -> bind (eval' env e2) (fun v -> eval' (Cons((x, v), env)) e) | VTup _ -> None) | Tup e -> bind (eval' env e) (fun v -> Some (VTup v)) | Proj e -> bind (eval' env e) (fun v -> match v with | VAbs(_, _) -> None | VTup e -> Some e) |

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' = | VClos' 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 `VClos'`

and adds an environment:

type ornament value_value' : value => value' with | VAbs(x, e) => VClos'(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 they 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 (VClos'(x, env, e)) | App(e1, e2) -> bind (eval'' env e1) (fun v -> match v with | VClos'(x, _, e) -> bind (eval'' env e2) (fun v -> eval'' (Cons((x, v), env)) e) | VTup' _ -> None) | Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v)) | Proj e -> bind (eval'' env e) (fun v -> match v with | VClos'(_, _, _) -> None | VTup' v -> Some v) |

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, there is one hole:

let rec eval'' env e = match e with | Var x -> assoc x env | Abs(x, e) -> Some (VClos'(x, #37, e)) | App(e1, e2) -> bind (eval'' env e1) (fun v -> match v with | VClos'(x, _, e) -> bind (eval'' env e2) (fun v -> eval'' (Cons((x, v), env)) e) | VTup' _ -> None) | Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v)) | Proj e -> bind (eval'' env e) (fun v -> match v with | VClos'(_, _, _) -> None | VTup' v -> Some v) |

The programmer can then write the patch that will fix the single hole `#30`

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 | #37 <- 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
(* This feature is 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, _))
(* This feature is not implemented yet *) |

In all cases, we shall get the following code:

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

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 (VClos'(x, env, e))
| App(e1, e2) ->
bind (eval'' env e1)
(fun v ->
match v with
| VClos'(x, closure_env, e) ->
bind (eval'' env e2)
(fun v -> eval'' (Cons((x, v), closure_env (* was env *))) e)
| VTup' _ -> None)
| Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v))
| Proj e ->
bind (eval'' env e)
(fun v ->
match v with
| VClos'(_, _, _) -> None
| VTup' v -> Some v) |

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) -> bind (eval' env e1) (fun v -> match v with | ((Var' _ | App'(_, _)) | Proj' _) -> fail () | Abs'(x, e) -> bind (eval' env e2) (fun v -> eval' (Cons((x, v), env)) e) | Closure'(x, _, e) -> bind (eval' env e2) (fun v -> eval' (Cons((x, v), env)) e) | Tup' _ -> None) | Tup' e -> bind (eval' env e) (fun v -> Some (Tup' v)) | Proj' e -> bind (eval' env e) (fun v -> match v with | ((Var' _ | App'(_, _)) | Proj' _) -> fail () | (Abs'(_, _) | Closure'(_, _, _)) -> None | Tup' e -> Some e) |

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) ->
bind (eval' env e1)
(fun v ->
match v with
| Var' _ -> fail ()
| Abs'(x, e) ->
bind (eval' env e2)
(fun v -> eval' (Cons((x, v), env)) e)
| Closure'(x, closure_env, e) ->
bind (eval' env e2)
(fun v -> eval' (Cons((x, v), closure_env (* was env *))) e)
| App'(_, _) -> fail ()
| Tup' _ -> None
| Proj' _ -> fail ())
| Tup' e ->
bind (eval' env e) (fun v -> Some (Tup' v))
| Proj' e ->
bind (eval' env e)
(fun v ->
match v with
| Var' _ -> fail ()
| (Abs'(_, _) |Closure'(_, _, _)) -> None
| App'(_, _) -> fail ()
| Tup' e -> Some e
| Proj' _ -> fail ()) |

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) => VClos'(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 (VClos'(x, env, e)) | App(e1, e2) -> bind (eval'' env e1) (fun v -> match v with | VClos'(x, env1, e) -> bind (eval'' env e2) (fun v -> eval'' (Cons((x, v), env1)) e) | VTup' _ -> None) | Tup e -> bind (eval'' env e) (fun v -> Some (VTup' v)) | Proj e -> bind (eval'' env e) (fun v -> match v with | VClos'(_, _, _) -> None | VTup' e -> Some e) |