通过库里 - 霍华德通信的德摩根在哈斯克尔的定律

Question

我在Haskell实施了四个De Morgan定律中的三个:

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

   这不是一个好的解决方案,因为这是一个比德摩根定律更弱的法律.

我们知道De Morgan的定律是正确的,但我认为最后的定律不能用Haskell编码是正确的吗？这对库里 - 霍华德同构有什么看法？如果每个证据都不能转换成等效的计算机程序,那么它并不是真正的同构,对吧？

Answer 1

第四定律不是直觉主义的.你需要被排除在中间的公理:

lem :: Either a (a -> c)

或皮尔斯定律:

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

证明这一点.

Answer 2

对我而言突出的一件事是，您似乎在任何地方都不使用定义或否定的任何属性。

在阅读了关于CHI的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