0 | module Promise
  1 |
  2 | import Control.Monad.Either
  3 | import Control.Monad.Maybe
  4 | import Control.Monad.RWS
  5 | import Control.Monad.Reader
  6 | import Control.Monad.State
  7 | import Control.Monad.Trans
  8 | import Control.Monad.Writer
  9 |
 10 | public export
 11 | record Callbacks e (m : Type -> Type) a where
 12 |   constructor MkCallbacks
 13 |   onSucceded : a -> m ()
 14 |   onFailed : e -> m ()
 15 |
 16 | public export
 17 | record Promise e (m : Type -> Type) a where
 18 |   constructor MkPromise
 19 |   continuation : Callbacks e m a -> m ()
 20 |
 21 | export %inline
 22 | runPromise : (a -> m ()) -> (e -> m ()) -> Promise e m a -> m ()
 23 | runPromise onSucceded onFailed promise = continuation promise $ MkCallbacks onSucceded onFailed
 24 |
 25 | export
 26 | succeed : a -> Promise e m a
 27 | succeed a = MkPromise $ \cb => cb.onSucceded a
 28 |
 29 | export
 30 | fail : e -> Promise e m a
 31 | fail e = MkPromise $ \cb => cb.onFailed e
 32 |
 33 | export
 34 | mapFailure : (e -> e') -> Promise e m a -> Promise e' m a
 35 | mapFailure fn (MkPromise conta) = MkPromise $ \cb => conta $ MkCallbacks
 36 |   { onSucceded = cb.onSucceded
 37 |   , onFailed = cb.onFailed . fn
 38 |   }
 39 |
 40 | export
 41 | Functor (Promise e m) where
 42 |   map f (MkPromise ca) = MkPromise $ \cb => ca $ MkCallbacks
 43 |     { onSucceded = cb.onSucceded . f
 44 |     , onFailed = cb.onFailed
 45 |     }
 46 |
 47 | mutual
 48 |
 49 |   export
 50 |   Applicative (Promise e m) where
 51 |     pure = succeed
 52 |     fn <*> pa = fn >>= \f => map f pa
 53 |
 54 |   export
 55 |   Monad (Promise e m) where
 56 |     (>>=) (MkPromise conta) f = MkPromise $ \cb => conta $ MkCallbacks
 57 |         { onSucceded = \a =>
 58 |             let MkPromise contb = f a
 59 |             in contb cb
 60 |         , onFailed = cb.onFailed
 61 |         }
 62 |
 63 | export
 64 | MonadTrans (Promise e) where
 65 |   lift ma = MkPromise $ \cb => ma >>= cb.onSucceded
 66 |
 67 | export
 68 | HasIO m => HasIO (Promise e m) where
 69 |   liftIO = lift . liftIO
 70 |
 71 | export
 72 | MonadError e (Promise e m) where
 73 |   throwError = fail
 74 |   catchError (MkPromise conta) fn = MkPromise $ \cb => conta $ MkCallbacks
 75 |     { onSucceded = cb.onSucceded
 76 |     , onFailed = \e =>
 77 |         let (MkPromise contb) = fn e
 78 |         in contb $ MkCallbacks
 79 |           { onSucceded = cb.onSucceded
 80 |           , onFailed = cb.onFailed
 81 |           }
 82 |     }
 83 |
 84 | public export
 85 | interface Monad m => Monad n => MonadPromise e n m | m where
 86 |   promise : ((resolve: a -> n ()) -> (reject: e -> n ()) -> n ()) -> m a
 87 |
 88 | export
 89 | resolve : MonadPromise e n m => a -> m a
 90 | resolve = pure
 91 |
 92 | export
 93 | reject : MonadPromise e n m => e -> m a
 94 | reject e = promise $ \_, reject' => reject' e
 95 |
 96 | export
 97 | liftPromise : MonadPromise e n m => Promise e n a -> m a
 98 | liftPromise p = promise $ \resolve', reject' => runPromise resolve' reject' p
 99 |
100 | public export
101 | Monad n => MonadPromise e n (Promise e n) where
102 |   promise fn = MkPromise $ \cb => fn cb.onSucceded cb.onFailed
103 |
104 | public export
105 | MonadPromise e n m => MonadPromise e n (EitherT e' m) where
106 |   promise fn = MkEitherT $ promise $ \resolve, reject => fn (resolve . Right) reject
107 |
108 | public export
109 | MonadPromise e n m => MonadPromise e n (MaybeT m) where
110 |   promise fn = MkMaybeT $ promise $ \resolve, reject => fn (resolve . Just) reject
111 |
112 | public export
113 | MonadPromise e n m => MonadPromise e n (RWST r w s m) where
114 |   promise fn = MkRWST $ \r,s,w => promise $ \resolve, reject => fn (\a => resolve (a, (s, w))) reject
115 |
116 | public export
117 | MonadPromise e n m => MonadPromise e n (ReaderT r m) where
118 |   promise fn = MkReaderT $ \r => promise fn
119 |
120 | public export
121 | MonadPromise e n m => MonadPromise e n (StateT s m) where
122 |   promise fn = ST $ \s => promise $ \resolve, reject => fn (\a => resolve (s,a)) reject
123 |
124 | public export
125 | MonadPromise e n m => MonadPromise e n (WriterT w m) where
126 |   promise fn = MkWriterT $ \w => promise $ \resolve, reject => fn (\a => resolve (a,w)) reject
127 |