Probabilistic Effects. λθ

Continuations

What are continuations?

Continuations represent the future of a computation, as a function from an intermediate result to the final result. Direct-style functions are computations which return their result directly, with general type a -> b.

The direct-style factorial fac takes a single argument.

fac :: Integral a => a -> a
fac 0 = 1
fac n = n * fac (n - 1)

Continuation-passing-style functions are suspended computations with general type a -> (b -> r) -> r, which represent direct-style functions with type a -> b. When given both a value and another function as an argument, produces and returns a final result. The argument of type (b -> r) is the continuation - it specifies how the computation will be brought to a conclusion.

The CPS factorial facCPS takes an argument and a continuation.

facCPS :: a -> (a -> r) -> r
facCPS 0 k = k 1
facCPS n k = facCPS (n - 1) (\a -> k (n * a))

Any function calling a CPS’d function must either provide a new continuation or pass its own continuation. Also, note that it is not a necessity that the type of the non-continuation argument and the type of the continuation’s argument must coincide.

Below we have an ordinary monadic pipeline. A computation m is run - its result is fed into f, whose result is fed into g, whose result is fed into h.

m >>= f >>= g >>= h

The continuation of m is the portion of the program that executes after m. The continuation takes the value produced by m and feeds it into the rest of the program.

\x -> f x >>= g >>= h

There is a standard way to transform a program written normally or in monadic style, into a program in which continuations (represented as functions) are passed around explicitly. This is known as the CPS transform which is what the Cont/ContT monad does.

Defining Data Types in CPS

Given a data type Foo, we can create a CPS’d version of it FooCPS in the form of a newtype which contains a function unFooCPS. The type of this should be

newtype FooCPS a = FooCPS {
   unFooCPS :: forall r.
               any inputs to functions contained in constructors ->
               continuations for each constructor ->
               r
   }

Each CPS’d datatype FooCPS is accompanied by a function runFooCPS. When defining this function, it should take the CPS’d version of the data type, and return something from the original un-CPS’d type – what this is depends on the context - this can be the original un-CPS’d version of the data type, or just one of its arguments, etc. A vague example is:

runFooCPS :: FooCPS a -> Foo a
runFooCPS m = (unFooCPS m) ...

When defining the Applicative and Monad instances, the general blueprint is:

instance Applicative FooCPS where
   pure x = FooCPS (\k_1 k_2 .. -> k_i x)
   (FooCPS mf) <*> (FooCPS mx) =
      FooCPS (\k_1 k_2 .. ->
                  mf k_1 (\f -> mx k_1 (\x -> k_i (f x))))

instance Monad FooCPS where
   return = pure
   (FooCPS mx) >>= f =
      FooCPS (\k_1 k_2 .. ->
                  mx k_1 (\x -> (unFooCPS $ f x) k_1 k_2 ..))

Embedded inside the FooCPS constructor is a lambda function which takes as inputs the continuations k_1, k_2, etc. representing the continations needed for each constructor case in FooCPS. The body of the lambda function then uses mf and mx to figure out how to return the type r.

In the applicative case, as mf and mx both share the same general function type (found in FooCPS), they must each be passed the necessary continuations for each constructor case. For mf, one of these continuations describes how to continue in the situation that we are given an f. Inside that continuation, we then use mx where one of its continuations describes how to continue in the situation that we are given an x. Inside that continuation, we apply f to x, and then apply the correct continuation k_i to the result, which describes what we do with the final result f x.

In the monad case, we only need to use mx and provide it with its continuations. One of these continuations describes how to proceed when we are given an x – in this case, we first apply f :: a -> FooCPS b to x :: a to create a type f x :: FooCPS b. Finally, to continue we must then extract the function inside FooCPS b by calling unFooCPS, and pass it the necessary continuations k_1, k_n, etc. that we were given at the start.

• Trace

data Trace a
  = Trace
      { variables :: [Double],
        output    :: a,
        density   :: (Log Double)
      }

instance Applicative Trace where
  pure x = Trace {variables = [], output = x, density = 1}
  tf <*> tx =
    Trace
      { variables = variables tf ++ variables tx,
        output = output tf (output tx),
        density = density tf * density tx
      }

instance Monad Trace where
  t >>= f =
    let t' = f (output t)
     in t' {variables = variables t ++ variables t', density = density t * density t'}

newtype TraceCPS a = TraceCPS { unTraceCPS :: forall r. ([Double] -> a -> Log Double -> r) -> r }

runTraceCPS :: TraceCPS a -> Trace a
runTraceCPS m = (unTraceCPS m) Trace

instance Applicative TraceCPS where
  pure x = TraceCPS (\k -> k [] x 1)
  (TraceCPS mf) <*> (TraceCPS mx) =
    TraceCPS (\k ->
      mf (\v f d -> mx (\v' x d' -> k (v ++ v') (f x) (d * d') ) ) )

instance Monad TraceCPS where
  return = pure
  (TraceCPS mx) >>= f =
    TraceCPS (\k ->
      mx (\v x d -> (unTraceCPS $ f x) (\v' x' d' -> k (v ++ v') x' (d * d') ) ) )

• Maybe

data Maybe a = Just a | Nothing

newtype MaybeCPS a = MaybeCPS { unMaybeCPS :: forall r. (a -> r) -> (() -> r) -> r }
-- or
newtype MaybeCPS a = MaybeCPS { unMaybeCPS :: forall r. (a -> r) -> r -> r }

runMaybeCPS :: MaybeCPS a -> Maybe a
runMaybeCPS m = (unMaybeCPS m) Just (\() -> Nothing)
-- or
runMaybeCPS m = (unMaybeCPS m) Just Nothing

instance Applicative MaybeCPS where
  pure a = MaybeCPS (\k_just k_nothing -> k_just a)
  (MaybeCPS mf) <*> (MaybeCPS mx) =
    MaybeCPS (\k_just k_nothing ->
                mf (\f -> mx (\x -> k_just (f x)) k_nothing) k_nothing)

instance Monad MaybeCPS where
  return               = pure
  (MaybeCPS mx) >>= f  =
    MaybeCPS (\k_just k_nothing ->
                mx (\x -> unMaybeCPS (f x) k_just k_nothing) k_nothing)

For multiple constructor data types, as this is a coproduct, we require a continuation for each possible constructor case.

• Either

data Either e a = Left e | Right a

newtype EitherCPS e a = EitherCPS { unEitherCPS :: forall r. (e -> r) -> (a -> r) -> r }

runEitherCPS :: EitherCPS e a -> Either e a
runEitherCPS m = (unEitherCPS m) Left Right

instance Applicative (EitherCPS e) where
  pure x = EitherCPS (\k_left k_right -> k_right x)
  (EitherCPS mf) <*> (EitherCPS mx) =
    EitherCPS (\k_left k_right ->
                 mf k_left (\f -> mx k_left (\x -> k_right (f x))))

instance Monad (EitherCPS e) where
  return = pure
  (EitherCPS mx) >>= f =
    EitherCPS (\k_left k_right ->
                 mx k_left (\x -> unEitherCPS (f x) k_left k_right ))

• Writer

newtype Writer w a = Writer { runWriter :: (a, w) }

newtype WriterCPS w a = WriterCPS { unWriterCPS :: forall r. (a -> w -> r) -> r}

runWriterCPS :: Monoid w => WriterCPS w a -> (a, w)
runWriterCPS m = (unWriterCPS m) (\a w -> (a, w))

instance Monoid w => Applicative (WriterCPS w) where
  pure x = WriterCPS (\k -> k x mempty)
  (WriterCPS mf) <*> (WriterCPS mx) =
    WriterCPS (\k ->
      mf (\f w1 -> mx (\x w2 -> k (f x) (w1 `mappend` w2))))

instance Monoid w => Monad (WriterCPS w) where
  return = pure
  (WriterCPS mx) >>= f =
    WriterCPS (\k ->
      mx (\x w1 -> unWriterCPS (f x) (\x' w2 -> k x' (w1 `mappend` w2))))

• Reader

newtype Reader env a = Reader { runReader :: env -> a }

newtype ReaderCPS env a = ReaderCPS { unReaderCPS :: forall r. env -> (a -> r) -> r }

runReaderCPS :: Monoid env => ReaderCPS env a -> env -> a
runReaderCPS m env = (unReaderCPS m) env (\a -> a)
-- or
runReaderCPS m env = (unReaderCPS m) env id

instance Applicative (ReaderCPS env) where
  pure x = ReaderCPS (\env k -> k x)
  (ReaderCPS mf) <*> (ReaderCPS mx) =
    ReaderCPS (\env k ->
      mf env (\f -> mx env (\x -> k (f x) ) ) )

instance Monad (ReaderCPS env) where
  return = pure
  (ReaderCPS mx) >>= f =
    ReaderCPS (\env k ->
      mx env (\x -> (unReaderCPS $ f x) env k) )

• State

newtype State s a = State { runState :: s -> (a, s) }

newtype StateCPS s a = StateCPS { unStateCPS :: forall r. s -> (a -> s -> r) -> r }

runStateCPS :: StateCPS s a -> s -> (a, s)
runStateCPS m s = (unStateCPS m) s (\a s' -> (a, s))

instance Applicative (StateCPS s) where
  pure x = StateCPS (\s k -> k x s)
  (StateCPS mf) <*> (StateCPS mx) =
    StateCPS (\s k -> mf s (\f s' -> mx s' (\x s'' -> k (f x) s'')))

instance Monad (StateCPS s) where
  return = pure
  (StateCPS mx) >>= f =
    StateCPS (\s k -> mx s (\x s' -> (unStateCPS $ f x) s' k))

• MaybeT

newtype MaybeT m a = MaybeT { runMaybeT :: m (Maybe a) }

newtype MaybeTCPS m a = MaybeTCPS { unMaybeTCPS :: forall r. (a -> m r) -> (() -> m r) -> m r }
-- or
newtype MaybeTCPS m a = MaybeTCPS { unMaybeTCPS :: forall r. (a -> m r) -> m r -> m r }

runMaybeTCPS :: Monad m => MaybeTCPS m a -> m (Maybe a)
runMaybeTCPS m = (unMaybeTCPS m) (return . Just) (return . Nothing)
-- or
runMaybeTCPS m = (unMaybeTCPS m) (return . Just') (return Nothing)

• EitherT

newtype EitherT e m a = EitherT { runEitherT :: m (Either e a) }

newtype EitherTCPS e m a = EitherTCPS { unEitherTCPS :: forall r. (e -> m r) -> (a -> m r) -> m r }

runEitherTCPS :: Monad m => EitherTCPS e m a -> m (Either e a)
runEitherTCPS m = (unEitherTCPS m) (return . Left') (return . Right')

• WriterT

newtype WriterT w m a = Writer { runWriterT :: m (a, w) }

newtype WriterTCPS w m a = WriterTCPS { unWriterTCPS :: forall r. (a -> w -> m r) -> m r}

runWriterTCPS :: Monad m => WriterTCPS w m a -> m (a, w)
runWriterTCPS m = (unWriterTCPS m) (\a w -> return (a, w))

• ReaderT

newtype ReaderT env m a = Reader { runReaderT :: env -> m a }

newtype ReaderTCPS env m a = ReaderTCPS { unReaderTCPS :: forall r. env -> (a -> m r) -> m r }

runReaderTCPS :: (Monoid env, Monad m) => ReaderTCPS env m a -> env -> m a
runReaderTCPS m env = (unReaderTCPS m) env (\a -> return a)

• StateT

type State s = StateT s Identity
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }

newtype StateTCPS s m a = StateTCPS { unStateTCPS :: forall r. s -> (a -> s -> m r) -> m r }

runStateTCPS :: Monad m => StateTCPS s m a -> s -> m (a, s)
runStateTCPS (StateTCPS f) s = f s (\x s' -> return (x, s))

instance Applicative (StateTCPS s m) where
  pure x = StateTCPS (flip ($ x))
  (StateTCPS mx) <$> (StateTCPS my) =
      StateTCPS (\s k -> mf s (\f s' -> mx s' (\x s'' -> k (f x) s'')))

instance Monad (StateTCPS s m) where
  return = pure
  (StateTCPS mx) >>= f =
   StateTCPS (\s k -> mx s (\x s' -> unStateTCPS (f x) s' k))

With constructors containing functions, when CPS’ing, the inputs stay as inputs, the outputs get turned into a function, and then we can also curry the function when otherwise we would have returned a tuple.

• ParsecT

type ParsecT m a = StateT String (MaybeT m) a
-- or
newtype ParsecT m a = ParsecT { runParsecT :: String -> m (Maybe (a, String)) }

data ParsecTCPS m a = ParsecTCPS { unParsecTCPS :: forall r. String -> (String -> a -> m r) -> (String -> m r) -> m r }

runParsecTCPS :: Monad m => ParsecTCPS m a -> String -> m (Maybe (a, String))

  • MN: I’m seeing two different versions of what the result r is when CPS’ing data types, for instance:

    newtype Maybe a = Maybe { unMaybe :: forall r. (a -> r) -> r}

    and

    newtype Maybe a = Maybe { unMaybe :: forall r. (a -> Maybe r) -> Maybe r}

    Are either/both correct?

  • JW: Neither is correct. They are both missing the Nothing continuation. However, the first is more correct. The second is technically more correct without the second continuation, but is far too strong. We want the r to be as weak as possible. Your second one is the codensity maybe.

The Cont monad

• The Cont type

Continuations, represented as a -> r, are functions that take some value of type a produced by the current computation, and return the final result of type r from it.

newtype Cont r a = Cont { runCont :: (a -> r) -> r }

The type Cont r a represents a continuation-passing-style function (a -> r) -> r that takes a single continuation as its only input - (instances of these will be referred to as Cont objects in this explanation). In other words, it is a function that:

  1. Takes a continuation a -> r as an argument
  2. Does whatever it needs to do
  3. Produces a value of type r at the end, presumably by invoking the continuation.

• Sequencing continuation-style computations

Cont objects can be chained together. The way they chain is the way Cont works: each object in the chain invokes a continuation that makes sure that the next object’s computation is prepended to the final continuation.

To elaborate, let’s say we have a chain of Cont objects, f1 -> f2 -> f3 and we have a continuation k3 that we want to pass to the chain. Then:

  • f3 needs to invoke a continuation k3 when it’s done.
  • f2 needs to invoke a continuation k2, which will invoke f3 which will invoke k3.
  • f1 needs to invoke a continuation k3, which will invoke f2 which will invoke k2, which will invoke f3 which will invoke k3.

To chain the Cont objects together, we need to create the appropriate continuations k1 and k2 and make sure they get passed as the continuation argument to f1 and f2 respectively.

• Defining Cont as a Monad

Extending the concept of the Cont type to the Monad class involves allowing for the value of one computation to affect which Cont object gets invoked next. In this context:

  • Ignoring the Cont newtype constructor, return is defined as:

    return :: a -> (a -> r) -> r
return x = \k -> k x

    It takes a value and produces a Cont object which passes that value to its continuation.

    Using the Cont constructor, return is defined as:

    return :: a -> Cont r a
return x = Cont $ \k -> k x

  • Ignoring the Cont newtype constructor, the definition of (>>=) is:

    (>>=) :: ((a -> r) -> r) -> (a -> (b -> r) -> r) -> (b -> r) -> r
(mx >>= f) k = mx (\x -> f x k)

    So given:

    (>>=) mx f k
    • The mx is the first thing the computation can do, but it needs to know what it can do after it’s done.
    • The f needs an a from the first computation, but it also needs to know what to do after it’s done.
    • The continuation k is what the entire computation has been told to do next; this is what f should do after it’s done.

    Hence now we can see that once we’ve done mx, we need to use its value to give to f, which finishes off by performing k. This is expressed in the definition for (>>=):

    (mx >>= f) k = mx (\x -> f x k)

    Using the Cont constructor, (>>=) is defined as:

    (>>=) :: Cont r a -> (a -> Cont r b) -> Cont r b
mx >>= f = Cont $ \k -> runCont mx $ \x -> runCont (f x) k

    So this says: run mx’s computation, and after it’s done, run the continuation \x -> runCont (f x) k - this consists of mx passing its output x to f to run the computation f x, and after it’s done, run the continuation k.

• Using Continuations to implement tail recursion

Consider the function fib:

fib :: Int -> Int
fib 0 = 1
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

It would be nice if this were tail recursive - we can achieve this by using continuations. Instead of returning an integer, fibCPS will take a continuation which tells it what to do next. What can happen after fib is arbitrary, so we represent this with r:

fibCPS :: Int -> (Int -> r) -> r
fibCPS 0 k = k 1
fibCPS 1 k = k 1
fibCPS n k = fibCPS (n - 1) $ \x -> fibCPS (n - 2) $ \y -> k (x + y)

Here we are explicit about what we want to happen after each fibCPS call. In any case where we would have previously returned from the fib, we instead call the next function k.

Naturally, it’s a pain to write functions like this, which is why the Cont monad is a thing; it abstracts the pattern (a -> r) -> r found in fibCPS. Using Cont, we can just write:

fibCPS' :: Int -> Cont r Int
fibCPS' 0 = return 1
fibCPS' 1 = return 1
fibCPS' n = (+) <$> fib'' (n - 1) <*> fib'' (n - 2)
-- or equivalently using (>>=) instead of applicative style
fibCPS' n = fib'' (n - 1) >>= \x -> fib'' (n - 2) >>= \y -> return (x + y)

• CallCC

Cont r a is simply a newtype wrapper around (a -> r) -> r. The continuation a -> r is “hidden” by Cont r a in the sense that the normal code we write in the Cont monad doesn’t explicitly see the continuation - it’s all handled under the hood by the monad instance. So how do we manipulate the continuations using Cont r a?

An extension to the Cont monad is the MonadCont class which provides a callCC operation - this exposes the hidden continuation in Cont r a by introducing the (a -> m b) parameter in the (a -> m b) -> m a function; that is the continuation that follows from this line in the do block (and this is normally hidden inside the monad).

The definition of the function callCC is given below:

callCC :: ((a -> m b) -> m a) -> m a
callCC fk = Cont (\k -> runCont (fk (\x -> Cont (\_ -> k x))) k)

We can see that k is provided as the continuation to fk, but fk is also given an escape continuation that when used, ignores the continuation it was told to do next and uses k instead. The \_ expresses ignoring the continuation it was given.

The function callCC stands for “call with current continuation” and it brings the current continuation into scope. This is the idea that we can create an escape hatch. The code that happens after is packaged up into a function of type a -> m b, and we run a “program” (a -> m b) -> m a which says “if you tell me how to continue with the computation after i’m done, then i can do something”. Crucially, we don’t have to use the escape continuation - we could always just reach the end of the fragment normally. The computation always returns a type a, but we can escape mid-way through by calling the function with an a. It can thought of like a go-to instruction.

  • The type (a -> m b) is the actual exit mechanism.
  • The whole thing of type (a -> m b) -> m a is the computation that wants an exit mechanism. The exit mechanism is (\x -> Cont (\_ -> k x)).

Importantly, by exposing the hidden continuation inside Cont, the function callCC allows to name our continuations. This means we can call a named continuation at any time to jump to that point in the code, and we can reuse and invoke these continuations as many times as we like, with different arguments.

A good example is writing a little virtual machine. When we execute the halt function, we would like to exit the interpreter - but we might be very deep inside the interpreter and we don’t want to have to unwind it and check at each step whether the machine halted or not. Hence, callCC provides the mechanism to do that for us. Below we have named our continuation as exit.

do callCC (\exit -> executeMachine ... exit)
   ... -- do something after the machine has finished running

executeMachine Halt exit = exit ()

And this lets us magically escape. We can implement exceptions this way - callCC is a try/catch mechanism and is very powerful.

Example of CallCC

The following program:

validateName name exit = do
  when (null name) (exit "you forgot to tell me your name")

whatsYourName :: String -> Cont r String
whatsYourName name =   do 
  response <- callCC $ \exit -> do
    validateName name exit
    return $ "welcome, " ++ name
  return response

Inlines to:

whatsYourName :: String -> Cont r String
whatsYourName name = 
  cont (\k -> runCont (do validateName name (\x -> cont (\_ -> k x))
                          return $ "welcome, " ++ name
                      ) k
       )

In other words, the exit mechanism that callCC produces is always (\x -> cont (\_ -> k x)). Therefore, calling exit on some value x will always ignore the following continuation in the do block (i.e. return $ "welcome, " ++ name); this is shown by the snippet \_ -> k x. The continuation k is the final continuation that we want to apply, and it is passed to the runCont used to run the entire computation: for example id in runCont (whatsYourName "minh") id.

Here’s an example where we always exit with the string “exited”, and never return the name.

whatsYourName :: String -> Cont r String
whatsYourName name = do
  response <- cont (\k -> runCont (do (\x -> cont (\_ -> k x)) "exited"
                                      return $  name
                                  ) k
                   )
  return response

-- Below is type `Cont r a` because `cont` takes a parameter of type (a -> m r),
-- but since the type `a` is ignored in `\_ -> id x`, we can't concretise it.
(\x -> cont (\_ -> x)) :: r -> Cont r a
-- If we then pass it a type `String` as `r`, then `r` becomes concretised.
(\x -> cont (\_ -> id x)) "name"             :: Cont String a
-- Below is type `Cont String ()` because `when` has type (Bool -> f () -> f ()), so 
-- we can infer that the type `a` must be concretised as `()`.
when True ((\x -> cont (\_ -> id x)) "name") :: Cont String ()
-- If we pass `undefined` to the exit mechanism, then we haven't yet defined what the
-- type of the result is yet.
when True ((\x -> cont (\_ -> id x)) undefined) :: Cont r ()

Because k :: String -> r, we force the value that is passed to exit to be a string.

• CallCC and When: Implementing imperative-style return statements

We can also use callCC to implement “imperative style” return statements.

import Control.Monad.Cont

weirdFib :: Int -> Int
weirdFib n = flip runCont id $
   let impFib n = callCC $ \ret ->
         do when (n == 0) (ret 1)
            when (n == 1) (ret 1)
            x <- impFib (n - 1)
            y <- impFib (n - 2)
            return (x + y)
   in  impFib n

The definition of the function ret is given below:

ret :: a -> (b -> a)
ret x = \_ -> id x

Whenever the function ret is used, it acts like a real return statement in an imperative language. If n == 0, then it will call ret 1 which in this case ignores the continuation (which would be \_ -> when (n == 1) ...) and escapes immediately. The definition of ret here specifically would be \x -> Cont (\_ -> id x) because nothing follows the callCC and nothing follows impFib n, so the continuation will be id as given in the first line of the function. So ret in some sense has exposed the continuation id to the rest of the program.

The definition of the function when is given below:

when :: Monad m => Bool -> m () -> m ()
when True  mx = mx
when False _  = return ()
--- and below is the Cont specific version of "when"
when :: Bool -> ((() -> r) -> r) -> (() -> r) -> r
when False _ k = k ()
when True mx k = mx k

How the function when works along with (>>=) is the following:

For the case of when True ...:

do when True mx
   x <- impFib (n - 1)
   ...

-- evaluates to:

mx (\_ -> impFib (n - 1) (\x -> ...))

For the case of when False ...:

do when False mx
   x <- impFib (n - 1)
   ...

-- evaluates to:

when False mx (\_ -> impFib (n - 1) (\x -> ...))

-- which evaluates to:

(\_ -> impFib (n - 1) (\x -> ...)) ()

• CallCC and When: Deriving an incorrect example program

To give a sense of what happens when we use callCC in the wrong place, consider the following code (which may look plausible from a first glance):

weirdFib :: Int -> Int
weirdFib n = flip runCont id $ callCC $ \ret ->
   let impFib n =
         do when (n == 0) (ret 1)
            when (n == 1) (ret 1)
            x <- impFib (n - 1)
            y <- impFib (n - 2)
            return (x + y)
   in  impFib n

However, this program always returns 1. To see why, let’s evaluate impFib 2 with ret x = \_ -> id x.

impFib 2 k

= {- both "when"'s are "return ()" so I've omitted them -}
  ...
  x <- impFib (n - 1)
  y <- impFib (n - 2)
  return (x + y)


= {- expanding out impFib -}
  ...
  x <- do when (n == 0) (ret 1)
          when (n == 1) (ret 1)
          x' <- impFib (n - 1)
          ...
  y <- do when (n == 0) (ret 1)
          when (n == 1) (ret 1)
          ...
  return (x + y)


= {- when False _ k = k () -}
  {- (mx >>= f) k = mx (\x -> f x k) -}
  ...
  x <- (when (n == 1) (ret 1) (\_ -> impFib (n - 1) (...))) ()
  y <- do when (n == 0) (ret 1)
          when (n == 1) (ret 1)
          ...
  return (x + y)


= {- when True mx k = mx k -}
  {- (mx >>= f) k = mx (\x -> f x k) -}
  ...
  x <- (ret 1) (\_ -> impFib (n - 1) (...)) ()
  y <- (ret 1) (\_ -> when (n == 1) (ret 1) (...))


= {- ret x = \_ -> id x -}
  ...
  x <- \_ -> id 1
  y <- \_ -> id 1
  return (x + y)


= {- (mx >>= f) k = mx (\x -> f x k) -}
  ...
  (\_ -> id 1) (\x -> (\_ -> id 1) (\y -> return (1 + 1)))

= id 1

= 1
Last updated on 13 Nov 2020
Published on 13 Nov 2020