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

Question

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

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

现在我想要一个函数add来求和a 'a num和a 'b num并返回一个int numif 'a和'bare int,并且float num如果它们中至少有一个是a float.此外,类型系统应该知道输出将使用哪个构造函数.也就是说,在函数调用中应该静态地知道输出是类型int num的.

那可能吗？到目前为止,我只能管理签名函数type a b. a num * b num -> a num,因此总是必须提供(更一般的)float作为第一个参数.int num * float num必须不允许这种情况,导致非穷举模式匹配和运行时异常.

似乎需要一个签名,例如type a b. a num * b num -> c(a,b) numwhere 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:静态地知道只添加两个Is会产生一个I.但是,您可以更改 to_int为to_float(并调整printf).这些操作容易组成和传播类型信息.

具有嵌套match表达式的foolery 是我将在邮件列表中询问的黑客攻击.我以前从未见过这件事.

一般类型功能

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是结果.不幸的是,你必须传递add一个promotionfor 的实例'c,即这样的东西不会(AFAIK)工作:

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

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

尽管事实'c完全由GADT 决定,'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 +多态变体解决方案那样可组合,因为证据永远不会被推断.

未来的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"

使用模块化含义,您还可以简单地添加无标记的浮动和整数.此示例对应于调度函数"见证":

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

从4.04.0版开始,OCaml无法以这种方式编码类型级依赖项.打字规则必须更简单.

一种选择是为此使用简单的变体类型,将所有内容包装成一个(可能很大)类型并匹配:

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)

另一种方法是将输入值限制为具有匹配类型:

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)

最后,其中一个输入值的类型可用于约束返回值的类型.在此示例中,返回值将始终与第二个参数具有相同的类型:

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)