Curry-Howard, void, and type checking in Haskell

Question

I am trying to understand an example of theorem proving via type checking in Haskell given here. The example is as follows.

Using the Curry-Howard isomorphism, construct an inhabitant of the type and prove that $N= (A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow ((\neg B\& A)\vee ((A\rightarrow B)\&(B\rightarrow A)))$ holds.

The author provides a following code.

data Void
nnot :: Void -> a
nnot = undefined
proposition :: (Either a (b -> a), (c, c -> b)) -> Either (Void -> b, a) (b -> a)
proposition (Left x, (y, f)) = Left (nnot, x)
proposition (Right g, (y,f)) = Left (nnot, (g (f y)))

The implication $(A\vee (B\rightarrow A))\& (C\&(C\rightarrow B))\rightarrow (\neg B \& A)$ does not hold. But the constructed term is claimed to prove it, and the type checker is satisfied by it. Why?

I feel that the transcription of the initial formulae to the type of proposition is incorrect, since the negation of b is represented with Void -> b which is the absurdity (and it is defined as nnot). I.e. from the logical point of view, the pair (Void -> b, a) corresponds to the term $\bot \& A$. But that does not give an answer why the type checker verifies the code above. Thus, I will greatly appreciate any hints on the following two questions.

1. Why does the Haskell compiler approve the type of proposition?
2. If that is the case when Curry-Howard is not in place then how I can actually use the type checker to prove formulas with negation via Curry-Howard?

I do not know either this question is more appropriate on cs or stackoverflow, so please sorry if it is off-topic.

EDIT: Given the following corrected proposition:

proposition :: (Either a (b -> a), (c, c -> b)) -> Either (b -> Void, a) (b -> a)

I have written the following "proof" for it, and the type checker was satisfied. I do not know whether I can believe that the proposition can be counted as being proved after the type check.

proposition (Left x, (y, f)) = Right ((\z1 z2 -> z1) x)
proposition (Right g, (y,f)) = Right ((\z1 z2 -> z1) (g (f y))) 

And still I have no idea whether it is possible to prove any negation by the type checking procedure.

Edit2: I thought I had got some understanding of the topic, but then I tried the following:

prop1 :: ((Either a b), c) -> b
prop1 (Right x, y) = x

This code is Ok for Haskell (for example, there). But it seems to be ill-typed from the point of view of logic: the corresponding type is $(A\vee B)\& C\rightarrow B$. It is obvious that the case given in prop1(Right x, y) = x has the right (heh) type, but I did not define the case for prop1(Left x, y), thus the proposition is not proved for this case. Hence, I can have problems with the disjunction as well.

Answer 1

I would find a different tutorial because the author of that one is fundamentally confused. They wrongly claim that $\neg a$ and $\bot\to a$ are equivalent ($a\to\bot$ would be correct), and also wrongly claim that you can't write a function of type $\texttt{Void}\to a$.

$\texttt{Void}\to a$ is vacuously true. In principle a function of that type should require no definition at all because the number of cases for which you need to define it is zero. GHC doesn't accept that, but (with -XEmptyCase) it does accept

f :: Void -> a
f x = case x of {}

which is a perfectly valid, logically sound definition.

Why does the Haskell compiler approve the type of proposition?

The proposition as written in the Haskell code is actually true. The proof is invalid though since it uses $\texttt{undefined}$.

If you replaced the right hand side with $(b\to\texttt{Void},a)$ then it would be false, but you could still "prove" it using $\texttt{undefined}$; in fact you could just write $\texttt{proposition} = \texttt{undefined}$ and the type checker would accept that. It would also accept $\texttt{proposition} = \texttt{proposition}$. If you want to use Haskell as a Curry-Howard sandbox you have to take care that your code doesn't throw an exception or fail to terminate, because the compiler won't catch those errors.

---

Response to edit: your proof is correct but it can be simplified. In the first case, there's no need to create a function and immediately apply it to one of its arguments. Instead of (\z1 z2 -> z1) x you can write \z2 -> x, or \_ -> x since the argument/premise isn't used. In the second case, you don't need to prove b -> a since you already have g :: b -> a. The simplified proof is

proposition (Left x, _) = Right (\_ -> x)
proposition (Right g, _) = Right g

In addition to the pitfalls that Dan Doel mentioned in a comment, missing cases are another thing to watch out for. GHC by default doesn't even warn about them. With -Werror=incomplete-patterns it will refuse to accept programs with missing cases.

You can prove negations. You need to return a value of type $\texttt{Void}$, which you can't create yourself but you can get from elsewhere. For example here's a proof of $((P\Rightarrow Q) \mathbin{\&} \neg Q)\Rightarrow \neg P$:

f :: (a -> b, b -> Void) -> (a -> Void)
f (x, y) = \z -> y (x z)

You may reasonably wonder where your caller got the value of type $\texttt{Void}$, but that's the caller's problem, not yours. Deriving a contradiction in a subproof doesn't mean the logic is inconsistent, it just means you've shown that you'll never actually reach this point in the real world.