GADTs for typed option getter/setter

Learning
1

I’ve had a nice use-case of GADTs recently in ocaml-srt that I thought I would share.

On the C side, the library implements an API a la syscall with named options and polymorphic types:

SRT_API int srt_getsockflag  (SRTSOCKET u, SRT_SOCKOPT opt, void* optval, int* optlen);
SRT_API int srt_setsockflag  (SRTSOCKET u, SRT_SOCKOPT opt, const void* optval, int optlen);

And the socket options are listed in an enum:

typedef enum SRT_SOCKOPT {
   SRTO_MSS = 0,             // the Maximum Transfer Unit
   SRTO_SNDSYN = 1,          // if sending is blocking
   SRTO_RCVSYN = 2,          // if receiving is blocking
   SRTO_ISN = 3,             // Initial Sequence Number (valid only after srt_connect or srt_accept-ed sockets)
   SRTO_FC = 4,              // Flight flag size (window size)
   SRTO_SNDBUF = 5,          // maximum buffer in sending queue
   SRTO_RCVBUF = 6,          // UDT receiving buffer size
...
};

On the OCaml side, it is then pretty natural to also want a polymorphic API:

type 'a socket_opt

val messageapi : bool socket_opt
val payloadsize : int socket_opt
val rcvsyn : bool socket_opt
val sndsyn : bool socket_opt

val getsockflag : socket -> 'a socket_opt -> 'a
val setsockflag : socket -> 'a socket_opt -> 'a -> unit

This can be achieved in a cool type-safe way and without writing any C by combining ctypes and GADTs!

First, we export the socket option enums as OCaml polymorphic variants using the ctypes API:

  type socket_opt =
    [ `Messageapi
    | `Payloadsize
    | `Rcvsyn
    | `Sndsyn]

  let socket_opt : socket_opt typ =
    enum "SRT_SOCKOPT"
      [
        (`Messageapi, constant "SRTO_MESSAGEAPI" int64_t);
        (`Payloadsize, constant "SRTO_PAYLOADSIZE" int64_t);
        (`Rcvsyn, constant "SRTO_RCVSYN" int64_t);
        (`Sndsyn, constant "SRTO_SNDSYN" int64_t)
      ]

Next, on our public OCaml API side, we use regular variant types with a type annotation to use for GADTs pattern matching and match them with the polymorphic variants returned by ctypes:

type _ socket_opt =
  | Messageapi : bool socket_opt
  | Payloadsize : int socket_opt
  | Rcvsyn : bool socket_opt
  | Sndsyn : bool socket_opt

let messageapi = Messageapi
let payloadsize = Payloadsize
let rcvsyn = Rcvsyn
let sndsyn = Sndsyn

let srt_socket_opt_of_socket_opt (type a) : a socket_opt -> Srt.socket_opt =
  function
  | Messageapi -> `Messageapi
  | Payloadsize -> `Payloadsize
  | Rcvsyn -> `Rcvsyn
  | Sndsyn -> `Sndsyn

ctypes also. gives us bindings to the get/set functions from the C library:

  let getsockflag =
    foreign "srt_getsockflag"
      (int @-> socket_opt @-> ptr void @-> ptr int @-> returning int)

  let setsockflag =
    foreign "srt_setsockflag"
      (int @-> socket_opt @-> ptr void @-> int @-> returning int)

Now, we’re ready to implement our get/set polymorphic functions:

let getsockflag : type a. socket -> a socket_opt -> a =
 fun sock opt ->
  let arg = allocate int 0 in
  let arglen = allocate int (sizeof int) in
  ignore
    (check_err
       (getsockflag sock
          (srt_socket_opt_of_socket_opt opt)
          (to_voidp arg) arglen));
  let to_bool () = !@arg <> 0 in
  let to_int () = !@arg in
  match opt with
    | Rcvsyn -> to_bool ()
    | Sndsyn -> to_bool ()
    | Messageapi -> to_bool ()
    | Payloadsize -> to_int ()

let setsockflag : type a. socket -> a socket_opt -> a -> unit =
 fun sock opt v ->
  let f t v = to_voidp (allocate t v) in
  let of_bool v =
    let v = if v then 1 else 0 in
    (f int v, sizeof int)
  in
  let of_int v = (f int v, sizeof int) in
  let arg, arglen =
    match opt with
      | Rcvsyn -> of_bool v
      | Sndsyn -> of_bool v
      | Messageapi -> of_bool v
      | Payloadsize -> of_int v

:warning: Question :warning:

I wasn’t able to join cases of the same type, for instance this:

  match opt with
    | Rcvsyn
    | Sndsyn
    | Messageapi -> to_bool ()
    | Payloadsize -> to_int ()

Is this a theoretical or implementation limitation?

7 Likes
2

It’s an implementation limitation. There are some details at Support GADTs in or-patterns · Issue #5736 · ocaml/ocaml · GitHub

1 Like
3

Slightly related to the problem of sharing constants between the C side and the OCaml side but much less sophisticated:

For my small epoll library polly I am creating a function in C using a macro that returns the constant:

/* Make all constants available to clients by exporting them via a
 * function. This avoids having to hard code them on the client side. 
 * */

#define CONSTANT(name) \
  CAMLprim value caml_polly_ ## name(value unit) { return Val_int(name); }

CONSTANT(EPOLLIN);
CONSTANT(EPOLLPRI);
CONSTANT(EPOLLOUT);

In the bindings I have one function per constant and call it once to obtain the constant; the actual value of the constant is not part of the OCaml code.

  type t = int

  external polly_IN : unit -> t = "caml_polly_EPOLLIN"
  external polly_PRI : unit -> t = "caml_polly_EPOLLPRI"
  external polly_OUT : unit -> t = "caml_polly_EPOLLOUT"

  let inp = polly_IN ()
  let pri = polly_PRI ()
  let out = polly_OUT ()
2 Likes