Корреспондент Карри-Говарда двойного отрицания ((a-> r) → r) или ((a-> ⊥) → ⊥)?

Ответ 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 в этом контексте, и мы знаем, что мы не можем построить a 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, пока вы поддерживаете надлежащую дисциплину, которая позволяет конвертировать бывший для последнего, если он действительно необходим.

Ответ 2

Вы правы, что (a -> r) -> r является правильной кодировкой двойного отрицания в соответствии с изоморфизмом Карри-Говарда. Однако тип вашей функции не подходит для этого типа! Следующее:

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)

Обратите внимание, что вы не можете написать правильное определение double-neg, не отключая проверку завершения (которая обманывает!). Если вы снова попробуете свое определение, вы также получите ошибку типа:

  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

Здесь !=< означает, что "не является подтипом".

Ответ 3

Подводя итог, подход p2/T2 более дисциплинирован, но мы не можем вычислить какую-либо практическую ценность из него. С другой стороны, p1/T1 позволяет создать экземпляр r, но для выполнения runCont :: Cont r a -> (a -> r) -> r или runContT необходимо создать экземпляр и получить из него любой результат и побочный эффект.

Однако мы можем эмулировать p2/T2 внутри Control.Monad.Cont, создавая экземпляр 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.