language-agnostic - 编码为通用时编码与使用存在类型

Question

在将编码转换为通用类型之后，我试图更好地理解编码的细微差别，而不是使用存在的类型。简而言之，在我看来，使用存在性类型比编码类型要容易得多，下面将对我解释这对我来说意味着什么。为了更好地解释这一点，让我们从逻辑的两个规则开始


∀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。（P（x）⇒Q）。

换句话说，如果函数的第一个参数是存在的，我们可以向左拉出存在的类型并将其表示为通用类型。这就是所谓的存在规则的使用。现在，通常当人们谈论普遍型和存在型之间的对等时，我们看到

∃x.P（x）=∀y。（∀x.P（x）⇒y）⇒y。

这就是我所说的存在性规则的编码。为了看到这种等效性，我们有


∀y。（∀x.P（x）⇒y）⇒y
∀y。（（（∃x.P（x））⇒y）⇒y
∀y.¬（（∃x.P（x））⇒y）⩖y
∀y.¬（¬（∃x.P（x））⩖y）y y
∀y。（（（∃x.P（x））⩕¬y）⩖y
∀y。（（（∃x.P（x））⩖y）⩕（y v¬y）
∀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和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是专门的，因此它们并不是通用的。通常，我没有更好的名字。

Answer 1

我不太了解您的问题，但是您对存在性的编码似乎不正确。

如前所述，如果要模仿∃'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)