确保我使用的功能在Haskell中返回正确的值。 （IE不包含“错误”``或类似）
Haskell经常被吹捧为要进行证明的语言。（在开始推荐Agda，Idris或Coq之前）。 但是，这条代码不是潜在的问题还是我理解错误的概念？
x :: Int -> Int
x n
| x == 0 = error "Error"
| otherwise = n + 1
据我所知，这对于检查证明不是很好（因为返回int不是强制性的。）
据我了解， 有什么方法可以解决此问题吗？我不明白如何。 仅仅是因为该语言提供的更严格的类型系统或其他一些保证
？
Haskell is often touted as the language to do proofs in. (Before they start recomnding Agda, Idris or Coq).
However, is this piece of code not potentially problematic or am I understanding the concept wrong?
x :: Int -> Int
x n
| x == 0 = error "Error"
| otherwise = n + 1
As far as I understand this is not very good for checking proofs(since returning Int is not mandatory here.)
Is there a way we could solve this?
As far as I understand, the other aforementioned languages avoid this.[1] I do not understand how. Is it simply because of the stricter type-system or some other guarantee provided by the language?
So far I have looked at the language documentations at a high level but found nothing.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
如果有人建议您在Haskell 中的证明中索要您的钱。 （但是，请务必对您理解。也许他们说要做有关Haskell 的证据，并且您的内存不好！）
您是正确的：对于检查证明，这不是很好。 Haskell作为逻辑是不一致的。这意味着您可以证明任何东西。我不时想到的另一个智能哈斯克勒的报价。我找不到确切的措辞，但它类似于“程序员都是逻辑学家，他们所有时间都以过于复杂的方式证明了微不足道的定理”。这只是另一个例子。一位真正的逻辑学家一旦发现不一致，他们就会停止尝试证明其他事情，因为他们已经完成了一切。
您提到的语言（COQ，AGDA和IDRIS）不仅需要证明您要证明的东西的证明，还可以证明您编写的证明最终评估了。 （大多数情况下，第二个证明是通过限制您可以编写的证明类的隐式强制执行的，但是人们一直在扩展始终通过自动检查的证明类别。）一旦您要求终止，就不再可以实现<代码。 > error :: string-＆gt; 首先。 （当然，除非是编译器原始的……所以他们只是不这样做。）
If somebody recommended that you do in proofs in Haskell, ask for your money back. (But be sure to double check you understood. Maybe they said to do proofs about Haskell and your memory is bad!)
You are correct: it is not very good for checking proofs. Haskell is, as a logic, inconsistent. That means you can prove anything. There's a quote from another smart Haskeller that I think of from time to time; I can't find the exact wording, but it goes something like "programmers are logicians that spend all their time proving trivial theorems in overly complicated ways". This is just another example of that; a real logician, once they found an inconsistency, would stop trying to prove other things because they've already finished proving everything.
The languages you mention (Coq, Agda, and Idris) get around this problem by requiring not just a proof of the thing you want to prove, but also a proof that the proof you wrote finishes evaluating eventually. (Mostly that second proof is implicitly enforced by restricting the class of proofs you can write, but people are extending the class of proofs that pass the automatic checks all the time.) Once you demand termination, it is no longer possible to implement
error :: String -> ain the first place. (Except as a compiler primitive, of course... so they just don't do that.)