De Morgan's Laws in Haskell via the Curry-Howa

问题:

I implemented three of the four De Morgan's Laws in 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

However, I don't suppose that it's possible to implement the last law (which has two inhabitants):

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

The way I see it, there are two possible solutions:

1. Use undefined in place of ?. This is not a good solution because it's cheating.

2. Either use monomorphic types or bounded polymorphic types to encode a default value.

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

   This is not a good solution because it's a weaker law than De Morgan's law.

We know that De Morgan's laws are correct but am I correct in assuming that the last law can't be encoded in Haskell? What does this say about the Curry-Howard Isomorphism? It's not really an isomorphism if every proof can't be converted into an equivalent computer program, right?

回答1:

One thing that stands out to me is that you don't seem to be using the definition or any property of negation anywhere.

After reading the Haskell Wikibooks article on the CHI here is a proof assuming that you have a law of the excluded middle as a theorem:

exc_middle :: Either a (a -> Void)

and the proof of the notAandB de Morgan law would go like:

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

回答2:

The fourth law is not intuitionistic. You'll need the axiom of excluded middle:

lem :: Either a (a -> c)

or Pierce's law:

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

to prove it.