How to break the infinite loop

It's easy to create an infinite loop in Haskell.

main = mapM_ print [1..]
-- 1
-- 2
-- 3
-- ...

Of course, you can create infinite loops in other languages as well with while(1), but can you break and escape from the infinite loop as you do in an imperative programming language?

Here's how we can do it in Haskell.

import Control.Monad.Cont

main :: IO ()
main = do
  putStrLn "Start"

  withBreak $ \break ->
    forM_ [1..] $ \i -> do
      liftIO . putStrLn $ "Loop: " ++ show i
      when (i == 5) $ break ()

  putStrLn "End"
  where
    withBreak = flip runContT pure . callCC

and run it.

$ runhaskell Main.hs
Start
Loop: 1
Loop: 2
Loop: 3
Loop: 4
Loop: 5
End

Most important part is here.

withBreak $ \break ->
  forM_ [1..] $ \i -> do
    liftIO . putStrLn $ "Loop: " ++ show i
    when (i == 5) $ break ()

Here is the same code in C.

int i = 0;
while (1) {
  i++;
  printf("Loop: %d\n", i);
  if (i == 5) break;
}

I'll explain withBreak later in this article. forM_ is implemented simply as a function with flipped mapM_ arguments.

forM_ :: (Monad m) => [a] -> (a -> m b) -> m ()
forM_ = flip mapM_

liftIO is a function for using IO actions in withBreak, and when executes the second argument only when the condition of the first argument is satisfied.

The list passed to forM_ is [1..], which is indeed an infinite list, but as you can see in the execution result, the process ends with break.

First, let's look at the implementation of withBreak.

withBreak = flip runContT pure . callCC

The two most important ones are runContT and callCC.

runContT :: ContT r m a -> (a -> m r) -> m r

callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a

ContT is called a continuation monad, which is a monad that can handle subsequent calculations.

In fact, the break in withBreak $ \break -> ... just throws away the subsequent calculation.

Let's break down withBreak further to understand what's going on here. First of all, ContT is defined like this, which is just isomorphic to (a -> m r) -> m r.

newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r }

The implementation of callCC is

callCC :: ((a -> ContT r m b) -> ContT r m a) -> ContT r m a
callCC f = ContT $ \ c -> runContT (f (\ x -> ContT $ \ _ -> c x)) c

, but if you try hard to rewrite it using isomorphic, it becomes

callCC :: ((a -> (b -> m r) -> m r) -> (a -> m r) -> m r) -> (a -> m r) -> m r
callCC f c = f (\x _ -> c x) c

. The type has become more complex, but the implementation has become very easy. With this, withBreak will be

withBreak :: ((a -> (b -> m r) -> m r) -> (a -> m r) -> m r) -> m r
withBreak f = f (\x _ -> pure x) pure

. The correspondence to f in the first program is \break -> ....　Finally, it turns out that break is

break :: a -> (b -> m r) -> m r
break = \x _ -> pure x

.

Let's go back to the continuation monad again. The implementation of the ContT monad is as follows.

instance Monad (ContT r m) where
  return x = ContT ($ x)
  m >>= k  = ContT $ \c -> runContT m (\x -> runContT (k x) c)

Let's rewrite >>= according to isomorphic of ContT.

(>>=) :: ((a -> m r) -> m r) -> (a -> ((b -> m r) -> m r)) -> (b -> m r) -> m r
m >>= k = \c -> m (\x -> (k x) c)

Again, the type is more complex, but the implementation is easier to read. If you look at the implementation, you'll see that it evaluates k and then uses that value to evaluate m.

Now that we are ready, let's consider the following expression to see the behavior of break.

actionA >> break () >> actionB

First, expand the >> on the left side.

(\c -> actionA (\_ -> break () c)) >> actionB

Next, expand break.

(\c -> actionA (\_ -> pure ()) >> actionB

At this point, we can see that the subsequent calculation c has disappeared.

Expand the last remaining >>.

\c -> actionA (\_ -> pure ())

actionB has disappeared nicely.

Finally, let's go back to the first program.

withBreak $ \break ->
  forM_ [1..] $ \i -> do
    liftIO . putStrLn $ "Loop: " ++ show i
    when (i == 5) $ break ()

As we've already seen, once i reached 5 and break was evaluated, the infinite calculations that followed were discarded.

Comments

[raducu427]

Interesting, I once needed to break out of an possible infinite effectfull loop so I've write an apomorphism based on the free monad