确保我使用的函数在 haskell 中返回正确类型的值。（即不包含`错误“”`或类似内容）

Question

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

Answer 1

如果有人建议您使用Haskell进行校样，请要求退款。（但一定要仔细检查你是否理解了。也许他们说要做关于 Haskell 的证明，而你的记忆力很差！）

你是对的：它不太适合检查校样。从逻辑上看，Haskell 是不一致的。这意味着你可以证明任何事情。我时常想起另一位聪明的 Haskeller 的一句话：我找不到确切的措辞，但它的意思是“程序员是逻辑学家，他们把所有的时间都花在以过于复杂的方式证明琐碎的定理上”。这只是另一个例子；一个真正的逻辑学家，一旦发现不一致，就会停止尝试证明其他事情，因为他们已经证明了一切。

你提到的语言（Coq、Agda 和 Idris）解决了这个问题，不仅需要你想要证明的事情的证明，还需要你编写的证明最终完成评估的证明。（大多数情况下，第二个证明是通过限制您可以编写的证明类别来隐式强制执行的，但是人们一直在扩展通过自动检查的证明类别。）一旦您要求终止，就不再可能error :: String -> a在第一名。（当然，除了作为编译器原语......所以他们只是不这样做。）