Законы де Моргана в Хаскеле через переписку Карри-Ховарда

Question

Я реализовал три из четырех законов Де Моргана в Хаскеле:

notAandNotB :: (a -> c, b -> c) -> Either a b -> c
notAandNotB (f, g) (Left x)  = f x
notAandNotB (f, g) (Right y) = g y

notAorB :: (Either a b -> c) -> (a -> c, b -> c)
notAorB f = (f . Left, f . Right)

notAorNotB :: Either (a -> c) (b -> c) -> (a, b) -> c
notAorNotB (Left f)  (x, y) = f x
notAorNotB (Right g) (x, y) = g y

Тем не менее, я не думаю, что возможно реализовать последний закон (который имеет двух жителей):

notAandBLeft  :: ((a, b) -> c) -> Either (a -> c) (b -> c)
notAandBLeft  f = Left  (\a -> f (a, ?))

notAandBRight :: ((a, b) -> c) -> Either (a -> c) (b -> c)
notAandBRight f = Right (\b -> f (?, b))

На мой взгляд, есть два возможных решения:

1. использование undefined на месте ?, Это не хорошее решение, потому что это обман.

2. Либо используйте мономорфные типы, либо ограниченные полиморфные типы для кодирования значения по умолчанию.

   notAandBLeft  :: Monoid b => ((a, b) -> c) -> Either (a -> c) (b -> c)
   notAandBLeft  f = Left  (\a -> f (a, mempty))
   
   notAandBRight :: Monoid a => ((a, b) -> c) -> Either (a -> c) (b -> c)
   notAandBRight f = Right (\b -> f (mempty, b))
   

   Это не хорошее решение, потому что это более слабый закон, чем закон де Моргана.

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

Answer 1

Одна вещь, которая выделяется для меня, это то, что вы, кажется, нигде не используете определение или какое-либо свойство отрицания.

После прочтения статьи в Haskell Wikibooks о ОМС приведем доказательство того, что в качестве теоремы у вас есть закон исключенного среднего:

exc_middle :: Either a (a -> Void)

и доказательство notAandB Закон де Моргана будет выглядеть так:

notAandB' :: Either a (a -> Void) -> ((a,b) -> Void) -> Either (a -> Void) (b -> Void)
notAandB' (Right notA) _ = Left notA
notAandB' (Left a)     f = Right (\b -> f (a,b))

notAandB = notAandB' exc_middle

Answer 2

Четвертый закон не интуиционистский. Вам понадобится аксиома исключенного среднего:

lem :: Either a (a -> c)

или закон Пирса:

pierce :: ((a -> c) -> c) -> a

чтобы доказать это.