Type of a function accepting a block argument and adding to its set of effects

[timbertson]

I'm just starting out with koka 👋

I'm writing a function to operate on a resource, so it accepts a function parameter (block: (resource) -> e a) to use the resource and return anything.

The acquisition of this resource requires io, so I figure the return type of the whole function should be <io|e> a, which I read as "IO, plus whatever effect the block needs". This seems like it would be a pretty common idiom given koka's with syntax.

Here's a simplified version of the code which uses an int resource. Without the acquisition using IO, it works fine:

fun use-int(block: (int) -> e a): e a
  block(55)

fun main()
  use-int fn (i)
    println("got: " ++ i.show)

> got: 55

But if I change use-int signature to:

fun use-int(block: (int) -> e a): <io|e> a

Then I get the error:

main.kk(1,42): type error: effects do not match
  context        : fun use-int(block: (int) -> e a): <io|e> a
                     block(55)
  term           :                                          
                     block(55)
  inferred effect: $e
  expected effect: <io|$e>

Failed to compile main.kk

Thoughts:

• why is it $e? In this context I thought it would just be e? Is $ a qualifier for a generic type perhaps?
• it inferrred the effect to be $e, but it wanted (expected) <io|$e>. I thought that any effect x would always be a subtype (sub-effect-type?) of <x|anything-else>`, so I don't understand why this doesn't match.

---

I also tried adding a println to the top of the use-int function, like so:

fun use-int(block: (int) -> e a): <io|e> a
  println("hi")
  block(55)

And the error now is:

main.kk(2, 3): type error: effects do not match
  context        :   println("hi")
  term           :   println("hi")
  inferred effect: $e
  expected effect: <console/console|_e1>

Which seems similar, although now it's referring to _e1 which sounds unrelated to $e. But I don't know why the inferred effect would be $e, shouldn't it be console?

---

$ koka --version
Koka 3.1.2, 00:00:00 Jan  1 1980 (ghc release version)
version: 3.1.2
bin    : /nix/store/5w1jv9y3fbq98jh56p6mdkhznf1scjhx-koka-3.1.2/bin
lib    : /nix/store/5w1jv9y3fbq98jh56p6mdkhznf1scjhx-koka-3.1.2/lib/koka/v3.1.2
share  : /nix/store/5w1jv9y3fbq98jh56p6mdkhznf1scjhx-koka-3.1.2/share/koka/v3.1.2
output : .koka/v3.1.2/cc-debug-25957a
cc     : /nix/store/700a0ayy1s1h7zg9dqiqy0xvmhfr26l6-clang-wrapper-16.0.6/bin/cc

[TimWhiting]

Yes, any effect type <x> would be a subtype of <x,a,b,c...>.
However, with polymorphic effect type variables this changes a bit.

Let's use something other than io to make it a little more explicit. Let's just do exception.

So this is the program you are trying to write, and it is causing errors:

fun use-int(block: (int) -> e a): <exn|e> a
  throw("10") 
  block(55)

fun main()
  use-int fn (i)
    println("got: " ++ i.show)

The problem here is that block can throw exception. (After all the variable e can unify with anything).
Since it can throw an exception, which handler should handle it? The same one that catches errors thrown by use-int? Or a different one? In other words, is the handler that use-int throws to a "general" exception handler or one that is only intended to catch "internal" errors from use-int.

If it is the former, we want to state that block has the same "maximal" effect type as the result (i.e. they are run under the same handlers). This is the most common thing to do. To do this you should generally always make sure that your function parameters have the same effect type as the return effect type (unless you are adding a handler), see below for the change. You might be worried that this means that all blocks will need to throw exceptions. This is not the case. This is the maximum effect that block can have. Which since it was already e which could unify to anything - you were already allowing exceptions. Koka will do the right "subtyping", so that you can use blocks that don't throw here - they don't need exn in their effects. Another way to think about this is that block and use-int are run under the same handlers in the runtime stack - which since you didn't add another handler between them makes perfect sense.

fun use-int(block: (int) -> <exn|e> a): <exn|e> a // just change the effect type of the block to <exn|e>
  throw("10") 
  block(55)

fun main()
  // handler for exn ...
  use-int fn (i)
    // Okay to throw an exception here, will be caught by same handler as for the use-int function.
    println("got: " ++ i.show)

If you want the exceptions thrown by use-int to be internal, you can create a custom "exception-like" handler, or you can use mask<exn>. mask makes it so that a function parameter sees fewer effects in scope. However e can still unify with anything, so block can still throw an exception. If it does however, it will not be caught by the innermost handler (the one above use-int), but the one above that. However, typically if I have an effect that I want to handle "internally" and not let out to the users, I most often create a specialized handler for that so I'm sure to handle it myself, and not accidentally make a mistake of letting it propagate.

fun use-int(block: (int) -> e a): <exn|e> a
  throw("10") 
  mask<exn> // added mask
    block(55)

fun main()
  // handler for exn (if the block throws) ...
  // handler for exn ...
  use-int fn (i)
    // Cannot throw an exception here unless I have two exception handlers
    println("got: " ++ i.show)

By the way, if the rest of the block will be indented (i.e. use-int is a tail call), you can use the following syntax:

  with i <- use-int 
  // Cannot throw an exception here unless I have two exception handlers
  println("got: " ++ i.show)

It's one nice way to avoid indentation.

[TimWhiting]

BTW, feel free to join the community on discord as well: https://discord.gg/CEkHHnTqEv

[timbertson]

That was exactly the answer I needed, thanks!