库里 - 霍华德是双重否定的通讯员((a-> r) - > r)还是((a->⊥) - >⊥)？

Question

这是库里 - 霍华德的双重否定的记者a; (a -> r) -> r或者(a -> ?) -> ?,或两者兼而有之？

两种类型都可以在Haskell中编码如下,其中?编码为forall b. b.

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

Wadler 2003的论文以及 Haskell中的实现似乎采用了前者,而其他一些文献(例如本文)似乎支持后者.

我目前的理解是后者是正确的.我理解前者的风格,因为你可以创建类型的值的困难a,从forall r. ((a -> r) -> r)使用纯计算:

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

这似乎与你不能获得直觉逻辑相矛盾a的??a.

所以,我的问题是:可以p1并且p2都被视为库里 - 霍华德的记者 ??a吗？如果是这样,我们如何构建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只需要实例化forallwith 就自动获得一个值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编码非常简单,我们实例化forallwith 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更容易处理......特别是如果你使用缺少nullary数据类型和更高等级类型的Haskell98.没有这些,唯一的"有效"编码Void是

newtype Void = Void Void

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

如果你不需要它可能不是最好的东西.那么是什么确保我们可以使用T1呢？好吧,只要我们只考虑不允许r用特定类型变量实例化的代码,那么我们实际上就好像它是一个没有操作的抽象或存在类型.这足以处理许多与双重否定(或延续)相关的参数,所以只讨论属性可能更简单,forall r . (a -> r) -> r而不是(a -> Void) -> Void只要你维持一个适当的规则,允许你将前者转换为后者,如果真的需要.

Answer 2

(a -> r) -> r根据Curry-Howard同构,你是正确的双重否定编码.但是,您的函数类型不适合该类型!下列:

double_neg :: forall a r . ((a -> r) -> r)
double_neg = (($42) :: (Int -> r) -> r ) 

给出一个类型错误:

Couldn't match type `a' with `Int'
      `a' is a rigid type variable bound by
          the type signature for double_neg :: (a -> r) -> r at test.hs:20:22
    Expected type: (a -> r) -> r
      Actual type: (Int -> r) -> r
    Relevant bindings include
      double_neg :: (a -> r) -> r (bound at test.hs:21:1)

更多细节:你如何编码底部并不重要.agda中的简短演示可以帮助显示这一点.假设只有一个公理 - 即ex falso quodlibet,字面意思是"来自虚假的任何东西".

record Double-Neg : Set? where
  field 
    ? : Set
    absurd : {A : Set} ? ? ? A

  ¬_ : Set ? Set
  ¬ A = A ? ? 

  {-# NO_TERMINATION_CHECK #-}
  double-neg : { P : Set } ? ¬ (¬ P) ? P
  double-neg f = absurd r where r = f (? _ ? r)

请注意,如果不关闭终止检查程序(这是作弊行为!),则无法写出双重的有效定义.如果再次尝试定义,则还会出现类型错误:

  data ? : Set where t : ?

  double-neg : { P : Set } ? ¬ (¬ P) ? P
  double-neg {P} f = f t 

给

? !=< (P ? ?)
when checking that the expression t has type ¬ P

这!=<意味着"不是"的子类型.