Ctypes and heterogeneous list typing problem

Learning
7

This can be done by switching to the right variant of heterogeneous list

type (_,_) hlist =
  | [] : ('r,'r) hlist
  | (::) : 'a objc_value * ('b,'r) hlist -> ('a -> 'b,'r) hlist

let rec t_of_m: type a b. b Ctypes.fn -> (a,b) hlist -> a Ctypes.fn
= fun base xs ->
  match xs with
  | [] -> base
  | {t; _} :: rest -> Ctypes. ( t @-> t_of_m base rest )

which is a common pattern when defining heterogeneous list types: one needs to add the required type-level computations when defining the type itself. This is why there are many different heterogeneous lists.

5 Likes