Today’s shower thought is: Is there a way to interpret double negation elimination as a program?

((a -> Void) -> Void) -> a

(Here, 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 a?

A hint comes from Peirce’s law, also known as call-with-current-continuation, which has a similar form:

callCC :: ((a -> Cont r) -> Cont a) -> Cont a

(We use 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 goto/return/break/longjmp to the outer scope, passing the result along the way.

Turns out doubleNegationElimination can be expressed in terms of callCC:

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"

then 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 Void.

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)