More generally, a good starting with GADTs is generally to start by trying to write the type of functions, failing to do so, and then add enough type-level information to the GADTs construction to be able to write a type.
For instance, a first tentative for the type of iter
would be
let iter: 'list. ('list -> unit) -> 'list exp_list -> unit
However, the visible issue is that 'list
is the list of type of the elements, not the type of a single elements.
From this point, there is a two solutions: either we know something more about the types of all the elements, or we make iter
takes a list of functions adapted to the list of elements to relate the type of the function to apply.
@dlesbre falls in the first alternative: one thing that we can know about all elements is that they belong to the same type family. Then if we have a function that works on all types of this familly, we can iter the list. We can apply this idea generically with a functor
type void = |
module Hlist(F:sig type 'a t end) = struct
type 'a t =
| [] : void t
| (::): 'a F.t * 'b t -> ('a * 'b) t
(* We can then define the type of functions that works
on any type 'a F.t *)
type f = { app: 'a. 'a F.t -> unit }
(* With this definition, the type of iter can be written easily *)
let rec iter: type list. f -> list t -> unit =
(* and the implementation follows *)
fun f l -> match l with
| [] -> ()
| x :: xs -> f.app x; iter f xs
end
A simple and silly example would be to define heterogeneous lists of lists
module Hlist_of_lists = Hlist(struct type 'a t = 'a list end)
In this example, we can exploit the fact that we can compute the length of any list to iter
a printer over a Hlist_of_lists.t
:
let printer l = print_int (List.length l)
let lengths l = Hlist_of_lists.(iter { app = printer } l)
let () = lengths [ [1]; [2.]; [] ]
The other alternative require to have two variants of heterogeneous lists: one for the functions to apply
module Flist = Hlist(struct type 'a t = 'a -> unit end)
and another for the arguments:
module Arg_list = Hlist(struct type 'a t = 'a end)
With this two kind of lists, we know that whenever the type parameter of a Flist.t
matches the type parameter of an Arg_list.t
, the types of all functions and argument match;;
let rec apply: type list. list Flist.t -> list Arg_list.t -> unit =
fun fs xs -> match fs, xs with
| [], [] -> ()
| f :: fs, x::xs -> f x; apply fs xs
| _ -> .
let () = apply [print_int; print_endline] [0;"zero"]