Barebones lambda cube in OCaml

a-preface.md

Barebones lambda cube in OCaml

For any formal system, we can really only understand its precise details after attempting to implement it.
    -- Simon Thompson, Type Theory & Functional Programming ¹

This post has been discussed on Reddit.

This post has a followup.

Since a type theory called "Calculus of Constructions (CoC)" was introduced by Thierry Coquand in 1985, its conceptual elegance has been a subject of interest to many enlightened mathematicians and computer scientists. Since then, its extended variants have found their use in proof assistants, such as Lean and Coq, and programming languages as well, such as Neut, Agda, Idris, and many others. For a logician, CoC can be used as a foundation of (constructive) mathematics; for a programmer, it can be seen as a basis of a programming language whose types correspond to logical propositions, thus making theorem proving and software development proceed within a single system.

The lambda cube is a formal system introduced by Henk Barendregt, that depicts the directions of how simply typed lambda calculus can be extended to form different combinations of terms and types depending on each other (i.e., function types). Thus, vertices in the cube correspond to specific type theories, and the most expressive vertex is CoC itself since it permits all the combinations of terms and types as input and output values:

(Adapted from Wikipedia.)

In the context of programming, this observation sums up the four base paradigms of structuring code:

Combination	Paradigm
Terms depending on terms	Algorithms and data structures.
Terms depending on types	Generic programming.
Types depending on types	Type-level programming; metaprogramming.
Types depending on terms	Dependent typing; formal verification.

Although CoC is a simple system, it is not straightforward to implement it on a computer: you need to guarantee capture-free substitution, alpha equivalence of terms, uniqueness of types up to beta conversion, and other peculiarities. For this reason, I wrote a minimalistic implementation of CoC in OCaml so that other learners of type theory could benefit from it. You will not see a parser, enhanced diagnostics, or any type system extensions -- everything you will see is just an abstract syntax representation, poor man's type inference, and beta reduction.

As an application of the developed system, I present the encoding of Church booleans, Church numerals, intuitionistic logic, and classical logic with the law of double negation. Finally, I provide unit tests for (almost) all functions involved in the implementation. The characteristics of the implementation are typing à la Church (explicitly typed binders), applicative order evaluation (arguments evaluated first), and a named representation of variables.

All the material presented here should be accessible after reading the first seven chapters from "Type Theory and Formal Proof: An Introduction". Other remarkable literature is included ^{2 3 4 5}.

See also: untyped lambda calculus on the C preprocessor.

Show unit tests

let test_free_vars () =
  assert (free_vars (Var "x") = [ "x" ]);
  assert (free_vars (lam "x" Star (Var "x")) = []);
  assert (free_vars (lam "x" (Var "y") (Var "x")) = [ "y" ]);
  assert (free_vars (lam "x" Star (Var "y")) = [ "y" ]);
  assert (free_vars (lam "x" (Var "x") (Var "y")) = [ "x"; "y" ]);
  assert (free_vars (Appl (Var "x", Var "y")) = [ "x"; "y" ]);
  assert (free_vars Star = []);
  assert (free_vars Box = [])

let test_binders () =
  assert (binders (Var "x") = []);
  assert (binders (lam "x" Star (Var "x")) = [ "x" ]);
  assert (binders (lam "x" (Var "y") (Var "x")) = [ "x" ]);
  assert (binders (lam "x" Star (Var "y")) = [ "x" ]);
  assert (binders (lam "x" (pi "y" Star (Var "y")) (Var "x")) = [ "x"; "y" ]);
  assert (binders (Appl (Var "x", Var "y")) = []);
  assert (
    binders (Appl (lam "x" Star (Var "z"), lam "y" Star (Var "z")))
    = [ "x"; "y" ]);
  assert (binders Star = []);
  assert (binders Box = [])

let test_fresh_var () =
  assert (freshen [] "x" = "x");
  assert (freshen [ "x" ] "y" = "y");
  assert (freshen [ "x" ] "x" = "x'");
  assert (freshen [ "x"; "x'"; "x''"; "y"; "z" ] "x" = "x'''")

let test_subst () =
  assert (subst "x" (Var "y") (Var "x") = Var "y");
  assert (subst "y" (Var "z") (Var "x") = Var "x");
  assert (subst "x" (Var "z") (Appl (Var "x", Var "y")) = Appl (Var "z", Var "y"));
  assert (subst "y" (Var "z") (Appl (Var "x", Var "y")) = Appl (Var "x", Var "z"));
  assert (subst "x" (Var "z") (Appl (Var "x", Var "y")) = Appl (Var "z", Var "y"));
  assert (subst "z" (Var "l") (Appl (Var "x", Var "y")) = Appl (Var "x", Var "y"));
  assert (subst "x" (Var "z") (lam "x" Star (Var "x")) = lam "x" Star (Var "x"));
  assert (
    subst "x" (Var "z") (lam "x" (Var "x") (Var "x"))
    = lam "x" (Var "z") (Var "x"));
  assert (subst "y" (Var "z") (lam "x" Star (Var "y")) = lam "x" Star (Var "z"));
  (* Check that the new binding variable does not accidentally capture the
     substitution term... *)
  assert (subst "y" (Var "x") (lam "x" Star (Var "y")) = lam "x'" Star (Var "x"));
  (* ... and that it does not capture free variables in the body. *)
  assert (
    subst "y" (Var "x") (lam "x" Star (Appl (Var "y", Var "x'")))
    = lam "x''" Star (Appl (Var "x", Var "x'")));
  (* ... and that it does not conflict with bindings in the body. *)
  assert (
    subst "y" (Var "x") (lam "x" Star (lam "x'" Star (Appl (Var "y", Var "x"))))
    = lam "x''" Star (lam "x'" Star (Appl (Var "x", Var "x''"))));
  assert (subst "x" (Var "z") Star = Star);
  assert (subst "x" (Var "z") Box = Box)

let test_alpha_eq () =
  assert (alpha_eq (Var "x", Var "x"));
  assert (not (alpha_eq (Var "x", Var "y")));
  assert (alpha_eq (Appl (Var "x", Var "y"), Appl (Var "x", Var "y")));
  assert (not (alpha_eq (Appl (Var "x", Var "z"), Appl (Var "x", Var "y"))));
  assert (not (alpha_eq (Appl (Var "z", Var "y"), Appl (Var "x", Var "y"))));
  assert (alpha_eq (lam "x" Star (Var "x"), lam "x" Star (Var "x")));
  assert (alpha_eq (lam "x" Star (Var "x"), lam "y" Star (Var "y")));
  assert (not (alpha_eq (lam "x" Star (Var "x"), lam "y" (Var "z") (Var "y"))));
  assert (alpha_eq (pi "x" Star (Var "x"), pi "x" Star (Var "x")));
  assert (alpha_eq (pi "x" Star (Var "x"), pi "y" Star (Var "y")));
  assert (not (alpha_eq (pi "x" Star (Var "x"), pi "y" (Var "z") (Var "y"))))

let test_eval () =
  assert (eval (Var "x") = Var "x");
  assert (eval (Appl (Var "x", Var "y")) = Appl (Var "x", Var "y"));
  assert (eval (Appl (lam "x" (Var "a") (Var "x"), Var "y")) = Var "y");
  (* If `m` in `Appl(m, n)` is not an immediate lambda, we must first normalise
     it and see if it is. *)
  assert (
    eval
      (Appl
         ( Appl (lam "x" (Var "a") (lam "x" (Var "a") (Var "x")), Var "z"),
           Var "y" ))
    = Var "y");
  (* If `m` in `Appl(m, n)` is not a redex, we must nonetheless evaluate `n` and
     return the application. *)
  assert (
    eval (Appl (Var "x", Appl (lam "x" (Var "a") (Var "x"), Var "y")))
    = Appl (Var "x", Var "y"));
  (* Check that an argument is evaluated. *)
  assert (
    eval
      (Appl
         ( lam "x" (Var "a") (Var "x"),
           Appl (lam "x" (Var "a") (Var "x"), Var "z") ))
    = Var "z");
  (* Check that a body after substitution is evaluated. *)
  assert (
    eval
      (Appl
         ( lam "x" (Var "a") (Appl (lam "y" (Var "a") (Var "y"), Var "x")),
           Var "z" ))
    = Var "z");
  assert (eval (lam "x" (Var "a") (Var "x")) = lam "x" (Var "a") (Var "x"));
  (* Both an argument type and a body must be evaluated. *)
  assert (
    eval
      (lam "x"
         (Appl (lam "x" (Var "a") (Var "x"), Var "y"))
         (Appl (lam "x" (Var "a") (Var "x"), Var "z")))
    = lam "x" (Var "y") (Var "z"));
  assert (eval Star = Star);
  assert (eval Box = Box)

let test_type_inference () =
  (* Super-type "*". *)
  assert (infer_type Star = Box);
  assert (infer_type ~ctx:[ ("x", Star); ("y", Var "x") ] Star = Box);
  (* Variables. *)
  assert (infer_type ~ctx:[ ("x", Star) ] (Var "x") = Star);
  assert (
    infer_type ~ctx:[ ("x", Star); ("y", Var "x"); ("z", Var "x") ] (Var "y")
    = Var "x");
  assert (infer_type ~ctx:[ ("x", Star); ("y", Var "x") ] (Var "y") = Var "x");
  (* Application. *)
  assert (
    infer_type
      ~ctx:[ ("a", Star); ("y", Var "a") ]
      (Appl (lam "x" (Var "a") (Var "x"), Var "y"))
    = Var "a");
  assert (
    infer_type ~ctx:[ ("y", Star) ] (Appl (lam "x" Star (Var "x"), Var "y"))
    = Star);
  (* A term depending on a term. *)
  assert (
    infer_type ~ctx:[ ("a", Star) ] (lam "x" (Var "a") (Var "x"))
    = pi "x" (Var "a") (Var "a"));
  (* A term depending on a type. *)
  assert (
    infer_type ~ctx:[ ("a", Star); ("y", Var "a") ] (lam "x" Star (Var "y"))
    = pi "x" Star (Var "a"));
  (* A type depending on a type. *)
  assert (infer_type (lam "x" Star (Var "x")) = pi "x" Star Star);
  (* A type depending on a term. *)
  assert (
    infer_type ~ctx:[ ("a", Star) ] (lam "x" (Var "a") (Var "a"))
    = pi "x" (Var "a") Star);
  assert (
    infer_type
      ~ctx:[ ("a", Star) ]
      (lam "x" (Var "a") (pi "y" (Var "a") (Var "a")))
    = pi "x" (Var "a") Star);
  (* Pi-types. *)
  assert (infer_type ~ctx:[ ("a", Star) ] (pi "x" (Var "a") (Var "a")) = Star);
  assert (
    infer_type
      ~ctx:[ ("a", Star) ]
      (pi "x" (Var "a") (pi "x" (Var "a") (Var "a")))
    = Star);
  assert (infer_type ~ctx:[ ("a", Box) ] (pi "x" (Var "a") (Var "a")) = Box);
  assert (
    infer_type
      ~ctx:[ ("a", Box) ]
      (pi "x" (Var "a") (pi "x" (Var "a") (Var "a")))
    = Box);
  (* Our evaluator must normalise all subexpressions. *)
  assert (
    infer_type
      ~ctx:[ ("a", Star); ("b", Star); ("y", Var "a"); ("z", Var "b") ]
      (lam "x"
         (Appl (lam "x" Star (Var "x"), Var "a"))
         (Appl (lam "x" (Var "b") (Var "x"), Var "z")))
    = pi "x" (Var "a") (Var "b"))

let test_print () =
  assert (print (Var "x") = "x");
  assert (print (Appl (Var "x", Var "y")) = "(x y)");
  assert (print (lam "x" (Var "z") (Var "x")) = "(λx:z.x)");
  assert (print (pi "x" Star (Var "x")) = "(Πx:*.x)");
  assert (print (pi "x" (Var "a") (Var "a")) = "(a→a)");
  assert (print (pi "a" Star (pi "x" (Var "a") (Var "a"))) = "(Πa:*.(a→a))");
  assert (print Star = "*");
  assert (print Box = "☐")

let () =
  test_free_vars ();
  test_binders ();
  test_fresh_var ();
  test_subst ();
  test_alpha_eq ();
  test_eval ();
  test_type_inference ();
  test_print ()

Footnotes

1. https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf ↩

2. https://github.com/steshaw/plt ↩

3. https://github.com/jozefg/learn-tt ↩

4. https://proofassistants.stackexchange.com/questions/930/so-many-data-types-so-little-time/940#940 ↩

5. http://lucacardelli.name/Papers/TypeSystems.pdf ↩

CoC.ml

(* The syntax of our calculus. Notice that types are represented in the same way
   as terms, which is the essence of CoC. *)
type term =
  | Var of string
  | Appl of term * term
  | Binder of binder * string * term * term
  | Star
  | Box

and binder = Lam | Pi

let lam x a m = Binder (Lam, x, a, m)
let pi x a m = Binder (Pi, x, a, m)

let rec free_vars = function
  | Var x -> [ x ]
  | Appl (m, n) -> free_vars m @ free_vars n
  | Binder (_, x, a, m) -> free_vars a @ List.filter (( <> ) x) (free_vars m)
  | Star | Box -> []

let rec binders = function
  | Appl (m, n) -> binders m @ binders n
  | Binder (_, x, a, m) -> [ x ] @ binders a @ binders m
  | Var _ | Star | Box -> []

let all_vars t = free_vars t @ binders t

(* Generates a fresh variable identifier that is not in a banlist. *)
let rec freshen (banlist : string list) (base : string) =
  if List.mem base banlist then freshen banlist (base ^ "'") else base

let rec print = function
  | Var x -> x
  | Appl (m, n) -> Printf.sprintf "(%s %s)" (print m) (print n)
  | Binder (Lam, x, a, m) -> Printf.sprintf "(λ%s:%s.%s)" x (print a) (print m)
  | Binder (Pi, x, a, m) ->
      if List.mem x (free_vars m) then
        Printf.sprintf "(Π%s:%s.%s)" x (print a) (print m)
      else Printf.sprintf "(%s→%s)" (print a) (print m)
  | Star -> "*"
  | Box -> "☐"

let rec subst x m = function
  | Var y when x = y -> m
  | Var y -> Var y
  | Appl (m', n) -> Appl (subst x m m', subst x m n)
  | Binder (binder, y, a, n) when x = y -> Binder (binder, y, subst x m a, n)
  | Binder (binder, y, a, n) when List.mem y (free_vars m) ->
      let banlist = free_vars m @ all_vars n in
      subst x m (rename (freshen banlist y) (binder, y, a, n))
  | Binder (binder, y, a, n) -> Binder (binder, y, subst x m a, subst x m n)
  | (Star | Box) as s -> s

and rename x' (binder, x, a, m) = Binder (binder, x', a, subst x (Var x') m)

(* With De Bruijn indices, alpha equivalence check amounts to structural
   equality. However, we use named representation because it is more convenient
   for the user interface. *)
let rec alpha_eq = function
  | Var x, Var x' -> x = x'
  | Appl (m, n), Appl (m', n') -> alpha_eq (m, m') && alpha_eq (n, n')
  | Binder (binder, x, a, m), Binder (binder', x', a', m') when x = x' ->
      binder = binder' && alpha_eq (a, a') && alpha_eq (m, m')
  | Binder (binder, x, a, m), Binder (binder', x', a', m') ->
      let banlist = all_vars m @ all_vars m' in
      let fresh_x = freshen banlist x in
      alpha_eq
        (rename fresh_x (binder, x, a, m), rename fresh_x (binder', x', a', m'))
  | Star, Star | Box, Box -> true
  | _, _ -> false

let panic fmt = Printf.ksprintf failwith fmt

(* Reduces a term to its beta normal form using applicative order. *)
let rec eval = function
  | Appl (m, n) -> eval_appl (eval m) (eval n)
  | Binder (binder, x, a, m) -> Binder (binder, x, eval a, eval m)
  | (Var _ | Star | Box) as t -> t

and eval_appl m n =
  match m with Binder (Lam, x, _a, m) -> eval (subst x n m) | _ -> Appl (m, n)

(* A list of variable declarations for type inference. *)
type context = (string * term) list

(* Infers a type, in beta normal form, of a term in a given (well-formed)
   context; throws an exception otherwise. *)
let rec infer_type ?(ctx : context = []) = function
  | Var x -> eval (List.assoc x ctx)
  | Appl (m, n) -> infer_appl ctx m n
  | Binder (Lam, x, a, m) ->
      let m_ty = infer_type ~ctx:((x, a) :: ctx) m in
      let lam_ty = Binder (Pi, x, a, m_ty) in
      (* Check that the lambda type we have inferred is well-formed. *)
      let _ = infer_type ~ctx lam_ty in
      eval lam_ty
  | Binder (Pi, x, a, m) ->
      let _s1 = infer_sort ctx a in
      let s2 = infer_sort ((x, a) :: ctx) m in
      s2
  | Star -> Box
  | Box -> panic "☐ has no type"

and infer_appl (ctx : context) m n =
  match infer_type ~ctx m with
  | Binder (Pi, x, a, m) ->
      let n_ty = infer_type ~ctx n in
      if alpha_eq (a, n_ty) then eval (subst x n m)
      else panic "Expected type %s, got %s: %s" (print a) (print n_ty) (print n)
  | m_ty ->
      panic "Application of argument %s to a non-lambda %s of type %s" (print n)
        (print m) (print m_ty)

and infer_sort (ctx : context) t =
  match infer_type ~ctx t with
  | (Star | Box) as s -> s
  | a -> panic "Expected a sort, got %s: %s" (print a) (print t)

let check_type ?(ctx : context = []) t expected_ty =
  assert (alpha_eq (infer_type ~ctx t, eval expected_ty))

usage.ml

(* Define some syntax for variable arguments. Left/right folds over lists
   beautifully mirror the left/right-associative nature of applications and
   lambda abstractions, respectively. *)

let binder' binder ctx m =
  match ctx with
  | [] -> failwith "Empty argument list"
  | ctx -> List.fold_right (fun (x, a) acc -> Binder (binder, x, a, acc)) ctx m

let lam' ctx m = binder' Lam ctx m
let pi' ctx m = binder' Pi ctx m

let appl = function
  | [] -> failwith "Empty application list"
  | t :: ts -> List.fold_left (fun m n -> Appl (m, n)) t ts

let check ?(ctx = []) t expected =
  (* Check that the term is actually well-typed before evaluating. *)
  let _ = infer_type ~ctx t in
  assert (alpha_eq (eval t, eval expected))

let church_booleans () =
  let t = lam' [ ("a", Star); ("x", Var "a"); ("y", Var "a") ] (Var "x") in
  let f = lam' [ ("a", Star); ("x", Var "a"); ("y", Var "a") ] (Var "y") in
  let bool_ty = pi' [ ("a", Star); ("x", Var "a"); ("y", Var "a") ] (Var "a") in
  assert (infer_type t = bool_ty);
  assert (infer_type f = bool_ty);
  let if_then_else =
    lam'
      [ ("a", Star); ("b", bool_ty); ("x", Var "a"); ("y", Var "a") ]
      (appl [ Var "b"; Var "a"; Var "x"; Var "y" ])
  in
  check
    ~ctx:[ ("a", Star); ("x", Var "a"); ("y", Var "a") ]
    (appl [ if_then_else; Var "a"; t; Var "x"; Var "y" ])
    (Var "x");
  check
    ~ctx:[ ("a", Star); ("x", Var "a"); ("y", Var "a") ]
    (appl [ if_then_else; Var "a"; f; Var "x"; Var "y" ])
    (Var "y");
  let my_not = lam "b" bool_ty (appl [ Var "b"; bool_ty; f; t ]) in
  check (appl [ my_not; t ]) f;
  check (appl [ my_not; f ]) t;
  let my_and =
    lam'
      [ ("a", bool_ty); ("b", bool_ty) ]
      (appl [ Var "a"; bool_ty; Var "b"; f ])
  in
  check (appl [ my_and; t; t ]) t;
  check (appl [ my_and; t; f ]) f;
  check (appl [ my_and; f; f ]) f;
  check (appl [ my_and; f; t ]) f;
  let my_or =
    lam'
      [ ("a", bool_ty); ("b", bool_ty) ]
      (appl [ Var "a"; bool_ty; t; Var "b" ])
  in
  check (appl [ my_or; t; t ]) t;
  check (appl [ my_or; t; f ]) t;
  check (appl [ my_or; f; f ]) f;
  check (appl [ my_or; f; t ]) t;
  let my_xor =
    lam'
      [ ("a", bool_ty); ("b", bool_ty) ]
      (appl [ Var "a"; bool_ty; appl [ my_not; Var "b" ]; Var "b" ])
  in
  check (appl [ my_xor; t; t ]) f;
  check (appl [ my_xor; t; f ]) t;
  check (appl [ my_xor; f; f ]) f;
  check (appl [ my_xor; f; t ]) t

let church_numerals () =
  let f_ty = pi "x" (Var "a") (Var "a") in
  let n_ty = pi' [ ("a", Star); ("f", f_ty); ("x", Var "a") ] (Var "a") in
  let zero = lam' [ ("a", Star); ("f", f_ty); ("x", Var "a") ] (Var "x") in
  let succ =
    lam'
      [ ("n", n_ty); ("a", Star); ("f", f_ty); ("x", Var "a") ]
      (appl [ Var "f"; appl [ Var "n"; Var "a"; Var "f"; Var "x" ] ])
  in
  let one = appl [ succ; zero ] in
  let two = appl [ succ; one ] in
  let three = appl [ succ; two ] in
  let four = appl [ succ; three ] in
  assert (infer_type zero = n_ty);
  assert (infer_type one = n_ty);
  assert (infer_type two = n_ty);
  assert (infer_type three = n_ty);
  assert (infer_type four = n_ty);
  let add =
    lam'
      [ ("n", n_ty); ("m", n_ty); ("a", Star); ("f", f_ty); ("x", Var "a") ]
      (appl
         [
           Var "n";
           Var "a";
           Var "f";
           appl [ Var "m"; Var "a"; Var "f"; Var "x" ];
         ])
  in
  check (appl [ add; zero; zero ]) zero;
  check (appl [ add; zero; one ]) one;
  check (appl [ add; one; zero ]) one;
  check (appl [ add; three; one ]) four;
  let mul =
    lam'
      [ ("n", n_ty); ("m", n_ty); ("a", Star); ("f", f_ty); ("x", Var "a") ]
      (appl [ Var "n"; Var "a"; appl [ Var "m"; Var "a"; Var "f" ]; Var "x" ])
  in
  check (appl [ mul; zero; zero ]) zero;
  check (appl [ mul; zero; one ]) zero;
  check (appl [ mul; one; two ]) two;
  check (appl [ mul; two; two ]) four

let intuitionistic_logic () =
  (* A => (B => A) *)
  check_type
    (lam'
       [ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ]
       (Var "x"))
    (pi' [ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ] (Var "a"));
  let absurdity = pi "a" Star (Var "a") in
  let negate = lam "a" Star (pi "x" (Var "a") absurdity) in
  (* not A => (A => B) *)
  check_type
    (lam'
       [ ("a", Star); ("b", Star); ("x", appl [ negate; Var "a" ]) ]
       (lam "y" (Var "a") (appl [ Var "x"; Var "y"; Var "b" ])))
    (pi'
       [ ("a", Star); ("b", Star); ("x", appl [ negate; Var "a" ]) ]
       (pi "y" (Var "a") (Var "b")));
  (* A & B; product type *)
  let conj =
    lam'
      [ ("a", Star); ("b", Star) ]
      (pi'
         [
           ("c", Star); ("x", pi' [ ("l", Var "a"); ("m", Var "b") ] (Var "c"));
         ]
         (Var "c"))
  in
  let a_and_b_ty = appl [ conj; Var "a"; Var "b" ] in
  let b_and_a_ty = appl [ conj; Var "b"; Var "a" ] in
  (* A => B => A & B *)
  let conj_intro =
    lam'
      [ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ]
      (lam'
         [
           ("c", Star); ("k", pi' [ ("l", Var "a"); ("m", Var "b") ] (Var "c"));
         ]
         (appl [ Var "k"; Var "x"; Var "y" ]))
  in
  check_type conj_intro
    (pi'
       [ ("a", Star); ("b", Star); ("x", Var "a"); ("y", Var "b") ]
       a_and_b_ty);
  (* A & B => A *)
  let conj_elim1 =
    lam'
      [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ]
      (appl
         [ Var "x"; Var "a"; lam' [ ("l", Var "a"); ("m", Var "b") ] (Var "l") ])
  in
  check_type conj_elim1
    (pi' [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ] (Var "a"));
  (* A & B => B *)
  (let conj_elim2 =
     lam'
       [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ]
       (appl
          [
            Var "x"; Var "b"; lam' [ ("l", Var "a"); ("m", Var "b") ] (Var "m");
          ])
   in
   check_type conj_elim2
     (pi' [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ] (Var "b"));
   (* A & B => B & A *)
   check_type
     (lam'
        [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ]
        (appl
           [
             conj_intro;
             Var "b";
             Var "a";
             appl [ conj_elim2; Var "a"; Var "b"; Var "x" ];
             appl [ conj_elim1; Var "a"; Var "b"; Var "x" ];
           ]))
     (pi' [ ("a", Star); ("b", Star); ("x", a_and_b_ty) ] b_and_a_ty));
  (* A | B; sum type *)
  let disj =
    lam'
      [ ("a", Star); ("b", Star) ]
      (pi'
         [
           ("c", Star);
           ("x", pi "l" (Var "a") (Var "c"));
           ("y", pi "l" (Var "b") (Var "c"));
         ]
         (Var "c"))
  in
  let a_or_b_ty = appl [ disj; Var "a"; Var "b" ] in
  let b_or_a_ty = appl [ disj; Var "b"; Var "a" ] in
  (* A => A | B *)
  let disj_intro1 =
    lam'
      [ ("a", Star); ("b", Star); ("v", Var "a") ]
      (lam'
         [
           ("c", Star);
           ("x", pi "l" (Var "a") (Var "c"));
           ("y", pi "l" (Var "b") (Var "c"));
         ]
         (appl [ Var "x"; Var "v" ]))
  in
  check_type disj_intro1
    (pi' [ ("a", Star); ("b", Star); ("v", Var "a") ] a_or_b_ty);
  (* B => A | B *)
  let disj_intro2 =
    lam'
      [ ("a", Star); ("b", Star); ("v", Var "b") ]
      (lam'
         [
           ("c", Star);
           ("x", pi "l" (Var "a") (Var "c"));
           ("y", pi "l" (Var "b") (Var "c"));
         ]
         (appl [ Var "y"; Var "v" ]))
  in
  check_type disj_intro2
    (pi' [ ("a", Star); ("b", Star); ("v", Var "b") ] a_or_b_ty);
  (* A | B => B | A *)
  check_type
    (lam'
       [ ("a", Star); ("b", Star); ("x", a_or_b_ty) ]
       (appl
          [
            Var "x";
            b_or_a_ty;
            lam "l" (Var "a") (appl [ disj_intro2; Var "b"; Var "a"; Var "l" ]);
            lam "l" (Var "b") (appl [ disj_intro1; Var "b"; Var "a"; Var "l" ]);
          ]))
    (pi' [ ("a", Star); ("b", Star); ("x", a_or_b_ty) ] b_or_a_ty);
  let not_a_or_b = appl [ negate; appl [ disj; Var "a"; Var "b" ] ] in
  let not_a_and_not_b =
    appl [ conj; appl [ negate; Var "a" ]; appl [ negate; Var "b" ] ]
  in
  (* not (A | B) => (not A) & (not B) *)
  check_type
    (lam'
       [ ("a", Star); ("b", Star); ("x", not_a_or_b) ]
       (appl
          [
            conj_intro;
            appl [ negate; Var "a" ];
            appl [ negate; Var "b" ];
            lam "y" (Var "a")
              (appl
                 [ Var "x"; appl [ disj_intro1; Var "a"; Var "b"; Var "y" ] ]);
            lam "y" (Var "b")
              (appl
                 [ Var "x"; appl [ disj_intro2; Var "a"; Var "b"; Var "y" ] ]);
          ]))
    (pi' [ ("a", Star); ("b", Star); ("x", not_a_or_b) ] not_a_and_not_b);
  (* Universal quantification; dependent function type. *)
  let forall =
    lam'
      [ ("a", Star); ("p", pi "x" (Var "a") Star) ]
      (pi "x" (Var "a") (appl [ Var "p"; Var "x" ]))
  in

  (* We get the introduction and elimination rules for universal quantification
     for free: they are just lambda abstraction and application. *)

  (* Existential quantification; sigma type. *)
  let exists =
    lam'
      [ ("a", Star); ("p", pi "x" (Var "a") Star) ]
      (pi'
         [
           ("c", Star);
           ( "f",
             pi' [ ("x", Var "a"); ("y", appl [ Var "p"; Var "x" ]) ] (Var "c")
           );
         ]
         (Var "c"))
  in
  (* x => P(x) => exists x, P(x) *)
  let exists_intro =
    lam'
      [
        ("a", Star);
        ("p", pi "x" (Var "a") Star);
        ("x", Var "a");
        ("y", appl [ Var "p"; Var "x" ]);
      ]
      (lam'
         [
           ("c", Star);
           ( "f",
             pi' [ ("x", Var "a"); ("y", appl [ Var "p"; Var "x" ]) ] (Var "c")
           );
         ]
         (appl [ Var "f"; Var "x"; Var "y" ]))
  in
  check_type exists_intro
    (pi'
       [
         ("a", Star);
         ("p", pi "x" (Var "a") Star);
         ("x", Var "a");
         ("y", appl [ Var "p"; Var "x" ]);
       ]
       (appl [ exists; Var "a"; Var "p" ]));
  (* not (exists x, P(x)) *)
  let not_exists = appl [ negate; appl [ exists; Var "a"; Var "p" ] ] in
  (* forall y, not (P(y)) *)
  let forall_not =
    appl
      [
        forall;
        Var "a";
        lam "y" (Var "a") (appl [ negate; appl [ Var "p"; Var "y" ] ]);
      ]
  in
  (* not (exists x, P(x)) => forall y, not (P(y)) *)
  check_type
    (lam'
       [ ("a", Star); ("p", pi "x" (Var "a") Star); ("x", not_exists) ]
       (lam'
          [ ("y", Var "a"); ("z", appl [ Var "p"; Var "y" ]) ]
          (appl
             [
               Var "x";
               appl [ exists_intro; Var "a"; Var "p"; Var "y"; Var "z" ];
             ])))
    (pi'
       [ ("a", Star); ("p", pi "x" (Var "a") Star); ("x", not_exists) ]
       forall_not)

let classical_logic () =
  (* The same as in our intuitionistic logic. *)
  let absurdity = pi "a" Star (Var "a") in
  let negate = lam "a" Star (pi "x" (Var "a") absurdity) in
  let dn = appl [ negate; appl [ negate; Var "a" ] ] in
  (* not (not A) => A; double negation law (DN) *)
  let dn_law = pi' [ ("a", Star); ("y", dn) ] (Var "a") in
  (* We can use CoC as a metacalculus for classical logic, by injecting either
     DN or ET (excluded third) into the context as axioms. However, for the sake
     of brevity, here we only deal with DN. *)
  check_type
    ~ctx:[ ("dn", dn_law); ("a", Star); ("x", dn) ]
    (appl [ Var "dn"; Var "a"; Var "x" ])
    (Var "a");
  let not_a = appl [ negate; Var "a" ] in
  (* (not A => A) => A *)
  check_type
    ~ctx:[ ("dn", dn_law) ]
    (lam'
       [ ("a", Star); ("x", pi "y" not_a (Var "a")) ]
       (appl
          [
            Var "dn";
            Var "a";
            lam "z" not_a (appl [ Var "z"; appl [ Var "x"; Var "z" ] ]);
          ]))
    (pi' [ ("a", Star); ("x", pi "y" not_a (Var "a")) ] (Var "a"));
  let not_a_implies_b = appl [ negate; pi "x" (Var "a") (Var "b") ] in
  (* not (A => B) => A *)
  check_type
    ~ctx:[ ("dn", dn_law) ]
    (lam'
       [ ("a", Star); ("b", Star); ("x", not_a_implies_b) ]
       (appl
          [
            Var "dn";
            Var "a";
            lam "z" not_a
              (appl
                 [
                   Var "x";
                   lam "v" (Var "a") (appl [ Var "z"; Var "v"; Var "b" ]);
                 ]);
          ]))
    (pi' [ ("a", Star); ("b", Star); ("x", not_a_implies_b) ] (Var "a"));
  let a_implies_b_implies_a = pi "x" (pi "y" (Var "a") (Var "b")) (Var "a") in
  (* ((A => B) => A) => A; Peirce's law *)
  check_type
    ~ctx:[ ("dn", dn_law) ]
    (lam'
       [ ("a", Star); ("b", Star); ("x", a_implies_b_implies_a) ]
       (appl
          [
            Var "dn";
            Var "a";
            lam "z" not_a
              (appl
                 [
                   Var "z";
                   appl
                     [
                       Var "x";
                       lam "v" (Var "a") (appl [ Var "z"; Var "v"; Var "b" ]);
                     ];
                 ]);
          ]))
    (pi' [ ("a", Star); ("b", Star); ("x", a_implies_b_implies_a) ] (Var "a"))

let () =
  church_booleans ();
  church_numerals ();
  intuitionistic_logic ();
  classical_logic ()

in proof assistants, such as Lean and Coq, and programming languages as well, such as Neut, Agda, Idris, and many others

Agda is much more a proof assistant than a programming language.

While Lean 4 can be considered more of a programming language than a proof assistant nowadays... 😅

applicative order evaluation (arguments evaluated first)

I'd say "applicative order of evaluation" but that not so important. What's important is CoC being strongly normalizing systems which means evaluation order doesn't matter (from a metatheoretical point at least).

Other well-known similar educational projects include

• Elaboration Zoo
• SmallTT

Agda is much more a proof assistant than a programming language.

Didn't know! If I understand it correctly, Agda's underlying theory was presented in a paper called "Towards a practical programming language based on dependent type theory". Did the author change the focus to theorem proving since then, or did I misunderstand something?

Did the author change the focus to theorem proving since then, or did I misunderstand something?

I'm not sure the focus ever was on programming. Nowadays you can't even easily run the programs, so... And I don't know anyone caring about running their Agda programs. 😏

Thank you for this great post!

You're welcome!

Did the author change the focus to theorem proving since then, or did I misunderstand something?

I'm not sure the focus ever was on programming. Nowadays you can't even easily run the programs, so... And I don't know anyone caring about running their Agda programs. smirk

https://github.com/WhatisRT/meta-cedille is written in 100% Agda and is supposed to be fully executable.

I'm not sure the focus ever was on programming. Nowadays you can't even easily run the programs, so... And I don't know anyone caring about running their Agda programs. smirk

https://github.com/WhatisRT/meta-cedille is written in 100% Agda and is supposed to be fully executable.

Awesome! 🔥

I retract my correction then. 😅

Speaking of proof vs. programming languages, there is one notable "newcomer" - Kind. Yes, dependently typed, fast (and maximally parallel), pure, etc.