Stuck in interleavedx from the structured async paper

[osa1]

I'm trying to port the code from the Structured Asynchrony with Algebraic Effects, but I'm unable to port the interleavedx function.

So far I have this:

import std/num/int32
import std/num/ddouble
import std/time/duration
import std/time/timestamp

alias io = <ndet,div,console,st<global>>

alias result<a> = either<exception,a>

alias async-resume<a> = result<a> -> io ()

alias initiate<a> = async-resume<a> -> io ()

alias async-resume1<a> = a -> io ()

alias initiate1<a> = async-resume1<a> -> io ()

alias async-resume0 = () -> io ()

alias initiate0 = async-resume0 -> io ()

effect async
  ctl await(initiate: initiate<a>): result<a>

alias asyncx = <async,exn>

fun await1(initiate: initiate1<a>): <async,exn> a
  val await-ret = await fn(async-resume) initiate(fn(x) async-resume(Right(x)))
  match await-ret
    Left(e) -> throw-exn(e)
    Right(a) -> return a

fun await0(initiate: initiate0): <async,exn> ()
  await1 fn(async-resume) initiate(fn() async-resume(()))

fun wait(dur: duration): <async,exn> ()
  await0 fn(res)
    set-timeout(res, dur.milli-seconds.int32)

extern set-timeout(cb: () -> io (), ms: int32) : io ()
  js inline "setTimeout(#1, #2)"

fun fork(): <async,exn> bool
  await1 fn(res)
    set-timeout({ res(True) }, 0.int32)
    res(False)

fun exit(): <async,exn> a
  match await fn(res) {}
    Left(e) -> throw-exn(e)
    Right(a) -> return a

inline extern inject-st : forall<e,a,h> (() -> e a) -> <> (() -> <st<h>|e> a)
  inline "#1"

// exn in the return value because of `fork`
fun interleavedx(a: () -> <asyncx|e> a, b: () -> <asyncx|e> b): <asyncx|e> (error<a>, error<b>)
  with local-scope
  var ares := Nothing // maybe<error<a>>
  var bres := Nothing // maybe<error<b>>
  if fork() then
    val br = try(b) // handles exn to error<a>
    bres := Just(br)
    match ares
      Nothing -> exit()
      Just(ar) -> (ar, br)
  else
    val ar = try(a)
    ares := Just(ar)
    match bres
      Nothing -> exit()
      Just(br) -> (ar, br)

val async-handler = handler
  ctl await(initiate)
    initiate(resume)

fun main()
  with async-handler
  println("Waiting...")
  try({ wait(3.seconds) })
  println("Ohai")

The problem is in interlavedx:

async.kk(101, 5): type error: effects do not match
  context        :     val br = try(b) // handles exn to error<a>
                       bres := Just(br)
  term           :     val br = try(b) // handles exn to error<a>
                       bres := Just(br)
  inferred effect: <local<_h>,async,exn|_e1>
  expected effect: <async|$e>

I don't understand why the expected type doesn't have local and exn. exn is in the return type of interleavedx, and local should be added by with local-scope, which is defined as:

koka/lib/std/core/types.kk

Lines 415 to 416 in a7c4292

	pub inline fun local-scope<a,e>( action : forall<h> () -> <local<h> | e> a) : e a
	unsafe-no-local-cast(action)()

What am I doing wrong?

[osa1]

I managed to make it work:

fun interleavedx(a: () -> <asyncx,div|e> a, b: () -> <asyncx,div|e> b): <asyncx,div|e> (error<a>, error<b>)
  var ares := Nothing // maybe<error<a>>
  var bres := Nothing // maybe<error<b>>

  if fork() then
    val br = mask<local>({ mask<exn>({ try(b) }) }) // handles exn to error<a>
    bres := Just(br)
    match ares
      Nothing -> exit()
      Just(ar) -> (ar, br)
  else
    val ar = mask<local>({ mask<exn>({ try(a) }) })
    ares := Just(ar)
    match bres
      Nothing -> exit()
      Just(br) -> (ar, br)

But I still don't understand why I need to add the divs to the async callbacks and the result type. Without it I get this error:

async.kk(103,11): type error: effects do not match
  context        :           ares
  term           :           ares
  inferred effect: <div|_e1>
  expected effect: <async,exn|$e>

How can a variable read use div?

[TimWhiting]

Divergence analysis is very basic in Koka, and very conservative. See this paper, section 2.7 for the particular reasons why divergence is inferred here: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/koka-effects-2013.pdf.

TLDR; heaps can store cyclic references that could cause divergence. Although this does not happen for non-function types, since the return value is polymorphic we cannot make guarantees. You can of course try arguing specific cases, such as if you aren't calling a heap-read value, but how is that knowledge of the fact that a function came from a heap propagated to a polymorphic return value? You would need a flow sensitive analysis to get more precision in the types. I'm not 100% certain of all the details here, but at least I know the paper to read :).