-- | -- Module : Control.Monad.Stepwise -- Copyright : Arie Middelkoop -- License : LGPL -- -- Maintainer : ariem@cs.uu.nl -- Stability : experimental -- Portability : non-portable (GADTs) -- -- Note: Some documentation may not be visible in the Haddock documentation; -- also check the comments directly in the source code. -- -- A module for the step-wise evaluation of pure computations, in particular -- suitable to resolve non-deterministic choices in computations. -- -- This module provides a monadic interface for a special form of pure -- /coroutines/ that, upon disgression of the caller, yield lazily the result -- of the coroutine, or evaluates strictly until it can yield next -- callee-determined progress report. -- Due to the monadic interface, such a coroutine is an ordinary composable -- monadic haskell function, with the exception that it may be decorated with -- statements that yield progress reports. -- Both the result and progress reports are purely functional: given an -- expression written with this interface, the evaluated value as well as all the -- progress reports are uniquely determined by the values for the free variables -- of the expression. -- -- Given such a coroutine @m@, we can both refer to its progress reports and its -- value from another coroutine. Given a coroutine @m@, the conventional way to -- access its value is via a coroutine @m >>= f@, where @f@ is itself a coroutine -- that takes @m@'s value as parameter. -- The progress reports of @m@ are incorporated as part of the progress reports of -- @m >>= f@, ordered such that the progress reports of @m@ are emitted before -- those of @f@. -- Alternatively, we can ask @m@ to yield the next progress report via -- @smallStep m@. This returns a progress report, and an updated coroutine to be -- used as continuation. In this case, @m@ evaluated one step, hence 'step-wise'. -- -- Stepwise evaluation provides a means to encode non-deterministic choices in -- a deterministic way via advanced search strategies. For example, with this -- module, we can define a coroutine that determines its result by making a -- choice between the results of two other coroutines. For that, we step through -- the evaluation of both coroutines until we saw sufficient progress reports -- to make a choice. Meanwhile, we already yield progress reports. Finally, we -- make a choice by integrating the coroutine in the conventional way. -- Consequently, the choice is optimized away, and the coroutine that is not -- selected becomes garbage. -- -- With this approach, we encode a breadth-first evaluation by letting each -- couroutine emitting steps regularly, and alternate the coroutine to take -- steps from. We get depth-first behavior by fully -- stepping through one of the choices first before considering the other -- choice. Custom strategies are possible by emitting progress reports. For -- example, a coroutine can emit statistics about the work done so far and -- predictions of the work still to do to produce the result, which can -- subsequently be used to direct the evaluation process. -- -- A coroutine has the type @BF e i w a@, where @a@ is the final result -- computed by the coroutine. Such a computation may fail, with reasons -- indicated by the type @e@. Progress reports are of the type @i w@, -- i.e. parameterized in the type of a /watcher/ @w@. A watcher is a -- type index that allows the progress reports to be different depending -- on the caller of a coroutine: both the callee and its caller (and the -- caller's caller, etc.) coroutines must share the same type @i@ for -- progress reports. Specific callee/caller combinations may decide on -- a common type @w@ to communicate special-typed progress information. -- To emit such a progress report to a caller with a different watcher-type, -- it has to be /transcoded/ first via e.g. 'transcode'. -- -- In some situations, the choice between a coroutine @a@ and @b@ may -- depend on what happends when we pick i.e. @a@ and our caller continues -- its evaluation. For example, suppose that the continued evaluation is -- represented by some unknown coroutine @r@, and we we define a coroutine -- @c = choice a b@. This means that the actual evaluation is @choice a b >>= r@. -- We may want to lift this choice over @r@, to @choice' (a >>= r) (b >>= r)@. -- Since @r@ is unknown, @choice'@ cannot base its choice on the value -- computed by @a >>= r@ or @b >>= r@. Both the type of the result and the -- watcher type are existential. However, we can inspect if one of -- the alternatives fails, and inspect progress reports that are independent of -- the watcher type. -- We provide this choice-lifting via a special operation call 'lookahead'. -- It provides us with our continuation @r@, and we must define the coroutine -- denoting @c' >>= r@, where @c'@ denotes our choice. -- This lifting comes with a price: requesting a step from a coroutine may -- require us to provide it a continuation that represents what we are -- going to do afterwards with it. For example, if we pass 'return', there -- is no lookahead beyond the evaluation of the coroutine. However, if we -- pass the continuation obtained through @lookahead@, we potentially look -- ahead through a possible future. -- The difference between progress report type and watcher type is important -- here. We cannot make assumptions about the wachter of the continuation: -- but we do know that we get progress reports of type @i@ with unspecified -- watcher type. -- -- When we request a step from @e = m >>= f@, we gradually reduce it until -- it emits the next progress report. It first gradually reduces @m@. When -- it is entirely finished with @m@, it continues with @f@, after parametrizing -- it with the value computed for @m@. However, given such a partially reduced -- @e' = m' >>= f'@, when we ask for the @lazyEval e@, we immediately get the -- result @lazyEval (f' (lazyEval m'))@. 'lazyEval' discards any progress -- reports and immediately produces a lazy result. When @f@ is not strict in -- its first argument, this means that a value can already be produced, possibly -- without even evaluating the remainder of @m'@. For example, @lazyEval (choice a b)@ -- strictly evaluates @a@ and @b@ as long as it is asking for steps. Once @choice@ -- selects one alternative, lazy evaluation takes over. This allows us to produce -- /online/ results when choices have been resolved. -- -- Benchmark results show that a 'Stepwise' bind is approximately 10 times -- slower compared to a bind of the identity monad (independent of the -- amount of binds). Stepwise evaluation of a bind via 'stepwiseEval' is only -- marginally (e.g. approx 10%) slower compared to 'lazyEval' of a bind. -- -- A downside of the monadic interface is that it requires code to be written in a -- sequential way (it enforces monadic style upon the program). -- For tree traversals, we eliminate this downside with Attribute Grammars. -- For the class of Ordered Attribute Grammars (non-cyclic tree-traversals fall in this class), -- the UUAG system has an option to automatically derive code for this library. -- -- This library is a generalization of the Steps-technique presented in -- `Polish parsers, Step by Step` by R. J. M. Hughes and -- S. D. Swierstra, and the later work in `Combinator Parsing: A Short Tutorial' by -- S. D. Swierstra. The key difference is that we do not construct a -- single function @f :: a -> b@ in @Apply f@ (as mentioned in the latter paper) that represents a continuation of -- what still needs to be computed. Instead, we explicitly build a stack of -- all pending right-hand sides @g1..gn@ that follow the currently active computation -- @m@ in @m >>= g1 >>= ... gn@. The functions @g@ on the stack thus have the monadic type -- @g :: a -> BF e i w b@. When we request a new progress report and @m@ -- is fully reduced, we reduce the pending-stack: pop off @g1@, parametrize it with -- the result of @m@, then start reducing that value. Consequently, we have no -- difficulties dealing with the monadic bind in this approach. -- This representation, however, does not impair laziness. We still manage to map this representation -- back to a function @f :: a -> b@. This transformation is performed by 'lazyEval'. -- A smaller difference is that our interface to deal with progress reports does not -- expose the above mentioned stack, which reduces complexity for the programmer. -- module Control.Monad.Stepwise ( module Control.Monad.Stepwise.Core , module Control.Monad.Stepwise.Derived ) where import Control.Monad.Stepwise.Core import Control.Monad.Stepwise.Derived import Control.Monad.Stepwise.Proofs import Control.Monad.Stepwise.Examples