Top

This has been processed with:

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

## 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'