Skip to content

Instantly share code, notes, and snippets.

@atacratic
Created August 10, 2021 23:37
Show Gist options
  • Save atacratic/a77762683097aa7c92754511fea8c807 to your computer and use it in GitHub Desktop.
Save atacratic/a77762683097aa7c92754511fea8c807 to your computer and use it in GitHub Desktop.
Attempt at a sketch of a pure handler for Unison's Async
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment