A five-line lambda calculus with OCaml's polymorphic variants

lambda-calculus.ml

let rec eval = function
  | `Appl (m, n) -> (
      let n' = eval n in
      match eval m with `Lam f -> eval (f n') | m' -> `Appl (m', n'))
  | (`Lam _ | `Var _) as t -> t

let sprintf = Printf.sprintf

(* Print a given term using De Bruijn levels. *)
let rec pp lvl = function
  | `Lam f -> sprintf "(λ . %s)" (pp (lvl + 1) (f (`Var lvl)))
  | `Appl (m, n) -> sprintf "(%s%s)" (pp lvl m) (pp lvl n)
  | `Var lvl -> sprintf "%d" lvl

let () =
  let s =
    `Lam
      (fun x ->
        `Lam (fun y -> `Lam (fun z -> `Appl (`Appl (x, z), `Appl (y, z)))))
  in
  let k = `Lam (fun x -> `Lam (fun _ -> x)) in
  let i = `Appl (`Appl (s, k), k) in
  (* (λ . (λ . 0)) *)
  print_endline (pp 0 (eval (`Appl (i, k))))