types - 可以在 OCaml 中的类型之间编码二进制函数吗？

Question

我想知道是否可以在 OCaml 中构建类似于多次调度的东西。为此，我尝试为多方法的输入签名创建一个显式类型。例如，我定义了一个数字类型

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

现在我想要一个函数 add总结 'a num和 'b num并返回 int num如果两者都是 'a和 'b是 int , 和 float num如果其中至少一个是 float .此外，类型系统应该知道输出将使用哪个构造函数。 IE。应该在函数调用中静态知道输出的类型为 int num例如。

那可能吗？到目前为止我只能管理一个签名功能 type a b. a num * b num -> a num例如，这样(更一般的)浮点数总是必须作为第一个参数提供。案例 int num * float num将不得不被禁止，从而导致非详尽的模式匹配和运行时异常。

似乎需要一个像 type a b. a num * b num -> c(a,b) num 这样的签名。在哪里 c是一个包含类型提升规则的类型函数。我不认为 OCaml 有这个。开放类型或对象是否能够捕捉到这一点？我不是在寻找类型之间最通用的函数，如果我可以明确列出少数输入类型组合和相应的输出类型就足够了。

Answer 1

您询问的具体情况可以使用 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_float转至 to_int : 是静态的
知道只加两个 I s 结果为 I .但是，您可以更改 to_int至 to_float (并调整 printf )。这些操作很容易组合和传播类型信息。

嵌套的愚蠢 match表达是一个黑客我会问
关于邮件列表。我以前从未见过这样做过。

一般类型函数

AFAIK 在当前 OCaml 中评估通用类型函数的唯一方法需要
用户提供见证，即一些额外的类型和值信息。这
可以通过多种方式完成，例如将参数包装在额外的构造函数中
(参见@mookid 的回答)，使用一流的模块(也在接下来讨论
部分)，提供一小部分抽象值可供选择(其中
实现真正的操作，包装器分派(dispatch)给这些值)。这
下面的示例使用第二个 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是结果。不幸的是，你必须通过 add一个 promotion 的实例对于 'c被磨碎，即这样的事情不会
(AFAIK)工作:

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 等)和参数/结果类型
组合，可以相互正交；打字可以是
更好，事情可以稍微更容易使用和实现。

编辑 实际上可以删除 I和 F构造函数，即

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

这使得使用更加简单:

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

然而，在这两种情况下，这都不像 GADT+多态变体解决方案那样可组合，因为从未推断出见证。

future 的 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"