church_graded.ml

let Closed A = ∀(G : Grade). A [G]
// closed as it is unknown how many copies it will be needed(0..1)
let Bool : Type = ∀(A : Type). Closed A -> Closed A -> Closed A
let true : Closed Bool =
  // safe to ignore y as it is used 0 times
  ΛG. [ΛA. fun x y -> let [y] = y 0 in x]
let false : Closed Bool =
  ΛG. [ΛA. fun x y -> let [y] = x 0 in y]

// same applies to nats but (0..n)
let Nat : Type = ∀(A : Type). Closed A -> Closed (A -> A) -> Closed A;
let zero : Closed Nat =
  ΛG. [ΛA. fun z s -> let [s] = s 0 in z];
let one : Closed Nat =
  ΛG. [ΛA. fun z s -> let [s] = s 1 in s z];
let two : Closed Nat =
  ΛG. [ΛA. fun z s -> let [s] = s 2 in s (s z)];