爲什麼非詳盡的衛兵造成無可辯駁的模式匹配失敗？

Question

我有這個功能在Haskell：

test :: (Eq a) => a -> a -> Maybe a 
test a b 
    | a == b = Just a 
test _ _ = Nothing 

這是我當我試圖用不同的輸入功能：

ghci>test 3 4 
Nothing 
ghci>test 3 3 
Just 3 

根據真實世界哈斯克爾，第一模式是無可辯駁的。但似乎test 3 4不會失敗的第一種模式，並匹配第二種。我預計會出現某種錯誤 - 也許是「非窮舉的守衛」。那麼這裏究竟發生了什麼，有沒有辦法在發生這種意外情況時啓用編譯器警告？

Answer 1

第一個模式確實是一個「顛撲不破模式」，但是這並不意味着它將始終選擇相應的功能右側。它仍然受制於可能會失敗的守衛，就像你在例子中那樣。

爲了確保涵蓋所有的情況，通常使用otherwise來建立一個總是成功的最終後衛。

test :: (Eq a) => a -> a -> Maybe a 
test a b 
    | a == b = Just a 
    | otherwise = Nothing 

請注意，關於otherwise沒有什麼魔術。它在前奏中定義爲otherwise = True。然而，在最後一種情況下使用otherwise是慣用的。

在一般情況下，編譯器會警告有關非顯式警衛是不可能的，因爲它會涉及解決暫停問題，但是存在諸如Catch之類的工具，它們試圖比編譯器在確定是否全部工作方面做得更好案件被覆蓋或不在一般情況下。

Answer 2

衛兵不是無可辯駁的。但是，是很常見的（和好）的做法，以增加最後一個後衛是趕上其他情況，所以你的函數變爲：

test :: (Eq a) => a -> a -> Maybe a 
test a b 
    | a == b = Just a 
    | True = Nothing 

Answer 3

如果你忽略了第二個子句，也就是說，如果你的最後一個匹配有一組守衛，其中最後一個不是平凡真實的，那麼編譯器應該警告你。

一般來說，測試警衛的完整性顯然是不可能的，因爲它會像解決暫停問題一樣困難。

答案馬特的評論：

看一下例子：

foo a b 
    | a <= b = True 
    | a > b = False 

一個人可以看到，無論後衛之一必須是真實的。但編譯器不知道a <= b或a > b。

現在看看另一個例子：

fermat a b c n 
    | a^n + b^n /= c^n = .... 
    | n < 0 = undefined 
    | n < 3 = .... 

爲了證明這組警衛齊全，編譯器必須證明費爾馬大定理。在編譯器中做這件事是不可能的。請記住，警衛的數量和複雜程度不受限制。編譯器必須是解決數學問題的一般解決方案，這是Haskell本身所陳述的問題。

更正式地，以最簡單的情況：

f x | p x = y 

編譯器必須證明，如果p x是不是底部，然後p x是True所有可能的X。換句話說，無論x是或者評估爲True，它都必須證明p x是底部（不停止）。