GADT的失敗全面性檢查

Question

考慮下面的代碼：

data (:+:) f g a = Inl (f a) | Inr (g a) 

data A 
data B 

data Foo l where 
    Foo :: Foo A 

data Bar l where 
    Bar :: Bar B 

type Sig = Foo :+: Bar 

fun :: Sig B -> Int 
fun (Inr Bar) = 1 

即使樂趣是一個詳盡的比賽，與-Wall編譯時，GHC抱怨缺少的情況。但是，如果我添加另一個構造函數：

data (:+:) f g a = Inl (f a) | Inr (g a) 

data A 
data B 

data Foo l where 
    Foo :: Foo A 
    Baz :: Foo B 

data Bar l where 
    Bar :: Bar B 

type Sig = Foo :+: Bar 

fun :: Sig B -> Int 
fun (Inr Bar) = 1 
fun (Inl Baz) = 2 

然後GHC正確檢測樂趣是總。

我在我的工作中使用類似於此的代碼，並希望GHC在發生錯誤的情況下發出警告，如果沒有，則不會發出警告。爲什麼GHC會抱怨第一個程序，我怎樣才能在沒有警告的情況下編譯第一個樣本，而不添加虛假的構造函數或案例？

Answer 1

實際報告的問題是：

Warning: Pattern match(es) are non-exhaustive 
     In an equation for `fun': Patterns not matched: Inl _ 

這是真的。您爲構造函數Inr提供了一個例子，但不提供構造函數Inl。

什麼你希望的是，因爲沒有辦法提供一個使用Inl構造Sig B類型的值（它需要Foo B類型的參數，但對於Foo唯一的構造是Foo A型），即ghc會注意到你不需要處理構造函數Inl。

問題是由於底部每種類型都有人居住。有是值類型Sig B使用Inl構造函數;甚至還有非底值。他們必須底部包含，但他們不是自己底部。因此，該程序可能正在評估對fun的調用失敗;這是ghc警告的。

因此，要解決這個問題，你需要改變fun到這樣的事情：

fun :: Sig B -> Int 
fun (Inr Bar) = 1 
fun (Inl foo) = error "whoops" 

不過現在當然，如果你在以後添加Baz :: Foo B此功能是一個定時炸彈等待發生。對於ghc來說，的值得警惕，但是唯一能做到的方式是將foo與當前詳盡的一組模式進行匹配。不幸的是有是沒有有效的模式，你可以放在那裏！ foo已知爲類型Foo B，它只有底部居住，並且不能爲底部寫入圖案。

但是你可以將它傳遞給一個接受多態類型爲Foo a的參數的函數。然後該函數可以與所有當前存在的Foo構造函數相匹配，以便稍後添加一個構造函數時會收到警告。事情是這樣的：

fun :: Sig B -> Int 
fun (Inr Bar) = 1 
fun (Inl foo) = errorFoo foo 
    where 
     errorFoo :: Foo a -> b 
     errorFoo Foo = error "whoops" 

現在你已經妥善處理的:+:所有構造函數中fun，「不可能」的情況下簡單的錯誤了，如果曾經實際發生它，如果你曾經添加Baz :: Foo B你得到一條警告非詳盡模式errorFoo，這至少會指導您查看fun，因爲它在附件where中定義。

不利的一面，當你添加無關的構造函數來Foo（多說Foo A型的），你將有更多的情況下增加errorFoo，而這可能是unfun（雖然簡單，機械的），如果你有很多應用此模式的函數。

Answer 2

我很遺憾地告訴你，但你認爲這是你的第一個例子是不是很詳盡：

∀x. x ⊢ fun (Inl (undefined :: Foo B)) 
*** Exception: Test.hs:48:1-17: Non-exhaustive patterns in function fun 

惱人的，是的，但他們的休息時間。 ⊥是爲什麼我們不能擁有美好的事物。 ：[