Есть ли способ реализовать функцию типа ((a -> b) -> b) -> либо ab?

Question

Предложения (P -> Q) -> Q и P \/ Q эквивалентны.

Есть ли способ засвидетельствовать эту эквивалентность в Haskell:

from :: Either a b -> ((a -> b) -> b)
from x = case x of
         Left a -> \f -> f a
         Right b -> \f -> b

to :: ((a -> b) -> b) -> Either a b
to = ???

, такой что

from . to = id и to . from = id?

Answer 1

Предложения (P -> Q) -> Q и P \/ Q эквивалентны.

Это верно в классической логике, но не в конструктивной логике.

В конструктивной логике мыу нас нет закона исключенного среднего , то есть мы не можем начать наше размышление с "либо P истинно, либо P неверно".

Классически мы рассуждаем как:

• если P истинно (то есть у нас есть (x :: P)), тогда вернуть Left x.
• если P ложно, то в языке Хаскелла у нас будет функция nx :: P -> Void. Затем absurd . nx :: P -> Q (мы можем достигнуть пика любого типа, мы берем Q) и вызвать f :: (P -> Q) -> Q) с absurd . nx, чтобы получить значение типа Q.

Проблема в том, чтоне являются общими функциями типа:

lem :: forall p. Either p (p -> Void)

Для некоторых конкретных типов, например, Bool обитаем, поэтому мы можем написать

lemBool :: Either Bool (Bool -> Void)
lemBool = Left True -- arbitrary choice

, но опять же, в общем, мыне могу.

Answer 2

Нет, это невозможно. Рассмотрим специальный случай, когда Q = Void.

Either P Q равен Either P Void, что изоморфно P.

iso :: P -> Either P Void
iso = Left

iso_inv :: Either P Void -> P
iso_inv (Left p)  = p
iso_inv (Right q) = absurd q

Следовательно, если бы у нас был функциональный член

impossible :: ((P -> Void) -> Void) -> Either P Void

у нас также может быть термин

impossible2 :: ((P -> Void) -> Void) -> P
impossible2 = iso_inv . impossible

В соответствии с соответствием Карри-Говарда это будет тавтологией в интуиционистской логике:

((P -> False) -> False) -> P

Но вышеизложенное - это устранение двойного отрицания, которое, как известно, невозможно доказать в интуиционистской логике - отсюда и противоречие. (Тот факт, что мы могли бы доказать это в классической логике, не имеет значения.)

(Последнее замечание: это предполагает, что наша программа на Haskell завершается. Конечно, используя бесконечную рекурсию, undefinedи аналогичные способы, позволяющие на самом деле избежать возврата результата, мы можем использовать в Хаскеле любого типа.)

Answer 3

Нет, это невозможно, но это немного неуловимо. Проблема заключается в том, что переменные типа a и b определены количественно.

to :: ((a -> b) -> b) -> Either a b
to f = ...

a и b определены количественно. Вызывающая сторона выбирает, какой они тип, поэтому вы не можете просто создать значение любого типа. Это означает, что вы не можете просто создать значение типа Either a b, игнорируя аргумент f. Но использование f также невозможно. Не зная, что такое типы a и b, вы не можете создать значение типа a -> b для передачи f. Просто недостаточно информации, когда типы универсально определены количественно.

Насколько изоморфизм не работает в Хаскеле - вы уверены, что эти предложения эквивалентны в конструктивной интуиционистской логике? Haskell не реализует классическую дедуктивную логику.

Answer 4

Как уже отмечали другие, это невозможно, потому что у нас нет закона исключенной середины. Позвольте мне пройти через это немного более явно. Предположим, у нас есть

bogus :: ((a -> b) -> b) -> Either a b

и мы установили b ~ Void. Тогда мы получим

-- chi calls this `impossible2`.
double_neg_elim :: ((a -> Void) -> Void) -> a
bouble_neg_elim f = case bogus f of
             Left a -> a
             Right v -> absurd v

Теперь давайте докажем двойное отрицание закона исключенного среднего применительно к конкретному предложению .

nnlem :: forall a. (Either a (a -> Void) -> Void) -> Void
nnlem f = not_not_a not_a
  where
    not_a :: a -> Void
    not_a = f . Left

    not_not_a :: (a -> Void) -> Void
    not_not_a = f . Right

Итак, теперь

lem :: Either a (a -> Void)
lem = double_neg_elim nnlem

lem явно не может существовать, потому что a может закодировать предположение, что любая конфигурация машины Тьюринга, которую я случайно выберу, остановит.

---

Давайте проверим, что lemдостаточно:

bogus :: forall a b. ((a -> b) -> b) -> Either a b
bogus f = case lem @a of
  Left a -> Left a
  Right na -> Right $ f (absurd . na)

Answer 5

Я понятия не имею, является ли это допустимым с точки зрения логики или что это значит для вашей эквивалентности, но да, можно написать такую ​​функцию в Haskell.

Чтобы построить Either a bнам нужно либо значение a, либо значение b. У нас нет никакого способа построить значение a, но у нас есть функция, которая возвращает b, которую мы могли бы вызвать. Для этого нам нужно предоставить функцию, которая преобразует a в b, но, учитывая типы, неизвестные, мы могли бы в лучшем случае создать функцию, которая возвращает константу b. Чтобы получить это значение b, мы не можем построить его каким-либо иным способом, чем раньше, поэтому это становится круговым рассуждением - и мы можем решить это, просто создав fixpoint :

to :: ((a -> b) -> b) -> Either a b
to f = let x = f (\_ -> x) in Right x