%{{ # From HOAS to De Bruijn, and back We show that the HOAS (Higher-Order Abstract Syntax) term representation, where we use the LF-level abstraction as a generic binder, is isomorphic to the first-order De Bruijn representation, where variables are represented by naturals. }}% LF tp : type = | o : tp | arr : tp -> tp -> tp; %{{ ## Simply typed λ-terms in HOAS They are represented as customary, as an LF-level `type`. }}% LF hoas : tp -> type = | lam : (hoas A -> hoas B) -> hoas (arr A B) | app : hoas (arr A B) -> hoas A -> hoas B; %{{ These terms are intrinsically well-typed: values of LF type `hoas` correspond uniquely to λ-terms up to α-equivalence. For instance, here is an HOAS λ-term with one free variable, `z`: }}% let ex1 : [z : hoas (arr o o) |- hoas (arr (arr o o) (arr o o))] = [z:hoas (arr o o) |- lam \x. lam \y. app z (app x y)]; %{{ If we traverse such a term, we will have to represent open terms, that are valid in a context of a certain form. This context schema is a list of terms together with their types: }}% schema ctx = some [t:tp] hoas t; %{{ ## Simply typed λ-terms with De Bruijn indexes We can define first-order, De Bruijn-indexed λ-terms as a computational type, a `ctype`, since it is strictly positive. They are parameterized by a (LF-level) type `tp` and a context `ctx`. Instead of defining a data type of list of types, we reuse Beluga's built-in data structure of context, classified by the schema above. }}% inductive DB : {gamma:ctx} [|- tp] -> ctype = | Lam : DB [gamma, x:hoas A[]] [|- B] -> DB [gamma] [|- arr A B] | App : DB [gamma] [|- arr A B] -> DB [gamma] [|- A] -> DB [gamma] [|- B] | O : DB [gamma, x:hoas A[]] [|- A] | S : DB [gamma] [|- B] -> DB [gamma, x:hoas A[]] [|- B]; %{{ For instance, here is the same λ-term as above, in De Bruijn encoding: }}% let ex2 : DB [z:hoas (arr o o)] [|- arr (arr o o) (arr o o)] = Lam (Lam (App (S (S O)) (App (S O) O))); %{{ ## From HOAS to De Bruijn The following function descend recursively inside a (possibly open) LF object of type `hoas A` to construct the equivalent De Bruijn term. }}% rec db : (gamma:ctx) [gamma |- hoas A[]] -> DB [gamma] [|- A] = fn m => case m of | [gamma |- app M N] => App (db [gamma |- M]) (db [gamma |- N]) | [gamma |- lam \x. M] : [gamma |- hoas (arr A[] B[])] => Lam (db [gamma, x:hoas A[] |- M]) | [gamma, x:hoas A[] |- x ] => O | [gamma, x:hoas B[] |- #p[..]] => S (db [gamma |- #p]); %{{ Note that, in the `lam` case, we used type annotation in the pattern to bind a type variable `A` refered to in the branch. The quantification over contexts `(gamma:ctx)` in the type is implicit: `g` is not bound in the term (nor is `A`). There are two variable cases, corresponding respectively to whether the variable is the "top" variable, or a variable deeper in the environment. As a test, the following declaration computes the expected value, i.e. `ex2`: }}% let test : DB [z : hoas (arr o o)] [|- arr (arr o o) (arr o o)] = db ex1; %{{ ## From De Bruijn to HOAS The following recursive function descend recursively in an indexed, computational object `DB` to construct the equivalent HOAS contextual object. }}% rec hoas : (gamma:ctx) DB [gamma] [|- A] -> [gamma |- hoas A[]] = fn m => case m of | Lam m => let [gamma, x: hoas _ |- M] = hoas m in [gamma |- lam \x. M] | App m n => let [gamma |- M] = hoas m in let [gamma |- N] = hoas n in [gamma |- app M N] | O => let (m : DB [gamma, x:hoas _] [|- B]) = m in [gamma, x:hoas _ |- x] | S m => let [gamma |- M] = hoas m in [gamma, x |- M[..]]; %{{ Note that, contrarily to the previous function, the recursive calls' values are bound to metavariables by `let`s, and cannot be inlined in the returned value, because they belong to the LF level. In the `O` case, a dummy `let` is used to bind the environment tail `g`, so that it can be refered to in the returned value. As a test, the following declaration computes the expected value, i.e. `ex1`: }}% let test : [z : hoas (arr o o) |- hoas (arr (arr o o) (arr o o))] = hoas ex2;