Peano, List, Proof

main.ml

module List =
struct
  include List

  let empty = []
  let cons x r = x :: r
end

type z = Z
type +'a s = S

type _ nat =
  | Z : ('l * 'l) nat
  | S : ('l * 'm) nat -> ('l * 'm s) nat

(* no tail-rec *)
let rec shift : type l m. (l * m) nat -> (l s * m s) nat = function
  | Z -> Z
  | S i -> S (shift i)

let rec add : type l m n. (l * m) nat -> (m * n) nat -> (l * n) nat =
  fun i1 i2 -> match i2 with
    | Z -> i1
    | S i -> add (S i1) (shift i)

let shift : type l m. (l * m) nat -> (l s * m s) nat =
  let rec aux : type l m c. ((l s * m s) nat -> c) -> (l * m) nat -> c =
    fun k i -> match i with
      | Z -> k Z
      | S j -> aux (fun i -> k (S i)) j
  in fun i -> aux (fun x -> x) i

let rec add : type l m n. (l * m) nat -> (m * n) nat -> (l * n) nat =
  fun i1 i2 -> match i2 with
    | Z -> i1
    | S i -> add (S i1) (shift i)

let rec to_int
  : type l m. (l * m) nat -> int
  = function
  | Z -> 0
  | S i -> 1 + (to_int i)

type ('a, 'l) vec =
  | [] : ('a, 'l * 'l) vec
  | (::) : 'a * ('a, 'l * 'm) vec -> ('a, 'l * 'm s) vec
let rec to_list
  : type l m. ('a, l * m) vec -> 'a list
  = function
    | [] -> List.[]
    | x :: r -> let r = to_list r in List.(x :: r)

let rec map2
  : type l m. ('a * 'b -> 'c) -> ('a, z * m) vec -> ('b, z * m) vec -> ('c, z * m) vec
  = fun f v1 v2 -> match v1, v2 with
    | [], [] -> []
    | (x1 :: r1), (x2 :: r2) -> f (x1, x2) :: (map2 f r1 r2)

let head
  : type m. ('a, z * m s) vec -> 'a = function
  | x :: _ -> x

let tail
  : type m. ('a, z * m s) vec -> ('a, z * m) vec = function
  | x :: r -> r

let empty : ('a, 'l * 'l) vec = []
let cons  : type l m. 'a -> ('a, l * m) vec -> ('a, l * m s) vec = fun x r -> x :: r

let shift
  : type l m. ('a, l * m) vec -> ('a, l s * m s) vec
  =
  let rec aux : type l m c. (('a, l s * m s) vec -> c) -> ('a, l * m) vec -> c =
      fun k -> function
        | [] -> k []
        | x :: r -> aux (fun r -> k (x :: r)) r
  in fun l -> aux (fun x -> x) l

let rev_append
  : type l m n. ('a, m * n) vec -> ('a, l * m) vec -> ('a, l * n) vec
  =
  let rec aux
    : type l m n. ('a, l * m) vec -> ('a, m * n) vec -> ('a, l * n) vec
    = fun l1 l2 -> match l2 with
      | [] -> l1
      | x :: r -> aux (x :: l1) (shift r)
  in
  fun l2 l1 -> aux l1 l2

let rev l = rev_append l []

let length
  : type l m. ('a, l * m) vec -> int =
  let rec aux
    : type l m c. ((l s * m s) nat -> c) -> ('a, l * m) vec -> c
    = fun k -> function
      | [] -> k Z
      | _ :: r -> aux (fun i -> k (S i)) r
  in fun l -> aux to_int l

type ('a, 'l) v = Vector : ('l * 'm) nat * ('a, 'l * 'm) vec -> ('a, 'l) v

let nil : ('a, 'l) v = Vector (Z, [])
let cons : 'a -> ('a, 'l) v -> ('a, 'l) v = fun x (Vector (n, r)) -> Vector (S n, x :: r)

let to_v : 'a list -> ('a, 'l) v =
  fun lst -> List.fold_right cons lst nil

type (_, _) eq = Refl : ('a, 'a) eq

let cast_v
  : type l m n. ('a, l * m) vec -> (m, n) eq -> ('a, l * n) vec
  = fun l e -> match e with Refl -> l

let option_map
  : ('a -> 'b) -> 'a option -> 'b option
  = fun f -> function
    | Some a -> Some (f a)
    | None -> None

let equality_s
  : type m n. (m, n) eq -> (m s, n s) eq
  = function Refl -> Refl

let rec equality_nat
  : type l m n. (l * m) nat -> (l * n) nat -> (m, n) eq option
  = fun m n -> match m, n with
    | (Z, Z) -> Some Refl
    | (S m', S n') -> option_map equality_s (equality_nat m' n')
    | _ -> None

let to_vec
  : type l m. (l * m) nat -> 'a list -> ('a, l * m) vec option =
  fun n lst -> match to_v lst with
    Vector (n', l') -> option_map (cast_v l') (equality_nat n' n)

let zero  = Z
let one   = S zero
let two   = S one
let three = S two
let four  = S three
let five  = S four

let () =
  let rec go acc = match read_int () with
    | n -> go (List.cons n acc)
    | exception End_of_file -> List.rev acc
  in

  go List.empty |> to_vec five |> function
  | Some lst ->

    (* in this case, we ensure than [lst] has 5 elements. *)

    map2 (fun (x, y) -> x + y) lst [0;1;2;3;4]
    |> to_list
    |> List.iter print_int
  | None -> raise (Invalid_argument "Invalid list")

👍