Top

This file has been processed with:

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

Refactoring expressions, with higher-order syntax

Let us enrich the example of expressions: we now have both functions (representing by a function in ML) and integers.

type expr = | Const of int | Add of expr * expr | Mul of expr * expr | Abs of (expr -> expr option) | App of expr * expr

The evaluator for this syntax tree is partial, and has type expr -> expr option:

let rec eval e = match e with | Const i -> Some(Const i) | Add ( u , v ) -> begin match (eval u, eval v) with | (Some (Const i1), Some (Const i2)) -> Some(Const (add i1 i2)) | _ -> None end | Mul ( u , v ) -> begin match (eval u, eval v) with | (Some (Const i1), Some (Const i2)) -> Some(Const (mul i1 i2)) | _ -> None end | Abs f -> Some(Abs f) | App(u, v) -> begin match eval u with | Some(Abs f) -> begin match eval v with None -> None | Some x -> f x end | _ -> None end

As previously, we can merge the the constuctors Add and Mul into Binop' to obtain the following type expr':

type binop' = | Add' | Mul' type expr' = | Const' of int | Binop' of binop' * expr' * expr' | Abs' of (expr' -> expr' option) | App' of expr' * expr'

Notice that the types expr and expr' have recursion in negative positions. We can still define an ornament oexpr taking expr to expr':

type ornament oexpr : expr => expr' with | Const ( i ) => Const' ( i ) | Add ( u , v ) => Binop' ( Add' , u , v ) when u v : oexpr | Mul ( u , v ) => Binop' ( Mul' , u , v ) when u v : oexpr | Abs f => Abs' f when f : oexpr -> oexpr option | App ( u , v ) => App' ( u , v ) when u v : oexpr

In the clause of Abs, the lifting of the argument is specified by an higher-order ornament type oexpr -> oexpr option that recursively uses oexpr as argument of another type, and on the left of a an arrow. We can then use this to lift the function eval:

let eval' = lifting eval : oexpr -> oexpr option with ornament * <- @id

The clause ornament * <- @id is necessary to specify how the intermediate tuples are to be oranmented, although in this case we could safely default to identity without any user indication.

The output is rather long because some of the wildcards in pattern matching get expanded: [XXX the order of argument should be fixed]

let rec eval' e = match e with | Const' i -> Some (Const' i) | Binop'(Add', u, v) -> begin match (eval' u, eval' v) with | (Some (Const' i), Some (Const' i1)) -> Some (Const' (add i i1)) | _ -> None end | Binop'(Mul', u, v) -> begin match (eval' u, eval'v) with | (Some (Const' i), Some (Const' i1)) -> Some (Const' (mul i i1)) | _ -> None end | Abs' f -> Some (Abs' f) | App'(u, v) -> begin match eval' u with | Some (Abs' f) -> begin match eval' v with | None -> None | Some x -> f x end | _ -> None end

Notice, that this program is longer than the original just because, we expanded the wildcards. We could reintroduce them a posteriori automatically—but haven not implemented this yet, and factor our the two binop cases, leading to the following code:

let rec eval' e = match e with | Const' i -> Some (Const' i) | Abs' f -> Some (Abs' f) | Binop'(bin, u, v) -> begin match eval' u with | Some (Const' i1) -> begin match v with | Some (Const' i2) -> Some (Const' ((match bin with Add -> add | Mul -> mul) i1 i2)) | _ -> None end | None -> None end | App'(u, v) -> begin match eval' u with | Some (Abs' f) -> begin match eval' v with | None -> None | Some x -> f x end | _ -> None end

Splitting expressions and values

The example illustrates how the recursive structure can be changed during ornamentation.

This example is also developped on its own in the file exprval.html

We notice that the eval function only returns values from a limited subset of expressions that represent values. Similarly, the functions in abstractions are only called with values. This invariant can be expressed using the following mutually recursive types of expressions expr'' and values value'':

type expr'' = | Const'' of int | Binop'' of binop' * expr'' * expr'' | Abs'' of (value'' -> value'' option) | App'' of expr'' * expr'' and value'' = | Int'' of int | Fun'' of (value'' -> value'' option)

We can relate this new representation to the representation expr' by the following mutually recursive ornaments: while oexpr' is able to map all expression constructors, the ornament oval' is partial and only maps the constructors that actually correspond to values. This is an ornament, because deleting a constructor is equivalent to asking for an information that cannot be produced (i.e. a value of the empty type). We still have to match all possible constructors, but we map them to the empty pattern, written ~.

type ornament oexpr' : expr' => expr'' with | Const' ( i ) => Const'' ( i ) | Binop' ( o , u , v ) => Binop'' ( o , u , v ) when u v : oexpr' | Abs' f => Abs'' f when f : oval' -> oval' option | App' ( u , v ) => App'' ( u , v ) when u v : oexpr' and oval' : expr' => value'' with | Const' i => Int'' i | Abs' f => Fun'' f when f : oval' -> oval' option | Binop'(o,u,v) => ~ | App'(u,v) => ~

Note that in this case, we do not follow the recursive structure of the expr' datatype: some recursive occurences are transformed into values while others stay expressions.

We can then re-lift expr' using this ornament:

let eval'' = lifting eval' : oexpr' -> oval' option with ornament * <- @id

We obtain the following program. No patch is asked, because we can prove locally (i.e. without going through function calls) that the restriction to values is correct. Otherwise, we would have to produce a patch of the empty type.

let rec eval'' e = match e with | Const'' i -> Some (Int'' i) | Binop''(Add', u, v) -> begin match (eval'' u, eval'' v) with | (Some (Int'' i), Some (Int'' i1)) -> Some (Int'' (add i i1)) | _ -> None end | Binop''(Mul', u, v) -> begin match (eval'' u, eval'' v) with | (Some (Int'' i), Some (Int'' i1)) -> Some (Int'' (mul i i1)) | _ -> None end | Abs'' f -> Some (Fun'' f) | App''(u, v) -> begin match eval'' u with | Some (Fun'' f) -> begin match eval'' v with | None -> None | Some x -> f x end | _ -> None end

Again, reintroduction of wildcards and factorization of binops would lead to

let rec eval'' e = match e with | Const'' i -> Some (Int'' i) | Abs'' f -> Some (Fun'' f) | Binop''(bin, u, v) -> begin match eval'' u with | Some (Int'' i1) -> begin match eval'' v with | Some (Int'' i2) -> Some (Int'' ((match bin with Add' -> add | Mul' -> mul) i1 i2)) | _ -> None end | _ -> None end | App''(u, v) -> begin match eval'' u with | Some (Fun'' f) -> begin match eval'' v with | Some x -> f x | None -> None end | _ -> None end