Length-indexed lists

Vector.ml

(*
   We don't really care about the data constructors here
   but they are needed, cf:
   https://sympa.inria.fr/sympa/arc/caml-list/2013-10/msg00190.html
 *)
type zero    = Zero
type 'a succ = Succ

(*
   []   has length 0
   (::) adds one to the length of the tail
*)

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

let param  : (int, zero succ succ succ succ) vector = [3;1;0;4]
let param_ : (int, _) vector = [3;1;0;4]

let () = match param_ with
 (*  [x;y;z] -> print "Argh!\n" *)
  [x;y;z;t] -> print_string "Yeah!\n"

(*
   The simplest thing we can do with these vectors is to erase
   them back to lists:
*)

let rec toList : type n. ('a, n) vector -> 'a list = function
  | []       -> List.[]
  | x :: xs' -> List.(x :: toList xs')

(*
   It's also really easy to, starting from a list, build up a pair
   of a length and a vector of that length.
*)

type _ nat =
  | Zero : zero nat
  | Succ : 'n nat -> 'n succ nat

type 'a evector = EVector : 'n nat * ('a, 'n) vector -> 'a evector

let enil  : 'a evector = EVector (Zero, [])
let econs : 'a -> 'a evector -> 'a evector =
  fun x (EVector (n, xs)) -> EVector (Succ n, x :: xs)

let toEVector : 'a list -> 'a evector =
  fun xs -> List.fold_right econs xs enil

(*
   Converting from a list to a vector of a given length cannot be free:
   we have no guarantee whatsoever that it will have the appropriate size!
   So we need to have a runtime check. A clean way of doing that is to
   check that the length is equal to the natural number we wanted and
   then cast the vector.

   So here is the GADT representing equality. It has one constructor
   which states that both of its arguments are equal:
*)

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

(*
   And here is the function which, given a vector of size m and a proof
   that m equals n returns a vector of size n
*)

let cast_vector : type m n. ('a, m) vector -> (m, n) eq -> ('a, n) vector =
  fun xs e -> match e with Refl -> xs

(*
   Now, we prove that we can check that two natural numbers are equal
   (I could not find option_map so I defined it quickly here):
*)

let option_map (f : 'a -> 'b) (ma : 'a option) : 'b option =
  match ma with
  | Some a -> Some (f a)
  | None   -> None

let eq_succ : type m n. (m, n) eq -> (m succ, n succ) eq =
  function Refl -> Refl

let rec eq_nat : type m n. m nat -> n nat -> (m, n) eq option =
  fun m n -> match (m, n) with
  | (Zero   , Zero)    -> Some Refl
  | (Succ m', Succ n') -> option_map eq_succ (eq_nat m' n')
  | _                  -> None

(*
   We are now ready to write the function that given a size and a list,
   converts that list to a vector of that size provided that they match
   up. We simply use evector, have a runtime check making sure that it
   has the right size and use the proof of equality to cast it to the
   size we were expecting.
*)

let toVector (n : 'n nat) (xs : 'a list) : ('a, 'n) vector option =
  match toEVector xs with
    EVector (m, xs') -> option_map (cast_vector xs') (eq_nat m n)