为什么类型推理算法会因为“Fun.flip Option.bind”而感到困惑?

Why type inference algorithm confuses because of 'Fun.flip Option.bind'?

提问人:Valentyn Zakharenko 提问时间:5/8/2020 最后编辑:Valentyn Zakharenko 更新时间:5/8/2020 访问量:98

问:

模块中函数声明的常见签名是当最后一个参数具有主状态 (Module.t) 的类型时。就像在“列表”模块中一样。此窗体打开了使用“|>”运算符的功能,例如:

[1;2;3] |> List.filter ((>)2)
        |> List.map ((-)1)
        |> List.fold_left 0 (+)

但是“选项”模块中的函数“绑定”不遵循这种形式。它的第一个参数是“Option.t”

val bind : 'a option -> ('a -> 'b option) -> 'b option

但是好吧,我可以改变它。我以相反的参数顺序声明了函数“opt_bind”。

let opt_bind = Fun.flip Option.bind

但是这个行不通。并且编译了以下代码,并出现了以下错误

type a = A of int
type b = B of int 

let f x = Some (A x)
let g (A x) = Some (B x)  
let opt_bind = Fun.flip Option.bind 

let result = 
  (Some 42) |> opt_bind f
            |> opt_bind g
         |> opt_bind g
                     ^                     

错误:此表达式的类型为 -> b 选项,但表达式应>类型为 int -> 选项。类型 a 与类型 int 不兼容

与相同的情况

let result = 
  let x = opt_bind f (Some 42) in
  let x = opt_bind g x in
  x 

即使我注意到了所有类型,我仍然有同样的问题。

let f : int -> a option = fun x -> Some (A x)
let g : a -> b option = fun (A x) -> Some (B x)  
let opt_bind : ('a -> 'b option) -> 'a option -> 'b option = 
  Fun.flip Option.bind 

let result : b option = 
  let x : a option = opt_bind f (Some 42) in
  let x : b option = opt_bind g x in
  x ;;

let result = 
  let x = Option.bind (Some 42) f in
  let x = Option.bind x g in
  x 

工作正常。

为什么“opt_bind”对“g”有错误的类型期望,就好像“opt_bind”不是泛型的一样?
如何使用“bind”和“|>”表示法?

OCAML 类型推断 值限制

评论

1赞 Andreas Rossberg 5/8/2020
类型批注无法规避值限制。在这种情况下,它们并不意味着你所想的——仍然不是多态的;取而代之的是,AND 与弱类型变量统一。(注解中类型变量的这种误导性语义可以说是 OCaml 的一个错误特征。除了注释之外,您需要使用至少一个参数来“扩展”定义,如 Jeffrey 的回答所示。这避免了值限制。opt_bind'a'b
0赞 ivg 5/9/2020
另请参阅 ocamlverse.github.io/content/weak_type_variables.html

答:

4赞 Jeffrey Scofield 5/8/2020 #1

你的问题是你的定义不够多态。由于您将其定义为应用程序(从 Fun.flip 到 Option.bind),因此由于值限制,无法将其设置为多态性。opt_bind

如果你这样定义它:

let opt_bind a b = Fun.flip Option.bind a b

或者,等效地,像这样:

let opt_bind a b = Option.bind b a

然后事情就会奏效。

如果你询问你的定义类型,你会看到问题:opt_bind

# let opt_bind = Fun.flip Option.bind;;
val opt_bind :
  ('_weak3 -> '_weak4 option) -> '_weak3 option ->
  '_weak4 option = <fun>

“弱”类型变量告诉您,生成的函数不是多态的。

本质区别在于,在语法上是一个应用程序(函数调用)。这样的表达式不能是多态的。这两种替代形式定义为 lambda(函数值),它是值限制术语中的语法“值”。Fun.flip Option.bindbind_opt

需要值限制来确保多态函数是合理的(即,它们不允许对值进行不适当的操作)。

我选择的价值限制(尤其是在 OCaml 中实现的)的参考文献是这篇论文:放宽价值限制,Jacques Garrigue