Top

This file has been processed with:

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

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