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 |