
   0 | module Data.Swirl
   1 | 
   2 | import Data.Either
   3 | import Data.List.Lazy
   4 | import Data.List1
   5 | import Data.Maybe
   6 | import Data.These
   7 | 
   8 | import Control.Monad.Error.Interface
   9 | import Control.Monad.Identity
  10 | import Control.Monad.Trans
  11 | import public Control.MonadRec
  12 | import Control.WellFounded
  13 | 
  14 | import public Language.Implicits.IfUnsolved
  15 | 
  16 | %default total
  17 | 
  18 | -------------
  19 | --- Swirl ---
  20 | -------------
  21 | 
  22 | export
  23 | data Swirl : (Type -> Type) -> (error, result, output : Type) -> Type where
  24 |   Done   : r -> Swirl m e r o
  25 |   Fail   : e -> Swirl m e r o
  26 |   Yield  : o -> Lazy (Swirl m e r o) -> Swirl m e r o
  27 |   Effect : m (assert_total $ Swirl m e r o) -> Swirl m e r o
  28 |   BindR  : Lazy (Swirl m e r' o) -> (r' -> Swirl m e r o) -> Swirl m e r o
  29 |   BindE  : Lazy (Swirl m e' r o) -> (e' -> Swirl m e r o) -> Swirl m e r o
  30 |   Ensure : Lazy (Swirl m Void r' Void) -> Lazy (Swirl m e r o) -> Swirl m e (r', r) o
  31 | 
  32 | %name Swirl sw, sv, su
  33 | 
  34 | public export %inline
  35 | Swirlie : (Type -> Type) -> (error, output : Type) -> Type
  36 | Swirlie m e = Swirl m e ()
  37 | 
  38 | -- Discussion:
  39 | --
  40 | -- - `Effect` constructor.
  41 | --
  42 | --   The totality assertion is due to a functor requirement on the `m`, which
  43 | --   is used for the recursive use of the type.
  44 | --   This requirement is not depicted directly in the type of the constructor,
  45 | --   since it would lead to ambiguity errors, but it is meant to be present.
  46 | --
  47 | -- - `Ensure` constructor, output parameter of "finally" section.
  48 | --
  49 | --   The `finally` part must not emit values because of the following:
  50 | --   if the `finally` part can emit a value, it means that one can bind (`>>=`) the whole `Ensure` expression by
  51 | --   some `Swirl` which, in its order, may fail. This would lead to either ability of non-full "finally" block to be executed,
  52 | --   or the need of failure-ignoring variant of `>>=` to be used for it. Both it possible, but both are counter-intuitive.
  53 | --
  54 | --   By the way, at least at the time of writing this, the Scala's fs2 library has the same problem and generally the `release`
  55 | --   process of a bracket pattern *can* be interrupted by an exception in the RHS of the `flatMap` if it emits some values.
  56 | --
  57 | -- - `Ensure` constructor, error parameter of "finally" action.
  58 | --
  59 | --   An ability of the "finally" action to fail would lead the joining function to have the following signature
  60 | --
  61 | --   ```idris
  62 | --   squashOuts' : Functor m => Swirl m e r (Swirl m e' r' o) -> Swirl m (These e $ List1 e') (r, List r') o
  63 | --   ```
  64 | --
  65 | --   So strange resulting error type is because the error can occur in the finally section along with an error in the main section.
  66 | --   Several suberrors may occur if is was thrown in finally sections of both main section and outer error handler.
  67 | --
  68 | --   It all means that even if the error type of outer and inner `Swirl`s are the same, we cannot
  69 | --   use `Monad` signature for `>>=` and `join`.
  70 | --   Also, it means that the `finally` section of `Ensure` can be unintentionally interrupted by the subsequent binds.
  71 | --   This may lead a nessesity to use finally sections in finally sections which emit values, which all looks fragile.
  72 | --
  73 | --   That all lead to a decision of inability to fail for the "finally" action.
  74 | --
  75 | -- - `Ensure` constructor, its return type.
  76 | --
  77 | --   Resulting error type of the constructor could be `(r', e)`, to emphasize that finally section always executes,
  78 | --   Thus always returning `r'` in both channels.
  79 | 
  80 | --- Basic mapping ---
  81 | 
  82 | export
  83 | Functor m => Bifunctor (Swirl m e) where
  84 |   bimap fr fo $ Done x     = Done $ fr x
  85 |   bimap fr fo $ Fail x     = Fail x
  86 |   bimap fr fo $ Yield o sw = Yield (fo o) (bimap fr fo sw)
  87 |   bimap fr fo $ Effect msw = Effect $ msw <&> assert_total bimap fr fo
  88 |   bimap fr fo $ BindR x f  = BindR (bimap id fo x) (bimap fr fo . f)
  89 |   bimap fr fo $ BindE x h  = BindE (bimap fr fo x) (bimap fr fo . h)
  90 |   bimap fr fo $ Ensure l x = Ensure l (bimap id fo x) `BindR` Done . fr
  91 | 
  92 | %transform "swirl: mapFst id" mapFst {f=Swirl m e} (\x => x) x = x
  93 | %transform "swirl: mapSnd id" mapSnd {f=Swirl m e} (\x => x) x = x
  94 | %transform "swirl: bimap id id" bimap {f=Swirl m e} (\x => x) (\x => x) x = x
  95 | 
  96 | export
  97 | mapCtx : Functor m => (forall a. m a -> n a) -> Swirl m e r o -> Swirl n e r o
  98 | mapCtx f $ Done x     = Done x
  99 | mapCtx f $ Fail x     = Fail x
 100 | mapCtx f $ Yield x sw = Yield x $ mapCtx f sw
 101 | mapCtx f $ Effect msw = Effect $ f $ msw <&> assert_total mapCtx f
 102 | mapCtx f $ BindR x g  = BindR (mapCtx f x) (mapCtx f . g)
 103 | mapCtx f $ BindE x h  = BindE (mapCtx f x) (mapCtx f . h)
 104 | mapCtx f $ Ensure l x = Ensure (mapCtx f l) (mapCtx f x)
 105 | 
 106 | export
 107 | mapError : (e -> e') -> Swirl m e r o -> Swirl m e' r o
 108 | mapError f $ Done x     = Done x
 109 | mapError f $ Fail x     = Fail $ f x
 110 | mapError f $ BindE x h  = BindE x (mapError f . h)
 111 | mapError f sw           = BindE sw (Fail . f)
 112 | 
 113 | --- Basic combinators ---
 114 | 
 115 | namespace ComposeResults
 116 | 
 117 |   export
 118 |   concat' : Functor m => (resultComp : rl -> rr -> r) -> Swirl m el rl o -> Lazy (Swirl m er rr o) -> Swirl m (Either el er) r o
 119 |   concat' fr (Done x) sv = mapError Right . mapFst (fr x) $ sv
 120 |   concat' fr (Fail x) sv = Fail $ Left x
 121 |   concat' fr sw       sv = BindR (mapError Left sw) $ \x => mapError Right $ mapFst (fr x) sv
 122 | 
 123 |   export
 124 |   concat : Functor m => (resultComp : rl -> rr -> r) -> Swirl m e rl o -> Lazy (Swirl m e rr o) -> Swirl m e r o
 125 |   concat fr (Done x) sv = mapFst (fr x) sv
 126 |   concat fr (Fail x) sv = Fail x
 127 |   concat fr sw       sv = BindR sw $ \x => mapFst (fr x) sv
 128 | 
 129 | export %inline
 130 | (++) : Functor m => Semigroup r => Swirl m e r o -> Lazy (Swirl m e r o) -> Swirl m e r o
 131 | (++) = concat (<+>)
 132 | 
 133 | export
 134 | andThen : Swirl m e () o -> Lazy (Swirl m e r o) -> Swirl m e r o
 135 | andThen sw sv = BindR sw $ const sv
 136 | 
 137 | infixl 1 `andThen` -- as `>>`
 138 | 
 139 | --- Basic analysis ---
 140 | 
 141 | ||| Checks is the only thing left for the given swirl is just to succeed, without any additional actions
 142 | |||
 143 | ||| Returns the same swirl (with possibly changed parameters) is yes, and `Nothing` if no.
 144 | export
 145 | hasSucceeded : (0 _ : IfUnsolved m' m) =>
 146 |                (0 _ : IfUnsolved e' Void) =>
 147 |                (0 _ : IfUnsolved o' Void) =>
 148 |                Swirl m e r o -> Maybe $ Swirl m' e' r o'
 149 | hasSucceeded $ Done x = Just $ Done x
 150 | hasSucceeded _        = Nothing
 151 | 
 152 | --- Forgetting ---
 153 | 
 154 | export
 155 | forgetO : Functor m => (0 _ : IfUnsolved o Void) => Swirl m e r a -> Swirl m e r o
 156 | forgetO $ Done x     = Done x
 157 | forgetO $ Fail e     = Fail e
 158 | forgetO $ Yield x sw = forgetO sw
 159 | forgetO $ Effect msw = Effect $ msw <&> assert_total forgetO
 160 | forgetO $ BindR sw g = BindR (forgetO sw) (forgetO . g)
 161 | forgetO $ BindE sw h = BindE (forgetO sw) (forgetO . h)
 162 | forgetO $ Ensure l x = Ensure (forgetO l) (forgetO x)
 163 | 
 164 | export
 165 | forgetR : Functor m => Monoid r => (0 _ : IfUnsolved r ()) => Swirl m e r' a -> Swirl m e r a
 166 | forgetR $ Done x = Done neutral
 167 | forgetR $ Fail e = Fail e
 168 | forgetR sw       = BindR sw $ const $ Done neutral
 169 | 
 170 | --- Basic creation ---
 171 | 
 172 | ||| A postfix function modifier to create an effected swirl creation.
 173 | ||| E.g. `emit v` emits `v` without any action, and `emit.by mv` emits a value of type `v` from `mv` of type `m v`.
 174 | export %inline
 175 | (.by) : Functor m => (x -> Swirl m e r o) -> m x -> Swirl m e r o
 176 | f.by = Effect . map f
 177 | 
 178 | export %inline
 179 | by : Functor m => (x -> Swirl m e r o) -> m x -> Swirl m e r o
 180 | by = (.by)
 181 | 
 182 | infix 0 `by`
 183 | 
 184 | -- Output --
 185 | 
 186 | export %inline
 187 | preEmitTo : (0 _ : IfUnsolved e Void) =>
 188 |             Lazy (Swirl m e r o) ->
 189 |             o ->
 190 |             Swirl m e r o
 191 | preEmitTo = flip Yield
 192 | 
 193 | export %inline
 194 | emit : Monoid r =>
 195 |        (0 _ : IfUnsolved e Void) =>
 196 |        (0 _ : IfUnsolved r ()) =>
 197 |        o -> Swirl m e r o
 198 | emit = preEmitTo $ Done neutral
 199 | 
 200 | export %inline
 201 | preEmitsTo : (0 _ : IfUnsolved e Void) =>
 202 |              Lazy (Swirl m e r o) ->
 203 |              LazyList o ->
 204 |              Swirl m e r o
 205 | preEmitsTo = foldrLazy Yield
 206 | 
 207 | export %inline
 208 | emits : Monoid r =>
 209 |         (0 _ : IfUnsolved e Void) =>
 210 |         (0 _ : IfUnsolved r ()) =>
 211 |         LazyList o ->
 212 |         Swirl m e r o
 213 | emits = preEmitsTo $ Done neutral
 214 | 
 215 | export %inline
 216 | preEmitsTo' : Foldable f =>
 217 |               (0 _ : IfUnsolved e Void) =>
 218 |               (0 _ : IfUnsolved f List) =>
 219 |               Lazy (Swirl m e r o) ->
 220 |               f o ->
 221 |               Swirl m e r o
 222 | preEmitsTo' = force .: foldr (delay .: Yield)
 223 | 
 224 | export %inline
 225 | emits' : Monoid r =>
 226 |          Foldable f =>
 227 |          (0 _ : IfUnsolved e Void) =>
 228 |          (0 _ : IfUnsolved f List) =>
 229 |          (0 _ : IfUnsolved r ()) =>
 230 |          f o ->
 231 |          Swirl m e r o
 232 | emits' = preEmitsTo' $ Done neutral
 233 | 
 234 | --export %inline
 235 | --preEmitMsTo : Functor m =>
 236 | --              (0 _ : IfUnsolved e Void) =>
 237 | --              Lazy (Swirl m e r o) ->
 238 | --              LazyList (m o) ->
 239 | --              Swirl m e r o
 240 | --preEmitMsTo = foldrLazy $ \mx, xs => Effect $ mx <&> \x => Yield x xs
 241 | 
 242 | -- Result --
 243 | 
 244 | export %inline
 245 | succeed : (0 _ : IfUnsolved e Void) =>
 246 |           (0 _ : IfUnsolved o Void) =>
 247 |           r -> Swirl m e r o
 248 | succeed = Done
 249 | 
 250 | -- Error --
 251 | 
 252 | export %inline
 253 | fail : (0 _ : IfUnsolved r ()) =>
 254 |        (0 _ : IfUnsolved o Void) =>
 255 |        e -> Swirl m e r o
 256 | fail = Fail
 257 | 
 258 | -- Result or error --
 259 | 
 260 | export
 261 | succeedOrFail : (0 _ : IfUnsolved o Void) =>
 262 |                 Either e r -> Swirl m e r o
 263 | succeedOrFail = either fail succeed
 264 | 
 265 | -- Output or error --
 266 | 
 267 | export
 268 | emitOrFail : Monoid r =>
 269 |              (0 _ : IfUnsolved r ()) =>
 270 |              Either e o -> Swirl m e r o
 271 | emitOrFail = either fail emit
 272 | 
 273 | --- Adapters ---
 274 | 
 275 | export
 276 | emitRes' : Functor m => (r -> r') -> Swirl m e r Void -> Swirl m e r' r
 277 | emitRes' f $ Done x = Yield x $ Done $ f x
 278 | emitRes' f $ Fail x = Fail x
 279 | emitRes' f sw       = mapSnd absurd sw `BindR` \r => Yield r $ Done $ f r
 280 | 
 281 | export %inline
 282 | emitRes : Functor m =>
 283 |           Monoid r =>
 284 |           (0 _ : IfUnsolved r ()) =>
 285 |           Swirl m e r' Void -> Swirl m e r r'
 286 | emitRes = emitRes' $ const neutral
 287 | 
 288 | export
 289 | swallowM : Functor m => Swirl m e r (m o) -> Swirl m e r o
 290 | swallowM $ Done x     = Done x
 291 | swallowM $ Fail e     = Fail e
 292 | swallowM $ Yield x sw = Effect $ x <&> \x' => Yield x' $ swallowM sw
 293 | swallowM $ Effect msw = Effect $ msw <&> assert_total swallowM
 294 | swallowM $ BindR sw g = BindR (swallowM sw) (swallowM . g)
 295 | swallowM $ BindE sw h = BindE (swallowM sw) (swallowM . h)
 296 | swallowM $ Ensure l x = Ensure l $ swallowM x
 297 | 
 298 | --- Internal foldings ---
 299 | 
 300 | namespace ToResult
 301 | 
 302 |   export
 303 |   foldlRO : Functor m => (0 _ : IfUnsolved o'' Void) => (o' -> o -> o') -> o' -> (o' -> r -> r') -> Swirl m e r o -> Swirl m e r' o''
 304 |   foldlRO fo inito fr $ Done x     = Done $ fr inito x
 305 |   foldlRO fo inito fr $ Fail e     = Fail e
 306 |   foldlRO fo inito fr $ Yield x sw = foldlRO fo (fo inito x) fr sw
 307 |   foldlRO fo inito fr $ Effect msw = Effect $ msw <&> assert_total foldlRO fo inito fr
 308 |   foldlRO fo inito fr $ BindR x f  = BindR (foldlRO fo inito (,) x) $ \(into, r') => foldlRO fo into fr $ f r'
 309 |   foldlRO fo inito fr $ BindE x h  = BindE (foldlRO fo inito fr x) (foldlRO fo inito fr . h)
 310 |   foldlRO fo inito fr $ Ensure l x = Ensure l (foldlRO fo inito (,) x) `BindR` \(r', o', r) => Done $ fr o' (r', r)
 311 | 
 312 |   export %inline
 313 |   foldlRO' : Functor m => (0 _ : IfUnsolved o' Void) => (o -> o -> o) -> (o -> r -> r) -> Swirl m e r o -> Swirl m e r o'
 314 |   foldlRO' f g = foldlRO (Just .: maybe id f) Nothing (maybe id g)
 315 | 
 316 |   export %inline
 317 |   foldRO : Functor m => Semigroup o => (0 _ : IfUnsolved o' Void) => Swirl m e o o -> Swirl m e o o'
 318 |   foldRO = foldlRO' (<+>) (<+>)
 319 | 
 320 |   export %inline
 321 |   foldlO : Functor m =>
 322 |            (0 _ : IfUnsolved o' Void) =>
 323 |            (r -> o -> r) ->
 324 |            r ->
 325 |            Swirl m e () o ->
 326 |            Swirl m e r o'
 327 |   foldlO f x = foldlRO f x const
 328 | 
 329 |   export %inline
 330 |   foldO : Functor m =>
 331 |           Monoid o =>
 332 |           (0 _ : IfUnsolved o' Void) =>
 333 |           Swirl m e () o ->
 334 |           Swirl m e o o'
 335 |   foldO = foldRO . mapFst (const neutral)
 336 | 
 337 |   export %inline
 338 |   outputs : Functor m =>
 339 |             (0 _ : IfUnsolved o' Void) =>
 340 |             Swirl m e () o ->
 341 |             Swirl m e (SnocList o) o'
 342 |   outputs = foldlO (:<) [<]
 343 | 
 344 | namespace ToOutput
 345 | 
 346 |   foldlO'R : Functor m => (o' -> o -> o') -> o' -> Swirl m e r o -> Swirl m (e, o') (r, o') Void
 347 |   foldlO'R op init $ Done x     = Done (x, init)
 348 |   foldlO'R op init $ Fail e     = Fail (e, init)
 349 |   foldlO'R op init $ Yield x sw = foldlO'R op (init `op` x) sw
 350 |   foldlO'R op init $ Effect msw = Effect $ msw <&> assert_total foldlO'R op init
 351 |   foldlO'R op init $ BindR x f  = BindR (foldlO'R op init x) $ \(r', into) => foldlO'R op into $ f r'
 352 |   foldlO'R op init $ BindE x h  = BindE (foldlO'R op init x) $ \(e, into) => foldlO'R op into $ h e
 353 |   foldlO'R op init $ Ensure l x = Ensure l (foldlO'R op init x) `BindR` \(r', r, o') => Done ((r', r), o')
 354 | 
 355 |   ||| Emits the folded value once before both successful and failing ending.
 356 |   export
 357 |   foldlO' : Functor m => (o' -> o -> o') -> o' -> Swirl m e r o -> Swirl m e r o'
 358 |   foldlO' f i =
 359 |     (`BindE` \(e, o') => Yield o' $ Fail e) .
 360 |     (`BindR` \(x, o') => Yield o' $ Done x) .
 361 |       mapSnd absurd . foldlO'R f i
 362 | 
 363 |   ||| Emits the folded value once and only before the successful ending.
 364 |   export
 365 |   foldlO : Functor m => (o' -> o -> o') -> o' -> Swirl m e r o -> Swirl m e r o'
 366 |   foldlO f i =
 367 |     (`BindR` \(x, o') => Yield o' $ Done x) .
 368 |       mapError fst . mapSnd absurd . foldlO'R f i
 369 | 
 370 |   export
 371 |   foldO : Functor m => Monoid o => Swirl m e r o -> Swirl m e r o
 372 |   foldO = foldlO (<+>) neutral
 373 | 
 374 |   export
 375 |   outputs : Functor m => Swirl m e r o -> Swirl m e r (SnocList o)
 376 |   outputs = foldlO (:<) [<]
 377 | 
 378 | --- Flattenings ---
 379 | 
 380 | mergeSemi : Semigroup r => (r, Maybe r) -> r
 381 | mergeSemi (x, Nothing) = x
 382 | mergeSemi (x, Just y)  = x <+> y
 383 | 
 384 | namespace ComposeResults
 385 | 
 386 |   export
 387 |   mergeCtxs' : Applicative m => Applicative n => (r'' -> r' -> r'') -> r'' -> Swirl m e r (Swirl n e' r' o) -> Swirl (m . n) (Either e e') (r, r'') o
 388 |   mergeCtxs' ff fi $ Done x     = Done (x, fi)
 389 |   mergeCtxs' ff fi $ Fail e     = Fail $ Left e
 390 |   mergeCtxs' ff fi $ Yield x sw = mapCtx pure (mapError Right x) `BindR` \lr => mergeCtxs' ff (fi `ff` lr) sw
 391 |   mergeCtxs' ff fi $ Effect msw = Effect $ msw <&> pure . assert_total mergeCtxs' ff fi
 392 |   mergeCtxs' ff fi $ BindR x f  = BindR (mergeCtxs' ff fi x) $ \(y, ys) => mergeCtxs' ff ys $ f y
 393 |   mergeCtxs' ff fi $ BindE x h  = BindE (mergeCtxs' ff fi x) $ either (mergeCtxs' ff fi . h) (Fail . Right)
 394 |   mergeCtxs' ff fi $ Ensure l x = Ensure (mapCtx (map pure) l) (mergeCtxs' ff fi x) `BindR` \(rl, rr, rs) => succeed ((rl, rr), rs)
 395 | 
 396 | export
 397 | mergeCtxs : Applicative m => Applicative n => Semigroup r => Swirl m e r (Swirl n e r o) -> Swirl (m . n) e r o
 398 | mergeCtxs = (`BindR` Done . mergeSemi) . mapError fromEither . mergeCtxs' (\a, x => (a <+> Just x) @{Deep}) Nothing
 399 | 
 400 | namespace ComposeResults
 401 | 
 402 |   export
 403 |   squashOuts' : Functor m => (r'' -> r' -> r'') -> r'' -> Swirl m e r (Swirl m e' r' o) -> Swirl m (Either e e') (r, r'') o
 404 |   squashOuts' ff fi $ Done x     = Done (x, fi)
 405 |   squashOuts' ff fi $ Fail e     = Fail $ Left e
 406 |   squashOuts' ff fi $ Yield x sw = mapError Right x `BindR` \lr => squashOuts' ff (fi `ff` lr) sw
 407 |   squashOuts' ff fi $ Effect msw = Effect $ msw <&> assert_total squashOuts' ff fi
 408 |   squashOuts' ff fi $ BindR x f  = BindR (squashOuts' ff fi x) $ \(y, ys) => squashOuts' ff ys $ f y
 409 |   squashOuts' ff fi $ BindE x h  = BindE (squashOuts' ff fi x) $ either (squashOuts' ff fi . h) (Fail . Right)
 410 |   squashOuts' ff fi $ Ensure l x = Ensure l (squashOuts' ff fi x) `BindR` \(rl, rr, rs) => succeed ((rl, rr), rs)
 411 | 
 412 | export
 413 | squashOuts' : Functor m => Swirl m e r (Swirl m e' () o) -> Swirl m (Either e e') r o
 414 | squashOuts' = mapFst fst . squashOuts' (const id) ()
 415 | 
 416 | squashOuts : Functor m => Semigroup r => Swirl m e r (Swirl m e r o) -> Swirl m e r o
 417 | squashOuts = mapFst mergeSemi . mapError fromEither . squashOuts' (\a, x => (a <+> Just x) @{Deep}) Nothing
 418 | 
 419 | -- Unlike the `BindR` constructor, this function is significantly not lazy on its first argument.
 420 | export %inline
 421 | bindR : Swirl m e r' o -> (r' -> Swirl m e r o) -> Swirl m e r o
 422 | bindR (Done x) f = f x
 423 | bindR (Fail e) _ = Fail e
 424 | bindR sw       f = BindR sw f
 425 | 
 426 | export %inline
 427 | handleRes : (r' -> Swirl m e r o) -> Swirl m e r' o -> Swirl m e r o
 428 | handleRes = flip bindR
 429 | 
 430 | squashRes : Swirl m e (Swirl m e r o) o -> Swirl m e r o
 431 | squashRes sw = sw `bindR` id
 432 | 
 433 | --- Filtration ---
 434 | 
 435 | export
 436 | mapEither' : Functor m =>
 437 |              (0 _ : IfUnsolved e Void) =>
 438 |              (0 _ : IfUnsolved r ()) =>
 439 |              (o -> Either e' o') ->
 440 |              Swirl m e r o ->
 441 |              Swirl m (Either e e') r o'
 442 | mapEither' f = squashOuts' . mapSnd (emitOrFail . f)
 443 | 
 444 | export
 445 | mapEither : Functor m => (o -> Either e o') -> Swirl m e r o -> Swirl m e r o'
 446 | mapEither = mapError fromEither .: mapEither'
 447 | 
 448 | 
 449 | export
 450 | mapMaybe : Functor m => (o -> Maybe o') -> Swirl m e r o -> Swirl m e r o'
 451 | mapMaybe f $ Done x     = Done x
 452 | mapMaybe f $ Fail e     = Fail e
 453 | mapMaybe f $ Yield x sw = case f x of
 454 |                             Nothing => mapMaybe f sw -- no common subexpression, tail recursion instead
 455 |                             Just y  => Yield y $ mapMaybe f sw
 456 | mapMaybe f $ Effect msw = Effect $ msw <&> assert_total mapMaybe f
 457 | mapMaybe f $ BindR sw g = BindR (mapMaybe f sw) (mapMaybe f . g)
 458 | mapMaybe f $ BindE sw h = BindE (mapMaybe f sw) (mapMaybe f . h)
 459 | mapMaybe f $ Ensure l x = Ensure l (mapMaybe f x)
 460 | 
 461 | export
 462 | filter : Functor m => (a -> Bool) -> Swirl m e r a -> Swirl m e r a
 463 | filter f $ Done x     = Done x
 464 | filter f $ Fail e     = Fail e
 465 | filter f $ Yield x sw = case f x of
 466 |                           False => filter f sw -- no common subexpression, tail recursion instead
 467 |                           True  => Yield x $ filter f sw
 468 | filter f $ Effect msw = Effect $ msw <&> assert_total filter f
 469 | filter f $ BindR sw g = BindR (filter f sw) (filter f . g)
 470 | filter f $ BindE sw h = BindE (filter f sw) (filter f . h)
 471 | filter f $ Ensure l x = Ensure l (filter f x)
 472 | 
 473 | --- Interleaving ---
 474 | 
 475 | namespace ComposeResults
 476 | 
 477 | --  mirrorAll : Functor m => Swirl m (Either e e') (r, r') (Either o o') -> Swirl m (Either e' e) (r', r) (Either o' o)
 478 | --  mirrorAll = mapError mirror . bimap swap mirror
 479 | --
 480 | --  ||| Interleaves both output emits and effects of both streams
 481 | --  export
 482 | --  interleaveOE : Functor m => Swirl m e r o -> Swirl m e' r' o' -> Swirl m (Either e e') (r, r') (Either o o')
 483 | --  interleaveOE (Done x)     sv = mapError Right $ bimap (x,) Right sv
 484 | --  interleaveOE (Fail e)     sv = Fail $ Left e -- maybe, try to continue as much as possible?
 485 | --  interleaveOE (Yield x sw) sv = Yield (Left x) $ mirrorAll $ interleaveOE {m} sv sw
 486 | --  interleaveOE (Effect msw) sv = Effect $ msw <&> \sw => mirrorAll $ assert_total $ interleaveOE sv sw
 487 | --  interleaveOE (BindR x f)  sv = ?interleave'_rhs_4
 488 | --  interleaveOE (BindE x h)  sv = ?interleave'_rhs_5
 489 | --  interleaveOE (Ensure l x) sv = ?interleave'_rhs_6
 490 | 
 491 | --- Functor, Applicative, Monad ---
 492 | 
 493 | -- Implementations over the last type argument --
 494 | 
 495 | export %inline
 496 | Functor m => Functor (Swirl m e r) where
 497 |   map = mapSnd
 498 | 
 499 | export
 500 | Functor m => Monoid r => Applicative (Swirl m e r) where
 501 |   pure x = Yield x $ Done neutral
 502 |   fs <*> xs = squashOuts $ fs <&> flip map xs
 503 | 
 504 | export
 505 | Functor m => Monoid r => Monad (Swirl m e r) where
 506 |   join = squashOuts
 507 | 
 508 | -- particular cases of monad combinators, ignoring the result
 509 | infixl 1 :>>=, =<<:, :>>
 510 | 
 511 | export %inline
 512 | (=<<:) : Functor m => (o' -> Swirl m e () o) -> Swirl m e r o' -> Swirl m e r o
 513 | (=<<:) = mapError fromEither .: squashOuts' .: mapSnd
 514 | 
 515 | export %inline
 516 | (:>>=) : Functor m => Swirl m e r o' -> (o' -> Swirl m e () o) -> Swirl m e r o
 517 | (:>>=) = flip (=<<:)
 518 | 
 519 | export %inline
 520 | (:>>) : Functor m => Swirl m e r () -> Lazy (Swirl m e () o) -> Swirl m e r o
 521 | (:>>) sw sv = mapError fromEither $ squashOuts' $ mapSnd (const sv) sw
 522 | 
 523 | export %inline
 524 | HasIO io => Monoid r => HasIO (Swirl io e r) where
 525 |   liftIO = emit.by . liftIO
 526 | 
 527 | export %inline
 528 | Monoid r => MonadTrans (\m => Swirl m e r) where
 529 |   lift = emit.by
 530 | 
 531 | export %inline
 532 | Functor m => Monoid r => MonadError e (Swirl m e r) where
 533 |   throwError = Fail
 534 |   catchError = BindE . delay
 535 | 
 536 | -- Implementations over the second type argument --
 537 | 
 538 | namespace Functor
 539 | 
 540 |   export
 541 |   [ByResult] Functor m => Functor (\r => Swirl m e r o) where
 542 |     map = mapFst
 543 | 
 544 | namespace Applicative
 545 | 
 546 |   export
 547 |   [ByResult] Functor m => Applicative (\r => Swirl m e r o)
 548 |     using Functor.ByResult where
 549 |       pure = Done
 550 |       fs <*> xs = fs `bindR` (`mapFst` xs)
 551 | 
 552 | namespace Monad
 553 | 
 554 |   export
 555 |   [ByResult] Functor m => Monad (\r => Swirl m e r o)
 556 |     using Applicative.ByResult where
 557 |       join = squashRes
 558 |       (>>=) = bindR
 559 | 
 560 | namespace HasIO
 561 | 
 562 |   export %inline
 563 |   [ByResult] HasIO io => HasIO (\r => Swirl io e r o)
 564 |     using Monad.ByResult where
 565 |       liftIO = succeed.by . liftIO
 566 | 
 567 | namespace MonadTrans
 568 | 
 569 |   export %inline
 570 |   [ByResult] MonadTrans (\m, r => Swirl m e r o) where
 571 |     lift = succeed.by
 572 | 
 573 | namespace MonadError
 574 | 
 575 |   export %inline
 576 |   [ByResult] Functor m => MonadError e (\r => Swirl m e r o)
 577 |     using Monad.ByResult where
 578 |       throwError = Fail
 579 |       catchError = BindE . delay
 580 | 
 581 | --- Error handling ---
 582 | 
 583 | export
 584 | handleError : (0 _ : IfUnsolved e' Void) =>
 585 |               (e -> Swirl m e' r o) -> Swirl m e r o -> Swirl m e' r o
 586 | handleError = flip $ BindE . delay
 587 | 
 588 | --- Finally funning ---
 589 | 
 590 | export
 591 | withFinally' : Functor m => Swirl m Void r' Void -> Swirl m e r o -> Swirl m e (r', r) o
 592 | withFinally' l x = Ensure l x
 593 | 
 594 | export
 595 | withFinally : Functor m => Swirl m Void () Void -> Swirl m e r o -> Swirl m e r o
 596 | withFinally = mapFst snd .: withFinally'
 597 | 
 598 | export
 599 | bracket' : Functor m =>
 600 |            (0 _ : IfUnsolved e Void) =>
 601 |            (0 _ : IfUnsolved o Void) =>
 602 |            (init : Swirl m e res o) ->
 603 |            (cleanup : res -> Swirl m Void r' Void) ->
 604 |            (action : res -> Swirl m e r o) ->
 605 |            Swirl m e (r', r) o
 606 | bracket' init cleanup action = init `bindR` \res => withFinally' (cleanup res) (action res)
 607 | 
 608 | export
 609 | bracket : Functor m =>
 610 |           (0 _ : IfUnsolved e Void) =>
 611 |           (0 _ : IfUnsolved o Void) =>
 612 |           (init : Swirl m e res o) ->
 613 |           (cleanup : res -> Swirl m Void () Void) ->
 614 |           (action : res -> Swirl m e r o) ->
 615 |           Swirl m e r o
 616 | bracket init cleanup action = init `bindR` \res => withFinally (cleanup res) (action res)
 617 | 
 618 | export
 619 | bracketO : Functor m =>
 620 |            Monoid r =>
 621 |            (0 _ : IfUnsolved e Void) =>
 622 |            (0 _ : IfUnsolved r ()) =>
 623 |            (init : Swirl m e res Void) ->
 624 |            (cleanup : res -> Swirl m Void r Void) ->
 625 |            Swirl m e r res
 626 | bracketO init cleanup = bimap fst snd $ emitRes' id $ bracket' init cleanup succeed
 627 | 
 628 | --- Processes ---
 629 | 
 630 | export covering
 631 | repeat : Functor m =>
 632 |          (0 _ : IfUnsolved e Void) =>
 633 |          Swirl m e () o -> Swirl m e Void o
 634 | repeat sw = forgetR sw `andThen` repeat sw
 635 | 
 636 | ||| Emit units until given effect returns `True` or fails
 637 | export covering
 638 | tickUntil : Functor m =>
 639 |             Monoid r =>
 640 |             (0 _ : IfUnsolved r ()) =>
 641 |             (0 _ : IfUnsolved e Void) =>
 642 |             Swirl m e Bool Void -> Swirl m e r ()
 643 | tickUntil $ Done True     = Done neutral
 644 | tickUntil sw@(Done False) = Yield () $ tickUntil sw
 645 | tickUntil $ Fail e        = Fail e
 646 | tickUntil sw = map absurd sw `bindR` \stop => if stop then succeed neutral else Yield () $ tickUntil sw
 647 | 
 648 | --- Cutting outputs ---
 649 | 
 650 | take' : Functor m => Nat -> Swirl m e r o -> Swirl m (Nat, e) (Nat, r) o
 651 | take' Z     sw           = mapError (Z,) $ mapFst (Z,) $ forgetO sw
 652 | take' (S k) $ Yield x sw = Yield x $ take' k sw
 653 | take' n     $ Done x     = Done (n, x)
 654 | take' n     $ Fail e     = Fail (n, e)
 655 | take' n     $ Effect msw = Effect $ msw <&> assert_total take' n
 656 | take' n     $ BindR x f  = BindR (take' n x) $ \(n', r') => take' n' $ f r'
 657 | take' n     $ BindE x h  = BindE (take' n x) $ \(n', e') => take' n' $ h e'
 658 | take' n     $ Ensure l x = Ensure l (take' n x) `BindR` \(r', n', r) => Done (n, r', r)
 659 | 
 660 | export
 661 | take : Functor m => Nat -> Swirl m e r o -> Swirl m e r o
 662 | take = mapError snd .: mapFst snd .: take'
 663 | 
 664 | -- Additional bool parameter's semantics is roughly the last value returned by the condition function
 665 | %inline %tcinline
 666 | twCont : Functor m =>
 667 |          Bool ->
 668 |          (succMap : Lazy (Swirl m (Bool, e) (Bool, r) o) -> Swirl m (Bool, e) (Bool, r) o) ->
 669 |          (o -> Bool) ->
 670 |          Swirl m e r o ->
 671 |          Swirl m (Bool, e) (Bool, r) o
 672 | takeWhile' : Functor m => (o -> Bool) -> Swirl m e r o -> Swirl m (Bool, e) (Bool, r) o
 673 | takeWhile' _ $ Done x     = Done (True, x)
 674 | takeWhile' _ $ Fail e     = Fail (True, e)
 675 | takeWhile' w $ Yield x sw = twCont (w x) (Yield x) w sw
 676 | takeWhile' w $ Effect msw = Effect $ msw <&> assert_total takeWhile' w
 677 | takeWhile' w $ BindR x f  = BindR (takeWhile' w x) $ \(ct, r') => twCont ct force w $ f r'
 678 | takeWhile' w $ BindE x h  = BindE (takeWhile' w x) $ \(ct, e') => twCont ct force w $ h e'
 679 | takeWhile' w $ Ensure l x = Ensure l (takeWhile' w x) `BindR` \(r', b', r) => Done (b', r', r)
 680 | twCont False s _ sw = mapError (False,) $ mapFst (False,) $ forgetO sw
 681 | twCont True  s w sw = s $ delay $ takeWhile' w sw
 682 | 
 683 | export
 684 | takeWhile : Functor m => (o -> Bool) -> Swirl m e r o -> Swirl m e r o
 685 | takeWhile = mapError snd .: mapFst snd .: takeWhile'
 686 | 
 687 | drop' : Functor m => Nat -> Swirl m e r o -> Swirl m (Nat, e) (Nat, r) o
 688 | drop' Z     sw           = mapError (Z,) $ mapFst (Z,) sw
 689 | drop' (S k) $ Yield x sw = drop' k sw
 690 | drop' n     $ Done x     = Done (n, x)
 691 | drop' n     $ Fail e     = Fail (n, e)
 692 | drop' n     $ Effect msw = Effect $ msw <&> assert_total drop' n
 693 | drop' n     $ BindR x f  = BindR (drop' n x) $ \(n', r') => drop' n' $ f r'
 694 | drop' n     $ BindE x h  = BindE (drop' n x) $ \(n', e') => drop' n' $ h e'
 695 | drop' n     $ Ensure l x = Ensure l (drop' n x) `BindR` \(r', n', r) => Done (n, r', r)
 696 | 
 697 | export
 698 | drop : Functor m => Nat -> Swirl m e r o -> Swirl m e r o
 699 | drop = mapError snd .: mapFst snd .: drop'
 700 | 
 701 | -- Additional bool parameter's semantics is roughly the last value returned by the condition function
 702 | %inline %tcinline
 703 | dwCont : Functor m =>
 704 |          Bool ->
 705 |          (succMap : Lazy (Swirl m e r o) -> Swirl m e r o) ->
 706 |          (o -> Bool) ->
 707 |          Swirl m e r o ->
 708 |          Swirl m (Bool, e) (Bool, r) o
 709 | dropWhile' : Functor m => (o -> Bool) -> Swirl m e r o -> Swirl m (Bool, e) (Bool, r) o
 710 | dwCont True  s w sw = dropWhile' w sw
 711 | dwCont False s _ sw = mapError (False,) $ mapFst (False,) $ s sw
 712 | dropWhile' _ $ Done x     = Done (True, x)
 713 | dropWhile' _ $ Fail e     = Fail (True, e)
 714 | dropWhile' w $ Yield x sw = dwCont (w x) (Yield x) w sw
 715 | dropWhile' w $ Effect msw = Effect $ msw <&> assert_total dropWhile' w
 716 | dropWhile' w $ BindR x f  = BindR (dropWhile' w x) $ \(ct, r') => dwCont ct force w $ f r'
 717 | dropWhile' w $ BindE x h  = BindE (dropWhile' w x) $ \(ct, e') => dwCont ct force w $ h e'
 718 | dropWhile' w $ Ensure l x = Ensure l (dropWhile' w x) `BindR` \(r', b', r) => Done (b', r', r)
 719 | 
 720 | export
 721 | dropWhile : Functor m => (o -> Bool) -> Swirl m e r o -> Swirl m e r o
 722 | dropWhile = mapError snd .: mapFst snd .: dropWhile'
 723 | 
 724 | --- Extension ---
 725 | 
 726 | intersperseOuts' : Functor m => (sep : Swirl m e () o) -> Swirl m e r o -> Swirl m (Bool, e) (Bool, r) o
 727 | %inline prepO : Functor m => Bool -> (sep : Swirl m e () o) -> Swirl m e r o -> Swirl m (Bool, e) (Bool, r) o
 728 | prepO True  sep sw = mapError ((True,) . fromEither) $ mapFst (True,) $ squashOuts' $ map (\x' => concat const sep $ emit x') sw
 729 | prepO False sep sw = intersperseOuts' sep sw
 730 | intersperseOuts' sep $ Done x     = Done (False, x)
 731 | intersperseOuts' sep $ Fail e     = Fail (False, e)
 732 | intersperseOuts' sep $ Yield x sw = Yield x $ prepO True sep sw
 733 | intersperseOuts' sep $ Effect msw = Effect $ msw <&> assert_total intersperseOuts' sep
 734 | intersperseOuts' sep $ BindR x f  = BindR (intersperseOuts' sep x) $ \(fwas, r') => prepO fwas sep $ f r'
 735 | -- CAUTION! the following `assert_total` has no clear evidence of being valid
 736 | intersperseOuts' sep $ BindE x h  = BindE (assert_total intersperseOuts' (mapError Right sep) (mapError Left x)) $ \(fwas, ee) =>
 737 |                                       case ee of
 738 |                                         Left e' => prepO fwas sep $ h e'
 739 |                                         Right e => Fail (fwas, e)
 740 | intersperseOuts' sep $ Ensure l x = Ensure l (intersperseOuts' sep x) `BindR` \(r', b, r) => Done (b, r', r)
 741 | 
 742 | export
 743 | intersperseOuts : Functor m => (sep : Swirl m e () o) -> Swirl m e r o -> Swirl m e r o
 744 | intersperseOuts = mapError snd .: mapFst snd .: intersperseOuts'
 745 | 
 746 | export
 747 | iterateAlong : Functor m => (i -> i) -> i -> Swirl m e r o -> Swirl m e r (i, o)
 748 | iterateAlong next = mapError snd .: mapFst snd .: go where
 749 |   go : forall e, r. i -> Swirl m e r o -> Swirl m (i, e) (i, r) (i, o)
 750 |   go n $ Done x     = Done (n, x)
 751 |   go n $ Fail e     = Fail (n, e)
 752 |   go n $ Yield x sw = Yield (n, x) $ go (next n) sw
 753 |   go n $ Effect msw = Effect $ msw <&> assert_total go n
 754 |   go n $ BindR x f  = go n x `BindR` \(n', r') => go n' $ f r'
 755 |   go n $ BindE x h  = go n x `BindE` \(n', e') => go n' $ h e'
 756 |   go n $ Ensure l x = Ensure l (go n x) `BindR` \(r', i, r) => Done (i, r', r)
 757 | 
 758 | export %inline
 759 | zipWithIndex : Functor m => Swirl m e r o -> Swirl m e r (Nat, o)
 760 | zipWithIndex = iterateAlong S Z
 761 | 
 762 | --- Eliminators ---
 763 | 
 764 | -- to lazy list --
 765 | 
 766 | export
 767 | toLazyList' : Swirl Identity e r o -> (Either e r, Lazy (LazyList o))
 768 | toLazyList' $ Done x         = (Right x, [])
 769 | toLazyList' $ Fail e         = (Left e, [])
 770 | toLazyList' $ Yield x sw     = (x ::) <$> toLazyList' sw
 771 | toLazyList' $ Effect $ Id sw = toLazyList' sw
 772 | toLazyList' $ BindR x f      = let (ir, ll) = toLazyList' x in
 773 |                                case ir of
 774 |                                  Left  e => (Left e, ll)
 775 |                                  Right r => toLazyList' (f r) <&> \rr => ll ++ rr
 776 | toLazyList' $ BindE x h      = let (ir, ll) = toLazyList' x in
 777 |                                case ir of
 778 |                                  Left e  => toLazyList' (h e) <&> \rr => ll ++ rr
 779 |                                  Right r => (Right r, ll)
 780 | toLazyList' $ Ensure l x     = let (Right r', Delay []) = toLazyList' l in
 781 |                                map (r',) `mapFst` toLazyList' x
 782 | 
 783 | export %inline
 784 | toLazyList : Swirl Identity Void () o -> LazyList o
 785 | toLazyList = force . snd . toLazyList'
 786 | 
 787 | -- to an underlying monad --
 788 | 
 789 | data Ctx : (Type -> Type) -> (inE, inR, outE, outR : Type) -> Type where
 790 |   Nil : Ctx m e r e r
 791 |   BiR : (r' -> Swirl m e r Void) -> Ctx m e r e0 r0 -> Ctx m e r' e0 r0
 792 |   BiE : (e' -> Swirl m e r Void) -> Ctx m e r e0 r0 -> Ctx m e' r e0 r0
 793 |   Ens : Swirl m Void r' Void -> Ctx m e (r', r) e0 r0 -> Ctx m e r e0 r0
 794 | 
 795 | data St : (Type -> Type) -> (finalE, finalR : Type) -> Type where
 796 |   AtCtx : Swirl m e' r' Void -> Ctx m e' r' e r -> St m e r
 797 | 
 798 | data StLT : St m e r -> St m e r -> Type where
 799 |   BiRLT : (sw `AtCtx` ctx) `StLT` (sv `AtCtx` BiR f ctx)
 800 |   BiELT : (sw `AtCtx` ctx) `StLT` (sv `AtCtx` BiE f ctx)
 801 |   EnsLT : (sw `AtCtx` ctx) `StLT` (sv `AtCtx` Ens l ctx)
 802 | 
 803 |   SwBR : (Force sw `AtCtx` BiR f         ctx) `StLT` (BindR sw f `AtCtx` ctx)
 804 |   SwBE : (Force sw `AtCtx` BiE f         ctx) `StLT` (BindE sw f `AtCtx` ctx)
 805 |   SwEn : (Force sw `AtCtx` Ens (Force l) ctx) `StLT` (Ensure l sw `AtCtx` ctx)
 806 | 
 807 |   EfLT : (sw `AtCtx` ctx) `StLT` (Effect msw `AtCtx` ctx)
 808 |   -- No relation between `sw` and `msw` depicted here :-(
 809 | 
 810 | covering
 811 | WellFounded (St m e r) StLT where
 812 |   wellFounded st = wellFounded st
 813 | 
 814 | -- Why does the following function pass totality checker once we have only covering wellfoundness implementation?
 815 | 
 816 | export
 817 | runSwirlE : MonadRec m => Swirl m e r Void -> m $ Either e r
 818 | runSwirlE sw = trWellFounded (sw `AtCtx` []) () $ \sw, () => case sw of
 819 | 
 820 |   Done x `AtCtx` []        => pure $ Done $ Right x
 821 |   Done x `AtCtx` BiR f ct  => pure $ Cont (f x `AtCtx` ct) BiRLT ()
 822 |   Done x `AtCtx` BiE _ ct  => pure $ Cont (Done x `AtCtx` ct) BiELT ()
 823 |   Done x `AtCtx` Ens sv ct => pure $ Cont ((mapError absurd $ mapFst (,x) $ sv) `AtCtx` ct) EnsLT ()
 824 | 
 825 |   Fail e `AtCtx` []        => pure $ Done $ Left e
 826 |   Fail e `AtCtx` BiR _ ct  => pure $ Cont (Fail e `AtCtx` ct) BiRLT ()
 827 |   Fail e `AtCtx` BiE h ct  => pure $ Cont (h e `AtCtx` ct) BiELT ()
 828 |   Fail e `AtCtx` Ens sv ct => pure $ Cont ((mapError absurd (forgetR sv) `andThen` Fail e) `AtCtx` ct) EnsLT ()
 829 | 
 830 |   Effect msw `AtCtx` ct => msw <&> \sw => Cont (sw `AtCtx` ct) EfLT ()
 831 | 
 832 |   BindR sw f  `AtCtx` ct => pure $ Cont (sw `AtCtx` BiR f ct) SwBR ()
 833 |   BindE sw h  `AtCtx` ct => pure $ Cont (sw `AtCtx` BiE h ct) SwBE ()
 834 |   Ensure l sw `AtCtx` ct => pure $ Cont (sw `AtCtx` Ens l ct) SwEn ()
 835 | 
 836 | export
 837 | runSwirl : MonadRec m => Swirl m Void a Void -> m a
 838 | runSwirl = map (\(Right x) => x) . runSwirlE
 839 | 
 840 | -------------
 841 | --- Whirl ---
 842 | -------------
 843 | 
 844 | export
 845 | data Whirl : (Type -> Type) -> (error, output, result : Type) -> Type where
 846 |   MkWhirl : Swirl m e r o -> Whirl m e o r
 847 | 
 848 | %name Whirl wh, wi, wj
 849 | 
 850 | public export %inline
 851 | Whirlie : (Type -> Type) -> (error, result : Type) -> Type
 852 | Whirlie m e = Whirl m e Void
 853 | 
 854 | export %inline
 855 | toWhirl : Swirl m e r o -> Whirl m e o r
 856 | toWhirl = MkWhirl
 857 | 
 858 | export %inline
 859 | toSwirl : Whirl m e o r -> Swirl m e r o
 860 | toSwirl $ MkWhirl sw = sw
 861 | 
 862 | export %inline
 863 | mapAsSwirl : (Swirl m e r o -> Swirl m' e' r' o') -> Whirl m e o r -> Whirl m' e' o' r'
 864 | mapAsSwirl f = toWhirl . f . toSwirl
 865 | 
 866 | export %inline
 867 | apAsSwirl : (Swirl m1 e1 r1 o1 -> Swirl m2 e2 r2 o2 -> Swirl m e r o) -> Whirl m1 e1 o1 r1 -> Whirl m2 e2 o2 r2 -> Whirl m e o r
 868 | apAsSwirl f x y = toWhirl $ f (toSwirl x) (toSwirl y)
 869 | 
 870 | export %inline
 871 | Functor m => Bifunctor (Whirl m e) where
 872 |   bimap = mapAsSwirl .: flip bimap
 873 | 
 874 | export %inline
 875 | Functor m => Functor (Whirl m e o) where
 876 |   map = mapAsSwirl . map @{ByResult}
 877 | 
 878 | export %inline
 879 | Functor m => Applicative (Whirl m e o) where
 880 |   pure = toWhirl . pure @{ByResult}
 881 |   (<*>) = apAsSwirl $ (<*>) @{ByResult}
 882 | 
 883 | export %inline
 884 | Functor m => Monad (Whirl m e o) where
 885 |   join = mapAsSwirl (join @{ByResult}) . map toSwirl
 886 |   x >>= f = toWhirl $ (>>=) @{ByResult} (toSwirl x) (toSwirl . f)
 887 | 
 888 | export %inline
 889 | HasIO m => HasIO (Whirl m e o) where
 890 |   liftIO = toWhirl . liftIO @{ByResult}
 891 | 
 892 | export %inline
 893 | MonadTrans (\m => Whirl m e o) where
 894 |   lift = toWhirl . lift @{ByResult}
 895 | 
 896 | export %inline
 897 | Functor m => MonadError e (Whirl m e o) where
 898 |   throwError = toWhirl . throwError @{ByResult}
 899 |   catchError wh h = toWhirl $ catchError @{ByResult} (toSwirl wh) (toSwirl . h)
 900 |