hirrolot · November 13, 2024 04:32 · gabriel-fallen · Feb 26, 2023 · Pitometsu · Mar 2, 2023
diff --git a/a-preface.md b/a-preface.md
diff --git a/CoC.ml b/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 -> 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
          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)
diff --git a/usage.ml b/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 ]) ) )
                    ) ) );
    ]
    (* A typing context must contain only evaluated types. *)
    |> List.map eval
    (* Context bindings must be indexed by De Bruijn indices, not levels. *)
    |> 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))
	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 -> 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
	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)
	(* 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 ]) ) )
	) ) );
	]
	(* A typing context must contain only evaluated types. *)
	\|> List.map eval
	(* Context bindings must be indexed by De Bruijn indices, not levels. *)
	\|> 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))