How should `Promise`s be composed?

[gergoerdi]

I haven't managed to find an implementation Monad Promise in the package, and in fact it is a bit tricky because it seems in JS a Promise's .then() callback can return either a pure value or yet another Promise...

For my project I ended up adding the following, hastily-thrown-together definitions:

%foreign "javascript:lambda:(_a, _b, p, k) => p.then(x => k(x)())"
prim__then : {0 a : Type} -> {0 b : Type} -> Promise a -> (a -> PrimIO (Union2 b (Promise b))) -> PrimIO (Promise b)

raw__then : Promise a -> (a -> JSIO (NS I [b, Promise b])) -> JSIO (Promise b)
raw__then p k = primIO $ prim__then p $ \x =>
  toPrim $ eitherT (\err => assert_total $ idris_crash $ dispErr err) (pure . toUnion2) $ k x

infixl 10 `then_`

export
then_ : Promise a -> (a -> JSIO (Promise b)) -> JSIO (Promise b)
then_ p k = raw__then p $ \x => inj <$> k x
  where
    inj : Promise b -> NS I [b, Promise b]
    inj x = inject x

%foreign "javascript:lambda:(_a, x) => new Promise((resolve, reject) => resolve(x))"
raw__ready : {0 a : Type} -> a -> Promise a

export
ready : a -> Promise a
ready = raw__ready

export sequenceP : List (Promise a) -> JSIO (Promise (List a))
sequenceP [] = pure $ ready []
sequenceP (p :: ps) = p `then_` \x => do
  k <- sequenceP ps
  k `then_` \xs => pure $ ready $ x :: xs

export concatP : List (Promise (List a)) -> JSIO (Promise (List a))
concatP ps = do
  p <- sequenceP ps
  p `then_` \xss => pure $ ready $ concat xss

Several things suck about it:

1. Using ready is a huge pain, but making then_ polymorphic in the callback's return type also leads to pain: I haven't managed to get the types inferred in that case, leading to lots of tedium.
2. Since then_ is in JSIO, it isn't really a monadic bind.
3. Among the fallout from point 2 is that things like sequenceP and concatP need to be hand-written.

[stefan-hoeck]

I haven't used Promises a lot so far, so I don't really have an opinion or a solution here. You could have a look at how they do this at PureScript and use that as a place to start. Note, however, that although then_ is not a monadic bind, you can still name it (>>=) and use do notation in Idris2.

I'm afraid I don't have the time to look into this. But Promises are lacking a proper API, so feel freed to draft some PRs, if you come up with a solution you like.

One more thing: Does it make sense to use assert_total together with idris_crash in the implementation of raw_then. This is a crash that can happen at runtime, so this is definitely not total? It might be better, if the value wrapped in a Promise was actually an Either JSErr a, so we'd get to proper handle the errors here.

[gergoerdi]

Good point on looking at PureScript. Unfortunately, I don't really know PureScript, and what I found at https://pursuit.purescript.org/packages/purescript-promises/1.0.0/docs/Control.Monad.Promise just looks weird, since it has then' as a pure function, but in JS you can very much observe that a promise has already had another promise chained to it:

> var p = fetch("hello.ipkg");
> p.then((x) => x.arrayBuffer());
< Promise {<pending>}
> p.then((x) => x.arrayBuffer());
< Promise {<rejected>: TypeError: Failed to execute 'arrayBuffer' on 'Response': body stream already read
    at <anonymou…}[[Prototype]]: Promise[[PromiseState]]: "rejected"[[PromiseResult]]: TypeError: Failed to execute 'arrayBuffer' on 'Response': body stream already read
    at <anonymous>:1:17
VM12636:1 Uncaught (in promise) TypeError: Failed to execute 'arrayBuffer' on 'Response': body stream already read
    at <anonymous>:1:17
(anonymous) @ VM12636:1

[gergoerdi]

One more thing: Does it make sense to use assert_total together with idris_crash in the implementation of raw_then[?]

Most probably not. However, I wasn't able to figure out how else to unpack a JSIO a into a PrimIO a.

[gergoerdi]

What do you think of an approach where we stay inside JSIO for as long as possible, and only create the raw JavaScript Promise at the last possible moment?

Here is a sketch of an API of what I'm thinking of. Of course, I'm happy to make a real PR once we have a plan, but for now, this is just me thinking out loud so a PR would be a lot of potentially wasted effort if the design has some fatal flaws.

The two new FFI calls needed are:

%foreign "javascript:lambda:(_a, m) => new Promise(function(resolve, reject) { resolve(m()) })"
prim__liftIO : {0 a : Type} -> PrimIO a -> PrimIO (Promise a)

%foreign "javascript:lambda:(_a, _b, p, k) => p.then(x => k(x)())"
prim__then : {0 a : Type} -> {0 b : Type} -> Promise a -> (a -> PrimIO (Union2 b (Promise b))) -> PrimIO (Promise b)

We'll be using prim__then via the utility function from my original comment (putting aside the fact that it uses idris_crash):

then' : Promise a -> (a -> JSIO (NS I [b, Promise b])) -> JSIO (Promise b)
then' p k = primIO $ prim__then p $ \x =>
  toPrim $ eitherT (\err => assert_total $ idris_crash $ dispErr err) (pure . toUnion2) $ k x

Now for the meat of it. The unimaginatively named Promise' type is just a Promise waiting to be created in JSIO:

record Promise' a where
  constructor Pack
  promise : JSIO (Promise a)

(I managed to cram THREE horribly undescriptive names into one definition!)

This can be made into a proper Monad:

Functor Promise' where
  map f p = Pack $ do
    p <- promise p
    p `then'` \x => pure $ inject $ f x

promiseIO : IO a -> Promise' a
promiseIO act = Pack $ primIO $ prim__liftIO $ toPrim act

Applicative Promise' where
  pure = promiseIO . pure

  pf <*> px = Pack $ do
    pf <- promise pf
    pf `then'` \f => do
      px <- promise px
      map (\x => inject x) $ the (JSIO (Promise b)) $ px `then'` \x => do
        pure $ inject $ f x

Monad Promise' where
  px >>= k = Pack $ do
    px <- promise px
    px `then'` \x => do
      py <- promise $ k x
      pure $ inject py

HasIO Promise' where
  liftIO = promiseIO

Now, if only all non-Raw functions are typed at Promise', we can write quite nice programs, for example using fetch:

%foreign "browser:lambda:r => fetch(r)"
prim__fetch : Union2 String Request -> PrimIO (Promise Response)

raw__fetch : NS I [String, Request] -> JSIO (Promise Response)
raw__fetch = primIO . prim__fetch . toUnion2

fetch : {auto prf : Elem a [String, Request]} -> a -> Promise' Response
fetch {prf = prf} x = Pack $ raw__fetch $ inject {prf = prf} x

arrayBuffer : {auto 0 conArg : JSType t1} -> {auto 0 _ : Elem Types.Body (Types t1)} -> t1 -> Promise' ArrayBuffer
arrayBuffer = Pack . Web.Raw.Fetch.Body.arrayBuffer

-- Just to see something happening
%foreign "browser:lambda:(_a, _b, x, y) => ((console.log(x),y))"
export traceConsole : a -> b -> b

main : IO ()
main = runJS $ do
  _ <- promise $ do
    stream <- fetch "hello.ipkg"
    buf <- arrayBuffer stream
    let buf8 = the UInt8Array $ cast buf
    putStrLn "Loaded"
    pure $ traceConsole buf8 ()
  pure ()

[stefan-hoeck]

What about going the other way, and wrap the possibility of failure into the value stored in the Promise itself:

then' : Promise a -> (a -> JSIO (NS I [b, Promise b])) -> IO (Promise $ Either JSErr b)

This would move error handling where it belongs.

[Thimoteus]

For PureScript inspiration, I'd look at https://github.com/purescript-web/purescript-web-promise instead. I'm the author of the other one, and I wrote it overnight at an airport when I didn't really understand how promises worked 😅

web-promise uses the Flatten typeclass to deal with the funky semantics of return types, and it's also the package we use at work.