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 ¹

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_binding_vars () =
  assert (binding_vars (Var "x") = []);
  assert (binding_vars (lam "x" Star (Var "x")) = [ "x" ]);
  assert (binding_vars (lam "x" (Var "y") (Var "x")) = [ "x" ]);
  assert (binding_vars (lam "x" Star (Var "y")) = [ "x" ]);
  assert (
    binding_vars (lam "x" (pi "y" Star (Var "y")) (Var "x")) = [ "x"; "y" ]);
  assert (binding_vars (Appl (Var "x", Var "y")) = []);
  assert (
    binding_vars (Appl (lam "x" Star (Var "z"), lam "y" Star (Var "z")))
    = [ "x"; "y" ]);
  assert (binding_vars Star = []);
  assert (binding_vars Box = [])

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

let test_subst () =
  assert (subst (Var "x") "x" (Var "y") = Var "y");
  assert (subst (Var "x") "y" (Var "z") = Var "x");

  assert (subst (Appl (Var "x", Var "y")) "x" (Var "z") = Appl (Var "z", Var "y"));
  assert (subst (Appl (Var "x", Var "y")) "y" (Var "z") = Appl (Var "x", Var "z"));
  assert (subst (Appl (Var "x", Var "y")) "x" (Var "z") = Appl (Var "z", Var "y"));
  assert (subst (Appl (Var "x", Var "y")) "z" (Var "l") = Appl (Var "x", Var "y"));

  assert (subst (lam "x" Star (Var "x")) "x" (Var "z") = lam "x" Star (Var "x"));
  assert (
    subst (lam "x" (Var "x") (Var "x")) "x" (Var "z")
    = lam "x" (Var "z") (Var "x"));
  assert (subst (lam "x" Star (Var "y")) "y" (Var "z") = lam "x" Star (Var "z"));

  (* Check that the new binding variable does not accidentally capture the
     substitution term... *)
  assert (subst (lam "x" Star (Var "y")) "y" (Var "x") = lam "x'" Star (Var "x"));

  (* ... and that it does not capture free variables in the body. *)
  assert (
    subst (lam "x" Star (Appl (Var "y", Var "x'"))) "y" (Var "x")
    = lam "x''" Star (Appl (Var "x", Var "x'")));

  (* ... and that it does not conflict with bindings in the body. *)
  assert (
    subst (lam "x" Star (lam "x'" Star (Appl (Var "y", Var "x")))) "y" (Var "x")
    = lam "x''" Star (lam "x'" Star (Appl (Var "x", Var "x''"))));

  assert (subst Star "x" (Var "z") = Star);
  assert (subst Box "x" (Var "z") = 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"))))

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")) = "(xy)");
  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_binding_vars ();
  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

type binder = Lam | Pi

(* 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

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

let rec free_vars (t : term) =
  match t with
  | Var x -> [ x ]
  | Appl (m, n) -> free_vars m @ free_vars n
  | Binder (_, x, ty, m) -> free_vars ty @ List.filter (( <> ) x) (free_vars m)
  | Star | Box -> []

let rec binding_vars (t : term) =
  match t with
  | Appl (m, n) -> binding_vars m @ binding_vars n
  | Binder (_, x, ty, m) -> [ x ] @ binding_vars ty @ binding_vars m
  | _ -> []

let all_vars (t : term) = free_vars t @ binding_vars t

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

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

let rec subst (t : term) (x : string) (m : term) =
  match t with
  | Var y -> if y = x then m else t
  | Appl (m', n) -> Appl (subst m' x m, subst n x m)
  | Binder (binder, y, ty, n) when x = y -> Binder (binder, y, subst ty x m, n)
  | Binder (binder, y, ty, n) when List.mem y (free_vars m) ->
      let banlist = free_vars m @ all_vars n in
      let fresh_y = fresh_var banlist y in
      let renamed_n = subst n y (Var fresh_y) in
      Binder (binder, fresh_y, subst ty x m, subst renamed_n x m)
  | Binder (binder, y, ty, n) -> Binder (binder, y, subst ty x m, subst n x m)
  | Star | Box -> t

(* 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 (m : term) (n : term) =
  match (m, n) with
  | Var x, Var y -> x = y
  | Appl (m, n), Appl (m', n') -> alpha_eq m m' && alpha_eq n n'
  | Binder (_, x, ty, m), Binder (_, x', ty', m') ->
      if x = x' then alpha_eq ty ty' && alpha_eq m m'
      else
        let banlist = all_vars m @ all_vars m' in
        let fresh_x = fresh_var banlist x in
        alpha_eq ty ty'
        && alpha_eq (subst m x (Var fresh_x)) (subst m' x' (Var fresh_x))
  | Star, Star | Box, Box -> true
  | _, _ -> false

(* Reduces a term to its beta normal form using applicative order. *)
let rec eval (t : term) =
  match t with
  | Appl (m, arg) -> (
      (* Application is left-associative. *)
      match eval m with
      | Binder (Lam, x, _, m) -> eval (subst m x (eval arg))
      | Binder (Pi, _, _, _) ->
          failwith
            (Printf.sprintf
               "Ill-typed application of argument %s to non-lambda %s"
               (print arg) (print m))
      | _ -> Appl (m, eval arg))
  | Binder (binder, x, ty, m) -> Binder (binder, x, eval ty, eval m)
  | Var _ | Star | Box -> t

(* 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 = []) (t : term) =
  match t with
  | Var x -> eval (List.assoc x ctx)
  | Appl (m, n) -> (
      match (infer_type ~ctx m, infer_type ~ctx n) with
      | Binder (Pi, x, ty, m), arg_ty ->
          if alpha_eq ty arg_ty then eval (subst m x n)
          else
            failwith
              (Printf.sprintf
                 "Argument type mismatch in %s: expected %s, found %s" (print t)
                 (print ty) (print arg_ty))
      | m_ty, n_ty ->
          failwith
            (Printf.sprintf
               "Application of argument %s (type %s) to non-lambda %s (type %s)"
               (print n) (print n_ty) (print m) (print m_ty)))
  | Binder (Lam, x, ty, m) ->
      let m_ty = infer_type ~ctx:((x, ty) :: ctx) m in
      let lam_ty = Binder (Pi, x, ty, m_ty) in
      let _ = infer_type ~ctx lam_ty in
      eval lam_ty
  | Binder (Pi, x, ty, m) ->
      let _s1 = infer_type ~ctx ty in
      let s2 = infer_type ~ctx:((x, ty) :: ctx) m in
      s2
  | Star -> Box
  | Box -> failwith "☐ has no type"

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

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' (b : binder) (ctx : context) (m : term) =
  match ctx with
  | [] -> failwith "Empty argument list"
  | ctx -> List.fold_right (fun (x, ty) acc -> Binder (b, x, ty, acc)) ctx m

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

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

let check ?(ctx = []) t expected =
  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 ()