Ctypes and heterogeneous list typing problem

Learning
1

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
2

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.

3

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
1 Like
4

I mean this precisely does look impossible, but what if

type _ hlist = 
  | [] : unit hlist
  | (::) : 'a tval * 'b hlist -> ('a -> 'b) hlist
1 Like
5

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.”

6

Fair point, I thought more liberally, about expressing the same functionality.

1 Like
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.

4 Likes
8

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
1 Like
9

I’ll continue this thread as the following problem seems related. Is there a typing trick to make this function typecheck?

let id = Ctypes.(ptr void)
let _SEL = Ctypes.(ptr char)

let t_of_enc : string -> 'a Ctypes.fn -> ('b -> 'a) Ctypes.fn =
  fun s ret ->
    match s with
    | "@" -> id @-> ret
    | ":" -> _SEL @-> ret
    | _ -> assert false
10

Not at it is: values cannot create type information. In other words, the 'b type variable

string -> 'a Ctypes.fn -> ('b ->'a) Ctypes.fn

must be derived from existing type information and not from the content of the string. For instance, you could split the function in two: one function for the "@", another for the ': case. Or in equivalent way, you could replace the string with a GADT with two cases.

1 Like