Де Моргана в Haskell через Карри-Говарда заочного

Question

я реализовал три Законов в четверке Де Моргана в Haskell:

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

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

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

Answer 1

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

После прочтения Haskell Wikibooks article on the CHI здесь доказательство при условии, что у вас есть закон исключенного третьего как теорема:

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

Четвертый закон - not intuitionistic. Вы будете нуждаться в аксиому исключенного третьего:

lem :: Either a (a -> c) 

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

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

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