0 | ||| The simplest stack-safe monadic evaluation
 1 | module Control.Monad.Eval
 2 |
 3 | import Control.MonadRec
 4 |
 5 | %default total
 6 |
 7 | ||| The simplest monad of stack-safe pure computations
 8 | |||
 9 | ||| This is effectively an `Identity` monad with stack-safe implementations
10 | ||| of standard combinators.
11 | |||
12 | ||| It can be used as a simplest transformation of a pure functional
13 | ||| non-stack-safe code to stack-safe one with minimal changes in code.
14 | |||
15 | ||| For example, consider the tree data type example and ordinary
16 | ||| non-stack-safe implementation of `Functor` for it:
17 | |||
18 | ||| ```idris
19 | ||| data Tree a = Leaf a | Node a (List1 (Tree a))
20 | |||
21 | ||| Functor Tree where
22 | |||   map f (Leaf x)    = Leaf $ f x
23 | |||   map f (Node x xs) = Node (f x) $ map @{Compose} f xs
24 | ||| ```
25 | |||
26 | ||| Using the `Eval` monad, you can turn it do a stack-safe one
27 | |||
28 | ||| ```idris
29 | ||| Functor Tree where
30 | |||   map f = eval . go where
31 | |||     go : Tree a -> Eval $ Tree b
32 | |||     go (Leaf x)    = pure $ Leaf $ f x
33 | |||     go (Node x xs) = defer $ Node (f x) <$> traverse go xs
34 | |||
35 | ||| ```
36 | export
37 | data Eval : Type -> Type where
38 |   Pure : a -> Eval a
39 |   Bind : Eval s -> (s -> Eval a) -> Eval a
40 |
41 | export %inline
42 | lazy : Lazy a -> Eval a
43 | lazy x = Pure () `Bind` \() => Pure x
44 |
45 | ||| Suspends a lazy evaluation into the `Eval` monad
46 | |||
47 | ||| This can be used to suspend the recursive calls, or the whole expressions
48 | ||| containing the recursive calls, in order to provide stack-safety
49 | export %inline
50 | defer : Lazy (Eval a) -> Eval a
51 | defer x = Pure () `Bind` \() => x
52 |
53 | export %inline
54 | Functor Eval where
55 |   map f e = Bind e $ Pure . f
56 |
57 | export %inline
58 | Applicative Eval where
59 |   pure = Pure
60 |   f <*> x = Bind f (<$> x)
61 |
62 | export %inline
63 | Monad Eval where
64 |   (>>=) = Bind
65 |
66 | -- This implementation is indeed tail-recursive because it solely calls
67 | -- a constructor and the recursive call is suspended in a function
68 | export
69 | MonadRec Eval where
70 |   tailRecM x (Access acc) s next = next x s `Bind` \case
71 |     Done x      => Pure x
72 |     Cont y r s' => tailRecM y (acc y r) s' next
73 |
74 | export
75 | eval : Eval a -> a
76 | eval = assert_total go [] where
77 |
78 |   data FnStack : Type -> Type -> Type where
79 |     Nil  : forall a. FnStack a a
80 |     (::) : forall a, b. (a -> Eval b) -> FnStack b c -> FnStack a c
81 |
82 |   covering
83 |   go : forall a, b. FnStack a b -> Eval a -> b
84 |   go []      $ Pure x   = x
85 |   go (f::fs) $ Pure x   = go fs $ f x
86 |   go fs      $ Bind x f = go (f::fs) x
87 |