{-# LANGUAGE DeriveDataTypeable #-}

-- | An interface to continuations using Peirce's law
--
-- This module is bogus, as the following proof demonstrates:
--
--   peirce (\f -> f 1 == f 2) == 1
--
--   peirce (\f -> f 2 == f 1) == 2
--
--   f 1 == f 2
--   
--   Therefore, 1 == 2.
module Acme.Peirce (falseVoid, peirce, lem, doubleNeg) where

import System.IO.Unsafe
import Data.Void
import Data.Typeable
import Control.Concurrent.MVar
import Control.Exception
import Prelude hiding (catch)

data ContinueException = ContinueException deriving (Show, Typeable)

instance Exception ContinueException

-- | Ex falso
falseVoid :: Void -> a
falseVoid x = x `seq` undefined

-- | Peirce's law
peirce f = unsafePerformIO $ do
	mvar <- newEmptyMVar
	catch
		(return $! f $ \x -> unsafePerformIO $ do
			putMVar mvar $! x
			throwIO ContinueException)
		$ \ContinueException -> tryTakeMVar mvar
			>>= maybe (throwIO ContinueException) return

-- | Law of excluded middle
lem :: (a -> b) -> ((a -> Void) -> b) -> b
lem f g = peirce $ \h -> g $ h . f

-- | Double negation law
doubleNeg f = lem id (falseVoid . f)