This 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 |

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 the wildcard 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) -> let x = eval' v in begin match eval' u with | ((((None |Some (Binop'(Add', _, _))) |Some (Binop'(Mul', _, _))) |Some (Abs' _)) |Some (App'(_, _))) -> None | Some (Const' i) -> begin match x with | ((((None |Some (Binop'(Add', _, _))) |Some (Binop'(Mul', _, _))) |Some (Abs' _)) |Some (App'(_, _))) -> None | Some (Const' i1) -> Some (Const' (add i i1)) end end | Binop'(Mul', u, v) -> let x = eval' v in begin match eval' u with | ((((None |Some (Binop'(Add', _, _))) |Some (Binop'(Mul', _, _))) |Some (Abs' _)) |Some (App'(_, _))) -> None | Some (Const' i) -> begin match x with | ((((None |Some (Binop'(Add', _, _))) |Some (Binop'(Mul', _, _))) |Some (Abs' _)) |Some (App'(_, _))) -> None | Some (Const' i1) -> Some (Const' (mul i i1)) end end | Abs' f -> Some (Abs' f) | App'(u, v) -> begin match eval' u with | ((((None |Some (Const' _)) |Some (Binop'(Add', _, _))) |Some (Binop'(Mul', _, _))) |Some (App'(_, _))) -> None | Some (Abs' f) -> begin match eval' v with | None -> None | Some x -> f x end end |

Notice, that this program is longer than the original just because, we expanded the wildcards. We could reintroduce them a posteriori automatically—but have not implemented this yet, and factor out 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 | Some x -> f x | None -> None end | _ -> None end |

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) -> let x = eval'' v in begin match eval'' u with | (None |Some (Fun'' _)) -> None | Some (Int'' i) -> begin match x with | (None |Some (Fun'' _)) -> None | Some (Int'' i1) -> Some (Int'' (add i i1)) end end | Binop''(Mul', u, v) -> let x = eval'' v in begin match eval'' u with | (None |Some (Fun'' _)) -> None | Some (Int'' i) -> begin match x with | (None |Some (Fun'' _)) -> None | Some (Int'' i1) -> Some (Int'' (mul i i1)) end end | Abs'' f -> Some (Fun'' f) | App''(u, v) -> begin match eval'' u with | (None |Some (Int'' _)) -> None | Some (Fun'' f) -> begin match eval'' v with | None -> None | Some x -> f x end 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 |