我试图更好地理解编码的细微差别，而不是在我们将编码转换为通用类型后使用存在类型。 简而言之，在我看来，使用存在类型比编码存在类型要容易得多，我将在下面解释这对我意味着什么。 为了更好地解释这一点，让我们从逻辑中的两个规则开始
- ∀x.P(x) ⇒ ¬(∃x.¬P(x))
- ∃x.P(x) ⇒ ¬(∀x.¬P(x))
由此，我们有
- ∀x.(P(x) ⇒ Q)
- ∀x.(¬P(x) ⩖ Q)
- (∀x.¬P(x)) ⩖ Q
- (¬¬(∀x.¬P(x))) ⩖ Q
- (¬(¬(∀x.¬P(x)))) ⩖ Q
- (¬(∃x.P(x))) ⩖ Q
- (∃x.P(x)) ⇒ Q
因此
(∃x.P(x)) ⇒ Q = ∀x.(第(x)⇒ 问)。
换句话说，如果函数的第一个参数是存在主义的，我们可以把存在主义类型拉到左边，把它表示为一个普遍的。这就是我所说的存在主义规则的使用。 现在，通常当人们谈论普遍类型和存在类型之间的等价时，我们看到
∃x.P(x) = ∀y。(∀x.P(x) ⇒ y) ⇒ y.
这就是我所说的存在主义规则的编码。 为了看到这种等价性，我们有
- ∀年(∀x.P(x) ⇒ y) ⇒ y
- ∀。((∃x.P(x)) ⇒ y) ⇒ y
- ∀y.¬((∃x.P(x)) ⇒ y) ⩖ y
- ∀y.¬(¬(∃x.P(x)) ⩖ y) ⩖ y
- ∀。((∃x.P(x)) ⩕ ¬y) ⩖ y
- ∀。((∃x.P(x)) ⩖ y) ⩕ (y v ¬y)
- ∀。(∃x.P(x)) ⩖ y
- (∃x.P(x)) ⩖ ∀y.y
- ∃x.P(x)
好吧，所以这个规则告诉我的是，存在类型是一个接受将 P(x) 转换为 y 然后输出 y 的程序的函数。
现在，这就是我的意思 使用存在主义和构建存在主义之间的区别。 假设我们想用像OCaml这样的语言构建一个穷人的模块，我们可以通过这样的程序来实现。
type 't mypackage = {
add : 't * 't -> 't;
fromInt : int -> 't;
toString : 't -> string};;
let int_package = {
add = (fun (x,y) -> x+y) ;
fromInt = (fun x->x) ;
toString = (fun x->string_of_int x)};;
let str_package = {
add = (fun (x,y) -> x^y) ;
fromInt = (fun x->string_of_int x) ;
toString = (fun x-> x)};;
let simpleProg fns =
let exp01 = fns.fromInt 1 in
let exp02 = fns.fromInt 2 in
let exp03 = fns.add (exp01,exp02) in
fns.toString exp03
let _ = simpleProg int_package;;
let _ = simpleProg str_package;;
这使用了自上而下的存在主义规则。 就类型而言，我们有
val int_package : int mypackage
val str_package : string mypackage
val simpleProg : 'a mypackage -> string = <fun>
基本上，我们要设计一个名为simpleProg的函数：(∃x.mypackage(x))⇒字符串。 为了做到这一点，我们构建了一个类型为 ∀x.mypackage(x) 的函数⇒字符串，并使用通用编码我们的包，这在大多数函数式语言中都很简单。 现在，如果我们想将int_package和str_package编码为存在包而不是通用包，我们使用存在规则的编码，我们最终得到的代码如下：
type 't mypackage = {
add : 't * 't -> 't;
fromInt : int -> 't;
toString : 't -> string};;
let apply (arg : 't mypackage) (f : 't mypackage -> 'u) : 'u =
f arg;;
let int_package_ = {
add = (fun (x,y) -> x+y) ;
fromInt = (fun x->x) ;
toString = (fun x->string_of_int x)};;
let int_package = apply int_package_;;
let str_package_ = {
add = (fun (x,y) -> x^y) ;
fromInt = (fun x->string_of_int x) ;
toString = (fun x-> x)};;
let str_package = apply str_package_;;
let simpleProg_ fns =
let exp01 = fns.fromInt 1 in
let exp02 = fns.fromInt 2 in
let exp03 = fns.add (exp01,exp02) in
fns.toString exp03
(* Notice that we have inverted how we use the existentials here. We give the
existential the program and don't give the program the existential *)
let _ = int_package simpleProg_;;
let _ = str_package simpleProg_;;
(* This flips things *)
let simpleProg fns =
fns simpleProg_;;
let _ = simpleProg int_package;;
let _ = simpleProg str_package;;
在这里，我们有
val int_package : (int mypackage -> '_a) -> '_a = <fun>
val str_package : (string mypackage -> '_a) -> '_a = <fun>
这基本上就是我们想要的。 int 和字符串类型隐藏在包装中。 然后，我们看到
val simpleProg : (('a mypackage -> string) -> 'b) -> 'b = <fun>
这又是我们想要的。 真的，我们有点想要
val simpleProg : (('a mypackage -> 'b) -> 'b) -> string = <fun>
但是类型变量为我们解决了这个问题(或者我犯了一个可怕的错误。 两者之一。
无论如何，从普遍性实际创建存在主义的结构似乎非常沉重，因为第二个程序显示，而使用存在主义的结构似乎非常简单，第一个程序显示了这一点。 基本上，这就是我的意思，使用存在主义比制作存在主义要容易得多。
所以，实际上，我的两个问题是：
- 如果我们只关心在函数中使用存在包，那么编码为通用类型是否比创建独立存在的存在包容易得多？ 假设这是真的，这似乎是因为我们可以使用通用包(上面的 mypackage 类型)对存在包进行编码。
- 如果我们限制自己仅仅使用存在主义规则并使用这些通用软件包，我们最终会失去什么？ 同样，通过通用包，我的意思是上面 mypackage 类型的技巧。
编辑 1
Camlspotter和Leo White是对的，我的类型被暴露了，包裹搞砸了。 这是相同代码的重写且非常冗长的版本
(* Creates the type forall t.P(t) *)
type 't mypackage = {
add : 't * 't -> 't;
fromInt : int -> 't;
toString : 't -> string};;
(* Creates the type forall u.(forall t.P(t) -> u) *)
type 'u program_that_takes_open_package_and_returns_u = {
code : 't. 't mypackage -> 'u};;
(* Creates the type forall u.(forall t.P(t) -> u) -> u *)
type 'u applies_program_to_specified_packaged_and_produces_u =
'u program_that_takes_open_package_and_returns_u -> 'u;;
(* Has type P(int) *)
let int_package = {
add = (fun (x,y) -> x+y) ;
fromInt = (fun x->x) ;
toString = (fun x->string_of_int x)};;
(* Has type forall u.(forall.t P(t) -> u) -> u. *)
let (applies_prog_to_int_package :
'u applies_program_to_specified_packaged_and_produces_u) =
(* Has type forall u.(forall.t P(t) -> u) *)
(* Even though we specify an int_package, the program must accept all
packages *)
fun (program:'u program_that_takes_open_package_and_returns_u) ->
program.code int_package;;
(* Has type P(string) *)
let str_package = {
add = (fun (x,y) -> x^y) ;
fromInt = (fun x->string_of_int x) ;
toString = (fun x-> x)};;
(* Has type forall u.(forall.t P(t) -> u) -> u. *)
let (applies_prog_to_str_package :
'u applies_program_to_specified_packaged_and_produces_u) =
(* Has type forall u.(forall.t P(t) -> u) *)
(* Even though we specify an str_package, the program must accept all
packages *)
fun (program:'u program_that_takes_open_package_and_returns_u) ->
program.code str_package_;;
(* The code of a program that takes a package called fns and produces a string *)
let simpleProg = { code = fun fns ->
let exp01 = fns.fromInt 1 in
let exp02 = fns.fromInt 2 in
let exp03 = fns.add (exp01,exp02) in
fns.toString exp03}
(* Apply the program to each of the packages *)
let _ = applies_prog_to_int_package simpleProg;;
let _ = applies_prog_to_str_package simpleProg;;
(* Show that we can, in fact, keep all of the packages in a list *)
let _ = [applies_prog_to_int_package;applies_prog_to_str_package];;
我想我在这个过程中学到的最重要的事情本质上是这个重新编码技巧颠倒了事物的构建顺序。 从本质上讲，这些包构建了一个过程，在该过程中，它们接受一个程序，然后将该程序应用于其内部表示。 通过玩这个把戏，包的内部类型被隐藏了。 虽然这在理论上等同于存在主义类型，但就我个人而言，我发现这个过程不同于存在主义的直接实现，例如，皮尔斯的类型和编程语言一书所描述的。
直接回答我上面的问题
- 通用包技巧有效，如果您只对将包直接传递给函数感兴趣，则更容易实现。 它绝对不是一个存在主义包，但它的使用与在同一上下文中使用的真正的存在主义包非常相似，但没有解包。 类似地，我的意思是，我们保留了将基于不同类型的包的不同表示传递到函数中的能力，然后使用这些表示进行一般计算。
- 我们在这些通用软件包中失去的是将这些软件包视为真正的头等舱成员的能力。 最简单的例子是，我们不能把一堆这些通用包放到一个列表中，因为它们的类型是公开的。 一个真正的存在包隐藏了类型，因此更容易传递一个更大的程序。
此外，通用包装是一个可怕的词。 int_package和str_package是专门的，所以它们并不是真正普遍的。 大多数情况下，我没有更好的名字。
我不太明白你的问题，但你对存在的编码似乎是不正确的。
正如你提到的，如果你想模仿∃'t. 't mypackage，那么你必须创建一个类型
∀'y. (∀'t. 't mypackage -> 'y) -> 'y
但这不是OCaml 类型的('t mypackage -> 'y) -> 'y更准确地说，
∀'y. ∀'t. ('t mypackage -> 'y) -> 'y
查看量词的位置。
OCaml 的类型方案被量化最多，它不能像∀'y. (∀'t. 't mypackage -> 'y) -> 'y那样有更高的秩类型，但我们可以用它的记录多态字段来模拟它：
type 'y packed = { unpacked : 't. 't mypackage -> 'y }
(* mimicing ∀'t. 't mypackage -> 'y *)
使用此类型，存在类型可以实现为
type 'y closed_package = 'y packed -> 'y
(* mimicing a higher ranked type ∀'y. (∀'t. 't mypackage -> 'y) -> 'y,
which is equivalent with ∃'t. 't mypackage *)
如果您不喜欢暴露的类型变量'y可以使用记录多态字段再次隐藏它：
type really_closed_package = { l : 'y. 'y closed_package }
包实现可以打包到此接口中，如下所示：
let closed_int_package = { l = fun packed -> packed.unpacked int_package }
let closed_str_package = { l = fun packed -> packed.unpacked str_package }
由于这些打包版本具有相同的类型，我们可以将它们放入列表中：
let closed_packages = [ closed_int_package; closed_str_package ]
这通常是我们想对存在主义者做的事情。
现在编码已完成。使用它也需要一些复杂性，但相当微不足道：
let doubled_int_string p x =
let x = p.fromInt x in
p.toString (p.add (x,x))
doubled_int_string适用于打开的包裹，我们不能简单地将其用于封闭的包裹。我们需要一些转换：
let () =
(* Using "universal" packages *)
print_endline (double_int_string int_package 3);
print_endline (double_int_string str_package 3);
(* Equivalents using "existential" packages *)
print_endline (closed_int_package.l { unpacked = doubled_int_string } 3);
print_endline (closed_str_package.l { unpacked = doubled_int_string } 3)
正如camlspotter所指出的，你的编码不太正确，它应该使用一个类型：
type 'k mypackage_cont = { p: 't. 't mypackage -> 'k }
然后，编码的包将具有以下类型：
val int_package1 : 'k mypackage_cont -> 'k
val str_package1 : 'k mypackage_cont -> 'k
而您的其他版本具有以下类型：
val int_package2 : int mypackage
val str_package2 : string mypackage
请注意，编码版本是真正的存在型，因为它没有在其类型中提及存在类型(int 或字符串)。这是关键的区别。
例如，考虑创建一个异构列表。您可以使用正确的编码来做到这一点：
# [ int_package1; str_package1; ];;
- : ('a mypackage_cont -> 'a) list = [<fun>; <fun>]
但不适用于非编码版本：
# [ int_package2; str_package2 ];;
Characters 16-28:
[ int_package2; str_package2 ];;
^^^^^^^^^^^^
Error: This expression has type string mypackage
but an expression was expected of type int mypackage
Type string is not compatible with type int
坦率地说，这有点超出我的头脑，但我想我明白你的基本想法。我记得，Haskell在支持存在主义类型方面也有类似的东西。
但是，您的第二个构造的类型对我来说看起来并不那么有用：
val int_package : (int mypackage -> '_a) -> '_a = <fun>
这是一种单态类型，其中_a尚未指定。它不是多态类型。这意味着您只能给它一种类型的程序。如果你编写了第二个想要返回 int 而不是字符串的程序，你的存在包将不允许你调用它。至少，在我看来是这样的。
第一个构造具有真正的多态类型，因此看起来它应该更好地工作。
(一个知识渊博的类型理论类型的人可能会提供更多帮助：-)