Elegant typing solution desired, typing of one parameter is a function of another

Question

I have a somewhat complicated typing issue, at least to me.

say we have this:

type rr = A | AAA | BBB

type resolve_result_t = List of string list
                        | MX_records of mx_record list
                        | Srv of srv_record list
                        | Soa of soa_record
                        | Error of string
  and mx_record = { exchange : string; priority: int; }
  and srv_record = { priority: int; weight : int; port : int; name : string; }
  and soa_record = { nsname : string;
                     hostmaster: string;
                     serial : int;
                     refresh: int;
                     retry : int;
                     expire : int;
                     minttl : int; }


let resolve ?(rr_type=A) ~host (f : (resolve_result_t -> unit) : unit = 
match rr_type with 
| A -> 
  let g = fun raw -> f (List (raw |> some_string_list_func))
  ...code that uses g
| BBB -> 
  let g = fun raw -> f (MX_records (raw |> some_mx_record_list_func))
...

then in caller's code we have to do stuff like this:

resolve ~host:"google.com" begin function 
  List l -> .. code that uses l | _ -> assert false (* Or deal with the warning *)
end

or

resolve ~rr_type:BBB ~host:"google.com" begin function 
  MX_records l -> ...similiar to previous example.

Even though those other cases can never occur since the typing of the function depends on the typing of another parameter.

I keep thinking there's some type system trick or usage of GADTs, but I'm never sure entirely when I need to reach for those.

Answer 1

type _ rr =
  | A : string list rr
  | AAA : srv_record list rr
  | BBB : mx_record list rr

and _ resolve_result_t =
  | List : string list -> string list resolve_result_t
  | MX_records : mx_record list -> mx_record list resolve_result_t
  | Srv : srv_record list -> srv_record list resolve_result_t
  | Soa : soa_record list -> soa_record list resolve_result_t
  | Error : string -> string resolve_result_t

and mx_record  = { exchange : string; mx_priority: int; }

and srv_record = { srv_priority: int; weight : int; port : int; name : string; }

and soa_record = { nsname : string;
                   hostmaster: string;
                   serial : int;
                   refresh: int;
                   retry : int;
                   expire : int;
                   minttl : int; }

let resolve : type a. a rr -> string -> (a resolve_result_t -> unit) -> unit =
  fun rr_type host f ->
    match rr_type with
    | A -> f (List ["123"])
    | AAA -> f (Srv [{srv_priority=1;weight=1;port=1;name="123"}])
    | BBB -> f (MX_records [{exchange="123"; mx_priority=1}])

let () =
  let f = fun (List l) -> () in
  resolve A "google.com" f

In the above code, I assume when you want to use A, AAA, BBB, only List, Srv, and MX_records will show up, respectively. Pattern matching in last three lines is exhaustive thanks to GADT.

Also, note that, in mx_record and srv_record, you would like to name two prioritys differently, otherwise you'll get a warning (related to subtyping and type definition shadowing: {priority=1} will always have type srv_record)

Update:

As for your requirement that f in resolve should also handle Error, here is another try.

type _ rr =
  | A : string list rr
  | AAA : srv_record list rr
  | BBB : mx_record list rr

and _ resolve_result_t =
  | List : string list -> string list resolve_result_t
  | MX_records : mx_record list -> mx_record list resolve_result_t
  | Srv : srv_record list -> srv_record list resolve_result_t
  | Soa : soa_record list -> soa_record list resolve_result_t
  | Error : string -> string resolve_result_t

and 'a rrt =
  | Ok of 'a resolve_result_t
  | Err of string resolve_result_t

and mx_record  = { exchange : string; mx_priority: int; }

and srv_record = { srv_priority: int; weight : int; port : int; name : string; }

and soa_record = { nsname : string;
                   hostmaster: string;
                   serial : int;
                   refresh: int;
                   retry : int;
                   expire : int;
                   minttl : int; }

let resolve : type a. a rr -> string -> (a rrt -> unit) -> unit =
  fun rr_type host f ->
    match rr_type with
    | A -> f (Ok (List ["123"]))
    | AAA -> f (Ok (Srv [{srv_priority=1;weight=1;port=1;name="123"}]))
    | BBB -> f (Ok (MX_records [{exchange="123"; mx_priority=1}]))

let () =
  let f = function
    | Ok (List l) -> ()
    | Err (Error s) -> print_endline s in
  resolve A "google.com" f

GADT-heavy code is much more complicated to write. A few more _ -> assert false won't hurt.