As Task Join

Stream: lean4

[Mac]

Lean currently has methods to to produce an asynchronous task from a synchronous action (e.g., asTask : BaseIO a -> BaseIO (Task a) and to bind a asynchronous action after a task bindTask : Task a -> (b -> BaseIO (Task a)) -> BaseIO (Task b), but there does not appear to be an efficient way to combine the two. That is, convert a synchronous action that returns a spawned a task (e.g., act : BaseIO (Task a)) into an asynchronous action that performs that task afterwards (i.e., also a BaseIO (Task a)). The only way I currently see to do this is to use act.asTask.map (·.map (·.get)) which does not seem particularly efficient.

Am I missing something? Is there already a better way to do this? If not, would adding an a method to do so efficiently the Lean core be reasonable?

[Sebastian Ullrich]

act.asTask.map (·.bind id)? That doesn't seem particularly inefficient to me.

[Mac]

@Sebastian Ullrich thanks! good to know!