4

エンコーディングのニュアンスと、存在型をユニバーサルに変換した後の使用のニュアンスをよりよく理解しようとしています。要するに、存在型を使用することは、エンコードするよりもはるかに簡単であるように思われます。それが私にとって何を意味するのかを以下で説明します。これをよりよく説明するために、ロジックからの 2 つのルールから始めましょう。

  1. ∀xP(x) ⇒ ¬(∃x.¬P(x))
  2. ∃xP(x) ⇒ ¬(∀x.¬P(x))

これから、私たちはそれを持っています

  1. ∀x.(P(x) ⇒ Q)
  2. ∀x.(¬P(x) ⩖ Q)
  3. (∀x.¬P(x)) ⩖ Q
  4. (¬¬(∀x.¬P(x))) ⩖ Q
  5. (¬(¬(∀x.¬P(x)))) ⩖ Q
  6. (¬(∃xP(x))) ⩖ Q
  7. (∃xP(x)) ⇒ Q

したがって、

(∃xP(x)) ⇒ Q = ∀x.(P(x) ⇒ Q)。

つまり、関数の最初の引数が存在型である場合、その存在型を左側に引き出して、それをユニバーサルとして表すことができます。これを私は実存的ルールの使用と呼んでいます。通常、人々が普遍型と実存型の同等性について話すとき、

∃xP(x) = ∀y.(∀xP(x) ⇒ y) ⇒ y.

これは、私が存在規則のエンコーディングと呼んでいるものです。この等価性を確認するために、

  1. ∀y.(∀xP(x) ⇒ y) ⇒ y
  2. ∀y.((∃xP(x)) ⇒ y) ⇒ y
  3. ∀y.¬((∃xP(x)) ⇒ y) ⩖ y
  4. ∀y.¬(¬(∃xP(x))⩖y)⩖y
  5. ∀y.((∃xP(x)) ⩕ ¬y) ⩖ y
  6. ∀y.((∃xP(x)) ⩖ y) ⩕ (yv ¬y)
  7. ∀y.(∃xP(x))⩖y
  8. (∃xP(x)) ⩖ ∀yy
  9. ∃xP(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)) ⇒ string という関数を設計したいと考えています。そのために、代わりに ∀x.mypackage(x) ⇒ string 型の関数を作成し、パッケージをユニバーサルでエンコードします。これは、ほとんどの関数型言語で簡単に実行できます。代わりに、実際に 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>

しかし、型変数がこれを整理してくれます (または、私はひどい間違いを犯しました。2 つのうちの 1 つです)。

いずれにせよ、2 番目のプログラムが示すように、ユニバーサルから実存を実際に作成するための構造は非常に重く見えますが、最初のプログラムが示すように、実存を使用するための構造は非常に単純に見えます。基本的に、それは私が意味することであり、存在を使用することは、作成するよりもはるかに簡単です.

だから、本当に、私の2つの質問は次のとおりです。

  1. 関数内で存在パッケージを使用することのみを気にする場合、ユニバーサル型へのエンコードは、独立して存在するパッケージを作成するよりもはるかに簡単ですか? これが正しいと仮定すると、これは、既存のパッケージをユニバーサル パッケージ (上記のタイプ mypackage) でエンコードできるためと思われます。
  2. 存在規則の使用とこれらの普遍的なパッケージの使用だけに制限すると、最終的に何を失うのでしょうか? 繰り返しになりますが、ユニバーサル パッケージとは、上記のタイプ 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 の本「Types and Programming Languages」などで説明されているように、実存型の直接実装とはプロセスが異なると思います。

上記の私の質問に対する直接の回答として

  1. パッケージを関数に直接渡すことのみに関心がある場合は、ユニバーサル パッケージのトリックが機能し、実装がはるかに簡単になります。これは絶対に実在するパッケージではありませんが、その使用法は、この同じコンテキストで使用される真の実在するパッケージと非常に似ていますが、解凍は必要ありません。同様に、異なる型に基づくパッケージの異なる表現を関数に渡し、これらの表現で一般的に計算する機能を保持することを意味します。
  2. これらのユニバーサル パッケージで失われるのは、これらのパッケージを真のファースト クラス メンバーのように扱う能力です。最も単純な例は、それらのタイプが公開されているため、これらのユニバーサル パッケージの束をリストに入れることができないということです。真の存在パッケージは型を隠しているため、より大きなプログラムに渡すのがはるかに簡単です。

また、ユニバーサルパッケージはひどい言葉です。int_package と str_package は特殊化されているため、実際には普遍的ではありません。ほとんどの場合、私はより良い名前を持っていません。

4

3 に答える 3

4

私はあなたの質問をよく理解していませんが、existential のエンコードが間違っているようです。

あなたが言ったように、あなたが模倣したいのであれば∃'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)
于 2014-01-23T09:36:44.363 に答える
2

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 または string) が記載されていないため、真に存在型であることに注意してください。これが主な違いです。

たとえば、異種リストの作成を考えてみましょう。適切なエンコーディングでそれを行うことができます：

# [ 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
于 2014-01-23T18:19:44.073 に答える