Curry's paradox in Haskell?

Question

Curry's paradox (named after the same person as the present programming language) is a construction possible in a faulty logic that allows one to prove anything.

I know nothing about logic, but how hard can it be?

module Main where

import Data.Void
import Data.Function

data X = X (X -> Void)

x :: X
x = fix \(X f) -> X f

u :: Void
u = let (X f) = x in f x

main :: IO ()
main = u `seq` print "Done!"

It certainly does loop. (How does GHC know?!)

% ghc -XBlockArguments Z.hs && ./Z
[1 of 1] Compiling Main             ( Z.hs, Z.o )
Linking Z ...
Z: <<loop>>

 

• Is this a faithful translation? Why?
• Can I do the same without fix or recursion? Why?

Answer 1

The encoding of Curry's paradox looks more like this:

x :: X
x = X (\x'@(X f) -> f x')

X can indeed be read as the sentence "if X is true, then there is a contradiction", or equivalently, "X is false".

But using fix to prove X is not really meaningful, because fix is blatantly incorrect as a reasoning principle. Curry's paradox is more subtle.

How do you actually prove X?

x :: X
x = _

X is a conditional proposition, so you can start by assuming its premise to show its conclusion. This logical step corresponds to inserting a lambda. (Constructively, a proof of an implication is a mapping from proofs of the premise to proofs of the conclusion.)

x :: X
x = X (\x' -> _)

But now we have an assumption x' :: X, we can unfold the definition of X again to get f :: X -> Void. In informal descriptions of Curry's paradox, there is no explicit "unfolding step", but in Haskell it corresponds to pattern-matching on the newtype constructor when X is an assumption, or applying the constructor when X is the goal (in fact, as we did above):

x :: X
x = X (\x'@(X f) -> _)

Finally, we now have f :: X -> Void and x' :: X, so we can deduce Void by function application:

x :: X
x = X (\x'@(X f) -> f x')