This has been processed with:

ocamlorn --library stdlib.mli \ --library --input --lifting \ >

Restiction of the domain

type expr = | Const of bool | Abs of (expr -> expr) | App of expr * expr
let rec eval e = match e with | Const i -> Some (Const i) | Abs f -> Some (Abs f) | App (u, v) -> begin match eval u with | Some (Abs f) -> begin match eval v with | Some x -> eval (f x) | None -> None end | _ -> None end

Splitting expressions and values

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

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' = | Val of value | App' of expr' * expr' and value = | Const' of bool | Abs' of (value -> expr')

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 => Val (Const' i) | Abs f => Val (Abs' f) when f : oval -> oexpr | App ( u , v ) => App' ( u , v ) when u v : oexpr and oval : expr => value with | Const i => Const' i | Abs f => Abs' f when f : oval -> oexpr | 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 | Val (Const' i) -> Some (Const' i) | Val (Abs' f) -> Some (Abs' f) | App'(u, v) -> begin match eval' u with | (None |Some (Const' _)) -> None | Some (Abs' f) -> begin match eval' v with | None -> None | Some x -> eval' (f x) end end

We should also lift the creation of values. However, this will only succeed if we check in the creation of abstractions that the argument is always a value form. We define the function cval for that purpose:

let cval x = match x with | App (u, v) -> fail | Const i -> Const i | Abs f -> Abs f

We should then use it in the construction of abstractions as follows

let id = Abs (fun x -> cval x) let xx = Abs (fun x -> App (cval x, cval x)) let z = App (App (xx, id), Const True) let v _x = eval z
let cval' = lifting cval : oval -> oexpr let id' = lifting id : oexpr let xx' = lifting xx : oexpr let z' = lifting z : oexpr let v' = lifting v : _ -> oval option
let cval' x = match x with | Const' i -> Val (Const' i) | Abs' f -> Val (Abs' f) let id' = Val (Abs' (fun x -> cval' x)) let xx' = Val (Abs' (fun x -> App'(cval' x, cval' x))) let z' = App'(App'(xx', id'), Val (Const' True)) let v' _x = eval' z'