Top
This file has been processed with:
From named variables to De Bruijn indices: (des)ornamentation of an interpreter
This example demonstrates an interesting transformation of a tiny interpreter
with named variables to an interpreter using De Bruijn indices. This can not be
described as ornamentation nor desornamentation, it is a combination of them.
Indeed, at the same time, string values are removed and int are added.
val prev: int -> int
val zero: int
let eq a b = True |
Let us take a simple interpreter :
type 'a list = Nil | Cons of 'a * 'a list
type 'a option = None | Some of 'a
type expr =
| App of expr * expr
| Const of int
| Abs of string * expr
| Var of string box
let rec assoc n l = match l with
| Nil -> None
| Cons((a, b), q) ->
match n with
| Box n' ->
match eq a n' with
| True -> Some b
| False -> assoc (Box n') q
let rec eval env e =
match e with
| Const i -> Some (Const i)
| App(a, b) ->
begin
match eval env b with
| None -> None
| Some e -> begin match eval env a with
| Some (Abs(n, v)) -> eval (Cons((n, e), env)) v
| _ -> None
end
end
| Abs(n, v) -> Some (Abs(n, v))
| Var(n) -> assoc n env |
Note that a box type is used to get a generic term more general: a term is generalized
at constructor call site and pattern matching site, so using boxes makes it possible to
get a more generalized term.
In particular, here, it is needed to generalize against the first argument of assoc
(in a version without a box, this argument would only be used to make an
eq call, hence this value could not be ornamented).
We define an ornament that allow us to change a box content:
type ornament ('a, 'b) erase_box: 'a box => 'b box with
| Box _ => Box _ |
We still call this last transformation an ornament, however it is generally not
considered an ornament as it removes the content of the box, and adds a new one,
completely different. That part justifies the fact that, strictly speaking, we
can not call the whole transformation an ornamentation nor a desornamentation.
Now, let us define De Bruijn expressions:
type expr_de_bruijn =
| App' of expr_de_bruijn * expr_de_bruijn
| Const' of int
| Abs' of expr_de_bruijn
| Var' of int box |
We then define the ornament between expr and expr’ datatypes.
type ornament bruijnification: expr => expr_de_bruijn with
| Var a => Var' a when a: (string, int) erase_box
| App (a, b) => App'(a, b) when a b: bruijnification
| Const i => Const' i
| Abs(_, e) => Abs' e when e: bruijnification |
Environments are association lists for the first interpreter, and lists of
expressions for the De Bruijn interpreter. However, variables were already
stored in the binding order, so we only have to drop the first argument and
compose with the previous ornament.
type ornament env: (string * expr) list => expr_de_bruijn list with
| Nil => Nil
| Cons((_, a), q) => Cons(a, q) when q: env, a: bruijnification |
Then, we can request the lifting of both functions :
let assoc' =
lifting assoc: (string, int) erase_box -> env -> _ option with
ornament * <- bool |
type expr_de_bruijn =
| App' of expr_de_bruijn * expr_de_bruijn
| Const' of int
| Abs' of expr_de_bruijn
| Var' of int box
let rec assoc' n l = match l with
| Nil -> None
| Cons(b, q) ->
begin match eq #20 #14 with
| True -> Some b
| False -> assoc' (Box #5) q
end |
let assoc' =
lifting assoc: (string, int) erase_box -> env -> _ option with
ornament * <- bool
patch #5[prev (match n with Box n' -> n')]
patch #20[zero]
patch #14[match n with Box a -> a] |
let rec assoc' n l = match l with
| Nil -> None
| Cons(b, q) ->
begin match eq zero
begin match n with
| Box a -> a
end
with
| True -> Some b
| False ->
assoc'
(Box (prev
begin match n with
| Box n' -> n'
end))
q
end |
let eval_bruijnified =
lifting eval: env -> bruijnification -> bruijnification option |
let rec eval_bruijnified env e = match e with
| Const' i -> Some (Const' i)
| App'(a, b) ->
begin match eval_bruijnified env b with
| None -> None
| Some a1 ->
begin match eval_bruijnified env a with
| Some (Abs' e) ->
eval_bruijnified (Cons(a1, env)) e
| _ -> None
end
end
| Abs' e -> Some (Abs' e)
| Var' n -> (lifting #10 of assoc) n env |
let eval_bruijnified =
lifting eval: env -> bruijnification -> bruijnification option
with
lifting #10 <- assoc' |
let rec eval_bruijnified env e = match e with
| Const' i -> Some (Const' i)
| App'(a, b) ->
begin match eval_bruijnified env b with
| None -> None
| Some a1 ->
begin match eval_bruijnified env a with
| Some (Abs' e) ->
eval_bruijnified (Cons(a1, env)) e
| _ -> None
end
end
| Abs' e -> Some (Abs' e)
| Var' n -> assoc' n env |