vec.ml

(* type level naturals *)

type zero = |
type 'n suc = |

type _ nat =
  | Z : zero nat
  | S : 'n nat -> 'n suc nat

(* length indexed lists *)

type (_, _) vec =
  | [] : ('a, zero) vec
  | (::) : 'a * ('a, 'n) vec -> ('a, 'n suc) vec

let rec length : type n. (_, n) vec -> n nat =
  function
  | [] -> Z
  | _ :: xs -> S (length xs)

(* type level addition *)

type (_, _, _) add =
  | AddZ : (zero, 'n, 'n) add
  | AddS : ('a, 'b, 'c) add -> ('a suc, 'b, 'c suc) add

type (_, _) add_e = Add : ('n, 'm, 's) add -> ('n, 'm) add_e [@@unboxed]

let rec add : type n m. n nat -> m nat -> (n, m) add_e =
  fun n m ->
  match n with
  | Z -> Add AddZ
  | S n -> let Add p = add n m in Add (AddS p)

(* append *)

let rec append : type n m s. (n, m, s) add -> ('a, n) vec -> ('a, m) vec -> ('a, s) vec =
  fun p xs ys ->
  match p, xs with
  | AddZ, [] -> ys
  | AddS p, x :: xs -> x :: append p xs ys

(*****************)

let print_vec xs =
  let rec go : type n. string -> string -> (int, n) vec -> unit =
    fun s1 s2 xs ->
      match xs with
      | [] -> print_endline s2
      | x :: xs -> print_string s1; print_int x; go ";" "]" xs
  in
  go "[" "[]" xs

let () =
  let a = [1; 2; 3] in
  print_vec a;
  let b = [4; 5] in
  print_vec b;
  let Add p = add (length a) (length b) in
  let c = append p a b in
  print_vec c