I’ve been working on a side-project in OCaml that binds to the
libmnl library to interact
with netlink sockets to add/remove/update network links. I have been
taking my time and experimenting to learn more about OCaml rather than
just try to stick to what I’m comfortable with.
Netlink messages have several trailing “attributes” of the form
len[2] tag[2] payload[len]
, of various shapes and sizes. For
example:
IFLA_ADDRESS /* 6-byte ethernet address */
IFLA_IFNAME /* string, e.g. "eth0" */
IFLA_MTU /* 32-bit unsigned integer (host endian) */
My initial thought was to model these with variants, so I would
be able to use them in pattern matching:
type nlattr =
| IFLA_IFNAME of string
| IFLA_MTU of int32
| IFLA_ADDRESS of bytes
but I didn’t like that the payload was always attached to the tag.
I couldn’t do something like
let ifname = nlattr_find_opt IFLA_IFNAME nlmsg in
I could make the constructors take 0 arguments and group them by
their underlying type. This is what the Unix module does with the
socket_*_option types:
type nlattr_str =
| IFLA_IFNAME
| IFLA_IFALIAS
type nlattr_u32 =
| IFLA_MTU
| IFLA_LINK_NSID
val nlattr_get_u32 : nlmsg -> nlattr_u32 -> int32 option
val nlattr_get_str : nlmsg -> nlattr_str -> string option
(* and so on *)
But there are dozens of varying payloads, and some of them are only used
for one or two attributes. I tried modelling this using a GADT instead:
type _ nlattr =
| IFLA_IFNAME: string nlattr
| IFLA_MTU: int32 nlattr
| IFLA_ADDRESS: bytes nlattr
After some contortions, I was able to implement an iterator with the
following signature:
type 'a nlattr_fn = { f: 't. 'a -> 't nlattr_type -> 't -> 'a } [@@unboxed]
val nlattr_walk: 'a nlattr_fn -> 'a -> nlmsghdr -> 'a
This function got pretty hairy because attributes can be nested.
Anyway, I wanted to implement the nlattr_find_opt
function above,
which gets the payload for one attribute with the given tag, using
the more general nlattr_walk
. Here was my initial attempt:
let nlattr_find_opt (type a) nlh (attr: a nlattr_type) =
let f (type b) (init: a option) (k: b nlattr_type) (v: b) =
if k = attr
then Some v else init
in
nlattr_walk {f} None nlh
This failed to compile with the error:
727 | if k = attr
^^^^
Error: This expression has type a nlattr_type
but an expression was expected of type b nlattr_type
Type a is not compatible with type b
(exit status 1)
After some research, I eventually was able to satisfy the type checker
with a witness:
type (_, _) eq = Equal : ('a, 'a) eq
let nlattr_eq: type a b. a nlattr_type -> b nlattr_type -> (a, b) eq option =
fun a b ->
match a, b with
| IFLA_ADDRESS, IFLA_ADDRESS -> Some Equal
(* ... snip ... *)
| _ -> None
let nlattr_find_opt: type a. Nlmsghdr.t ptr -> a nlattr_type -> a option =
fun nlh attr ->
let f: type b. a option -> b nlattr_type -> b -> a option =
fun init k v ->
match nlattr_eq attr k with
| Some Eq -> Some v
| None -> init
in
nlattr_walk {f} None nlh
I understand that I need to prove to the type checker that the two
types are the same, but I haven’t quite wrapped my head around how the
nlattr_eq
function proves that. I did some experimentation to try and
figure out what was allowed and what wasn’t. For example, if I change
this case:
match a, b with
...
| IFLA_IFALIAS, IFLA_IFALIAS -> Some Eq (* string, string *)
to something nonsensical like
| IFLA_IFALIAS, IFLA_NUM_TX_QUEUES -> Some Eq (* string, int32 *)
I get the error
Error: This expression has type (a, a) eq
but an expression was expected of type (a, b) eq
Type a = string is not compatible with type b = int32
Type string is not compatible with type b = int32
but if I change it to this:
| IFLA_IFALIAS, IFLA_IFNAME -> Some Eq (* string, string *)
the program compiles, but as expected those two tags are treated as
equivalent in nlattr_find_opt. I can now see how I’d be able to use
this technique to simplify my program; for example I wouldn’t have
to enumerate every variant in my printing function; I can handle all
variants with the same payload at once.
I started this post before I got a working solution, and the process
of drafting the post helped me figure things out myself (funny how that
works!). But I’m posting anyway in case someone else is struggling with
GADTs, and also because I still have the lingering sensation that I’ve
performed some magical conjuring that I don’t fully understand.
Taking a simplified example
type (_, _) eq = Eq : ('a, 'a) eq
let nlattr_eq: type a b. a nlattr_type -> b nlattr_type -> (a, b) eq option =
fun a b ->
match a, b with
| IFA_ADDRESS, IFA_ADDRESS -> Some Eq
The thing that still confuses me is the constructor Eq
. Even though
I’m not providing any arguments, I somehow constructed a value of type
(a, b) eq
. How did the type checker know that’ what I was doing?
In the pattern match
match a, b with
Is (a, b)
not a tuple, but something else? Or is all the “magic” just
occurring in the function’s signature:
val nlattr_eq: type a b. a nlattr_type -> b nlattr_type -> (a, b) eq option
So by emitting Eq
when a ≠ b, I’m violating the type signature? That
makes more sense, but if that is the case, is there some more compact
way to show the type checker that two variants are the same, closer to
my initial attempt of just comparing them with =
? Something that does
not involve enumerating every possible variant?