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
1条答案
按热度按时间pgccezyw1#
如果有人建议你在Haskell* 做校样，要求退钱。（但是一定要仔细检查你是否理解。也许他们说做关于Haskell* 的校样，而你的记忆力很差！）
您是正确的：它不太适合检查证明。作为一个逻辑，Haskell是不一致的。这意味着你可以证明任何事情。我不时想起另一个聪明的Haskell的一句话;我找不到确切的措辞，但它是这样的：“程序员是逻辑学家，他们把所有的时间都花在用过于复杂的方法证明琐碎的定理上”。一个真实的的逻辑学家，一旦他们发现了不一致，就会停止试图证明其他的东西，因为他们已经证明完了一切。
你提到的语言（Coq、Agda和Idris）通过不仅要求你要证明的东西的证明，而且要求你写的证明最终完成求值的证明来绕过这个问题。（第二种证明通常是通过限制可以编写的证明类来隐含地实施的，但人们一直在扩展通过自动检查的证明类。）一旦你要求终止，首先就不可能实现
error :: String -> a了。（当然，除了作为编译器原语之外......所以他们不这样做。）