Skip to content

Instantly share code, notes, and snippets.

@akabe
Created October 29, 2015 07:06
Show Gist options
  • Save akabe/599de3905a3b01d81429 to your computer and use it in GitHub Desktop.
Save akabe/599de3905a3b01d81429 to your computer and use it in GitHub Desktop.
Static size checking for lists (loaded from files) by generative phantom types (GADT version)
(* 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
type pkg = C : 'n sized_list -> pkg
(** This function has a type like [string -> (exists n. n sized_list)]. *)
val load : string -> pkg
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 (+)
type pkg = C : 'n sized_list -> pkg
let load fname = C (load_list fname)
end
open SizedList
let () =
let (C x1) = load "file" in
let y = map (fun a -> a * 2) x1 in
let z = add x1 y in (* well-typed because x1 and y have the same length *)
let (C x2) = load "file" in
let w = add x1 x2 in (* ill-typed because x1 and x2 possibly have different
sizes *)
()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment