OCaml中类型和模块相等的规则是什么 [英] What are the rules for equality of types and modules in OCaml

问题描述

我无法全神贯注于OCaml中的模块相等性.函子本来应该是有用的(这就是Internet所宣称的)，但是有时这似乎失败了，我看不出它背后的一般规则.

I cannot wrap my head around equality of modules in OCaml. Functors are supposed to be applicative (that's what the Internet claims), but this seems to fail sometimes, and I cannot quite see the general rule behind it.

这是我的示例代码:

module type PT = sig end
module P = struct end

let () =
  Random.self_init ()

module OrigHashtbl = Hashtbl
module Hashtbl = struct
  module Make(Hash: OrigHashtbl.HashedType) = struct
    let random = Random.int 1000000

    type 'a t = { t_list: (Hash.t * 'a) list }

    let create _ =
      Format.printf "Random %d@." random;
      { t_list = [] }          

    let mem ht v =
      Format.printf "Random %d@." random;
      List.mem_assoc v ht.t_list          
  end
end

module Hash = struct
  type t = int
  let equal x1 x2 = x1 = x2
  let hash x = x
end

module Wrap(P: PT) = struct
  module H = Hashtbl.Make(Hash)
end

module Wrap1 = Wrap(P)
module Wrap2 = Wrap(P)
module H1 = Wrap1.H
module H2 = Wrap2.H

let () =
  let ht = H1.create 16 in
  Format.printf "%b@." (H2.mem ht 0)

ideone上的代码: https://ideone.com/5C8Muk

Code at ideone: https://ideone.com/5C8Muk

我在这里要做的是从Hashtbl模块创建一些函数的虚拟实现，并将其包装在函子Wrap中，我将其调用"两次，创建了H1和H2，它们可以互换使用尽管它们是不同的模块，它们捕获了不同的random值:

What I do here is I create a dummy implementation of some functions from Hashtbl module and wrap it in the functor Wrap which I 'call' twice, creating H1 and H2 which can be used interchangeably despite them being different modules that capture different value of random:

$ ./test.byte 
Random 501586
Random 681009
false

这是可以预期的，因为如Internet所言，OCaml函子是适用的.

This is expected, because, as the Internet claims, OCaml functors are applicative.

但是然后我尝试将Hash模块移到Wrap内，程序停止编译.

But then I try to move the Hash module inside Wrap and the program stops compiling.

module Wrap(P: PT) = struct
  module Hash = struct
    type t = int
    let equal x1 x2 = x1 = x2
    let hash x = x
  end

  module H = Hashtbl.Make(Hash)
end

Ideone上的代码: https://ideone.com/Gjxc32

Code at Ideone: https://ideone.com/Gjxc32

$ ocamlbuild test.byte
+ /home/XXX/.opam/4.04.0/bin/ocamlc.opt -c -o test.cmo test.ml
File "test.ml", line 41, characters 35-37:
Error: This expression has type 'a H1.t = 'a Hashtbl.Make(Wrap1.Hash).t
       but an expression was expected of type
         'b H2.t = 'b Hashtbl.Make(Wrap2.Hash).t

那是为什么?我希望如果Wrap1和Wrap2是相同的模块(因为函子应该是适用的，对吗?)，那么Wrap1.Hash和Wrap2.Hash也是相同的.比较模块背后的一般规则是什么?

Why is that? I'd expect that if Wrap1 and Wrap2 are the same module (because functors should be applicative, right?) then Wrap1.Hash and Wrap2.Hash are also the same. What's the general rule behind comparing modules?

注意:这是另一个问题的继续如何说服ocaml两个仿函数实例是相等的.唯一的答案就是"OCaml函子是生成性的"，这是错误的(至少有时是这样).

Note: This is a continuation of another question How to convince ocaml that two functor instantiations are equal. There the only answer I got was along the lines of "OCaml functors are generative" which is false (at least sometimes).

修改

也许，我问模块相等性是错误的.我真正感兴趣的是类型相等.为什么在某些情况下Wrap1.H.t等于Wrap2.H.t而在某些情况下-不等于

Perhaps, I was wrong asking about module equality. What I'm actually interested in is type equality. Why in some cases Wrap1.H.t equals Wrap2.H.t and in some cases - not.

答案

在与@Drup讨论之后，对我来说事情变得更加清楚了.适用性表示以下含义:如果为A = B，则为F(A) =/= F(B)，但为F(A).t = F(B).t.对于在F(A)和F(B)内部定义的模块，情况取决于这些模块的定义方式.在我的示例中，Wrap1.H.t = Wrap2.H.t是否取决于H的定义.在编译的变体中，Wrap1.H.t = Hashtbl(Hash).t = Wrap2.H.t.在未编译的变体中，Wrap1.H.t = Hashtbl(Wrap1.Hash).t和Wrap2.H.t = Hashtbl(Wrap2.Hash).t，它们是不同的.

After a discussion with @Drup, things became more clear for me. Applicativeness means the following: if A = B, then F(A) =/= F(B), but F(A).t = F(B).t. For the modules defined inside F(A) and F(B), things depend on how these modules are defined. In my example, whether or not Wrap1.H.t = Wrap2.H.t depends on the definition of H. In the variant that compiles, Wrap1.H.t = Hashtbl(Hash).t = Wrap2.H.t. In the variant that does not compile, Wrap1.H.t = Hashtbl(Wrap1.Hash).t and Wrap2.H.t = Hashtbl(Wrap2.Hash).t, and they are distinct.

推荐答案

应用函子"表示A = B表示F(A).t = F(B).t.它不是暗示F(A).M = F(B).M.这是关于类型，而不是模块.

"Applicative functors" means that A = B implies F(A).t = F(B).t. It doesn't implies that F(A).M = F(B).M. It's about types, not modules.

创建类型和创建模块之间的一个根本区别是创建类型是无副作用的(因此可以用一种应用行为来对待).创建模块并非没有副作用，因此您不能将两个不同的新模块视为相同. octachron在最后一个答案中给出了一个很好的例子.

One fundamental difference between creation of types and creation of modules is that creating types is side-effect free (hence can be treated with an applicative behavior). Creating a module is not side effect free, hence you can't consider two different fresh modules as being the same. octachron gave a pretty good example in the last answer.

如果要在仍然具有本地模块的同时保持相等性，则可以使用模块别名.如果您改为这样做:

If you want to keep the equality while still having local modules, you can use module aliases. If you do this instead:

module Hash0 = struct
  type t = int
  let equal x1 x2 = x1 = x2
  let hash x = x
end
module Wrap(P: PT) = struct
  module Hash = Hash0 (* the type of this module is "= Hash0" *)
  module H = Hashtbl.Make(Hash)
end

然后接受程序.

请注意，即使在失败的版本中，即使模块不相等，Wrap1.Hash.t = Wrap2.Hash.t也会保留(无论其定义如何).

Note that, even in your failing version, Wrap1.Hash.t = Wrap2.Hash.t holds (regardless of its definition), even if the modules are not equals.

这篇关于OCaml中类型和模块相等的规则是什么的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！