Attempt at a sketch of a pure handler for Unison's Async

async-test-handler.u

-- Aim is to make a handler for https://share.unison-lang.org/latest/types/distributed/up/async/Async
-- that works for tests and docs, so, a pure scheduler.

-- Key problem is how to make the types work in scheduleHandler.
-- - the awaitCompletion case is producing a 'resume' value - the continuation for 
--   how some task will resume after its call to tryAwait completes
-- - the completeTask case is producing a 'result' value - the output of some task, 
--   let's say one that another task is waiting on.
-- The latter has type 'Either Failure a', for some type a matching the return type
-- of the task.  The former wants to consume an 'Either Failure a'.  So it's 'just'
-- a matter of applying one to the other, `resume result`, but in a way that 
-- satisfies the typechecker that the a types match.

-- I've played with existential encodings, with no luck.  I can see how if you pack
-- in a function f with an argument x as a pair in this encoding, you can write a
-- function that calls `f x` on the packed existential.  But we don't get hold of our
-- f and our x at the same time.  I can't see how to use existentials to take an f 
-- and an x produced at different times at runtime, and bring them together.  I have
-- witnesses `Task a` at both times, which I am comparing at run time to justify the
-- match, but I don't think the typechecker can use this.  

-- It got me wondering if I'd need dependent pair types to make it work.

-- Or an escape hatch...

-- Separately, there are two interlocking handlers here, performing some weird 
-- gymnastics, and I'm not sure it will work out.  But I need it to typecheck before
-- I can find out...

unique ability Async' t g where
  Async'.tryAwait : t a ->{Async' t g} Either Failure a
  -- other operations stripped out for simplicity

unique type Task' a = Task' Nat

-- we'll interpret Async' down into Schedule
ability Schedule g where
  awaitCompletion : Task' a -> (Either Failure a ->{Async' Task' g} ()) ->{Schedule g} ()
  completeTask : Task' a -> Either Failure a -> ()

asyncTestHandler.impl : Task' a -> Request {Async' Task' {g}} a ->{g, base.Exception, Schedule g} a
asyncTestHandler.impl t = cases
  { a }                         ->
    completeTask t (Right a)
    a
  {Async'.tryAwait target -> k} ->
    k' r = k r; ()
    awaitCompletion target k'
    bug "can't get here"

type SchedulerState g = {
       workQueue : ['{Async' Task' g} ()]
  -- , waitingTasks : [exists a. (Task' a, Either Failure a ->{Async' Task' g} ())]  -- not unison!
}

scheduleHandler : Request {Schedule g} a ->{g, base.Exception} a -- !todo also needs Store (SchedulerState g)
scheduleHandler =
  cases
    { a } -> a
    { Schedule.awaitCompletion t resume -> _ } ->
      !todo -- add (t, resume) to waitingTasks
      asyncTestHandler scheduler
    { Schedule.completeTask t result -> k } ->
      -- get from waitingTasks the relevant item(s) (t', resume), i.e. for tasks waiting on this completion
      -- use the equality t == t' to persuade the typechecker that we can pass result
      -- to resume (it's the same type a in the Either Failure a); then add (resume result) to workQueue
      !todo
      handle !k with scheduleHandler

scheduler : '{Async' Task' {g}} x
scheduler _ =
  !todo -- drain work queue from state

asyncTestHandler : '{Async' Task' {g}} a ->{g, base.Exception} a
asyncTestHandler a = !todo -- handle (handle !a with asyncTestHandler.impl (Task'.Task' 0)) with scheduleHandler