为什么OCaml有时需要eta扩展?

逻辑链

如果我具有以下OCaml函数:

let myFun = CCVector.map ((+) 1);;

它在Utop中运行良好,Merlin并未将其标记为编译错误。但是,当我尝试编译它时,出现以下错误:

错误:此表达式的类型(int,'_a)CCVector.t->(int,'_b)CCVector.t包含无法归纳的类型变量

如果我对它进行eta-expand编译,则编译良好:

let myFun foo = CCVector.map ((+) 1) foo;;

因此,我想知道为什么它不能以eta简化的形式进行编译,以及为什么eta简化的格式似乎可以在顶级(Utop)中工作,但在编译时却不能使用?

哦,这里是CCVector的文档'_a部分可以是`RO或`RW,取决于它是只读的还是可变的。

卡姆斯波特

您在这里得到的是ML语言家族的价值多态性限制。

限制的目的是共同解决let多态性和副作用。例如,在以下定义中:

let r = ref None

r不能具有多态类型'a option ref否则:

let () =
  r := Some 1;       (* use r as int option ref *)
  match !r with
  | Some s -> print_string s  (* this time, use r as a different type, string option ref *)
  | None -> ()

错误地类型检查是有效的,但它崩溃,由于参考单元r被用于这两个不兼容的类型。

为了解决这个问题,在80年代进行了许多研究,价值多元主义就是其中之一。它仅将多态性限制为让定义形式为“非扩展”的绑定。eta扩展形式不可扩展,因此您的eta扩展版本myFun具有多态类型,但不适用于eta简化形式。(更确切地说,OCaml使用此值多态性的宽松版本,但故事基本上是相同的。)

当let绑定的定义扩展时,不会引入多态性,因此类型变量将不被泛化。这些类型'_a在顶层打印,其直观含义是:稍后必须将它们实例化为某些具体类型:

# let r = ref None                           (* expansive *)
val r : '_a option ref = {contents = None}   (* no polymorphism is allowed *)
                                             (* type checker does not reject this,
                                                hoping '_a is instantiated later. *)

我们可以'_a在定义后修复类型

# r := Some 1;;                              (* fixing '_a to int *)
- : unit = ()
# r;;
- : int option ref = {contents = Some 1}     (* Now '_a is unified with int *)

修复后,您将无法更改类型,这可以防止上述崩溃。

允许这种键入延迟,直到编译单元的键入结束为止。顶层是一个永无休止的单元,因此您可以'_a在会话的任何地方使用类型变量作为但是在单独的编译中,'_a必须将变量实例化为某种类型,而没有类型变量,直到ml文件末尾:

(* test.ml *)
let r = ref None (* r : '_a option ref *)
(* end of test.ml. Typing fails due to the non generalizable type variable remains. *)

这就是myFun编译器函数所发生的事情

AFAIK并不能完美解决多态性和副作用问题。像其他解决方案一样,值多态性限制也有其自身的缺点:如果要具有多态性值,则必须以非扩展的方式进行定义:必须使用eta-expand myFun这有点糟糕,但被认为可以接受。

您还可以阅读其他答案:

本文收集自互联网,转载请注明来源。

如有侵权,请联系[email protected] 删除。

编辑于
0

我来说两句

0条评论
登录后参与评论

相关文章

来自分类Dev

为什么完全合格的程序集名称有时需要空格?

来自分类Dev

为什么匿名对象有时需要默认构造函数?

来自分类Dev

为什么有时在动作参数中需要传递lambda而不是其他时间?

来自分类Dev

为什么Groovy有时有时不需要方法的返回类型(甚至def)?

来自分类Dev

为什么有时需要在`data.frame()`中将`.`括在`do`中的命名参数中?

来自分类Dev

为什么有时无法扩展用户环境变量?

来自分类Dev

为什么在Ruby中有时需要加括号?

来自分类Dev

为什么有时需要选择对象以避免“对象不支持此属性或方法”

来自分类Dev

为什么有时宏扩展会增加空间?

来自分类Dev

为什么jq有时需要过滤器表达式,而有时则不需要过滤器表达式?

来自分类Dev

为什么在Vue中使用$ refs时有时需要$ el?

来自分类Dev

为什么有时需要在docker上运行nginx?

来自分类Dev

为什么Visualforce页面需要无效的HTML?(有时)

来自分类Dev

为什么在熊猫中进行元素操作时有时需要添加.value?

来自分类Dev

为什么有时即使我的项目未直接使用Nuget依赖项,也有时需要添加它们?

来自分类Dev

为什么有时需要外部包装箱?

来自分类Dev

为什么有时宏扩展会增加空间?

来自分类Dev

为什么jq有时需要过滤器表达式,而有时则不需要过滤器表达式?

来自分类Dev

为什么有时有时需要手动重启路由器?

来自分类Dev

为什么在动作参数中有时需要传递lambda而不是其他时间?

来自分类Dev

为什么有时需要在将对象作为参数传递之前创建变量

来自分类Dev

为什么对大数进行数学运算有时需要中间变量才能返回正确的结果?

来自分类Dev

为什么有时有时需要手动导入密钥?

来自分类Dev

为什么有时需要通过kill -9来停止进程

来自分类Dev

为什么QEMU的hostfwd选项有时需要root访问,而有时却不需要root访问

来自分类Dev

为什么有时我们需要在根目录下挂载那些文件?

来自分类Dev

为什么“尝试/捕获”中的命令有时需要-ErrorAction停止,而有时则不需要?

来自分类Dev

为什么 Moq 有时需要在 Returns 中进行显式类型声明?

来自分类Dev

为什么滚动条有时会显示在 Chrome 扩展中有时不会显示

Related 相关文章

  1. 1

    为什么完全合格的程序集名称有时需要空格?

  2. 2

    为什么匿名对象有时需要默认构造函数?

  3. 3

    为什么有时在动作参数中需要传递lambda而不是其他时间?

  4. 4

    为什么Groovy有时有时不需要方法的返回类型(甚至def)?

  5. 5

    为什么有时需要在`data.frame()`中将`.`括在`do`中的命名参数中?

  6. 6

    为什么有时无法扩展用户环境变量?

  7. 7

    为什么在Ruby中有时需要加括号?

  8. 8

    为什么有时需要选择对象以避免“对象不支持此属性或方法”

  9. 9

    为什么有时宏扩展会增加空间?

  10. 10

    为什么jq有时需要过滤器表达式,而有时则不需要过滤器表达式?

  11. 11

    为什么在Vue中使用$ refs时有时需要$ el?

  12. 12

    为什么有时需要在docker上运行nginx?

  13. 13

    为什么Visualforce页面需要无效的HTML?(有时)

  14. 14

    为什么在熊猫中进行元素操作时有时需要添加.value?

  15. 15

    为什么有时即使我的项目未直接使用Nuget依赖项,也有时需要添加它们?

  16. 16

    为什么有时需要外部包装箱?

  17. 17

    为什么有时宏扩展会增加空间?

  18. 18

    为什么jq有时需要过滤器表达式,而有时则不需要过滤器表达式?

  19. 19

    为什么有时有时需要手动重启路由器?

  20. 20

    为什么在动作参数中有时需要传递lambda而不是其他时间?

  21. 21

    为什么有时需要在将对象作为参数传递之前创建变量

  22. 22

    为什么对大数进行数学运算有时需要中间变量才能返回正确的结果?

  23. 23

    为什么有时有时需要手动导入密钥?

  24. 24

    为什么有时需要通过kill -9来停止进程

  25. 25

    为什么QEMU的hostfwd选项有时需要root访问,而有时却不需要root访问

  26. 26

    为什么有时我们需要在根目录下挂载那些文件?

  27. 27

    为什么“尝试/捕获”中的命令有时需要-ErrorAction停止,而有时则不需要?

  28. 28

    为什么 Moq 有时需要在 Returns 中进行显式类型声明?

  29. 29

    为什么滚动条有时会显示在 Chrome 扩展中有时不会显示

热门标签

归档