Strange inferred type of a handler

[osa1]

The code below is copied from "Structured Asynchrony with Algebraic Effects" and modified for the syntax changes in the current version:

fun main()
  ()

effect exn_
  fun throw_(s: string): a

val try_ = handler
  return(x) -> Right(x)
  fun throw_(exn) -> Left(exn)

Error:

async.kk(9, 7): type error: types do not match
  context      :            handler
                   return(x) -> Right(x)
                   fun throw_(exn) -> Left(exn)
  term         :       throw_(exn) -> Left(exn)
  inferred type: forall<b,c,e1> hnd/clause1<string,either<string,b>,exn_,e1,c>
  expected type: forall<b> hnd/clause1<string,b,exn_,_e,_a>

It seems like desugaring details leaked into the erorr message, because I don't use hnd/clause1 in this code.

Questions:

• What is hnd/clause1? What are the type parameters to it?
• Is there a way to specify the types of handlers?
• What is the actual issue in this code?

I also tried this syntax:

val try_ = handler
  return(x)
    Right(x)
  fun throw_(exn)
    Left(exn)

But it generates the same error.

[chtenb]

I'm not sure about the reasoning behind this, but it compiles if you make exn polymorphic, like exn<a>.

[osa1]

I think that would be a different effect, in my code throw_ is never resumed so it can (or needs to) have type forall a . a, which is different than just a (where as is bound in the context and used in exn<a>).

[osa1]

Here's a demo of the two ways of defining exn:

fun main()
  val _ =
    with handler
      fun throw-resume(s: string)
        println("Error caught: " ++ s)
        123

    test-resume()

  val _ =
    with handler
      ctl throw-no-resume(s: string)
          println("Error caught: " ++ s)
          // I can't call `resume` here, I need a term with type `forall a . a`
          // However the error message if you try to resume is not good...

    test-no-resume()

  ()

// Throws `string`, the handler cannot resume the invoking code.
effect exn-no-resume
  ctl throw-no-resume(s: string): a

// Throws `string`, the handler can resume.
effect exn-resume<a>
  fun throw-resume(s: string): a

fun test-no-resume(): <exn-no-resume, console> ()
  println("test-no-resume 1")
  throw-no-resume("hi")
  println("test-no-resume 2")

fun test-resume(): <exn-resume<int>, console>()
  println("test-no-resume")
  val x: int = throw-resume("hi")
  println(x.show)

[osa1]

Aha, so the problem is I need to use exn instead of fun in the effect operation declaration:

val try_ = handler
  return(x) -> Right(x)
  ctl throw_(exn: string) -> Left(exn)

Maybe the fun/ctl distinction was added after the paper was written?

[TimWhiting]

Yes, I believe you are correct that the distinctions were added later:

We now have:

• val: dynamically scoped values
• fun: dynamically scoped functions / effects
• ctl: dynamically scoped delimited control
• final ctl: same as ctl, but never resumes
• raw ctl: same as ctl, but with an explicit handle for manual finalization (not only resumption).

[osa1]

Another code from the paper that doesn't type check:

fun main()
  ()

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

effect async
  fun await(initiate: (result<a> -> io ()) -> io ()): result<a>

val async-handle = handler
  fun await(initiate)
    initiate(resume) // io ()

Output:

test.kk(11, 5): type error: types do not match
  context      :       await
  term         :     initiate(resume)
  inferred type: result<_a>
  expected type: ()
  because      : type cannot be instantiated to match the annotation

How can initiate(resume) be result<_a> when initiate has type (...) -> io ()? Shouldn't it be io ()?

[osa1]

Same as above, fun needs to be ctl.