Control.Monad.Eval

The simplest stack-safe monadic evaluation

Definitions

data Eval : Type -> Type

  The simplest monad of stack-safe pure computations
  
  This is effectively an `Identity` monad with stack-safe implementations
  of standard combinators.
  
  It can be used as a simplest transformation of a pure functional
  non-stack-safe code to stack-safe one with minimal changes in code.
  
  For example, consider the tree data type example and ordinary
  non-stack-safe implementation of `Functor` for it:
  
  ```idris
  data Tree a = Leaf a | Node a (List1 (Tree a))
  
  Functor Tree where
    map f (Leaf x)    = Leaf $ f x
    map f (Node x xs) = Node (f x) $ map @{Compose} f xs
  ```
  
  Using the `Eval` monad, you can turn it do a stack-safe one
  
  ```idris
  Functor Tree where
    map f = eval . go where
      go : Tree a -> Eval $ Tree b
      go (Leaf x)    = pure $ Leaf $ f x
      go (Node x xs) = defer $ Node (f x) <$> traverse go xs
  
  ```

Totality: total
Visibility: export
Constructors:

Pure : a -> Eval a

Bind : Eval s -> (s -> Eval a) -> Eval a

Hints:

Applicative Eval

Functor Eval

Monad Eval

MonadRec Eval

lazy : Lazy a -> Eval a

Totality: total
Visibility: export

defer : Lazy (Eval a) -> Eval a

  Suspends a lazy evaluation into the `Eval` monad
  
  This can be used to suspend the recursive calls, or the whole expressions
  containing the recursive calls, in order to provide stack-safety

Totality: total
Visibility: export

eval : Eval a -> a

Totality: total
Visibility: export