我通讀了Wikipedia文章存在類型。我發現由于存在運算符（?），它們被稱為存在類型。不過，我不確定它的意義是什么。之間有什么區別T = ?X { X a; int f(X); }和T = ?x { X a; int f(X); }？
3 回答
慕神8447489
TA貢獻1780條經驗 獲得超1個贊
存在類型的值，例如，?x. F(x) 是包含某種類型 x和該類型的值的一對F(x)。而like多態類型的值?x. F(x)是一個具有某種類型并產生 type值的函數。在這兩種情況下，類型都會關閉某個類型構造器。xF(x)F
請注意，此視圖混合了類型和值。存在證明是一種類型和一種價值。通用證明是按類型（或從類型到值的映射）索引的整個值系列。
因此，您指定的兩種類型之間的區別如下：
T = ?X { X a; int f(X); }
這意味著：類型的值T包含一個稱為的類型X，一個值a:X和一個函數f:X->int。類型值的生產者T可以選擇任何類型，X消費者對此一無所知X。除了調用它的一個示例，a并且可以通過將其int賦予來將其轉換為一個值f。換句話說，類型的值T知道如何產生int某種方式。好吧，我們可以消除中間類型，X而只是說：
T = int
普遍量化的數字有些不同。
T = ?X { X a; int f(X); }
這意味著：類型的值T可以給出任何類型的X，它會產生一個值a:X，和功能f:X->int 不管是什么X是。換句話說：類型值的使用者T可以為選擇任何類型X。類型值的產生者T一無所知X，但是它必須能夠a為任何選擇產生一個值X，并能夠將這樣的值轉化為一個值int。
顯然，實現這種類型是不可能的，因為沒有程序可以產生每種可以想象的類型的值。除非您允許荒謬之類的話null。
由于一個存在性參數是一對，因此可以通過currying將一個存在性參數轉換為通用參數。
(?b. F(b)) -> Int
是相同的：
?b. (F(b) -> Int)
前者是2級生存者。這導致以下有用的屬性：
等級的每個存在量化類型都是等級n+1普遍量化類型n。
有一種標準的算法可以將存在物轉換為通用物，稱為Skolemization。
繁花如伊
TA貢獻2012條經驗 獲得超12個贊
我認為將存在性類型與通用類型一起解釋是有意義的，因為這兩個概念是互補的，即一個概念與另一個概念“相對”。
我無法回答有關存在性類型的每一個細節（例如給出確切的定義，列出所有可能的用途，它們與抽象數據類型的關系等），因為我對此沒有足夠的了解。我將僅演示（使用Java）HaskellWiki文章聲明存在類型的主要作用：
存在類型可以用于多種不同目的。但是他們要做的是在右側“隱藏”一個類型變量。通常，出現在右側的任何類型變量也必須出現在左側[…]
設置示例：
以下偽代碼不是完全有效的Java，即使很容易修復它也是如此。實際上，這正是我要在此答案中執行的操作！
class Tree<α>
{
α value;
Tree<α> left;
Tree<α> right;
}
int height(Tree<α> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
讓我為您簡要說明一下。我們正在定義...
Tree<α>表示二叉樹中的節點的遞歸類型。每個節點存儲value某種類型的α，并引用相同類型的可選樹left和right子樹。
該函數height返回從任何葉節點到根節點的最遠距離t。
現在，讓我們將上面的偽代碼height轉換為正確的Java語法?。楹啙嵠鹨姡覍⒗^續省略一些樣板，例如面向對象和可訪問性修飾符。）我將展示兩種可能的解決方案。
1.通用型解決方案：
最明顯的解決方法是height通過將類型參數α引入其簽名來簡單地實現泛型：
<α> int height(Tree<α> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
如果需要，這將允許您聲明變量并在該函數內創建類型為α的表達式。但...
2.現有類型解決方案：
如果查看我們方法的主體，您會注意到我們實際上并沒有訪問或使用α類型的任何東西！沒有那種類型的表達式，也沒有用那種類型聲明的變量……那么，為什么我們必須使height泛型成為根本呢？為什么我們不能簡單地忘記α？事實證明，我們可以：
int height(Tree<?> t)
{
return (t != null) ? 1 + max( height(t.left), height(t.right) )
: 0;
}
正如我在回答之初所寫的那樣，存在和通用類型本質上是互補/雙重的。因此，如果通用類型的解決方案要使通用性height 更高，那么我們應該期望存在性類型具有相反的效果：使其不通用，即通過隱藏/刪除類型參數α。
結果，您將無法再引用t.value此方法的類型，也不能操作該類型的任何表達式，因為沒有標識符綁定到該方法。（?通配符是一個特殊的令牌，而不是“捕獲”類型的標識符。）t.value實際上已經變得不透明了；也許您唯一仍能做的就是將其類型轉換為Object。
摘要：
===========================================================
| 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 |
- 3 回答
- 0 關注
- 593 瀏覽
添加回答
舉報
0/150
提交
取消