Haskell 經常被吹捧為用來做證明的語言。（在他們開始推薦 Agda、Idris 或 Coq 之前）。但是，這段代碼是否沒有潛在的問題，或者我對這個概念的理解是錯誤的？
x :: Int -> Int
x n
| x == 0 = error "Error"
| otherwise = n 1
據我了解，這對于檢查證明不是很好（因為Int這里不強制回傳。）
有沒有辦法解決這個問題？
據我了解，其他上述語言避免了這種情況。 [1] 我不明白怎么做。僅僅是因為更嚴格的型別系統還是語言提供的其他保證？
到目前為止，我已經從高層次上查看了語言檔案，但一無所獲。
[1] = https://www.reddit.com/r/haskell/comments/9toh6b/comment/e8y4gzi/?utm_source=share&utm_medium=web2x&context=3
uj5u.com熱心網友回復：
如果有人建議您在 Haskell中做證明，請要求退款。（但請務必仔細檢查您是否理解。也許他們說要對 Haskell進行證明，而您的記憶力很差！）
你是對的：它不適合檢查證明。從邏輯上講，Haskell 是不一致的。這意味著你可以證明任何事情。我時不時想起另一位聰明的 Haskeller 的話；我找不到確切的措辭，但它類似于“程式員是邏輯學家，他們將所有時間都花在以過于復雜的方式證明微不足道的定理上”。這只是另一個例子；真正的邏輯學家一旦發現不一致，就會停止嘗試證明其他事情，因為他們已經完成了所有事情的證明。
您提到的語言（Coq、Agda 和 Idris）解決了這個問題，不僅需要證明您要證明的事物，還需要證明您撰寫的證明最終完成評估。（大多數情況下，第二個證明是通過限制您可以撰寫的證明類別來隱式執行的，但是人們正在擴展始終通過自動檢查的證明類別。）一旦您要求終止，就不再可能error :: String -> a在第一名。（當然，除了作為編譯器原語......所以他們只是不這樣做。）
轉載請註明出處，本文鏈接：https://www.uj5u.com/qianduan/498430.html