[GADT] iterate over heterogeneous list

Even though I use OCaml since several years (just for side projects) I’m still not able to handle GADTs properly. How can I iterater over a heterogeneous list and print each element?

Here is my attempt:


type _ ty =
  | Int : int ty

type _ exp =
  | Val: 'a ty * 'a -> 'a exp

type _ exp_list =
  | Nil: unit exp_list
  | Cons: 'hd * 'tl exp_list -> ('hd -> 'tl) exp_list

let rec print: type a. a exp_list -> unit = fun xs ->
  match xs with
  | Nil -> ()
  | Cons(Val (Int, n), tl) ->
    print_int n;
    print tl

This is the error:

    | Cons(Val (Int, n), tl) ->
              ^^^^^^^^^^^^
    Error: This pattern matches values of type 'a exp
           but a pattern was expected which matches values of type $0

Your type exp_list doesn’t tell you elements are of type 'a exp, they can be of any type… So when you match a Cons in print, you only know that your type a is an arrow $0 -> $1, and that the first argument of Cons is of type $0. You can’t destruct the $0 to match it to Val _, since its an existential type (it could anything).

To fix this, change exp_list type to specify that all elements that appear in Cons are _ exp with

type _ exp_list =
  | Nil: unit exp_list
  | Cons: 'hd exp * 'tl exp_list -> ('hd -> 'tl) exp_list
2 Likes

Thank you so much.
Really appreciate you taking the time to answer my noob question.

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"]
3 Likes

Very impressed by the depth of your answer. Huge thank you.