Top

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

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 *) 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.

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) => ~

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

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)