理解 '不可能'

Question

Type-Driven Development with Idris禮物：

twoPlusTwoNotFive : 2 + 2 = 5 -> Void 
twoPlusTwoNotFive Refl impossible 

是對函數或值之上？如果它是前者，那麼爲什麼沒有可變參數，例如

add1 : Int -> Int 
add1 x = x + 1 

特別，我在twoPlusTwoNotFive缺乏=困惑。

Answer 1

impossible調出參數的組合，這是不可能的。在案件不可能的情況下，伊德里斯免除了您提供右手邊的責任。

在這個例子中，我們正在編寫一個(2 + 2 = 5) -> Void類型的函數。 Void是一種沒有價值的類型，所以如果我們成功地實現了這樣一個功能，我們應該期望它的所有情況都變成不可能的。現在，=只有一個構造函數（Refl : x = x），因此它在此處不能使用，因爲它需要=的參數在定義上相同 - 它們必須是纔是相同的x。所以，自然是impossible。任何人都不可能在運行時成功調用這個函數，並且我們可以從證明某些不真實的東西中得到保存，這將是一個相當大的問題。

這是另一個例子：你不能索引到一個空的向量。仔細檢查Vect並發現它是[]告訴我們，n ~ Z;因爲Fin n是小於n的自然數類型，調用者可以使用它來填充第二個參數。

at : Vect n a -> Fin n -> a 
at [] FZ impossible 
at [] (FS i) impossible 
at (x::xs) FZ = x 
at (x::xs) (FS i) = at xs i 

大部分時間你都可以完全忽略不可能的情況。

我對Agda的符號稍微偏愛相同的概念，它使用符號()明確指出輸入表達式的哪一位是不可能的。

twoPlusTwoNotFive : (2 + 2 ≡ 5) -> ⊥ 
twoPlusTwoNotFive() -- again, no RHS 

at : forall {n}{A : Set} -> Vec A n -> Fin n -> A 
at []() 
at (x ∷ xs) zero = x 
at (x ∷ xs) (suc i) = at xs i 

我喜歡它，因爲有時你只瞭解到的情況下做一些進一步的圖案參數匹配後，不可能的;當不可能的東西被埋沒幾層時，很高興有一個視覺幫助來幫助你發現它在哪裏。