所以，在我不斷嘗試通過小哈斯克爾練習半懂咖喱霍華德，我已經得到停留在這一點上： {-# LANGUAGE GADTs #-}
import Data.Void
type Not a = a -> Void
-- | The type of type equality proofs, which can only be instantiated if a = b.
data Equal
> {-# LANGUAGE RankNTypes #-}
我想知道是否有方法來表示haskell和/或其他函數式編程語言中的選擇公理。 正如我們所知，false由沒有值的類型表示（haskell中的Void）。 > import Data.Void
我們可以代表像這樣 > type Not a = a -> Void
我們可以表達排中律的類型a就像否定因此 > type LEM a
在維基百科中，bottom type被簡單地定義爲「沒有值的類型」。但是，如果b是這種空白類型，那麼產品類型(b,b)也沒有值，但似乎與b不同。我同意底部是無人居住的，但我不認爲這個屬性足以定義它。 通過Curry-Howard correspondence，底部與數學錯誤相關聯。現在有一個邏輯原則，說明False遵循任何命題。通過庫裏霍華德，這意味着類型forall a. bottom -> a
前一段時間我讀的功能類型a -> b對應關係a ≤ b，或者它是a ≥ b？這對我來說很有意義，因爲如果我們在它們之間有雙射（即(a ≈ b) ≡ (a -> b, b -> a)），那麼兩種類型是同構的。同樣，(a = b) ≡ (a ≤ b) ∧ (a ≥ b)。我知道這不是庫裏霍華德蘭貝克的對應關係（即類型理論，邏輯和範疇理論之間的對應關係）。這是類型理論和別的東西之間的對應關係。我想知道更