我想知道是否可以在 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 有这个。开放类型或对象是否能够捕捉到这一点?我不是在寻找类型之间最通用的函数,如果我可以明确列出少数输入类型组合和相应的输出类型就足够了。
最佳答案
您询问的具体情况可以使用 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"
关于types - 可以在 OCaml 中的类型之间编码二进制函数吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/41214000/