在我们将其转换为通用类型之后，我试图更好地理解编码与使用存在类型的细微差别。简而言之，在我看来，使用存在类型比编码要容易得多，我将在下面解释这对我意味着什么。为了更好地解释这一点，让我们从逻辑中的两条规则开始
- ∀xP(x) ⇒ ¬(∃x.¬P(x))
- ∃xP(x) ⇒ ¬(∀x.¬P(x))
由此，我们有
- ∀x.(P(x) ⇒ Q)
- ∀x.(¬P(x) ⩖ Q)
- (∀x.¬P(x)) ⩖ Q
- (¬¬(∀x.¬P(x))) ⩖ Q
- (¬(¬(∀x.¬P(x)))) ⩖ Q
- (¬(∃xP(x))) ⩖ Q
- (∃xP(x)) ⇒ Q
因此，
(∃xP(x)) ⇒ Q = ∀x.(P(x) ⇒ Q)。
换句话说，如果函数的第一个参数是存在的，我们可以将存在类型拉到左边并将其表示为通用的。这就是我所说的使用存在规则。现在，通常当人们谈论普遍类型和存在类型之间的等价性时，我们会看到
∃xP(x) = ∀y.(∀xP(x) ⇒ y) ⇒ y。
这就是我所说的存在规则的编码。为了看到这种等价性，我们有
- ∀y.(∀xP(x) ⇒ y) ⇒ y
- ∀y.((∃xP(x)) ⇒ y) ⇒ y
- ∀y.¬((∃xP(x)) ⇒ y) ⩖ y
- ∀y.¬(¬(∃xP(x)) ⩖ y) ⩖ y
- ∀y.((∃xP(x)) ⩕ ¬y) ⩖ y
- ∀y.((∃xP(x)) ⩖ y) ⩕ (yv ¬y)
- ∀y.(∃xP(x)) ⩖ y
- (∃xP(x)) ⩖ ∀yy
- ∃xP(x)
好的，所以这条规则对我说的是，存在类型是一个函数，它接受将 P(x) 转换为 ay 然后输出 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 和 string 类型隐藏在包装内。然后，我们看到
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];;
我想我在这个过程中学到的最大的东西本质上是这种重新编码技巧颠倒了事物的构造顺序。本质上，这些包建立了一个过程，在该过程中它们接受程序，然后将该程序应用于其内部表示。通过玩这个技巧，包的内部类型被隐藏了。尽管这在理论上等同于存在类型，但就个人而言，我发现该过程不同于直接实现存在的过程，例如 Pierce 的类型和编程语言一书中所描述的存在。
直接回答我上面的问题
- 如果您只对将包直接传递给函数感兴趣，通用包技巧很有效，并且更容易实现。它绝对不是一个存在包，但它的用途与在同一上下文中使用的真正存在包非常相似，但没有解包。类似地，我的意思是我们保留将基于不同类型的包的不同表示形式传递到函数中，然后使用这些表示形式进行通用计算的能力。
- 我们在这些通用包中失去的是将这些包视为真正的一流成员的能力。最简单的例子是我们不能把一堆这些通用包放到一个列表中，因为它们的类型是暴露的。真正的存在包隐藏了类型，因此更容易传递更大的程序。
此外，通用包是一个可怕的词。int_package 和 str_package 是专门的，因此它们并不是真正通用的。大多数情况下，我没有更好的名字。