With the recent tutorial and discussions on GADTs, I tried to implement a heterogeneous list in the context of a Ctypes bindings to Objective-C. I hit a roadblock in the definition of the function t_of_m below. Is that function possible, and what would be the correct type?

type 'a objc_value = { t : 'a Ctypes.typ; enc : string }
type _ hlist =
| [] : unit hlist
| (::) : 'a objc_value * 'b hlist -> ('a * 'b) hlist
let id = { t = Ctypes.(ptr void); enc = "@" }
let _SEL = { t = Ctypes.(ptr char); enc = ":" }
let rec enc_of_m
: type a. string -> a hlist -> string
= fun acc xs ->
match xs with
| [] -> acc
| {enc; _} :: rest -> enc_of_m (acc ^ enc) rest
;;
(* Need to fold the t's in the hlist into a C function type signature.
Is this function possible? *)
let rec t_of_m
: type a b. ? Ctypes.fn -> ?? hlist -> ??? Ctypes.fn
= fun acc xs ->
match xs with
| [] -> acc
| {t; _} :: rest -> t_of_m Ctypes.(t @-> acc) rest
;;
let m = [id; _SEL]
let x = enc_of_m "" m
let y = t_of_m Ctypes.(returning void) m

If it helps anyone else, I’ve rewritten this question to use a toy ToyTypes module instead of Ctypes so that expertise in that particular library is not needed:

module ToyTypes = struct
type _ typ =
| Int : int typ
| Bool : bool typ
| Float : float typ
type _ fn =
| Arrow : 'a typ * 'b fn -> ('a -> 'b) fn
let (@->) : 'a typ -> 'b fn -> ('a -> 'b) fn = fun a b -> Arrow (a, b)
end
type 'a tval = {t : 'a ToyTypes.typ; v : 'a}
type _ hlist =
| [] : unit hlist
| (::) : 'a tval * 'b hlist -> ('a * 'b) hlist
(* is there any way to make a function that does this type check? *)
let rec t_of_hlist fn_acc tvals = match tvals with
| [] -> fn_ac
| {typ; _} :: rest -> t_of_hlist ToyTypes.(typ @-> fn_acc) rest

The basic issue is that you want to be able to express that a function takes a value of type ('a * 'b * ... ) hlist and returns a value of type ('a -> 'b -> ...) fn. I kind of suspect that it’s not possible, but maybe there’s a way? My best guess is that there might be a way to construct some auxiliary GADT that step-by-step transforms the hlist into an identical type but that uses ->'s instead of *'s but I kind of doubt it because I can’t figure out how you’d express that kind of recursion on types.

EDIT: Actually, not quite. There’s one more complication: you’re actually trying to write a function that takes ('a * 'b * ... * 'z * unit) hlist and returns ('a ->'b -> ... -> 'z) fn.
My guess remains that this is not possible, and that you’re better off using code generation to handle tuples of a finite number of lengths rather than heterogenous lists.

EDIT 2: Sorry, one last detail: it’s actually suppoesd to take 'sig fn and ('a * ... * 'z * unit) hlist and return ('z -> ... -> 'a -> 'sig) fn.

Why would it not be possible? Seems possible on first glance (but I’m too tired to try today).

Also, in some restricted use cases instead of GADTs you can use non-uniform types. But it still requires GADT type inference.

type 'a variadic =
| Result of (unit -> 'a)
| Param_int of int ref * (int -> 'a) variadic
| Param_float of float ref * (float -> 'a) variadic
let rec apply : 'a. 'a variadic -> 'a =
fun (type b) (f : b variadic) ->
match f with
| Result rf -> rf ()
| Param_int (i, more) -> apply more !i
| Param_float (n, more) -> apply more !n

Just a hunch! Not super experienced with GADTs at all, just couldn’t think of how you could possibly express it in a type signature and so assumed that it wasn’t possible. If it is possible, I kind of imagine it’s one of those things you can do with GADTs but that require you to basically do proofs using witnesses and the like. A while back I remember trying the reverse a hlist twice puzzle and my takeaway was “here be dragons.”

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.

That’s a much more practical way than the way I did it! (I could not resist relearning how to use OCaml as a theorem prover).

module ToyTypes = struct
type _ typ =
| Int : int typ
| Bool : bool typ
| Float : float typ
| Void : unit typ
type _ fn =
| Ret : 'a typ -> 'a fn
| Arrow : 'a typ * 'b fn -> ('a -> 'b) fn
let (@->) : 'a typ -> 'b fn -> ('a -> 'b) fn = fun a b -> Arrow (a, b)
end
type 'a tval = {t : 'a ToyTypes.typ; v : 'a}
type _ hlist =
| [] : unit hlist
| (::) : 'a tval * 'b hlist -> ('a * 'b) hlist
type _ witness =
| Base : <init_acc: 'a; acc: 'a; xs: unit> witness
| Ind : <init_acc: 'x -> 'a; acc: 'b; xs: 'c> witness -> <init_acc: 'a; acc: 'b; xs: 'x * 'c> witness
type _ t_of_hlist =
| T_Of_HList : 'a ToyTypes.fn * <init_acc: 'b; acc: 'a; xs: 'c> witness -> <init_acc: 'b; xs: 'c> t_of_hlist
let rec t_of_hlist
: type acc xs. acc ToyTypes.fn -> xs hlist -> <init_acc: acc; xs: xs> t_of_hlist =
fun acc xs -> match xs with
| [] -> T_Of_HList (acc, Base)
| x :: xs ->
let T_Of_HList (acc, witness') = t_of_hlist ToyTypes.(x.t @-> acc) xs in
let witness = Ind witness' in
T_Of_HList (acc, witness)
let xs = let open ToyTypes in [{t = Int; v = 1}; {t = Float; v = 2.0}; {t = Bool; v = true}]
let t = t_of_hlist ToyTypes.(Ret Void) xs