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)

writeIORef ref value = liftIO (IO.writeIORef ref value)