passing function error

[ZMan1345]

When I try to write the following function:

fun do-some(action : () -> e a, message : string) <console|e> a
   println(message)
   val res = action()
   res

I get this error on the println line:

effects do not match
context        :   println(message)
term           :   println(message)
inferred effect: $e
expected effect: <console/console|_e1>

I fixed the error using ths declation of the function:
fun do-some(action : () -> <console|e> a, message : string) <console|e> a
But to my understanding I'm forcing the passing function to be with the console effect, although I passed a function without the console effect and it worked well.
Why does this error happen in the first place? And why did the new declaration work, while the function I passed was accepted?

[TimWhiting]

This is a common misconception. The type of parameters specifies the "maximum" effect type of functions that can be passed in. Because the overall effect includes console, the function passed as a parameter can also use the console effect.

When you pass in a function without the console effect Koka automatically "opens" the effect type before checking it against the parameter type. It is sort of a subtyping relation.

So you are not "forcing" the passed function to have the console effect. You are just saying that if a function needs fewer effects, and it is running in a context that has access to more effects, then it will still work since it will only use the effects it needs, and all of those are available.

Generally your function parameters will have the same effect type as the return type unless you are handling an effect, or "mask"ing an effect: https://koka-lang.github.io/koka/doc/book.html#sec-mask. While masking can allow you to get rid of the console effect in the parameter's function type, it shouldn't be used unless you have another reason for using it - especially for effects that are not user-handled like console.

[ZMan1345]

Great. Thank you very much!

[osa1]

I think this is one of the issues with row types, or the way they're used. I have the same issue in my programming language.

The reason why this code doesn't work is because when type checking action(), you unify action's effect type with the call site's effect type.

So you try to unify e ~ <console|e>, which fails.

Intuitively, I think most users (including myself) would think that effect type of a function type should indicate the effects the function may perform.

But what it actually indicates is something like: the handlers that are allowed to be handled at the call sites.

Even this definition may not be 100% accurate and may be confusing to explain some examples.

@TimWhiting I'd be interesting to know if you have any thoughts on this, or whether you see this as a problem.

[osa1]

Thanks for the insightful response.

There's really a lot to think about here.. but I just coincidentally came across this talk about capabilities in Scala 3: https://www.youtube.com/watch?v=CJ19_h5cECY

which AFAIU mostly the describes the work in https://dl.acm.org/doi/pdf/10.1145/3618003.

It seems quite different than the row polymorphic variants + an extra type in function types approach in Koka.

I don't understand how it works yet, but in the presentation Odersky shows this code:

val f: Proc^{io}
val g: Proc^{f, async}

Here the {...} parts are capabilities. The interesting part is that they refer to other term variables rather than type variables, f in the code.

They also employ subtyping somehow, which should help eliminating the type variables we have in Koka and similar systems.

(I don't know what io and async are in this code, maybe they're some library functions that async and io functions call to add the capabilities to their types?)

[TimWhiting]

@osa1 Thanks for the resources.
A few related papers from the Scala side:
Implicits: https://dl.acm.org/doi/abs/10.1145/3158130
Scala Native continuations: https://dl.acm.org/doi/abs/10.1145/3679005.3685979
I'll have to read that paper about capturing types.

What I find interesting is that Scala and Kotlin are both dealing with the problem with checked exceptions you previously mentioned to me (the large number of aggregate dependencies), but in very different ways.

As mentioned in that talk on Scala, they are going down the rabbit hole of dependent types because they think that polymorphic effects are hard to reason about, but this leads them to needing to check for escaping effects and looking at lifetime of effects. First of all that seems backwards to me. Most programmers are familiar with polymorphic effects, and not many are familiar with dependent types.

The thing about this though, is that they are trying to prevent escaping the stack. It seems much more intuitive to me to talk about the relative / polymorphic effects from the higher-order function and the passed function because there is a clear stack ordering. I've just started using Scala recently, and while I really like some aspects of it, it seems like they are headed too far down the hole of type theory to make it accessible to "regular" programmers. Even for someone who has used languages with dependent types I wasn't able to follow 100% of how I'm supposed to reason about these capability capturing. And I don't think every user of Scala is going to read the paper you linked.

Some additional resources on Scala checked exceptions: https://docs.scala-lang.org/scala3/reference/experimental/canthrow.html

Kotlin has also recently announced checked exceptions: https://youtu.be/F5NaqGF9oT4?feature=shared&t=734.
Instead of adding an effect type, they are just using union types in the result type though. I think this will run into problems really soon with wanting to "rethrow" or not handle several of the exceptions and concentrate on the successful cases and maybe handle a subset of the exceptions.

[TimWhiting]

After reading the paper you linked, I think that my concerns are maybe less valid. I think Scala has an interesting approach going on. I am curious to see how it works out in practice. I do wonder still though if we could get a similar syntax or end result, but in a different way, or simplify Koka's effect types to be more concise.

[osa1]

I also just finished the introduction part of the paper (until the calculus). It certainly feels more "scalable", for example if you use capability variables var1 with caps {cap1, cap2, cap3} and var2 with {cap4, cap5}, you don't get {cat1, ..., cap5}, you get {var1, var2}. That avoid transitively including all of the capabilities/effects in the types.

Not having type parameters for effects/capabilities should also help avoiding contagious types (e.g. a type parameter in a function type carrying itself to a struct type, and to its users, ... until the use site that instantiates it).

I'm not bright enough to immediately see the issues though, I have to implement and try it.

I don't understand how/whether this system handles things like: a function handling one effect and propagating the rest to the caller.

I'm also not sure how much of the capability sets can be inferred.

Capability sets are sets of term variables. If I have two functions that are the same in types but capture different variables, they will have different types. Do they "meet" in a common supertype implicitly when one passed as the other? Do I manually upcast?

I also don't understand how can you upcast from a cap set to {cap}. Doesn't that mean losing track of capabilities? What happens if you use a capability after losing track of it?

So many questions..

[TimWhiting]

Yeah, this is why I worry about the mental model the users will be required to think about. If common patterns are easy enough to recognize and mechanically do that is great, but users are inevitably going to come across examples that aren't easy to explain as a common pattern.

Not having type parameters for effects/capabilities should also help avoiding contagious types (e.g. a type parameter in a function type carrying itself to a struct type, and to its users, ... until the use site that instantiates it).

Yes, this would be ideal. I'd love to figure out if we could do something like this in Koka's effect system.

I don't understand how/whether this system handles things like: a function handling one effect and propagating the rest to the caller.

I believe the function have a function parameter that takes an implicit argument with the capability that you are providing. The function then creates the handler and provides it to that argument. The type system ensures that although the capability is lexically captured it doesn't escape the stack-scope.

I'm also not sure how much of the capability sets can be inferred.

I believe they keep the current requirements of Scala that it can infer everything except function arguments.

Capability sets are sets of term variables. If I have two functions that are the same in types but capture different variables, they will have different types. Do they "meet" in a common supertype implicitly when one passed as the other? Do I manually upcast?

There is a subtyping relation as far as I understand it. But with my quick reading, I'm not quite sure how this situation would work out.

I also don't understand how can you upcast from a cap set to {cap}. Doesn't that mean losing track of capabilities? What happens if you use a capability after losing track of it?

No, it means that the function requires all of the capabilities. If your function has this type in it's result, it should result in an error that something escaped the scope (as far as I understand it). However, it is also used to defer some aspects to the caller via the subtyping relationship in parameter types. For example if your parameter is fs: filesystem^{cap} and you pass it a variable fs0 then cap is instantiated to fs0 I think. Sort of like fs: filesystem<e> and instantiating e with the effects it requires when you know more about fs and the effects it requires. You could do something similar with Koka probably, but trying to approach the subtyping issue using effect variables instead. It just might run into issues when unifying multiple effect variables though. I'd have to think about it some more.