Является ли корреспондент Карри-Говарда двойного отрицания ((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, а также implementation in Haskell, кажется, принять бывший, в то время как некоторые другой литературе (например, this), кажется, поддерживает последние.

Мое настоящее понимание заключается в том, что последнее верно. У меня есть трудности в понимании прежнего стиля, так как вы можете создать значение типа a из forall r. ((a -> r) -> r) с использованием чистого вычисления:

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

, который, кажется, противоречит интуиционистской логике, что вы не можете вывести a из ￢￢a.

Итак, мой вопрос: может p1 и p2 оба будут рассматриваться как корреспондент Curry-Howard от ￢￢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, просто создавая экземпляр 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, пока вы поддерживаете правильную дисциплину, которая позволяет конвертировать первое в последнее если это действительно необходимо.

Answer 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) 

Примечания Вы не можете написать действительное определение двойных нег, не выключая завершение проверки (что обман!). Если вы попробуете свое определение еще раз, вы также получите сообщение об ошибке типа:

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 

Здесь !=< средство «не является подтипом».

Answer 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.