A simply typed lambda calculus in tagless-final (HOAS)

stlc-form-meaning-hoas.ml

module type Form = sig
  type 'a meaning

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

(* Evaluate a given term. *)
module Eval = struct
  type 'a meaning = 'a

  let lam f = f
  let appl f x = f x
end

(* Print a given term using De Bruijn levels. *)
module Print = struct
  type 'a meaning = int -> string

  let sprintf = Printf.sprintf
  let lam f lvl = sprintf "(λ . %s)" (f (fun _ -> sprintf "%d" lvl) (lvl + 1))
  let appl f x lvl = sprintf "(%s%s)" (f lvl) (x lvl)
end

module Test (F : Form) = struct
  open F

  let k = lam (fun x -> lam (fun _ -> x))
  let i = lam (fun x -> x)
  let expr = appl k i
end

let () =
  let module E1 = Test (Eval) in
  (* 123 *)
  print_endline (Printf.sprintf "%d" (E1.expr () 123));
  let module E2 = Test (Print) in
  (* ((λ . (λ . 0))(λ . 0)) *)
  print_endline (E2.expr 0)