21
4

3 回答 3

14

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

另一方面，如果我们有一个类型的值，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编码相当简单，我们实例化forallwitha然后应用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只要你保持适当的纪律，如果你真的可以将前者转换为后者需要。

于 2015-05-03T02:27:14.937 回答
7

您是正确的，这(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

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

于 2015-05-03T02:06:05.843 回答
0

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

Control.Monad.Cont但是，我们可以通过实例化r来模拟 p2/T2 内的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的类型签名有了更好的理解。

于 2015-05-04T15:41:56.860 回答