A simply typed lambda calculus in tagless-final (De Bruijn indices)

stlc-form-meaning-de-bruijn.ml

module type Form = sig
  type ('env, 'a) meaning

  val vz : ('a * 'env, 'a) meaning
  val vs : ('env, 'a) meaning -> ('b * 'env, 'a) meaning
  val lam : ('a * 'env, 'b) meaning -> ('env, 'a -> 'b) meaning

  val appl :
    ('env, 'a -> 'b) meaning -> ('env, 'a) meaning -> ('env, 'b) meaning
end

(* Evaluate a given term. *)
module Eval = struct
  type ('env, 'a) meaning = 'env -> 'a

  let vz (x, _xs) = x
  let vs go (_x, xs) = go xs
  let lam m env x = m (x, env)
  let appl f x env = (f env) (x env)
end

(* Print a given term using De Bruijn indices. *)
module Print = struct
  type ('a, 'env) meaning = string

  let sprintf = Printf.sprintf
  let vz = "0"
  let vs go = sprintf "%d" (int_of_string go + 1)
  let lam m = sprintf "(λ . %s)" m
  let appl f x = sprintf "(%s%s)" f x
end

module Test (F : Form) = struct
  open F

  let k = lam (lam (vs vz))
  let i = lam vz
  let expr1 = appl k i
  let expr2 x y = appl (appl expr1 x) y
end

let () =
  let module E1 = Test (Eval) in
  (* 123 *)
  print_endline
    (Printf.sprintf "%d" (E1.expr2 (fun () -> ()) (fun () -> 123) ()));
  let module E2 = Test (Print) in
  (* ((λ . (λ . 1))(λ . 0)) *)
  print_endline E2.expr1