您询问的特定情况可以使用 GADT 和多态变体很好地解决。M.add请参阅此代码底部的调用：
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"
那打印
3
3.000000
3.000000
3.000000
您不能将上述任何to_floats 更改为to_int：静态已知，仅添加两个Is 会导致I。但是，您可以将 更改
to_int为to_float（并调整printf）。这些操作很容易组合和传播类型信息。
嵌套match表达式的愚蠢是我将在邮件列表中询问的一个技巧。我以前从未见过这样做过。
一般类型函数
AFAIK 在当前 OCaml 中评估通用类型函数的唯一方法要求用户提供见证，即一些额外的类型和值信息。这可以通过多种方式完成，例如将参数包装在额外的构造函数中（参见@mookid 的回答），使用一流的模块（也在下一节中讨论），提供一小部分抽象值可供选择（实现真正的操作，并且包装器分派给这些值）。下面的示例使用第二个 GADT 来编码有限关系：
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"
在这里，类型函数是('a, 'b, 'c) promotion，其中'a，'b是参数，并且'c是结果。不幸的是，你必须通过一个foradd的实例才能被接地，即这样的事情不会（AFAIK）工作：promotion'c
type 'p result = 'c
constraint 'p = (_, _, 'c) promotion
val add : 'a num -> 'b num -> ('a, 'b, _) promotion result num
尽管这'c完全由'a和决定'b，但由于 GADT；编译器仍然认为这基本上只是
val add : 'a num -> 'b num -> 'c num
目击者并没有真正为您提供四个函数，除了操作集（add、multiply等）和参数/结果类型组合可以相互正交；打字可以更好，事情可以更容易使用和实现。
编辑实际上可以删除IandF构造函数，即
val add : ('a, 'b, 'c) promotion -> 'a -> 'b -> `c
这使得使用更加简单：
M.add IF 1 2. |> Printf.printf "%f\n"
然而，在这两种情况下，这都不像 GADT+多态变体解决方案那样可组合，因为从未推断出见证。
未来的 OCaml：模块化隐式
如果您的见证是一等模块，编译器可以使用模块化隐式自动为您选择它。4.02.1+modular-implicits-ber您可以在交换机中尝试此代码
。第一个示例只是将上一个示例中的 GADT 见证人包装在模块中，以让编译器为您选择它们：
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"
使用模块化隐式，您还可以简单地添加未标记的浮点数和整数。此示例对应于调度到函数“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"