Can one encode binary functions between types in OCaml?

Question

I am wondering if it is possible to build something similar to multiple dispatch in OCaml. To do that, I tried to make an explicit type for the input signature of a multimethod. As an example, I define a number type

type _ num =
| I : int -> int num
| F : float -> float num

Now I would like a function add to sum an 'a num and a 'b num and return an int num if both 'a and 'b are int, and a float num if at least one of them is a float. Also, the type system should know which constructor the output will use. I.e. it should be statically known at the function call that the output is of type int num for example.

Is that possible? So far I can only manage a function of signature type a b. a num * b num -> a num for example, so that the (more general) float would always have to be supplied as the first argument. The case int num * float num would have to be disallowed, leading to a non-exhaustive pattern match and runtime exceptions.

It seems that one would need a signature like type a b. a num * b num -> c(a,b) num where c is a type function which contains the type promotion rules. I don't think OCaml has this. Would open types or objects be able to capture this? I'm not looking for the most general function between types, it's enough if I can list a handful of input type combinations and the corresponding output type explicitly.

Answer 1

The specific case you are asking about can be solved nicely using GADTs and polymorphic variants. See calls to M.add at the bottom of this code:

type whole = [ `Integer ]
type general = [ whole | `Float ]

type _ num =
  | I : int -> [> whole ] num
  | F : float -> general num

module M :
sig
  val add : ([< general ] as 'a) num -> 'a num -> 'a num

  val to_int : whole num -> int
  val to_float : general num -> float
end =
struct
  let add : type a. a num -> a num -> a num = fun a b ->
    match a, b with
    | I n, I m -> I (n + m)
    | F n, I m -> F (n +. float_of_int m)
    (* Can't allow the typechecker to see an I pattern first. *)
    | _,   F m ->
      match a with
      | I n -> F (float_of_int n +. m)
      | F n -> F (n +. m)

  let to_int : whole num -> int = fun (I n) -> n

  let to_float = function
    | I n -> float_of_int n
    | F n -> n
end

(* Usage. *)
let () =
  M.add (I 1)  (I 2)  |> M.to_int   |> Printf.printf "%i\n";
  M.add (I 1)  (F 2.) |> M.to_float |> Printf.printf "%f\n";
  M.add (F 1.) (I 2)  |> M.to_float |> Printf.printf "%f\n";
  M.add (F 1.) (F 2.) |> M.to_float |> Printf.printf "%f\n"

That prints

3
3.000000
3.000000
3.000000

You cannot change any of the above to_floats to to_int: it is statically known that only adding two Is results in an I. However, you can change the to_int to to_float (and adjust the printf). These operations readily compose and propagate the type information.

The foolery with the nested match expression is a hack I will ask on the mailing list about. I've never seen this done before.

---

General type functions

AFAIK the only way to evaluate a general type function in current OCaml requires the user to provide a witness, i.e. some extra type and value information. This can be done in many ways, such as wrapping the arguments in extra constructors (see answer by @mookid), using first-class modules (also discussed in next section), providing a small list of abstract values to choose from (which implement the real operation, and the wrapper dispatches to those values). The example below uses a second GADT to encode a finite relation:

type _ num =
  | I : int -> int num
  | F : float -> float num

(* Witnesses. *)
type (_, _, _) promotion =
  | II : (int, int, int) promotion
  | IF : (int, float, float) promotion
  | FI : (float, int, float) promotion
  | FF : (float, float, float) promotion

module M :
sig
  val add : ('a, 'b, 'c) promotion -> 'a num -> 'b num -> 'c num
end =
struct
  let add (type a) (type b) (type c)
      (p : (a, b, c) promotion) (a : a num) (b : b num) : c num =
    match p, a, b with
    | II, I n, I m -> I (n + m)
    | IF, I n, F m -> F (float_of_int n +. m)
    | FI, F n, I m -> F (n +. float_of_int m)
    | FF, F n, F m -> F (n +. m)
end

(* Usage. *)
let () =
  M.add II (I 1) (I 2)  |> fun (I n) -> n |> Printf.printf "%i\n";
  M.add IF (I 1) (F 2.) |> fun (F n) -> n |> Printf.printf "%f\n"

Here, the type function is ('a, 'b, 'c) promotion, where 'a, 'b are arguments, and 'c is the result. Unfortunately, you have to pass add an instance of promotion for 'c to be ground, i.e. something like this won't (AFAIK) work:

type 'p result = 'c
  constraint 'p = (_, _, 'c) promotion

val add : 'a num -> 'b num -> ('a, 'b, _) promotion result num

Despite the fact that 'c is completely determined by 'a and 'b, due to the GADT; the compiler still sees that as basically just

val add : 'a num -> 'b num -> 'c num

Witnesses don't really buy you much over just having four functions, except that the set of operations (add, multiply, etc.), and the argument/result type combinations, can been made mostly orthogonal to each other; the typing can be nicer and things can be slightly easier to use and implement.

EDIT It's actually possible to drop the I and F constructors, i.e.

val add : ('a, 'b, 'c) promotion -> 'a -> 'b -> `c

This makes the usage much simpler:

M.add IF 1 2. |> Printf.printf "%f\n"

However, in both cases, this is not as composable as the GADT+polymorphic variants solution, since the witness is never inferred.

---

Future OCaml: modular implicits

If your witness is a first-class module, the compiler can choose it for you automatically with modular implicits. You can try this code in the 4.02.1+modular-implicits-ber switch. The first example just wraps the GADT witnesses from the previous example in modules, to get the compiler to choose them for you:

module type PROMOTION =
sig
  type a
  type b
  type c
  val promotion : (a, b, c) promotion
end

implicit module Promote_int_int =
struct
  type a = int
  type b = int
  type c = int
  let promotion = II
end

implicit module Promote_int_float =
struct
  type a = int
  type b = float
  type c = float
  let promotion = IF
end

(* Two more like the above. *)

module M' :
sig
  val add : {P : PROMOTION} -> P.a num -> P.b num -> P.c num
end =
struct
  let add {P : PROMOTION} = M.add P.promotion
end

(* Usage. *)
let () =
  M'.add (I 1) (I 2)  |> fun (I n) -> n |> Printf.printf "%i\n";
  M'.add (I 1) (F 2.) |> fun (F n) -> n |> Printf.printf "%f\n"

With modular implicits, you can also simply add untagged floats and ints. This example corresponds to dispatching to a function "witness":

module type PROMOTING_ADD =
sig
  type a
  type b
  type c
  val add : a -> b -> c
end

implicit module Add_int_int =
struct
  type a = int
  type b = int
  type c = int
  let add a b = a + b
end

implicit module Add_int_float =
struct
  type a = int
  type b = float
  type c = float
  let add a b = (float_of_int a) +. b
end

(* Two more. *)

module M'' :
sig
  val add : {P : PROMOTING_ADD} -> P.a -> P.b -> P.c
end =
struct
  let add {P : PROMOTING_ADD} = P.add
end

(* Usage. *)
let () =
  M''.add 1 2  |> Printf.printf "%i\n";
  M''.add 1 2. |> Printf.printf "%f\n"

Answer 2

OCaml, as of the 4.04.0 release, does not have a way to encode type-level dependencies in this way. The typing rules would have to be more simple.

One option is to use a simple variant type for this, wrapping everything into one (potentially large) type and match:

type vnum =
  | Int of int
  | Float of float

let add_vnum a b =
  match a, b with
  | Int ia, Int ib -> Int (ia + ib)
  | Int i, Float f
  | Float f, Int i -> Float (float_of_int i +. f)
  | Float fa, Float fb -> Float (fa +. fb)

Another approach is to restrict the input values to have matching types:

type _ gnum =
  | I : int -> int gnum
  | F : float -> float gnum

let add_gnum (type a) (x : a gnum) (y : a gnum) : a gnum =
  match x, y with
  | I ia, I ib -> I (ia + ib)
  | F fa, F fb -> F (fa +. fb)

Finally, the type of one of the input values could be used to constrain the return value's type. In this example the return value will always have the same type as the second argument:

type _ gnum =
  | I : int -> int gnum
  | F : float -> float gnum

let add_gnum' (type a b) (x : a gnum) (y : b gnum) : b gnum =
  match x, y with
  | I i1, I i2 -> I (i1 + i2)
  | F f1, F f2 -> F (f1 +. f2)
  | I i, F f -> F (float_of_int i +. f)
  | F f, I i -> I (int_of_float f + i)