为什么要学习Haskell？

问一个为什么？问题意味着我们想被告知一个原因。但是我们会接受任何理由吗？似乎没有，因为如果有足够的答案，那么答案就无关紧要了，那为什么还要打扰呢？

因此，我们问题的答案应该是一个很好的理由。但是什么是善良理由？

黄金标准是合乎逻辑的原因。即，答案应从可接受的前提开始，对它们应用一般规则，并得出结论。

前两个是我们理所当然的前提。但是，似乎还有其他事情是我们理所当然的。因此，魔术以某种方式产生结论。

这有待进一步研究。听起来相似，因此所有凡人都是苏格拉底。感觉不对。必须有一条隐藏的规则来规定我们可以从这两个前提中得出的结论。

似乎我们暗含了以下内容：假设Y表示Z；而Y表示Z。那么如果Ximplies Y，我们推导X隐含Z。让我们将此规则点称为“点”，并将其写为：

（-＆gt;）符号表示＆＃34;暗含＆＃34 ;，按照惯例，它与右相关联，即-> b-＆gt; c表示-＆gt; （b-> c）。因此，我们省略一些括号：

我们的符号对于确定我们是否进行逻辑推理至关重要。我们没有隐藏潜在的问题细节，而是明确指出了我们所使用的逻辑规则。 换句话说，我们应该在比赛之前就游戏规则达成一致，并且在比赛中，我们应该清楚哪些规则允许我们移动。 在此，x和y代表任意前提，例如Man-＆gt;。 凡人，或（（苏格拉底-> a->柏拉图-> b）->（柏拉图-> c））->凡人， （d-> Socrates）。 在上面的示例中，我们将x，y，z设为Socrates，Man和Mortal，因此适用点规则。 按照惯例，应用程序关联到左侧，因此我们可以用f g h代替（f g）h。 因此点p q实际上是一个两步过程，将y和z设置为Man and Mortal就足以得到点p： 如果X为true，则Y为true，X仍然为true。 我们将此常量称为： 如果X表示Y表示Z，则X表示Y，那么我们必须具有X表示Z。 我们称此为ap：

ap ::（x-＆gt; y-＆gt; z）-＆gt; （x-＆gt; y）-＆gt; x-＆gt; ž 看来我们可以继续制定合理的规则。 在极端情况下，我们可以针对每一个＆＃34;因此想到一个规则。 这将使逻辑缺乏说服力。 另一种选择是遵循我们认为理所当然的一小部分合理公理，从中我们推导出所有其他逻辑规则。 我们该如何设置？ 再一次，我们的符号拯救了我们。 取x，y，z为a，b-> 在ap规则中，我们得出： 也就是说，id规则是多余的，因为它由ap和const隐含。点规则同样是多余的。 经过适当的替换，我们发现： ap（const ap）const ::（y-> z）-＆gt; （x-＆gt; y）-＆gt; x-＆gt; ž 概括地说，这导致了希尔伯特系统，该系统根据ap和const公理构建了任何合理的逻辑规则。 [更准确地说，这些规则处理命题逻辑的直觉片段。]

我们从一个“为什么”开始。问题。然后，为了确定对我们问题的答案是否令人满意，我们开发了一种表示法，该表示法实际上是纯正的Haskell。

碰巧的是，计算机也可以解释Haskell，因此我们可以邀请theiraid检查逻辑参数的有效性。这是非常宝贵的实践，因为人类不善于遵循挑剔的规则。

在翻译“所有人都是凡人”时，我们可能已经过分简化了。和“敬畏一个人”符合我们的想法，但是从小处开始是很好的。如果我们无法处理简化版本，该如何处理真实交易？

＆gt;导入Control.Monad＆gt;点= ap（const ap）const＆gt; ：t dotdot ::（a-＆gt; b1）-＆gt; （b2-→a）-＆gt; b2-＆gt; b1＆gt;数据Socrates = Socrates＆gt;数据Man ＝ Man＆gt;数据Mortal = Mortal＆gt; p Man = Mortal＆gt; q苏格拉底=人＆gt; ：t点p qdot p q ::苏格拉底->凡人

点函数实际上应该是（。），但我想避免讨论Haskell的中缀运算符。这也是为什么我选择ap而不是（＆lt; *））的原因。

给定类似ap const const的表达式，我们如何知道它是否有意义？一种？ Hindley-Milnertype推论确定是否可以进行这种替换，如果可以，则返回最通用的解决方案。

我们已经忽略了不便的事实。 Haskell是不可靠的，因为例如undefined是任何命题的证明。但是，如果您知道这一点，那么您已经知道太多了，不用再去阅读本文了！

我们可以轻松地在Haskell中扩展逻辑，我们可以使用Left Right进行逻辑析取，可以使用（，）fst snd进行逻辑合取，也可以使用Data.Void类型进行逻辑取反。 的故事。 通过将Peano的公理添加到逻辑中，我们可以证明许多数学定理。这在Haskell中可以通过语言扩展来实现，但是其他语言（例如Coq，Agda和Idris）则更好。 本林恩[email protected]💡