Curry-Howard 是双重否定 ((a->r)->r) 还是 ((a->⊥)->⊥) 的对应者？

Posted 2023-05-08

【中文标题】Curry-Howard 是双重否定 ((a->r)->r) 还是 ((a->⊥)->⊥) 的对应者？

【英文标题】：Is Curry-Howard correspondent of double negation ((a->r)->r) or ((a->⊥)->⊥)?

【发布时间】：2015-07-12 14:04:09

【问题描述】：

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 的论文以及 implementation in Haskell 似乎采用前者，而有些 其他文献（例如this）似乎支持后者。

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

> 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

【问题讨论】：

⊥ 不是类型。你想要Void，就像en.wikibooks.org/wiki/Haskell/…一样。

@ReinHenrichs，我认为调用空类型⊥一点也不稀奇。它是类型格的“底部”。

@dfeuer 你当然是对的。我只是习惯于在价值上下文中看到它。

【参考方案1】：

构造T1 a = forall r . (a -> r) -> r 类型的值至少与构造T2 a = (a -> Void) -> Void 类型的值（例如Void ~ forall a . a）一样苛刻。这很容易看出，因为如果我们可以构造一个T1 a 类型的值，那么我们只需用Void 实例化forall，就可以自动获得T2 a 类型的值。

另一方面，如果我们有一个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 的编码相当简单，我们用a 实例化forall，然后应用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 的代码，那么我们实际上就好像它是没有操作的抽象或存在类型一样。这足以处理与双重否定（或延续）有关的许多论点，因此只要您保持适当的纪律，允许您转换如果确实需要，前者转后者。

【讨论】：

我要特别感谢您指出我们可以用 Void 实例化 r 。这帮助我理解了 T1 比 T2 编码更强，并帮助我构建了双重否定的“童话”语义:)

它是在实例化“forall with Void”还是“forall r with Void”？

"forall" 只是一个绑定，因为名称 r 最终仅在本地有意义，所以我尽量不提及它。这与应用函数 f 而不是函数 f x = ... 的方式相同。

newtype Void = Void Void 会让值存在：fix Void。

【参考方案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

这里!=< 的意思是“不是”的子类型。

【讨论】：

这里from_double_neg的存在和机制强烈表明forall r. (a -> r) -> r不是真正的双重否定编码。

我要感谢 user2407038 解决问题和 Abrahamson 代表我填写评论！我目前的理解是from_double_neg 破坏了编码，因为它实例化了r。 p1/T1 编码是不幸的，如果没有错的话，因为 Haskell 没有防止 r 实例化的机制。

【参考方案3】：

总而言之，p2/T2 方法更加规范，但我们无法从中计算出任何实际价值。另一方面，p1/T1 允许实例化r，但实例化是执行runCont :: Cont r a -> (a -> r) -> r 或runContT 并从中获得任何结果和副作用所必需的。

但是，我们可以在 Control.Monad.Cont 中模拟 p2/T2，方法是将 r 实例化为 Void，并且只使用副作用，如下所示：

-# LANGUAGE RankNTypes #-
import Control.Monad.Cont
import Control.Monad.Trans (lift)
import Control.Monad.Writer

newtype Bottom = Bottom  unleash :: forall a. a

type C = ContT Bottom
type M = C (Writer String)

data USD1G = USD1G deriving Show

say x = lift $ tell $ x ++ "\n"

runM :: M a -> String
runM m = execWriter $
  runContT m (const $ return undefined) >> return ()
-- Are we sure that (undefined :: Bottom) above will never be used?

exmid :: M (Either USD1G (USD1G -> M Bottom))
exmid = callCC f
  where
     f k = return (Right (\x -> k (Left x)))

useTheWish :: Either USD1G (USD1G -> M Bottom) -> M ()
useTheWish e = case e of
  Left money -> say $ "I got money:" ++ show money
  Right method -> do
    say "I will pay devil the money."
    unobtainium <- method USD1G
    say $ "I am now omnipotent! The answer to everything is:"
      ++ show (unleash unobtainium :: Integer)

theStory :: String
theStory = runM $ exmid >>= useTheWish

main :: IO ()
main = putStrLn theStory

-
> runhaskell bottom-encoding-monad.hs
I will pay devil the money.
I got money:USD1G

-

如果我们想进一步摆脱丑陋的undefined :: Bottom，我认为我需要避免重新发明并使用管道和机器等CPS库。使用machines 的示例如下：

-# LANGUAGE RankNTypes, ImpredicativeTypes, ScopedTypeVariables #-
import Data.Machine
import Data.Void
import Unsafe.Coerce

type M k a = Plan k String a
type PT k m a = PlanT k String m a

data USD = USD1G deriving (Show)

type Contract k m = Either USD (USD -> PT k m Void)

callCC :: forall a m k. ((a -> PT k m Void) -> PT k m a) -> PT k m a
callCC f = PlanT $
    \ kp ke kr kf ->
     runPlanT (f (\x -> PlanT $ \_ _ _ _ -> unsafeCoerce $kp x))
     kp ke kr kf

exmid ::  PT k m (Contract k m)
exmid = callCC f
  where
    f k =
       return $ Right (\x -> k (Left x))

planA :: Contract k m -> PT k m ()
planA e = case e of
  Left money ->
    yield $ "I got money: " ++ show money
  Right method -> do
    yield $ "I pay devil the money"
    u <- method USD1G
    yield $ "The answer to everything is :" ++ show (absurd u :: Integer)

helloMachine :: Monad m => SourceT m String
helloMachine = construct $ exmid >>= planA

main :: IO ()
main = do
  xs <- runT helloMachine
  print xs

感谢我们的谈话，现在我对 runPlanT 的类型签名有了更好的理解。