haskell - Curry-Howard 对应于双重否定 ((a->r)->r) 或 ((a->⊥)->⊥) 吗？

Question

这是a双重否定的Curry-Howard对应； (a -> r) -> r 或 (a -> ⊥) -> ⊥，或两者兼而有之？

这两种类型都可以在 Haskell 中编码如下，其中 ⊥ 编码为 forall b。 b.

p1 :: forall r. ((a -> r) -> r)
p2 :: (a -> (forall b. b)) -> (forall b. b)

论文作者Wadler 2003也 implementation in Haskell似乎采用前者，而有些其他文献(例如 this )似乎支持后者。

我目前的理解是后者是正确的。我很难理解前一种风格，因为您可以从 forall r 创建一个 a 类型的值。 ((a -> r) -> r) 使用纯计算:

> let p1 = ($42) :: forall r. (Int -> r) -> r
> p1 id
42

这似乎与直觉逻辑相矛盾，即您无法从 ￢￢a 派生出 a。

所以，我的问题是:p1和p2是否都可以被视为￢￢a的Curry-Howard通讯员？如果是这样，我们可以构造 p1 id::a 的事实如何与直觉逻辑相互作用？

<小时/>

为了方便讨论，我提出了更清晰的双重否定转换编码。感谢@user2407038!

{-# LANGUAGE RankNTypes #-}
to_double_neg :: forall a. a -> (forall r. (a->r)->r)
to_double_neg x = ($x)

from_double_neg :: forall a. (forall r. (a->r)->r) -> a
from_double_neg x = x id

Answer 1

构造 T1 a = forall r . (a -> r) -> r 类型的值至少与构造 T2 a = (a -> Void) -> Void 类型的值一样要求例如，Void ~ forall a . a 。这很容易看出，因为如果我们可以构造 T1 a 类型的值。那么我们会自动获得一个 T2 a 类型的值仅通过实例化forall与 Void .

另一方面，如果我们有一个 T2 a 类型的值我们不能回去。出现如下右图

dne :: forall a . ((a -> Void) -> Void) -> (forall r . (a -> r) -> r)
dne t2 = \f -> absurd (t2 (_ f)) -- we cannot fill _

但是这个洞_ :: (a -> r) -> (a -> Void)无法被填满——我们都“不知道”r在这种情况下，我们知道我们无法构建 Void .

<小时/>

这是另一个重要的区别:T1 a -> a编码相当简单，我们实例化 forall与 a然后申请id

project :: T1 a -> a
project t1 = t1 id

但是，另一方面，我们不能对 T2 a 执行此操作

projectX :: T2 a -> a
projectX t2 = absurd (t2 (_ :: a -> Void))

或者，至少我们不能不欺骗我们的直觉逻辑。

<小时/>

所以，这些应该给我们一个提示，告诉我们 T1 中的哪一个。和T2是真正的双重否定以及为什么使用每个否定。需要明确的是，T2确实是双重否定——就像你期望的那样——但是 T1更容易处理...特别是如果你使用Haskell98，它缺乏无效数据类型和更高级别的类型。如果没有这些，Void 的唯一“有效”编码是

newtype Void = Void Void

absurd :: Void -> a
absurd (Void v) = absurd v

如果您不需要它，这可能不是最好的介绍。那么什么保证我们可以使用 T1反而？好吧，只要我们只考虑不允许实例化的代码 r如果使用特定类型变量，那么我们实际上就好像它是一个没有任何操作的抽象或存在类型。这足以处理与双重否定(或延续)有关的许多参数，因此仅讨论 forall r . (a -> r) -> r 的属性可能会更简单。而不是(a -> Void) -> Void只要你保持适当的纪律，允许你在真正需要的时候将前者转换为后者。