荒謬功能的反轉

Question

是否有與Data.Void的absurd功能相反？

如果存在，它是如何實現的以及它用於什麼？

Answer 1

此功能不存在。（假設有嚴格的語義）

查看類型的代數，函數類型等價於指數運算。

現在功能absurd，其類型Void -> a對應的操作a^0等於1。這意味着只有一個absurd的實現，可以在Data.Void中找到。

反向的箭頭，你得到的類型a -> Void，相當於0^a或0，這意味着所需的功能不存在。

---

你也可以用庫裏霍華德同構證明這一點。由於函數類型對應於布爾函數「暗示」，你會得到以下條件：

True -> False 

這是假的，因此沒有功能a -> Void可以存在。

由於我剛剛開始學習類別理論，所以鼓勵由於語言不準確而引起的更正。

Answer 2

這取決於你的意思。 absurd證人同構Void = forall a.a的一側，並且從這一觀點，具有逆

void :: (forall a.a) -> Void 
void x = x 

這確實是一個同構。

有類型

forall a.a -> Void 

也沒有任何逆absurd與該類型的部分功能當中的無總功能。

Answer 3

很直觀，該功能不可能存在^†。假設我們有這樣一個功能：

drusba :: a -> Void 

那麼你可以做

GHCi> drusba (5 :: Int) 

...從而創造Void類型的值。 Well, that's exciting... also, congratulations, you're dead!

Hask（Haskell的類型類別，與Haskell函數作爲態射）是一種與bicartesian closed categoryinitial objectVoid。初始對象的定義是，對於任何類型的A，都只有一個函數Void -> A - 這些函數是absurd :: Void -> a的實例。此外，由於()是終端對象，因此只有一個功能B ->() - 任何此類功能都等同於​​。

現在，假設drusba ::() -> Void，我們將有

drusba . absurd :: Void -> Void 
drusba . absurd ≡ id 

，因爲只能有一個功能Void -> Void，我們知道id是一個;和

absurd . drusba ::() ->() 
absurd . drusba ≡ id 

出於同樣的原因。 IOW，drusba和absurd確實是相互顛倒的，這意味着()和Void是同構的。

但從這一點，將遵循任何類型A實際上是同構的兩個()和Void，因爲將有一個準確的功能() -> A和A ->()存在。所以基本上，如果存在函數drusba :: a -> Void，這意味着Haskell只有一個類型，它不包含任何值。那不會是一個特別有用的編程語言，會嗎？

---

^†_{當然，這一切只有當你不顧⊥成立。}