0 | module Control.Monad.Free
  1 |
  2 | import Control.MonadRec
  3 | import Data.Fuel
  4 | import Data.TCQueue
  5 |
  6 | %default total
  7 |
  8 | ||| The identity function specialized to `Type`.
  9 | public export
 10 | I : Type -> Type
 11 | I t = t
 12 |
 13 | ||| A stack safe free monad implementation
 14 | ||| storing sequences of bind operations in
 15 | ||| an efficient type aligned catenable list.
 16 | public export
 17 | data Free : (f : Type -> Type) -> (a : Type) -> Type
 18 |
 19 | ||| A *view* on a free monad over functor `f`, describing
 20 | ||| it either as a pure value, or a lifted value of
 21 | ||| type `f a` followed by a bind operation.
 22 | public export
 23 | data FreeView : (f : Type -> Type) -> (a : Type) -> Type
 24 |
 25 | ||| A type aligned sequence of bind operations
 26 | ||| over `Free f`.
 27 | public export
 28 | 0 Arrs : (f : Type -> Type) -> (a,b : Type) -> Type
 29 |
 30 | data Free where
 31 |   MkFree :  {0 t : _}
 32 |          -> (view : FreeView f t)
 33 |          -> (arrs : Arrs f t a)
 34 |          -> Free f a
 35 |
 36 | data FreeView where
 37 |   Pure : (val : a) -> FreeView f a
 38 |   Bind : (f b) -> (b -> Free f a) -> FreeView f a
 39 |
 40 | Arrs = TCQueue . Free
 41 |
 42 | ||| Converts a view to the corresponding free monad. O(1).
 43 | export %inline
 44 | fromView : FreeView f a -> Free f a
 45 | fromView f = MkFree f empty
 46 |
 47 | concatF : Free f a -> Arrs f a b -> Free f b
 48 | concatF (MkFree v r) l = MkFree v (r ++ l)
 49 |
 50 | ||| Converts a free monad to a view representing it.
 51 | ||| Amortized O(1).
 52 | export
 53 | toView : Free f a -> FreeView f a
 54 | toView (MkFree v s) = case v of
 55 |   Pure val => case uncons s of
 56 |     EmptyV   => Pure val
 57 |     (h :| t) => assert_total $ toView (concatF (h val) t)
 58 |
 59 |   Bind x k => Bind x (\va => concatF (k va) s)
 60 |
 61 | --------------------------------------------------------------------------------
 62 | --          Implementations
 63 | --------------------------------------------------------------------------------
 64 |
 65 | bind : Free f a -> (a -> Free f b) -> Free f b
 66 | bind (MkFree v r) g = MkFree v $ snoc r g
 67 |
 68 | public export
 69 | Functor (Free f) where
 70 |   map g fr = bind fr (fromView . Pure . g)
 71 |
 72 | public export
 73 | Applicative (Free f) where
 74 |   pure = fromView . Pure
 75 |   f <*> v = bind f (\f => map (f $) v)
 76 |
 77 | public export %inline
 78 | Monad (Free f) where
 79 |   (>>=) = bind
 80 |
 81 | public export
 82 | MonadRec (Free f) where
 83 |   tailRecM seed (Access rec) vst step = do
 84 |     Cont s2 prf vst2 <- step seed vst
 85 |       | Done v => pure v
 86 |     tailRecM s2 (rec s2 prf) vst2 step
 87 |
 88 | ||| Lift an arbitrary functor into a free monad.
 89 | export
 90 | lift : f a -> Free f a
 91 | lift v = fromView (Bind v pure)
 92 |
 93 | export
 94 | HasIO m => HasIO (Free m) where
 95 |   liftIO = lift . liftIO
 96 |
 97 | --------------------------------------------------------------------------------
 98 | --          Running Computations
 99 | --------------------------------------------------------------------------------
100 |
101 | export
102 | wrap : f (Free f a) -> Free f a
103 | wrap x = fromView (Bind x id)
104 |
105 | export
106 | substFree : (forall x . f x -> Free g x) -> Free f a -> Free g a
107 | substFree k f = case toView f of
108 |   Pure a   => pure a
109 |   Bind g i => assert_total $ bind (k g) (substFree k . i)
110 |
111 | ||| Unwraps a single layer of `f`, providing the continuation.
112 | ||| Amortized O(1).
113 | export
114 | resume' :
115 |      (forall b. f b -> (b -> Free f a) -> r)
116 |   -> (a -> r)
117 |   -> Free f a
118 |   -> r
119 | resume' k j fr = case toView fr of
120 |   Pure a   => j a
121 |   Bind g i => k g i
122 |
123 | ||| Unwraps a single layer of the functor `f`.
124 | ||| Amortized O(1).
125 | export
126 | resume : Functor f => Free f a -> Either (f (Free f a)) a
127 | resume fr = case toView fr of
128 |   Pure a   => Right a
129 |   Bind g i => Left $ map i g
130 |
131 | ||| Apply a morphism to change a free monad's functor.
132 | export
133 | mapK : (f : forall t . m t -> n t) -> Free m a -> Free n a
134 | mapK f = substFree (lift . f)
135 |
136 | ||| Run a computation described as a free monad in
137 | ||| a stack safe manner.
138 | export
139 | foldMap : MonadRec m => (forall x . f x -> m x) -> Free f a -> m a
140 | foldMap k fr = assert_total $ trSized forever fr $ \fu,frm => case fu of
141 |   More x => case toView frm of
142 |     Pure val => Done <$> pure val
143 |     Bind g i => Cont x (reflexive {rel = LTE}) . i <$> k g
144 |   Dry    => idris_crash "Control.Monad.Free.foldFree: ran out of fuel"
145 |
146 | ||| Run a pure computation in a stack-safe manner.
147 | export
148 | run : Free I a -> a
149 | run fr = case toView fr of
150 |   Pure a   => a
151 |   Bind v f => run (assert_smaller fr $ f v)
152 |
153 | export
154 | runM :
155 |      {auto _ : Functor m}
156 |   -> {auto _ : MonadRec n}
157 |   -> (m (Free m a)
158 |   -> n (Free m a))
159 |   -> Free m a
160 |   -> n a
161 | runM g free = assert_total $ trSized forever free $ \fu,fr => case fu of
162 |   More x => case resume fr of
163 |     Right va => pure (Done va)
164 |     Left  ma => Cont x (reflexive {rel = LTE}) <$> g ma
165 |   Dry    => idris_crash "Control.Monad.Free.runM: ran out of fuel"
166 |