问题标签 [curry-howard]

所以我最近阅读了以下打击帖子： http: //www.chuusai.com/2011/06/09/scala-union-types-curry-howard/

我真的很欣赏这种方法！我正在尝试制作一个功能

其中 neq[String, String] 不会编译，但 neq[String, Int] 会。看起来这应该是可能的，但我认为我没有足够深入地理解我们可以使用 curry-howard 对类型中的逻辑进行编码的方式。

我失败的尝试如下：

我认为我们想要的本质上是一个异或。所以我们想要

由于在进行隐式解析时我们在 scala 中所拥有的只是 <:<、=:= 之类的东西，我认为我需要在其中包含一个暗示，因为那是 <:<。所以我们说：

但是，如果我尝试执行以下操作，这将不起作用：

这是有道理的，因为类型根本不匹配。所以我真的不知道该去哪里！希望得到任何指导。

直观的逻辑，具有建设性，是函数式编程中类型系统的基础。经典逻辑不是建设性的，尤其是排中律A ∨ ¬A（或其等价物，例如双重否定消除或皮尔斯定律）。

但是，我们可以实现（构造）call-with-current-continuation运算符（AKA call/cc），例如在Scheme中。那么为什么call/cc没有建设性呢？

我一直在研究依赖类型，我了解以下内容：

1. 为什么全称量化被表示为依赖函数类型。∀(x:A).B(x)意思是“对于所有x类型A，都有一个类型的值B(x)”。因此，它被表示为一个函数，当给定任何x类型的值时，它返回一个类型的A值B(x)。
2. 为什么存在量化被表示为依赖对类型。∃(x:A).B(x)意思是“存在一个x类型的类型A，它有一个类型的值B(x)”。因此，它表示为一对，其第一个元素是type的特定值，其第二个元素是 type 的值。xAB(x)

旁白：有趣的是，普遍量化总是与物质暗示一起使用，而存在量化总是与逻辑连词一起使用。

无论如何，关于依赖类型的维基百科文章指出：

依赖类型的对立面是依赖对类型、依赖总和类型或sigma-type。它类似于联积或不相交的联合。

对类型（通常是乘积类型）如何类似于不相交的联合（总和类型）？这一直让我感到困惑。

此外，依赖函数类型与产品类型有何相似之处？

我想forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.在 Coq 中证明或证伪。这是我的方法。

但是，inversion H什么都不做。我想可能是因为 coq 的证明独立性（我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知），并且 coq 无法证明 One = Two -> False。但如果是这样，为什么必须 coq 消除证明的内容？

没有上述命题，我就无法证明以下命题或它们的否定。

所以我的问题是：

1. 如何或有可能forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.在 Coq 中证明或证伪？
2. 为什么inversion H什么都不做；是不是因为 coq 的证明独立性，如果是这样，为什么 Coq 这样做会浪费精力。

我在 Coq 中定义时遇到了一些问题，尤其是在使用 CHI 定义时。我已经设法获得了对基本原则的理解，但是当我尝试定义这一点时”

我一无所获，因为它一直告诉我：
"Error: The type of this term is a product while it is expected to be "C"。
我已经尝试过我之前在脚本中使用过的常用策略，并且我确信必须使用相同的方法（有趣）来解决这个问题，但是我似乎正在尝试的一切都以该错误消息结尾。有小费吗？

我读到影响是函数。但是我很难理解上述页面中给出的示例：

蕴涵 P → Q 的证明项是将 P 的证据作为输入并产生 Q 的证据作为其输出的函数。

引理 silly_implication ： (1 + 1) = 2 → 0 × 3 = 0。证明。介绍 H. 自反性。Qed。

我们可以看到，上述引理的证明项确实是一个函数：

打印 silly_implication。(* ===> silly_implication = fun _ : 1 + 1 = 2 => eq_refl : 1 + 1 = 2 -> 0 * 3 = 0 *)

确实，它是一个函数。但它的类型对我来说不合适。从我的阅读来看，证明项P -> Q应该是一个函数，并带有Q作为输出的证据。那么， 的输出 (1+1) = 2 -> 0*3 = 0应该是0*3 = 0, 单独的证据，对吗？

但是上面的 Coq 打印显示函数 image 是eq_refl : 1 + 1 = 2 -> 0 * 3 = 0，而不是eq_refl: 0 * 3 = 0。我不明白为什么假设1 + 1 = 2应该出现在输出中。谁能帮忙解释这里发生了什么？

谢谢。

我想知道是否有一种方法可以在 haskell 和/或其他一些函数式编程语言中表示选择公理。

众所周知，false 由没有值的类型表示（Void在 haskell 中）。

我们可以像这样表示否定

a我们可以为这样的类型表达排中律

这意味着我们可以将建设性逻辑变成一个Reader单子

例如，我们可以在其中进行双重否定消除

我们也可以有一个排中定律失效的单子

现在的问题是，我们如何制作一个代表选择公理的类型？选择公理是关于集合的集合。这意味着我们需要类型的类型或其他东西。是否有与可以编码的选择公理等效的东西？（如果您可以对否定进行编码，只需将其与排中律结合即可）。也许诡计会让我们拥有类型的类型。

注意：理想情况下，它应该是适用于Diaconescu 定理的选择公理的一个版本。

前段时间我读到函数类型a -> b对应于关系a ≤ b，或者是a ≥ b吗？这对我来说很有意义，因为如果我们在它们之间存在双射（即(a ≈ b) ≡ (a -> b, b -> a)），则两种类型是同构的。同样，(a = b) ≡ (a ≤ b) ∧ (a ≥ b)。

我知道这不是 Curry-Howard-Lambek 对应（即类型论、逻辑和范畴论之间的对应）。这是类型论和其他东西之间的对应关系。我想了解更多有关此通信的信息。有人能指出我正确的方向吗？

我知道这似乎不是一个编程问题，但它与编程有关，我希望一些函数式程序员对此有更多了解，并能指出我正确的方向。

我有一些这样的代码：

问题是，GHC 抱怨

伴随着一堆类似的错误。

有没有办法告诉 GHC 随机选择一个，因为我不在乎它使用哪个？（我什至不在乎它是否每次使用时都会选择不同的lem，因为这无关紧要。）