问题标签 [curry-howard]

当我有一个“枚举”类型时，即一种代数数据类型，其中没有任何案例包含任何其他数据，我通常喜欢将解析器/打印机从映射到字符串中投影出来，以确保解析器和打印机保持不变在我更改代码时同步。例如，在伊德里斯：

我可能会按如下方式实现打印功能：

问题是，我不想在Maybe这里。我想保证在编译时我已经涵盖了所有的案例，就像我通过 case-splitting on 编写这个函数一样RPS，穷举检查器将启动并且我可以只拥有print : RPS -> string. 在伊德里斯，我知道如何用证明来恢复它（你不只是爱伊德里斯吗！）：

现在在我看来，这太棒了。我可以在我的代码中准确地声明一个枚举案例与其相关字符串之间的相关性是什么，并且我可以有一个print函数和一个parse函数都用它编写（parse这里省略了该函数，因为与问题无关，但实现起来很简单）。不仅如此，我还能够让类型检查器相信print : RPS -> String我想要的签名不是伪造的，并且避免了使用任何偏函数！这就是我喜欢的工作方式。

但是在工作中，我的大部分代码都在 F# 中，而不是在 Idris 中，所以我最终要做的是使用 FsCheck 来通过基于属性的测试来准证明穷举性。这还不算太糟糕，但是

1. 基于属性的测试不与StrMap;搭配使用。它在不同的程序集中。我喜欢尽可能地将我的不变量与它们所指的内容搭配在一起。
2. 如果您例如添加了一个案例并忘记更改StrMap; 如果你只是坐在那里重新编译，就像我经常做的那样，你会错过它，直到你真正运行测试。
3. 由于类型系统较弱，我必须使用非详尽的函数来实现它。这使我试图教给我的同事的东西变得模糊不清；我一直试图让他们相信完全函数式编程的荣耀。

我们刚刚在 Haskell 中开始了一个新项目，我遇到了这样的场景。当然，我可以使用 QuickCheck 并fromJust实施 F# 策略，这应该没问题。

但我想知道的是：由于 Haskell 社区和生态系统以 F# 的社区和生态系统所没有的方式强调 Curry-Howard 对应关系，并且由于最近几天添加了各种花哨的扩展来启用依赖类型，我不应该为此遵循我的 Idris 策略吗？有人告诉我，如果我打开了足够多的扩展（并且愿意引入足够的冗长等），我应该能够将我可以在 Idris 中编写的任何内容翻译成 Haskell，而不会失去类型安全性。我不知道这是否属实，但如果是真的，我想知道要打开哪些扩展，以及编写什么样的代码，以便在 Haskell 中遵循我的 Idris 策略。另外值得注意的是：

如何将此 Idris 代码转换为 Haskell 以便在print :: RPS -> String不调用任何部分函数的情况下实现？

我已经开始阅读 Thinking With Types 这本书，这是我第一次涉足类型级编程。作者提供了一个练习和解决方案，我无法理解提供的解决方案如何正确。

练习是

我试图用以下方法解决这个练习

我觉得这是一个有效的解决方案，但是这本书给出了一个不同的解决方案，似乎没有进行类型检查，这让我相信我的整体理解是有缺陷的

我可以获得类型检查的书籍答案的唯一方法是：

因为单独的类型签名不排队

所以我的问题是，我的解决方案不正确吗？为什么书籍类型签名productToRuleBooks接受作为函数的第一个和第二个参数b -> a，c -> a当我理解x (multiplication)代数等于(,)in 类型时，为什么书籍答案没有(b -> a, c -> a)作为第一个参数？

我正在试验Jesper Cockx 和 Andreas AbelCoNat的这篇论文中的定义：

我定义zero和plus：

我定义了双相似性：

但我坚持plus zero n与n. 我的猜测是，在证明中我应该（至少）有一个 with 子句iszero n：

但是 Agda 抱怨以下错误消息：

我怎样才能做出这个证明？

以下定义编译并表现良好：

然而，这个不编译：

因为

我不明白为什么它们不相等。有什么区别以及为什么第二个变体不正确？

Curry 悖论 （以与目前的编程语言相同的人命名）是一种可能在错误逻辑中的构造，它允许人们证明任何事情。

我对逻辑一无所知，但它有多难？

它肯定会循环。（GHC怎么知道？！）

• 这是忠实的翻译吗？为什么？
• 我可以在没有fix递归的情况下做同样的事情吗？为什么？

通过 Curry Howard 对应，所有定理和引理都是类型，证明对象是值。举个例子：

当我这样做时，检查测试。Coq 的输出是：

但是当我检查“<=”的类型时，它是nat -> nat -> Prop。这意味着（0 <= 0）是Prop类型。这是否意味着'test'类型是Prop的子类型？一般来说，定理和引理标识符是 Prop 的子类型吗？

在范畴论 8.2的结尾，Bartosz Milewski 展示了一些逻辑、范畴论和类型系统之间对应关系的例子。

我在徘徊什么对应于逻辑异或运算符。我知道

所以我只解决了部分问题：a xor b对应于(Either a b, Either ? ?). 但是这两种缺失的类型是什么？

看来怎么写xor其实归结为怎么写not。

那么是什么¬a？我的理解是，a如果存在 type 的元素（至少一个），这是合乎逻辑的a。所以为了not a是真的，a应该是假的，即它应该是Void。因此，在我看来，有两种可能性：

但在最后一段中，我觉得我只是弄错了狗的结局。

（在此处跟进问题。）

当我问这个问题时，现在已删除的答案之一是暗示该类型Either对应于Curry-Howard 对应关系中的 XOR，而不是 OR ，因为它不能同时是Left和Right。

真相在哪里？

有一种编程“风格”（或者可能是范式，我不知道该怎么称呼它）如下：

首先，您编写规范：对您的（整个或部分）程序要做什么的正式描述。这是在编程系统内完成的；它不是一个单独的工件。

然后，您编写程序，但是——这是这种编程风格与其他风格之间的关键区别——这个写作任务的每一步都以某种方式受到你在上一步中编写的规范的指导。这种指导的具体发生方式千差万别；在 Coq 中，你有一种元编程语言 (Ltac)，它可以让你在幕后构建实际程序的同时“改进”规范，而在 Agda 中，你通过填充“漏洞”来编写程序（我实际上不确定它是如何进入的Agda，因为我主要习惯于 Coq）。

这并不是每个人都喜欢的编程风格，但我想尝试用通用的、流行的编程语言来练习它。至少在 Coq 中，我发现它相当容易上瘾！

...但是我什至如何在证明助理之外寻找方法呢？这就引出了一个问题：我正在为这种编程风格寻找一个名称，以便我可以尝试查找可以让我在其他编程语言中进行类似编程的工具。

请注意，当然更合适的问题是直接询问此类工具的示例，但要求答案列表的 AFAIK 问题不适合 Stack Exchange 站点。

需要明确的是，我并不是那么希望我真的会找到很多；这些主要是学术消遣，而您的典型编程语言并不真正适合这种编程风格（例如，规范语言最终可能会变得难以置信地复杂）。但值得一试！

我一直在学习命题逻辑的自然演绎（特别是 Chiswell 和 Hodges 的数学逻辑教科书第 2 章中描述的系统），并且一直在探索 Curry-Howard 对应关系。这展示了如何进行自然演绎推导并相当直接地转换为使用 Scala 或 Haskell 等语言的类型化程序。或者至少，对于不使用“Reducio ad absurdum”（RAA）规则的直觉证明，我可以。通过一些阅读，我发现也有一些方法可以探索经典证明的计算解释，也许使用控制运算符，如call/cc. 是否可以在真正的编程语言中使用这些想法？希望有人可以给出一些关于这可能如何工作的指示/示例。