Top
This file has been processed with:
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
| Some (Abs' f) ->
begin match eval' v with
| Some x -> eval' (f x)
| None -> None
end
| _ -> None
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' |