Static size checking for lists (loaded from files) by generative phantom types (first-class-module version)

generative_phantom_type_first_class_module.ml

(* http://akabe.github.io/2015/10/GenerativePhantomTypes *)

#load "str.cma";;

(** Loads a list of integers from a file of a given path (delimiters = spaces,
    tabs, or line feeds). *)
let load_list fname =
  let re = Str.regexp "[ \t]+" in
  let oc = open_in fname in
  let rec aux acc = try aux (input_line oc :: acc) with End_of_file -> acc in
  aux []
  |> List.rev_map (Str.split re)
  |> List.flatten
  |> List.map int_of_string

module SizedList : sig
  type 'n sized_list (** a type of lists of length ['n] (['n] is a phantom type
                         parameter, i.e., it does not appear in the r.h.s. of
                         the type definition) *)
  type z             (** a phantom type corresponding to zero *)
  type 'n s          (** a phantom type corresponding to successor (['n + 1]) *)

  val nil : z sized_list
  val cons : int -> 'n sized_list -> 'n s sized_list
  val hd : 'n s sized_list -> int
  val tl : 'n s sized_list -> 'n sized_list
  val map : (int -> int) -> 'n sized_list -> 'n sized_list
  val add : 'n sized_list -> 'n sized_list -> 'n sized_list

  module type S = sig
    type n
    val x : n sized_list
  end

  (** This function has a type like [string -> (exists n. n sized_list)]. *)
  val load : string -> (module S)
end = struct
  type 'n sized_list = int list
  type z
  type 'n s

  let nil = []
  let cons x l = x :: l
  let hd = List.hd
  let tl = List.tl
  let map = List.map
  let add = List.map2 (+)

  module type S = sig
    type n
    val x : n sized_list
  end

  let load fname = (module struct
                      type n
                      let x = load_list fname
                    end : S)
end

open SizedList

let () =
  let module M1 = (val load "file" : S) in (* M1.x : M1.n sized_list *)
  let y = map (fun a -> a * 2) M1.x in (* y : M1.n sized_list *)
  let z = add M1.x y in (* well-typed because M1.x and y have the same length *)
  let module M2 = (val load "file" : S) in (* M2.x : M2.n sized_list *)
  let w = add M1.x M2.x in (* ill-typed because M1.x and M2.x possibly have
                              different sizes (M1.n <> M2.n) *)
  ()