问题标签 [curry-howard]

您能否解释一下逻辑编程的基础与类型系统和常规逻辑之间的句法相似现象之间的基本联系是什么？

我在编程生涯中比较晚才接触到Curry-Howard 同构，也许这有助于我对它完全着迷。这意味着对于每个编程概念，在形式逻辑中都存在一个精确的类比，反之亦然。这是我想不到的此类类比的“基本”列表：

那么，对于我的问题：这种同构有哪些更有趣/更晦涩的含义？我不是逻辑学家，所以我确信我只是用这个列表触及了表面。

例如，以下是一些我不知道逻辑中精辟名称的编程概念：

以下是一些我在编程术语中尚未完全确定的逻辑概念：

编辑：

以下是从回复中收集的更多等价物：

我在互联网上搜索过，我找不到任何关于 CHI 的解释，这些解释不会迅速退化为逻辑理论的讲座，这让我大吃一惊。（这些人说的好像“直觉命题演算”是一个对正常人来说实际上意味着什么的短语！）

粗略地说，CHI 说类型是定理，程序是这些定理的证明。但这到底是什么意思？

到目前为止，我已经弄清楚了：

• 考虑id :: x -> x。它的类型是“假设 X 为真，我们可以得出结论 X 为真”。对我来说似乎是一个合理的定理。

• 现在考虑foo :: x -> y。正如任何 Haskell 程序员都会告诉你的那样，这是不可能的。你不能写这个函数。（好吧，无论如何不要作弊。）作为一个定理阅读，它说“鉴于任何 X 为真，我们可以得出任何 Y 为真的结论”。这显然是无稽之谈。而且，果然，你不能写这个函数。

• 更一般地，函数的参数可以被认为是“假设为真的这个”，而结果类型可以被认为是“假设所有其他事情都是真的”。如果有一个函数参数，比如说x -> y，我们可以将其视为 X 为真意味着 Y 必须为真的假设。

• 例如，(.) :: (y -> z) -> (x -> y) -> x -> z可以理解为“假设 Y 蕴涵 Z，X 蕴涵 Y，并且 X 为真，我们可以得出 Z 为真的结论”。这在我看来在逻辑上是明智的。

现在，到底是什么Int -> Int意思？o_O

我能想出的唯一明智的答案是：如果你有一个函数 X -> Y -> Z，那么类型签名会说“假设可以构造一个 X 类型的值和另一个 Y 类型的值，那么可以构造一个 Z 类型的值”。函数体准确地描述了你将如何做到这一点。

这似乎有道理，但不是很有趣。很明显，它肯定比这更多……

因此，为了帮助我理解一些更高级的 Haskell/GHC 功能和概念，我决定采用基于 GADT 的动态类型数据实现并将其扩展为涵盖参数类型。（我为这个例子的长度道歉。）

但是，对此的编译在最后一行失败（我的行号与示例不匹配）：

按照我的阅读方式，编译器无法确定 in Inductive :: Equal a b -> Equal (f a) (f b)，a并且b对于非底部值必须相等。所以我试过Inductive :: Equal a a -> Equal (f a) (f a)了，但是在定义中也失败了matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b)：

Changing the type of matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a b) to produce matchTypes :: TypeRep a -> TypeRep b -> Maybe (Equal a a) doesn't work (just read it as a proposition). Neither does matchTypes :: TypeRep a -> TypeRep a -> Maybe (Equal a a) (another trivial proposition, and this as I understand it would require users of fromDynamic' to know theain theTypeRep acontained in theDynamic`).

So, I'm stumped. Any pointers on how to move forward here?

Set，类似地[]具有完美定义的一元操作。问题是它们要求值满足Ord约束，因此无法定义return并且>>=没有任何约束。同样的问题适用于许多其他需要对可能值进行某种约束的数据结构。

标准技巧（在haskell-cafe post中向我建议）是包装Set到延续单子中。ContT不关心底层类型函子是否有任何约束。Set仅当将s 包装/展开到/从延续中时才需要约束：

这可以根据需要工作。例如，我们可以模拟一个非确定性函数，将其参数增加 1 或保持原样：

确实，stepN 5 0产量fromList [0,1,2,3,4,5]。如果我们改用[]monad，我们会得到

反而。

问题是效率。如果我们调用stepN 20 0输出需要几秒钟并且stepN 30 0没有在合理的时间内完成。事实证明，所有Set.union操作都是在最后执行的，而不是在每次单子计算之后执行。结果是只在最后Set构造和编辑了成倍增加的 s ，这对于大多数任务来说是不可接受的。union

有什么办法可以使这种建设高效吗？我试过但没有成功。

（我什至怀疑 Curry-Howard 同构和Glivenko 定理可能存在某种理论限制。Glivenko 定理说，对于任何命题重言式φ，公式¬¬φ都可以在直觉逻辑中得到证明。但是，我怀疑证明的长度（以正常形式）可以成倍地增长。所以，也许，将计算包装到延续单子中会使它成倍地增长？）

通过Curry-Howard 同构， ScalaUnit对应于逻辑真和Nothing逻辑假。任何事物都暗示了逻辑真这一事实由一个简单的函数证明，该函数只是丢弃了参数：

是否有一个函数可以证明逻辑 false 意味着什么，即 type 的函数Nothing => A？还是有一种惯用的方法来构建一个？

一个人总是可以做类似的事情

但这很丑 - 它没有使用Nothing没有价值的事实。应该有一种方法可以毫无例外地做到这一点。

中的absurd函数Data.Void具有以下签名，其中Void是该包导出的逻辑上无人居住的类型：

我确实知道足够的逻辑来获得文档的注释，即通过 Proposal-as-types 对应，这对应于有效的公式⊥ → a。

我感到疑惑和好奇的是：这个函数在什么样的实际编程问题中有用？我在想，在某些情况下，作为一种彻底处理“不可能发生”情况的类型安全方式，它可能很有用，但我对 Curry-Howard 的实际用途知之甚少，无法判断这个想法是否在完全正确。

编辑：最好在 Haskell 中举例，但如果有人想使用依赖类型的语言，我不会抱怨......

因此，在我不断尝试通过小型 Haskell 练习对 Curry-Howard 理解一半的过程中，我被困在了这一点上：

显然，该类型Equal Int Char没有（非底部）居民，因此在语义上应该有一个absurdEquality :: Equal Int Char -> a函数......但对于我的生活，我想不出除了使用undefined.

所以要么：

1. 我错过了一些东西，或者
2. 语言的某些限制使这成为一项不可能完成的任务，我还没有设法理解它是什么。

我怀疑答案是这样的：编译器无法利用没有Equal没有 a = b 的构造函数这一事实。但如果是这样，那它是真的吗？

我一直盯着这张脸看了好几个小时不明白:(

我需要使用 coq 解决一些定义，我应该通过 Curry Howard 同构来解决。我已经阅读了，但仍然不知道我在做什么。我查看了其他示例并尝试以这些方式进行操作，但我总是遇到错误。

例如，在这里我需要定义这个：

这是我的尝试：

我也试过

最终它只是说它期待的类型与我给出的不同，有时它会说：“预期有类型“？9 * ？10”。”

在阅读了我能找到的所有内容后，我真的很难理解这一点。

请有人解释一下:(

I am trying to understand "Löb and möb: strange loops in Haskell", but right now the meaning is sleaping away from me, I just don't see why it could be useful. Just to recall function loeb is defined as

or equivalently:

In the article there is an example with [] functor and spreadsheets implementation, but it is bit foreign for me just as spreadsheets themselves (never used them).

While I'm understanding that spreadsheet thing, I think it would help a lot for me and others to have more examples, despite lists. Is there any application for loeb for Maybe or other functors?