Today's shower thought is: Is there a way to interpret double negation elimination as a program?
((a -> Void) -> Void) -> a
Void denotes the empty type.)
At first glance, it seems preposterous: how does one expect to produce a return value of a completely arbitrary type
a merely from a function of type
(a -> Void) -> Void, which doesn't even return a value of type
callCC :: ((a -> Cont r) -> Cont a) -> Cont a
Cont to allow the code to be tested in a Haskell program.)
Peirce's law gives the program full control over its own state (i.e. stack frame). The application of
callCC to a callee
g :: (a -> Cont r) -> Cont a bestows upon it the power of a nonlocal jump:
example :: Cont String example = callCC $ \ yield -> do yield "escaped" pure "stayed"
This would return
"escaped" rather than
"stayed". It's as if the inner function performed a
longjmp to the outer scope, passing the result along the way.
doubleNegationElimination can be expressed in terms of
doubleNegationElimination :: ((a -> Cont Void) -> Cont Void) -> Cont a doubleNegationElimination doubleNegation = callCC $ \ yield -> do void <- doubleNegation $ \ x -> yield x -- goodbye! absurd void
From this, we can see the loophole: by passing in a continuation
a -> Cont Void into the
doubleNegation :: (a -> Cont Void) -> Cont Void, the program can capture and send the result to the caller through a non-local jump. The remaining part involving
absurd is just to satisfy the type checker.
For example, if the
doubleNegation was constructed like this:
doubleNegation :: (String -> Cont Void) -> Cont Void doubleNegation negation = negation "strings do exist"
doubleNegationElimination would be able to manifest the evidence
"strings do exist" by capturing the value and then immediately jumping to the outer scope, avoiding the crash that would have arisen from evaluating a
On a sidenote,
callCC is crazy powerful. You can implement Python-style generators with them!
import Control.Monad.Cont (MonadCont, MonadIO, (<=<), callCC, forever, liftIO, runContT) import Data.Foldable (for_) import Data.IORef (IORef) import Data.Void (Void, absurd) import qualified Data.IORef as IO main :: IO () main = runContT generatorExample pure generatorExample :: (MonadCont m, MonadIO m) => m () generatorExample = callCC $ \ stop -> do g <- newGenerator [0 .. 9 :: Integer] forever $ do result <- g case result of Nothing -> stop () Just x -> liftIO (print x) newGenerator :: (MonadCont m, MonadIO m) => [a] -> m (m (Maybe a)) newGenerator xs = callCC' $ \ ret -> do -- rNext stores the function used to jump back into the generator rNext <- newIORef ($ Nothing) -- rYield stores the function used to jump out of the generator rYield <- newIORef <=< callCC' $ \ next -> do writeIORef rNext next ret $ do -- the generator itself is just a function that saves the current -- continuation and jumps back into the generator via rNext callCC' $ \ yield -> do readIORef rNext >>= ($ yield) for_ xs $ \ i -> do -- save the current continuation then jump out of the generator writeIORef rYield <=< callCC' $ \ next -> do writeIORef rNext next readIORef rYield >>= ($ Just i) readIORef rYield >>= ($ Nothing) -- | This is just double negation elimination under a different name, which -- turns out to be a little more convenient than 'callCC' here. callCC' :: MonadCont m => ((a -> m Void) -> m Void) -> m a callCC' action = callCC ((absurd <$>) . action) newIORef :: MonadIO m => a -> m (IORef a) newIORef value = liftIO (IO.newIORef value) readIORef :: MonadIO m => IORef a -> m a readIORef ref = liftIO (IO.readIORef ref) writeIORef :: MonadIO m => IORef a -> a -> m () writeIORef ref value = liftIO (IO.writeIORef ref value)