存在タイプとは何ですか？
https://stackoverflow.com/questions/292274
-
08-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian質問
ウィキペディアの記事 存在タイプ を読みました。存在演算子（<！>＃8707;）のために、それらが存在型と呼ばれることを集めました。しかし、そのポイントが何であるかはわかりません。
の違いは何ですかT = ∃X { X a; int f(X); }
and
T = ∀x { X a; int f(X); }
？
解決
誰かが普遍的なタイプを定義するとき∀X彼らは言っています：あなたはあなたが望むどんなタイプでも差し込むことができます、私は仕事をするためにタイプについて何も知る必要はありません、私は参照するだけですそれにX として不透明に。
誰かが実在型を定義するとき∃X彼らは次のように言っています：ここで欲しいものは何でも使います。そのタイプについては何も知らないので、不透明にcopy として参照することしかできません。
ユニバーサルタイプを使用すると、次のように記述できます。
void copy<T>(List<T> source, List<T> dest) {
...
}
T関数は、runAllCompilersが実際に何であるかを知りませんが、その必要はありません。
実在型を使用すると、次のように記述できます。
interface VirtualMachine<B> {
B compile(String source);
void run(B bytecode);
}
// Now, if you had a list of VMs you wanted to run on the same input:
void runAllCompilers(List<∃B:VirtualMachine<B>> vms, String source) {
for (∃B:VirtualMachine<B> vm : vms) {
B bytecode = vm.compile(source);
vm.run(bytecode);
}
}
リスト内の各仮想マシンの実装は、異なるバイトコードタイプを持つことができます。 VirtualMachine.compile関数は、バイトコードタイプが何であるかを認識していませんが、その必要はありません。バイトコードをVirtualMachine.runからList<?>に中継するだけです。
Javaタイプのワイルドカード（例：VMWrapper）は、存在タイプの非常に限られた形式です。
更新：ユニバーサルタイプを使用して実在タイプをシミュレートすることができることを忘れていました。最初に、ユニバーサル型をラップして、型パラメーターを非表示にします。次に、制御を反転します（これにより、上記の定義の<！> quot; you <！> quot;と<！> quot; I <！> quot;の部分が交換されます。これは、実存と普遍性の主な違いです。
// A wrapper that hides the type parameter 'B'
interface VMWrapper {
void unwrap(VMHandler handler);
}
// A callback (control inversion)
interface VMHandler {
<B> void handle(VirtualMachine<B> vm);
}
これで、VMHandlerが独自のhandleを呼び出すことができます。これには、汎用的に型指定されたB関数があります。最終的な効果は同じで、コードでは<=>を不透明として処理する必要があります。
void runWithAll(List<VMWrapper> vms, final String input)
{
for (VMWrapper vm : vms) {
vm.unwrap(new VMHandler() {
public <B> void handle(VirtualMachine<B> vm) {
B bytecode = vm.compile(input);
vm.run(bytecode);
}
});
}
}
VM実装の例：
class MyVM implements VirtualMachine<byte[]>, VMWrapper {
public byte[] compile(String input) {
return null; // TODO: somehow compile the input
}
public void run(byte[] bytecode) {
// TODO: Somehow evaluate 'bytecode'
}
public void unwrap(VMHandler handler) {
handler.handle(this);
}
}
他のヒント
存在タイプの値は、∃x. F(x) はペアです、いくつかのタイプ xと値<タイプF(x)の/ em>。一方、∀x. F(x)のような多相型の値は、ある種のFを取り、型の値を生成する 関数です。どちらの場合も、型はいくつかの型コンストラクターTで閉じます。
このビューではタイプと値が混在していることに注意してください。存在証明は、1つのタイプと1つの値です。普遍的証明は、タイプ（またはタイプから値へのマッピング）でインデックス付けされた値のファミリ全体です。
したがって、指定した2つのタイプの違いは次のとおりです。
T = ∃X { X a; int f(X); }
これは、タイプXの値に、a:Xと呼ばれるタイプ、値f:X->int、および関数aが含まれていることを意味します。タイプintの値のプロデューサーは、fに対して any タイプを選択できますが、コンシューマーはnullについて何も知ることができません。 n+1と呼ばれる例が1つあり、この値をnに渡すことで<=>に変換できることを除きます。つまり、タイプ<=>の値は、何らかの方法で<=>を生成する方法を知っています。さて、中間タイプ<=>を削除して、次のように言うことができます。
T = int
普遍的に定量化されたものは少し異なります。
T = ∀X { X a; int f(X); }
これは、タイプ<=>の値には任意のタイプ<=>を指定でき、値<=>と関数<=> <=>に関係なく生成されます。つまり、タイプ<=>の値のコンシューマーは、<=>の任意のタイプを選択できます。そして、タイプ<=>の値のプロデューサーは<=>について全く何も知ることができませんが、<=>の選択に対して値<=>を生成できなければならず、そのような<=>への値。
この型を明らかに実装することは不可能です。想像できるすべての型の値を生成できるプログラムはないからです。 <=>やボトムスなどの不条理を許可しない限り。
実存はペアであるため、実存の引数はカリーを介して普遍的な引数に変換できます。
(∃b. F(b)) -> Int
と同じ：
∀b. (F(b) -> Int)
前者は rank-2 の実存です。これにより、次の有用なプロパティが得られます。
実存的に定量化されたランクのタイプ<=>は、一般的に定量化されたランクのタイプ<=>です。
スコーレム化 と呼ばれる、実在物をユニバーサルに変換する標準的なアルゴリズムがあります。
2つの概念は補完的であるため、実在型と普遍型を説明することは理にかなっていると思います。他の
存在タイプに関するすべての詳細（正確な定義を与える、考えられるすべての使用法をリストする、抽象データタイプとの関係など）に答えることはできません。 このHaskellWikiの記事の内容を（Javaを使用して）示すだけです。存在型の主な効果：
既存のタイプは、いくつかの異なる目的で使用することができます。しかし、彼らがすることは、右側の型変数を「隠す」ことです。通常、右側に表示される型変数は左側にも表示される必要があります[<！>＃8230;]
セットアップの例：
次の擬似コードは、それを修正するのに十分簡単であっても、完全に有効なJavaではありません。実際、それがまさにこの答えでやろうとしていることです！
class Tree<α>
{
α value;
Tree<α> left;
Tree<α> right;
}
int height(Tree<α> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
これについて簡単に説明させてください。定義しています<！>＃8230;
-
バイナリツリーのノードを表す再帰型
Tree<α>。各ノードには、あるタイプのvalue<！>＃945; が格納され、同じタイプのオプションのleftおよびrightサブツリーへの参照があります。 -
リーフノードからルートノード
heightへの最も遠い距離を返す関数t。
今、t.valueの上記の擬似コードを適切なJava構文に変えましょう！ （オブジェクト指向やアクセシビリティ修飾子など、簡潔にするために定型句を省略し続けます。）2つの可能な解決策を示します。
1。ユニバーサルタイプのソリューション：
最も明らかな修正は、型パラメーター <！>＃945; をその署名に導入することにより、単に?汎用にすることです。
<α> int height(Tree<α> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
これにより、必要に応じて、変数を宣言し、その関数内で <！>＃945; 型の式を作成できます。しかし...
2。存在型ソリューション：
メソッドの本体を見ると、タイプ <！>＃945; のいずれにも実際にアクセスしたり操作したりしていないことがわかります。その型を持つ式も、その型で宣言された変数もありません...それでは、なぜObjectジェネリックにする必要があるのでしょうか？ <！>＃945; を単純に忘れられないのはなぜですか？結局のところ、次のことができます。
int height(Tree<?> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
この答えの冒頭で書いたように、実存型と普遍型は、本質的に補完的/二重です。したがって、ユニバーサルタイプソリューションが<=> よりジェネリックにすることである場合、実在型には逆の効果があることを期待する必要があります。タイプパラメータ <！>＃945; を削除します。
その結果、識別子がバインドされていないため、このメソッドで<=>の型を参照したり、その型の式を操作したりできなくなります。 （<=>ワイルドカードは特別なトークンであり、 <！> quot; captures <！> quot; a type。）<=>は事実上不透明になりました。おそらくあなたがそれでまだできる唯一のことは、<=>に型キャストすることです。
概要：
===========================================================
| universally existentially
| quantified type quantified type
---------------------+-------------------------------------
calling method |
needs to know | yes no
the type argument |
---------------------+-------------------------------------
called method |
can use / refer to | yes no
the type argument |
=====================+=====================================
これらはすべて良い例ですが、少し違った答えをすることにしました。 <！>＃8704; xであることを数学から思い出してください。 P（x）は<！> quot;を意味し、すべてのxについて、P（x）<！> quot;であることを証明できます。言い換えれば、それは一種の関数であり、あなたは私にxを与え、あなたのためにそれを証明する方法を持っています。
型理論では、証明についてではなく、型について述べています。したがって、このスペースでは<！> quot;を指定します。X型については、特定のP <！> quot;型を指定します。さて、Pが型であるという事実以外にPにXに関する多くの情報を与えないので、PはXでそれを行うことができませんが、いくつかの例があります。 Pは、<！> quot;同じタイプのすべてのペア<！> quot ;: P<X> = Pair<X, X> = (X, X)のタイプを作成できます。または、オプションタイプP<X> = Option<X> = X | Nilを作成できます。ここで、NilはNULLポインターのタイプです。リストを作成できます：List<X> = (X, List<X>) | Nil。最後の要素は再帰的であり、List<X>の値は、最初の要素がXで2番目の要素が∃X.P<X>であるペア、またはNULLポインタであることに注意してください。
今、数学で<！>＃8707; x。 P（x）は<！> quot;を意味します。P（x）がtrue <！> quot;であるような特定のxがあることを証明できます。このようなxは多数あるかもしれませんが、それを証明するには1つで十分です。別の考え方として、空ではない証拠と証明のペア{（x、P（x））}のセットが存在する必要があるということです。
型理論への翻訳：ファミリP<X>の型は、型Xと対応する型<=>です。 XをPに渡す前に（Xについてはすべて知っていたが、Pについてはほとんど知らなかったように）、今ではその反対が成り立っていることに注意してください。 <=>は、Xについての情報を提供することを約束しません。Xが存在すること、そしてそれが実際に型であるということだけです。
これはどのように役立ちますか？ Pは、内部型Xを公開する方法を持つ型です。例としては、状態Xの内部表現を隠すオブジェクトがあります。それを直接操作する方法はありませんが、このタイプの実装は多数存在する可能性がありますが、選択された特定のタイプに関係なく、これらのタイプをすべて使用できます。
存在型は不透明型です。
Unixのファイルハンドルを考えてください。その型はintであることがわかっているので、簡単に偽造できます。たとえば、ハンドル43から読み取ろうとすることができます。プログラムがこの特定のハンドルで開かれたファイルを持っている場合は、読み取ります。コードは悪意がある必要はなく、単にずさんなだけです（たとえば、ハンドルが初期化されていない変数である可能性があります）。
存在タイプはプログラムから隠されています。 fopenが存在タイプを返した場合、この存在タイプを受け入れるいくつかのライブラリ関数でそれを使用するだけで済みます。たとえば、次の擬似コードはコンパイルされます。
let exfile = fopen("foo.txt"); // No type for exfile!
read(exfile, buf, size);
インターフェース<！> quot; read <！> quot;次のように宣言されています：
次のようなタイプTが存在します。
size_t read(T exfile, char* buf, size_t size);
変数exfileはintではなく、char*ではなく、構造体File <！>＃8212;型システムで表現できるものではありません。型が不明な変数を宣言することはできず、たとえば、その不明な型にポインターをキャストすることはできません。言語はあなたを許可しません。
質問に直接回答するには：
ユニバーサルタイプでは、Tの使用にはタイプパラメーターXを含める必要があります。たとえば、T<String>またはT<Integer>。存在タイプの場合、T<?>の使用は、不明または無関係であるため、そのタイプパラメーターを含めないでください。単にMyClass（またはJava ?）を使用してください。
詳細情報：
ユニバーサル/抽象型と実存型は、オブジェクト/関数のコンシューマ/クライアントとそのプロデューサ/実装の間の視点の二重性です。一方がユニバーサルタイプを見ると、もう一方は実存タイプを見ることになります。
Javaでは、ジェネリッククラスを定義できます。
public class MyClass<T> {
// T is existential in here
T whatever;
public MyClass(T w) { this.whatever = w; }
public static MyClass<?> secretMessage() { return new MyClass("bazzlebleeb"); }
}
// T is universal from out here
MyClass<String> mc1 = new MyClass("foo");
MyClass<Integer> mc2 = new MyClass(123);
MyClass<?> mc3 = MyClass.secretMessage();
-
MyClass<?>のクライアントの観点からすると、secretMessage()は普遍的です。これは、そのクラスを使用するときにObjectを任意の型に置き換えることができ、Tの実際の型を知る必要があるためですT<Int>のインスタンスを使用するときはいつでも
-
T<Long>自体のインスタンスメソッドの観点から見ると、<=>は実際のタイプの<=> を知らないため、存在しています。
- Javaでは、<=>は存在タイプを表します。したがって、クラス内では、<=>は基本的に<=>です。 <=>のインスタンスで<=>のインスタンスを処理する場合は、上記の<=>の例のように<=>を宣言できます。
別の場所で説明したように、実在型は何かの実装の詳細を隠すために時々使用されます。これのJavaバージョンは次のようになります。
public class ToDraw<T> {
T obj;
Function<Pair<T,Graphics>, Void> draw;
ToDraw(T obj, Function<Pair<T,Graphics>, Void>
static void draw(ToDraw<?> d, Graphics g) { d.draw.apply(new Pair(d.obj, g)); }
}
// Now you can put these in a list and draw them like so:
List<ToDraw<?>> drawList = ... ;
for(td in drawList) ToDraw.draw(td);
これを適切にキャプチャするのは少しトリッキーです。なぜなら、私はある種の関数型プログラミング言語のふりをしているからです。しかし、ここでのポイントは、ある種の状態とその状態で動作する関数のリストをキャプチャしていることであり、状態部分の実際のタイプはわかりませんが、関数はすでにそのタイプと一致しているためです。
現在、Javaでは、すべての非最終非プリミティブ型は部分的に存在しています。これは奇妙に聞こえるかもしれませんが、<=>として宣言された変数は潜在的に<=>のサブクラスになる可能性があるため、特定の型を宣言することはできません。<！> quot;この型またはサブクラス<！> quot;のみです。そのため、オブジェクトは、状態のビットと、その状態で動作する関数のリストとして表されます。どの関数を呼び出すかは、実行時にルックアップによって決定されます。これは、上記の存在タイプを使用して、存在状態部分とその状態で動作する関数を使用することに非常に似ています。
サブタイピングとキャストのない静的に型付けされたプログラミング言語では、存在型により、異なる型付けされたオブジェクトのリストを管理できます。 <=>のリストに<=>を含めることはできません。ただし、<=>のリストにはさまざまな<=>を含めることができ、多くの異なるタイプのデータをリストに入れて、それらをすべてintに変換することができます（またはデータ構造内で提供される操作を実行します） 。
クロージャを使用せずに、ほとんどの場合、実在型のレコードをレコードに変換できます。クロージャーも実在的に型付けされており、クロージャーが閉じられた自由変数は呼び出し元から隠されています。したがって、存在型ではなくクロージャーをサポートする言語を使用すると、オブジェクトの存在部分に入れたのと同じ隠し状態を共有するクロージャーを作成できます。
I <！>＃8217;少し遅れているようですが、とにかく、このドキュメントは存在タイプとは別の見方を追加します。具体的には言語に依存しませんが、存在タイプを理解するのはかなり簡単です：< a href = "http://www.cs.uu.nl/groups/ST/Projects/ehc/ehc-book.pdf" rel = "noreferrer"> http://www.cs.uu.nl/groups/ ST / Projects / ehc / ehc-book.pdf （第8章）
普遍的と実存的に数量化されたタイプの違いは、次の観察によって特徴付けられます：
<！>＃8704を持つ値の使用。限定型は、限定型変数のインスタンス化のために選択する型を決定します。たとえば、ID関数<！>＃8220; id :: <！>＃8704; a.a <！>＃8594;の呼び出し元a <！>＃8221; idのこの特定のアプリケーションのタイプ変数aに選択するタイプを決定します。関数アプリケーションの場合<！>＃8220; id 3 <！>＃8221;この型はIntと同じです。
<！>＃8707を使用した値の作成。数量化タイプは、数量化タイプ変数のタイプを決定し、非表示にします。たとえば、<！>＃8220; <！>＃8707; a。（a、<！>＃8594; Int）<！>＃8221; <！>＃8220;（3、<！>＃955; x <！>＃8594; x）<！>＃8221 ;;からそのタイプの値を構築した可能性があります。別の作成者が<！>＃8220;（<！>＃8217; x <！>＃8217 ;, <！>＃955; x <！>＃8594; ord x）<！ >＃8221 ;.ユーザーの観点からは、両方の値は同じタイプであるため、交換可能です。値には、型変数aに選択された特定の型がありますが、どの型かわからないため、この情報を利用することはできません。この値固有のタイプ情報は<！>＃8216; forgotten <！>＃8217 ;;存在することだけがわかっています。
タイプパラメータのすべての値にユニバーサルタイプが存在します。存在タイプは、存在タイプの制約を満たすタイプパラメータの値に対してのみ存在します。
たとえば、Scalaで存在型を表現する1つの方法は、いくつかの上限または下限に制約される抽象型です。
trait Existential {
type Parameter <: Interface
}
同様に、制約付きユニバーサルタイプは、次の例のように存在タイプです。
trait Existential[Parameter <: Interface]
インスタンス化可能なサブタイプはすべてInterfaceを実装する必要があるExistentialを定義する必要があるため、どの使用サイトでもtype Parameterを使用できます。
A Scalaの実在型の縮退ケースは、参照されることのない抽象型であるため、参照する必要はありません。任意のサブタイプによって定義されます。これには、ScalaのList[_] という短縮表記が効果的にあります。 およびJavaのList<?>。
私の答えは、Martin Oderskyの統一する提案に触発されました>抽象型および実存型。 付属スライド理解を助けます。
抽象データ型と情報隠蔽の研究により、実在型がプログラミング言語に導入されました。データ型を抽象化すると、その型に関する情報が隠されるため、その型のクライアントはそれを悪用できません。オブジェクトへの参照を持っているとしましょう。一部の言語では、その参照をバイトへの参照にキャストし、そのメモリに任意の操作を行うことができます。プログラムの動作を保証するために、オブジェクトのデザイナが提供するメソッドを介してのみオブジェクトへの参照に基づいて行動するように強制することは、言語にとって有用です。タイプは存在しますが、それ以上はありません。
参照：
抽象型には実在型、MITCHEL <！> amp;があります。 PLOTKIN
http://theory.stanford.edu/~jcm /papers/mitch-plotkin-88.pdf
この図を作成しました。厳密かどうかはわかりません。しかし、それが助けになれば嬉しいです。
私が理解しているように、それはインターフェース/抽象クラスを記述する数学的な方法です。
T = <！>＃8707; X {X a; int f（X）; }
C＃の場合、一般的な抽象型に変換されます。
abstract class MyType<T>{
private T a;
public abstract int f(T x);
}
<！> quot; Existential <！> quot;ここで定義されたルールに従うタイプがあることを意味します。
