0 | ||| Provides a data type for Monadic Stream Functions (MSFs)
  1 | ||| together with associated interface implementations and
  2 | ||| some core functionality.
  3 | |||
  4 | ||| An MSF is an effectful computation from an input of type `i`
  5 | ||| to an output of type `o`, that can be described using a rich
  6 | ||| library of combinators and evaluated using function
  7 | ||| `Data.MSF.Running.step`,
  8 | ||| which not only produces an output for every input value
  9 | ||| but also a new MSF to be used in the next evaluation step.
 10 | module Data.MSF.Core
 11 |
 12 | import public Data.MSF.Event
 13 |
 14 | %default total
 15 |
 16 | --------------------------------------------------------------------------------
 17 | --          n-ary  sums
 18 | --------------------------------------------------------------------------------
 19 |
 20 | ||| A monadic stream function (`MSF`) is used to
 21 | ||| convert streams of input values of type `i` to
 22 | ||| output values of type `o` in a monadic context `m`.
 23 | |||
 24 | ||| The [dunai](https://hackage.haskell.org/package/dunai)
 25 | ||| library implements them as
 26 | ||| `data MSF m i o = MSF (i -> m (o, MSF m i o))`
 27 | ||| but this most general form does not go well with
 28 | ||| the Idris totality checker.
 29 | |||
 30 | ||| It is therefore implemented as a set of primitive
 31 | ||| constructors, some of which are truly primitives,
 32 | ||| some of which are there for reasons of efficiency.
 33 | ||| In later versions of this library, `MSF` might
 34 | ||| no longer be publicly exported, so client code should
 35 | ||| use the provided combinators instead of accessing the
 36 | ||| data constructors directly.
 37 | |||
 38 | ||| `MSF` objects can be stepwise evaluated by invoking
 39 | ||| function `Data.MSF.Running.step`.
 40 | public export
 41 | data MSF : (m : Type -> Type) -> (i : Type) -> (o : Type) -> Type
 42 |
 43 | ||| A heterogeneous list of MSFs all of which
 44 | ||| accept the same input type. This is used for
 45 | ||| broadcasting an input value across several MSFs,
 46 | ||| collecting the result as an n-ary product.
 47 | ||| See also function `fan`.
 48 | public export
 49 | 0 FanList : (m : Type -> Type) -> (i : Type) -> (os : List Type) -> Type
 50 | FanList m i = All (MSF m i)
 51 |
 52 | ||| A heterogeneous list of MSFs all of which
 53 | ||| produce the same type of outup. This is used for
 54 | ||| choosing a single MSF for producing a result based
 55 | ||| on an n-ary sum as input. See also function `collect`.
 56 | public export
 57 | 0 CollectList : (m : Type -> Type) -> (is : List Type) -> (o : Type) -> Type
 58 | CollectList m is o = All (\i => MSF m i o) is
 59 |
 60 | ||| A heterogeneous list of MSFs. This is used both
 61 | ||| for running several unrelated MSFs in parallel, in
 62 | ||| which case it takes an n-ary product as input
 63 | ||| and produces an n-ary product as output (see
 64 | ||| function `par`), as well as for selecting a single
 65 | ||| MSF to run based on an n-ary sum as input, in which
 66 | ||| case a value of an n-ary sum is produced as output
 67 | ||| (see function `choice` for this use case).
 68 | public export
 69 | data ParList : (m : Type -> Type) -> (is,os : List Type) -> Type where
 70 |   Nil  : ParList m [] []
 71 |   (::) :  (sf : MSF m i o)
 72 |        -> (sfs : ParList m is os)
 73 |        -> ParList m (i :: is) (o :: os)
 74 |
 75 | data MSF where
 76 |   ||| The identity MSF
 77 |   Id        :  MSF m i i
 78 |
 79 |   ||| The constant MSF
 80 |   Const     :  o -> MSF m i o
 81 |
 82 |   ||| Lifts a pure function to an MSF
 83 |   Arr       :  (i -> o) -> MSF m i o
 84 |
 85 |   ||| Lifts an effectful computation to an MSF
 86 |   Lifted    :  (i -> m o) -> MSF m i o
 87 |
 88 |   ||| Sequencing of MSFs
 89 |   Seq       :  MSF m i x -> MSF m x o -> MSF m i o
 90 |
 91 |   ||| Parallelising MSFs
 92 |   Par       :  ParList m is os -> MSF m (HList is) (HList os)
 93 |
 94 |   ||| Broadcasting a value to a list of MSFs
 95 |   ||| all taking the same input
 96 |   Fan       :  FanList m i os -> MSF m i (HList os)
 97 |
 98 |   ||| Choosing an MSF based on an n-ary sum as input
 99 |   Choice    :  ParList m is os -> MSF m (HSum is) (HSum os)
100 |
101 |   ||| Choosing an MSF (all of which produce the same output)
102 |   ||| based on an n-ary sum as input
103 |   Collect   :  CollectList m is o -> MSF m (HSum is) o
104 |
105 |   ||| Feedback loops (stateful computations)
106 |   Loop      :  s -> MSF m (HList [s, i]) (HList [s, o]) -> MSF m i o
107 |
108 |   ||| Single time switching: Upon the first event,
109 |   ||| the second stream function is calculated,
110 |   ||| evaluated immediately and used henceforth.
111 |   Switch    :  MSF m i (Either e o) -> (e -> MSF m i o) -> MSF m i o
112 |
113 | --------------------------------------------------------------------------------
114 | --          Lifting Primitives
115 | --------------------------------------------------------------------------------
116 |
117 | ||| The identity MSF
118 | export %inline
119 | id : MSF m i i
120 | id = Id
121 |
122 | ||| A constant MSF
123 | export %inline
124 | const : o -> MSF m i o
125 | const = Const
126 |
127 | ||| Lifting a pure function to an MSF
128 | export %inline
129 | arr : (i -> o) -> MSF m i o
130 | arr = Arr
131 |
132 | ||| Lifting an effectful computation to an MSF
133 | export %inline
134 | arrM : (i -> m o) -> MSF m i o
135 | arrM = Lifted
136 |
137 | ||| Lifting a value in a context to an MSF
138 | export %inline
139 | constM : m o -> MSF m i o
140 | constM = Lifted . const
141 |
142 | --------------------------------------------------------------------------------
143 | --          Sequencing MSFs
144 | --------------------------------------------------------------------------------
145 |
146 | export infixr 1 >>>
147 |
148 | ||| Sequencing of MSFs
149 | export %inline
150 | (>>>) : MSF m i x -> MSF m x o -> MSF m i o
151 | (>>>) = Seq
152 |
153 | --------------------------------------------------------------------------------
154 | --          Paralellising MSFs
155 | --------------------------------------------------------------------------------
156 |
157 | ||| Runs a bundle of MSFs in parallel. This is
158 | ||| a generalization of `(***)` from `Control.Arrow`.
159 | export %inline
160 | par : ParList m is os -> MSF m (HList is) (HList os)
161 | par = Par
162 |
163 | ||| Broadcasts an input value across a list of MSFs,
164 | ||| all of which must accept the same type of input.
165 | ||| This is a generalization of `(&&&)` from `Control.Arrow`.
166 | export %inline
167 | fan : FanList m i os -> MSF m i (HList os)
168 | fan = Fan
169 |
170 | ||| Apply a binary function to the result of running
171 | ||| two MSFs in parallel.
172 | export %inline
173 | elementwise2 : (o1 -> o2 -> o3) -> MSF m i o1 -> MSF m i o2 -> MSF m i o3
174 | elementwise2 f x y = fan [x,y] >>> arr (\[a,b] => f a b)
175 |
176 | --------------------------------------------------------------------------------
177 | --          Selecting MSFs
178 | --------------------------------------------------------------------------------
179 |
180 | ||| Choose an MSF to run depending the input value
181 | ||| This is a generalization of `(+++)` from `Control.Arrow`.
182 | export %inline
183 | choice : ParList m is os -> MSF m (HSum is) (HSum os)
184 | choice = Choice
185 |
186 | ||| Choose an MSF all of which produce the same output.
187 | ||| This is a generalization of `(\|/)` from `Control.Arrow`.
188 | export %inline
189 | collect : CollectList m is o -> MSF m (HSum is) o
190 | collect = Collect
191 |
192 | --------------------------------------------------------------------------------
193 | --          Loops and Stateful computations
194 | --------------------------------------------------------------------------------
195 |
196 | ||| Feedback loops: Given an initial state value,
197 | ||| we can feedback the result of each evaluation
198 | ||| step and us it as the new state for the next step.
199 | export %inline
200 | feedback : s -> MSF m (HList [s,i]) (HList [s,o]) -> MSF m i o
201 | feedback = Loop
202 |
203 | --------------------------------------------------------------------------------
204 | --          Interfaces
205 | --------------------------------------------------------------------------------
206 |
207 | export %inline
208 | Functor (MSF m i) where
209 |   map f = (>>> arr f)
210 |
211 | export %inline
212 | Applicative (MSF m i) where
213 |   pure = Const
214 |   (<*>) = elementwise2 apply
215 |
216 | export %inline
217 | Semigroup o => Semigroup (MSF m i o) where
218 |   (<+>) = elementwise2 (<+>)
219 |
220 | export %inline
221 | Monoid o => Monoid (MSF m i o) where
222 |   neutral = Const neutral
223 |
224 | export %inline
225 | Num o => Num (MSF m i o) where
226 |   fromInteger = Const . fromInteger
227 |   (+) = elementwise2 (+)
228 |   (*) = elementwise2 (*)
229 |
230 | export %inline
231 | Neg o => Neg (MSF m i o) where
232 |   (-)    = elementwise2 (-)
233 |   negate = map negate
234 |
235 | export %inline
236 | Integral o => Integral (MSF m i o) where
237 |   mod = elementwise2 mod
238 |   div = elementwise2 div
239 |
240 | export %inline
241 | Fractional o => Fractional (MSF m i o) where
242 |   (/)  = elementwise2 (/)
243 |
244 | export %inline
245 | FromString o => FromString (MSF m i o) where
246 |   fromString = const . fromString
247 |