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.
- Why does the Haskell compiler approve the type of
- 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.