How to implement dependent types in 80 lines of code

a-preface.md

How to implement dependent types in 80 lines of code

The only difference(!) between Shakespeare and you was the size of his idiom list -- not the size of his vocabulary.
    -- Alan Perlis, Epigrams on Programming ¹

Dependent types are constantly gaining more and more attention in the world of functional programming. Some believe that, through the unification of type and term-level syntax ^{2 3}, they are capable of displacing many specific typing features of traditional languages, such as Haskell or OCaml, whereas others believe in the feasibility of proving theorems about code in the same language, through the fusion of programming and constructive mathematics ^{4 5}.

But what are dependent types, actually? Just as in most general-purpose programming languages we have types dependent on types, colloquially known as "generic types", in dependently typed languages, we have types dependent on terms. This addition makes the language very expressive, effectively enabling a user to perform term computation at compile-time. For example, consider what should happen when the type checker sees some argument x applied to f -- it should check that the type of x is computationally equal (or "beta-convertible", as used in the literature) to the parameter type of f; this check involves reducing these two types to their beta normal forms and comparing them for alpha equivalence ^{6 7}.

The fact that type checking can literally invoke evaluation makes dependent types not only interesting from a user's standpoint but also from that of a language implementer. In particular, one may wonder about the easiest way to implement dependent types. Of course, to fully answer the question, we must consider the exact features to be implemented -- dependent type systems range from some of the most minimalistic lambda calculi to some of the most sophisticated type systems used in practice. For the purposes of this writing, we are going to consider Calculus of Constructions (CoC) ⁸, which situates at the top of Barendregt's lambda cube. What makes CoC exciting is its simplicity and expressiveness: by permitting all four combinations of terms and types to depend on each other and by being strongly normalizing ⁹, it can serve both as a type theory for a programming language ¹⁰ and as a type-theoretical foundation of (constructive) mathematics; at the same time, it has only one syntactic category that accommodates both terms and types.

As it turns out, implementing CoC should not take much code. A few months ago, I demonstrated the implementation of CoC in about 120 lines of OCaml. It was using a named representation of variables -- this is how lambda calculi are described in a typical textbook. However, there is still room for improvement: since variables are strings, we should take care of capture-avoiding substitution, renaming of bound variables during an alpha-equivalence check, and so on. This approach is notoriously wordy, inefficient, and error-prone. Using De Bruijn indices would not grant much simplification either since free variables now have to be reindexed each time we substitute under a binder.

Naturally, to come up with the most succinct (yet readable) implementation, we should reuse as much of the metalanguage (OCaml in our case) as possible. Thus we arrive at Higher-Order Abstract Syntax (HOAS) -- a technique to encode object-language binders in terms of metalanguage functions ¹¹. By doing this, we can now get rid of the machinery that was in charge of manipulating the first-order representation and instead focus on the essential parts of the implementation. To allow the manipulation of open terms, we extend HOAS with a constructor for free variables represented as De Bruijn levels. The file CoC.ml below uses the technique just described and consists of 80 lines of standalone OCaml. In contrast to the previous implementation, it also employs bidirectional typing ^{12 13}, which lets us omit type annotations in certain cases, e.g., we can omit the parameter type of a lambda abstraction if the latter is located in the argument position.

As an application of the developed system, I present a classical example of using dependent types: vectors parameterized by their length. Since vector lengths now dwell on type-level, we can guarantee statically that, for example, the replicate operation returns a vector of a given length, concat returns a vector whose length is equal to the sum of lengths of two passed vectors, and zip takes two vectors of the same length and returns a vector of that length. The code relies on some rudimentary facilities of Church numerals and pairs, which also serve as a warm-up.

To learn about the theory behind Calculus of Constructions, I recommend reading the first seven chapters of "Type Theory and Formal Proof: An Introduction".

If something is unclear, feel free to ask in the comments ¹⁴.

Show unit tests

let test_print () =
  assert (print 123 @@ FreeVar 42 = "42");
  assert (print 42 Star = "*");
  assert (print 42 Box = "☐");
  (* Lambdas. *)
  assert (print 3 @@ Lam (fun x -> x) = "(λ3)");
  assert (print 3 @@ Lam (fun x -> Appl (x, FreeVar 42)) = "(λ(3 42))");
  (* Pi types. *)
  assert (print 3 @@ Pi (FreeVar 0, fun x -> x) = "(Π0.3)");
  assert (
    print 3 @@ Pi (FreeVar 0, fun x -> Appl (x, FreeVar 42)) = "(Π0.(3 42))");
  (* Applications. *)
  assert (print 42 @@ Appl (FreeVar 1, FreeVar 2) = "(1 2)");
  (* Annotations. *)
  assert (print 42 @@ Ann (FreeVar 1, FreeVar 2) = "(1 : 2)")

let test_equate () =
  let assert_eq t = assert (equate 42 (t, t)) in
  let assert_neq m n =
    assert (not @@ equate 42 (m, n));
    assert (not @@ equate 42 (n, m))
  in
  (* Free variables. *)
  assert_eq (FreeVar 0);
  assert_neq (FreeVar 0) (FreeVar 123);
  assert_neq (FreeVar 0) Star;
  (* Star and box. *)
  assert_eq Star;
  assert_neq Star (FreeVar 0);
  assert_eq Box;
  assert_neq Box (FreeVar 0);
  (* Lambdas. *)
  assert_eq (Lam (fun x -> x));
  assert_neq (Lam (fun x -> x)) (Lam (fun _ -> Star));
  assert_neq (Lam (fun x -> x)) Star;
  (* Pi types. *)
  assert_eq (Pi (FreeVar 0, fun x -> x));
  assert_neq (Pi (FreeVar 0, fun x -> x)) (Pi (FreeVar 123, fun x -> x));
  assert_neq (Pi (FreeVar 0, fun x -> x)) (Pi (FreeVar 0, fun _ -> Star));
  assert_neq (Pi (FreeVar 0, fun x -> x)) Star;
  (* Do not evaluate under a binder automatically. *)
  assert_neq (Lam (fun x -> x)) (Lam (fun x -> Appl (Lam (fun x -> x), x)));
  assert_neq
    (Pi (FreeVar 0, fun x -> x))
    (Pi (FreeVar 0, fun x -> Appl (Lam (fun x -> x), x)));
  (* Applications. *)
  assert_eq (Appl (FreeVar 0, FreeVar 1));
  assert_neq (Appl (FreeVar 0, FreeVar 1)) (Appl (FreeVar 123, FreeVar 1));
  assert_neq (Appl (FreeVar 0, FreeVar 1)) (Appl (FreeVar 0, FreeVar 123));
  assert_neq (Appl (FreeVar 0, FreeVar 1)) Star;
  (* Annotations. *)
  assert_eq (Ann (FreeVar 0, FreeVar 1));
  assert_neq (Ann (FreeVar 0, FreeVar 1)) (Ann (FreeVar 123, FreeVar 1));
  assert_neq (Ann (FreeVar 0, FreeVar 1)) (Ann (FreeVar 0, FreeVar 123));
  assert_neq (Ann (FreeVar 0, FreeVar 1)) Star

let test_eval () =
  let assert_eval t expected = assert (equate 0 (eval t, expected)) in
  assert_eval (FreeVar 42) (FreeVar 42);
  assert_eval Star Star;
  assert_eval Box Box;
  (* Lambdas. *)
  assert_eval (Lam (fun x -> x)) (Lam (fun x -> x));
  assert_eval (Lam (fun x -> Appl (Lam (fun x -> x), x))) (Lam (fun x -> x));
  (* Pi types. *)
  assert_eval (Pi (FreeVar 42, fun x -> x)) (Pi (FreeVar 42, fun x -> x));
  assert_eval
    (Pi (FreeVar 42, fun x -> Appl (Lam (fun x -> x), x)))
    (Pi (FreeVar 42, fun x -> x));
  (* Applications. *)
  assert_eval (Appl (Lam (fun x -> x), FreeVar 42)) (FreeVar 42);
  assert_eval (Appl (FreeVar 0, FreeVar 42)) (Appl (FreeVar 0, FreeVar 42));
  assert_eval
    (Appl (Appl (Lam (fun x -> x), FreeVar 0), FreeVar 42))
    (Appl (FreeVar 0, FreeVar 42));
  (* Annotations. *)
  assert_eval (Ann (FreeVar 42, FreeVar 0)) (FreeVar 42)

let assert_infer_sort ctx t expected_ty =
  let lvl = List.length ctx in
  assert (equate lvl (infer_sort lvl ctx t, expected_ty))

let test_infer_sort () =
  assert_infer_sort [] Star Box;
  assert_infer_sort [ Star ] (FreeVar 0) Star;
  assert_infer_sort [ Box ] (FreeVar 0) Box;
  try
    assert_infer_sort [ FreeVar 0; Star ] (FreeVar 1) Box;
    assert false
  with Failure msg -> assert (msg = "Want a sort, got 0: 1")

let assert_infer ctx t expected_ty =
  let lvl = List.length ctx in
  assert (equate lvl (infer_ty lvl ctx t, expected_ty))

let test_infer_var () =
  assert_infer [ Star ] (FreeVar 0) Star;
  assert_infer [ Box; Star ] (FreeVar 0) Star;
  assert_infer [ Box; Box; Star ] (FreeVar 0) Star;
  assert_infer [ Star; Box ] (FreeVar 1) Star;
  assert_infer [ Box; Star; Box ] (FreeVar 1) Star;
  assert_infer [ Star; Box; Box ] (FreeVar 2) Star;
  assert_infer [ Box; Star; Box; Box ] (FreeVar 2) Star;
  try
    assert_infer [ Star; Box; Box ] (FreeVar 3) Box;
    assert false
  with Invalid_argument msg -> assert (msg = "List.nth")

let test_infer_star_box () =
  assert_infer [] Star Box;
  assert_infer [ Box; Box; Box ] Star Box;
  try
    assert_infer [] Box Box;
    assert false
  with Failure msg -> assert (msg = "Has no type: ☐")

let test_infer_pi () =
  (* A term depending on a term. *)
  assert_infer
    [ Pi (FreeVar 0, fun _ -> Star); Star ]
    (Pi (FreeVar 0, fun x -> Appl (FreeVar 1, x)))
    Star;
  (* A term depending on a type. *)
  assert_infer
    [ Pi (Star, fun _ -> Star) ]
    (Pi (Star, fun x -> Appl (FreeVar 0, x)))
    Star;
  (* A type depending on a term. *)
  assert_infer
    [ Pi (FreeVar 0, fun _ -> Box); Star ]
    (Pi (FreeVar 0, fun x -> Appl (FreeVar 1, x)))
    Box;
  (* A type depending on a type. *)
  assert_infer
    [ Pi (Star, fun _ -> Box) ]
    (Pi (Star, fun x -> Appl (FreeVar 0, x)))
    Box;
  try
    assert_infer [ FreeVar 0; Star ] (Pi (FreeVar 1, fun _ -> Star)) Box;
    assert false
  with Failure msg -> (
    assert (msg = "Want a sort, got 0: 1");
    try
      assert_infer [ FreeVar 0; Star ] (Pi (Star, fun _ -> FreeVar 1)) Box;
      assert false
    with Failure msg -> assert (msg = "Want a sort, got 0: 1"))

let test_infer_appl () =
  (* An argument is checkable. *)
  assert_infer
    [ Pi (Pi (Star, fun _ -> Star), fun _ -> FreeVar 0); Star ]
    (Appl (FreeVar 1, Lam (fun x -> x)))
    (FreeVar 0);
  (* An argument is inferrable. *)
  assert_infer
    [ Pi (Star, fun x -> x); Star ]
    (Appl (FreeVar 1, FreeVar 0))
    (FreeVar 0);
  (* Evaluate the resulting type. *)
  assert_infer [ FreeVar 0; Star ]
    (Appl
       ( Ann
           ( Lam (fun _ -> FreeVar 1),
             Pi
               ( Star,
                 fun _ ->
                   Appl
                     ( Ann (Lam (fun x -> x), Pi (Star, fun _ -> Star)),
                       FreeVar 0 ) ) ),
         FreeVar 0 ))
    (FreeVar 0);
  try
    assert_infer [] (Appl (Star, Star)) Box;
    assert false
  with Failure msg -> assert (msg = "Want a Pi type, got ☐: *")

let test_infer_ann () =
  (* Annotate a checkable term. *)
  assert_infer [ Star ]
    (Ann (Lam (fun _ -> FreeVar 0), Pi (FreeVar 0, fun _ -> Star)))
    (Pi (FreeVar 0, fun _ -> Star));
  (* Annotate an inferrable term. *)
  assert_infer [ Star ] (Ann (FreeVar 0, Star)) Star;
  (* Evaluate the resulting type. *)
  assert_infer [ Star ]
    (Ann
       ( Lam (fun x -> x),
         Pi
           ( FreeVar 0,
             fun _ ->
               Appl (Ann (Lam (fun x -> x), Pi (Star, fun _ -> Star)), FreeVar 0)
           ) ))
    (Pi (FreeVar 0, fun _ -> FreeVar 0));
  try
    assert_infer [ FreeVar 0; Star ] (Ann (Star, FreeVar 1)) Box;
    assert false
  with Failure msg -> (
    assert (msg = "Want a sort, got 0: 1");
    try
      assert_infer [ FreeVar 0; Star ] (Ann (FreeVar 1, Star)) Box;
      assert false
    with Failure msg -> assert (msg = "Want type *, got 0: 1"))

let test_infer_lam () =
  try
    assert_infer [] (Lam (fun x -> x)) Box;
    assert false
  with Failure msg -> assert (msg = "Not inferrable: (λ0)")

let assert_check ctx t ty =
  let lvl = List.length ctx in
  assert (equate lvl (check_ty lvl ctx (t, ty), ty))

let test_check_lam () =
  assert_check
    [ Pi (Star, fun _ -> FreeVar 0); Star ]
    (Lam (fun x -> Appl (FreeVar 1, x)))
    (Pi (Star, fun _ -> FreeVar 0));
  try
    assert_check [ Star ] (Lam (fun x -> x)) (Pi (Star, fun _ -> FreeVar 0));
    assert false
  with Failure msg -> (
    assert (msg = "Want type 0, got *: 1");
    try
      assert_check [] (Lam (fun x -> x)) Star;
      assert false
    with Failure msg -> assert (msg = "Want a Pi type, got *: (λ0)"))

let test_check_infer () =
  assert_check [ Star ] (FreeVar 0) Star;
  try
    assert_check [ Box ] (FreeVar 0) Star;
    assert false
  with Failure msg -> assert (msg = "Want type *, got ☐: 0")

let impredicative_id () =
  let id_ty = Pi (Star, fun a -> Pi (a, fun _ -> a)) in
  let id_lam = Lam (fun _ -> Lam (fun x -> x)) in
  let id = Ann (id_lam, id_ty) in
  let id_id = Appl (Appl (id, id_ty), id) in
  assert_infer [] id_ty Star;
  assert_infer [] id id_ty;
  assert_infer [] id_id id_ty;
  assert (equate 0 (eval id_id, id_lam))

let () =
  test_print ();
  test_eval ();
  test_equate ();
  test_infer_sort ();
  test_infer_var ();
  test_infer_star_box ();
  test_infer_pi ();
  test_infer_appl ();
  test_infer_ann ();
  test_infer_lam ();
  test_check_lam ();
  test_check_infer ();
  impredicative_id ()

Footnotes

1. Epigrams on Programming by Alan Perlis ↩

2. Unified Syntax with Iso-Types by Yanpeng Yang, Xuan Bi, and Bruno C. d. S. Oliveira ↩

3. Cayenne — A Language with Dependent Types by Lennart Augustsson ↩

4. Curry–Howard correspondence by Wikipedia ↩

5. Idris: A Language for Type-Driven Development by Edwin Brady ↩

6. Two terms are alpha-equivalent if they are syntactically equal up to renaming of bound variables; e.g., \x . \y . x (the so-called "K combinator") is alpha-equivalent to \a . \b . a. ↩

7. Additional checks may apply to make type checking more permissive; this includes eta conversion -- when \x . f x and f are considered equal. ↩

8. The Calculus of Constructions by Thierry Coquand and Gérard Huet ↩

9. Strong normalization means that every term in the system eventually reduces to its value. ↩

10. One may argue that unrestricted recursion is essential for programming, which obviously destroys strong normalization. However, we can remedy this either by adding a fixed-point combinator to CoC (the Neut way) or by only executing total functions at type-level (the Idris way). ↩

11. One well-known problem with HOAS is that you can define "exotic" terms that pattern-match on a binder variable (e.g., using OCaml's match). At least two solutions exist: Parametric Higher-Order Abstract Syntax (PHOAS) ^{15 16 17} and Tagless Final ^{18 19 20}, both of which make an object language representation parametrically polymorphic over a binder type, thus prohibiting examination of binder variables. ↩

12. Bidirectional Typing Rules: A Tutorial by David Raymond Christiansen ↩

13. Minimal implementations for dependent type checking and elaboration by András Kovács ↩ ↩²

14. If you wish to adopt the implementation below for your needs, it may be worth using Normalization by Evaluation (NbE) ^{13 21}. With NbE, instead of term, you would have term and value, and instead of eval, you would have 1) eval, which goes from term to value, and 2) quote, which goes back from value to term. The apparent advantage of this approach is that you would have a dedicated type for values, which you could use in some places to guarantee type safety; e.g., infer_ty, infer_sort, and check_ty in our implementation could return value instead of term (you could also make the typing context contain only values). The "Boxes Go Bananas" ¹⁷ paper shows how to encode both term and value in terms of HOAS. ↩

15. Parametric Higher-Order Abstract Syntax for Mechanized Semantics by Adam Chlipala ↩

16. Parametric HOAS with first-class modules by Matthias Puech ↩

17. Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism by Geoffrey Washburn and Stephanie Weirich ↩ ↩²

18. Finally Tagless, Partially Evaluated by Jacques Carette, Oleg Kiselyov and Chung-chieh Shan ↩

19. Typed Tagless Final Interpreters by Oleg Kiselyov ↩

20. Tagless-Final Style: Applications and Examples by Oleg Kiselyov ↩

21. Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell version) by David Thrane Christiansen ↩

CoC.ml

type term =
  | Lam of (term -> term)
  | Pi of term * (term -> term)
  | Appl of term * term
  | Ann of term * term
  | FreeVar of int
  | Star
  | Box

let unfurl lvl f = f (FreeVar lvl)
let unfurl2 lvl (f, g) = (unfurl lvl f, unfurl lvl g)

let rec print lvl =
  let plunge f = print (lvl + 1) (unfurl lvl f) in
  function
  | Lam f -> "(λ" ^ plunge f ^ ")"
  | Pi (a, f) -> "(Π" ^ print lvl a ^ "." ^ plunge f ^ ")"
  | Appl (m, n) -> "(" ^ print lvl m ^ " " ^ print lvl n ^ ")"
  | Ann (m, a) -> "(" ^ print lvl m ^ " : " ^ print lvl a ^ ")"
  | FreeVar x -> string_of_int x
  | Star -> "*"
  | Box -> "☐"

let rec eval = function
  | Lam f -> Lam (fun n -> eval (f n))
  | Pi (a, f) -> Pi (eval a, fun n -> eval (f n))
  | Appl (m, n) -> (
      match (eval m, eval n) with Lam f, n -> eval (f n) | m, n -> Appl (m, n))
  | Ann (m, _a) -> eval m
  | (FreeVar _ | Star | Box) as t -> t

let rec equate lvl =
  let plunge (f, g) = equate (lvl + 1) (unfurl2 lvl (f, g)) in
  function
  | Lam f, Lam g -> plunge (f, g)
  | Pi (a, f), Pi (b, g) -> equate lvl (a, b) && plunge (f, g)
  | Appl (m, n), Appl (m', n') -> equate lvl (m, m') && equate lvl (n, n')
  | Ann (m, a), Ann (m', b) -> equate lvl (m, m') && equate lvl (a, b)
  | FreeVar x, FreeVar y -> x = y
  | Star, Star | Box, Box -> true
  | _, _ -> false

let panic lvl t fmt =
  let open Printf in
  let fail fmt = ksprintf failwith fmt in
  ksprintf (fun s -> fail "%s: %s" s (print lvl t)) fmt

let rec infer_ty lvl ctx = function
  | Pi (a, f) ->
      let _s1 = infer_sort lvl ctx a in
      let s2 = infer_sort (lvl + 1) (eval a :: ctx) (unfurl lvl f) in
      s2
  | Appl (m, n) -> (
      match infer_ty lvl ctx m with
      | Pi (a, f) ->
          let _ = check_ty lvl ctx (n, a) in
          eval (f n)
      | m_ty -> panic lvl m "Want a Pi type, got %s" (print lvl m_ty))
  | Ann (m, a) ->
      let _s = infer_sort lvl ctx a in
      check_ty lvl ctx (m, eval a)
  | FreeVar x -> List.nth ctx (lvl - x - 1)
  | Star -> Box
  | Box -> panic lvl Box "Has no type"
  | t -> panic lvl t "Not inferrable"

and infer_sort lvl ctx a =
  match infer_ty lvl ctx a with
  | (Star | Box) as s -> s
  | ty -> panic lvl a "Want a sort, got %s" (print lvl ty)

and check_ty lvl ctx = function
  | Lam f, Pi (a, g) ->
      let _ = check_ty (lvl + 1) (a :: ctx) (unfurl2 lvl (f, g)) in
      Pi (a, g)
  | Lam f, ty -> panic lvl (Lam f) "Want a Pi type, got %s" (print lvl ty)
  | t, ty ->
      let got_ty = infer_ty lvl ctx t in
      if equate lvl (ty, got_ty) then ty
      else panic lvl t "Want type %s, got %s" (print lvl ty) (print lvl got_ty)

usage.ml

(* Currying functions for lambdas. This is only for convenience. *)
let curry2 f = Lam (fun x -> Lam (fun y -> f x y))
let curry3 f = Lam (fun x -> curry2 (f x))
let curry4 f = Lam (fun x -> curry3 (f x))
let curry5 f = Lam (fun x -> curry4 (f x))

(* A left-folded application. *)
let appl f args = List.fold_left (fun m n -> Appl (m, n)) f args

(* Tests two terms for beta-convertibility. *)
let assert_beta_eq m n = assert (equate 0 (eval m, eval n))

let () =
  (* Church numerals. *)
  let n_ty =
    Pi (Star, fun a -> Pi (Pi (a, fun _x -> a), fun _f -> Pi (a, fun _x -> a)))
  in

  (* The zero constant and successor function. *)
  let zero = Ann (curry3 (fun _a _f x -> x), n_ty) in
  let succ =
    Ann
      ( curry4 (fun n a f x -> Appl (f, appl n [ a; f; x ])),
        Pi (n_ty, fun _n -> n_ty) )
  in

  (* 1, 2, 3, 4 derived from zero and the successor function. *)
  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 [] zero n_ty;
  assert_infer [] one n_ty;
  assert_infer [] two n_ty;
  assert_infer [] three n_ty;
  assert_infer [] four n_ty;

  (* The addition function on two numerals. *)
  let add_ty = Pi (n_ty, fun _n -> Pi (n_ty, fun _m -> n_ty)) in
  let add =
    Ann (curry5 (fun n m a f x -> appl n [ a; f; appl m [ a; f; x ] ]), add_ty)
  in
  assert_infer [] add add_ty;

  (* Test addition on the derived numerals. *)
  assert_beta_eq (appl add [ zero; zero ]) zero;
  assert_beta_eq (appl add [ zero; one ]) one;
  assert_beta_eq (appl add [ one; zero ]) one;
  assert_beta_eq (appl add [ three; one ]) four;

  (* Church pairs. *)
  let pair_ty = Pi (Star, fun _a -> Pi (Star, fun _b -> Star)) in
  let pair =
    Ann
      ( Lam
          (fun a ->
            Lam
              (fun b ->
                Pi
                  ( Star,
                    fun c ->
                      Pi (Pi (a, fun _x -> Pi (b, fun _y -> c)), fun _f -> c) ))),
        pair_ty )
  in
  assert_infer [] pair pair_ty;

  (* Type-safe programming with vectors. First, define a typing context that
     represents a hypothetical vector module. *)
  let vect_ty n a = appl (FreeVar 0) [ n; a ] in
  let item_ty = FreeVar 1 in

  let vect_ctx =
    [
      (* A vector parameterized by its length and item type. *)
      Pi (n_ty, fun _n -> Pi (Star, fun _a -> Star));
      (* The uninterpreted vector item type. *)
      Star;
      (* The item value. *)
      item_ty;
      (* The replicate function that constructs a vector containing N items
         of the same value. *)
      Pi (n_ty, fun n -> Pi (Star, fun a -> Pi (a, fun _x -> vect_ty n a)));
      (* The concatenate function on two vectors. *)
      Pi
        ( n_ty,
          fun n ->
            Pi
              ( n_ty,
                fun m ->
                  Pi
                    ( Star,
                      fun a ->
                        Pi
                          ( vect_ty n a,
                            fun _x ->
                              Pi
                                ( vect_ty m a,
                                  fun _y -> vect_ty (appl add [ n; m ]) a ) ) )
              ) );
      (* The zip function that takes two vectors of the same length and
         returns a new zipped vector. *)
      Pi
        ( n_ty,
          fun n ->
            Pi
              ( Star,
                fun a ->
                  Pi
                    ( Star,
                      fun b ->
                        Pi
                          ( vect_ty n a,
                            fun _x ->
                              Pi
                                ( vect_ty n b,
                                  fun _y -> vect_ty n (appl pair [ a; b ]) ) )
                    ) ) );
    ]
    |> List.rev
  in

  let vect_ty n = eval @@ vect_ty n item_ty in
  let item = FreeVar 2 in
  let replicate n x = appl (FreeVar 3) [ n; item_ty; x ] in
  let concat n m x y = appl (FreeVar 4) [ n; m; item_ty; x; y ] in
  let zip n x y = appl (FreeVar 5) [ n; item_ty; item_ty; x; y ] in

  let assert_infer = assert_infer vect_ctx in

  (* Produce a one-value, three-value, and four-value vectors using the
     functions above. *)
  let vect_one = replicate one item in
  let vect_three = replicate three item in
  let vect_four = concat one three vect_one vect_three in
  assert_infer vect_one (vect_ty one);
  assert_infer vect_three (vect_ty three);
  assert_infer vect_four (vect_ty four);

  (* If we attempt to zip two vectors of different lengths, the type checker
     will produce an appropriate error message. This would be impossible
     to assure statically without dependent types or a similar mechanism, such
     as refinement types. *)
  try
    assert_infer (zip four vect_one vect_four) Box;
    assert false
  with Failure msg ->
    let p = print (List.length vect_ctx) in
    assert (
      msg
      = Printf.sprintf "Want type %s, got %s: %s"
          (p @@ vect_ty four)
          (p @@ vect_ty one)
          (p vect_one))