什麼是底部類型？

在維基百科中，bottom type被簡單地定義爲「沒有值的類型」。但是，如果b是這種空白類型，那麼產品類型(b,b)也沒有值，但似乎與b不同。我同意底部是無人居住的，但我不認爲這個屬性足以定義它。什麼是底部類型？

通過Curry-Howard correspondence，底部與數學錯誤相關聯。現在有一個邏輯原則，說明False遵循任何命題。通過庫裏霍華德，這意味着類型forall a. bottom -> a是有人居住，即存在一個功能家庭f :: forall a. bottom -> a。

這些功能是什麼f？他們是否幫助定義底部，也許是所有類型的無限產品forall a. a？

2017-03-06 V. Semeria

在數學

底部是不具有值的類型。那就是：任何空的類型都可以起到底層作用。

那些f :: forall a . Bottom -> a功能是空的功能。在設定的函數的理論定義中「空」。

在編程

一個致力打造混凝土空類型有它作爲由編程語言基礎庫底部是爲了方便。每個人使用與底部相同的空白類型的代碼益處的可讀性和兼容性。

在Haskell

讓我們稱他們與更友好的名稱「底」 - > 「太虛」，「F」 - > 「荒謬的」。

{-# LANGUAGE EmptyDataDecls #-} 
data Void

此定義不包含任何構造函數=>它的一個實例不能被創建=>它是空的。

absurd :: Bottom -> a 
absurd = \ case {}

在案件表達式中，我們不必處理任何案件，因爲沒有任何案件。

2017-03-06 20:44:03 libeako

我在命題演算中看到3種公式。 1）重言式，在Heyting代數的每一種解釋中都是真實的。 2）否定是重言式的公式，在Heyting的每一種解釋中都是錯誤的。 3）數值取決於解釋的公式。由庫裏霍華德案例2和3都對應於空的類型。但是我認爲案例2應該在空白類型中單獨列出：只有那些類型應該被稱爲底部。 –

回答