Polymorphic effect cannot have seperate handlers

[iacore]

The following code should work in theory, since raise_baby is polymorphic. But currently, koka only accepts the one handler for polymorphic effects.

struct duck
struct swain

effect raise_baby<a, b>
    fun raise_baby(aaa: a, bbb: b): ()

fun main()
    with handler fun raise_baby(a: duck, b: duck)
        println("lead to water")
    with handler fun raise_baby(a: duck, b: swain)
        println("ignore")
    with handler fun raise_baby(a: swain, b: swain) // only this one is inferred
        println("put on back")
    val a = Duck()
    val c = Swain()
    raise_baby(a, a)
    raise_baby(a, c)
    raise_baby(c, c)

[iacore]

The example was from https://www.oxinabox.net/2020/02/09/whycompositionaljulia.html

[daanx]

Thanks for the example! I will try to read/see the talk that is linked so I can better understand the goals. (I will try to answer but perhaps I miss some design goals that are not apparent).

So, effect inference is not broken :-) but it behaves different than you expected. When doing inference on the effect "rows" only the name of the effect is matched (raise_baby) and then the type arguments (a,b) are unified with whatever is at the head of the row. This is essential for type inference to be decidable and having principal types.

In the example, the first raise_baby(a,a) entails an effect type <raise_baby<duck,duck>|e>
and then the next raise_baby(a,c) fails as it cannot unify raise_baby<duck,swan> with the head effect.

There are (at least) two ways around this:

1. use different effect types for the differently typed operations, eg. raise_baby_duck_duck, raise_baby_duck_swan etc.

2. use the mask keyword to explicitly skip the inner handler and pick the matching handler. This way we can construct the effect type <raise_baby<swan,swan>, raise_baby<duck,swan>, raise_baby<duck,duck>>. This is cumbersome though and not generally recommended.

Hope this helps!

(ps: just to be complete, here is the program with masking: (but try to avoid mask for this)

struct duck
struct swan

effect raise_baby<a, b>
  fun raise_baby(x : a, y : b): ()

fun main()
  with fun raise_baby(x : duck, y : duck)
    println("lead to water")
  with fun raise_baby(x : duck, y : swan)
    println("ignore")
  with fun raise_baby(x : swan, y : swan) // only this one is inferred
    println("put on back")
  val duck = Duck()
  val swan = Swan()
  mask<raise_baby>
    mask<raise_baby>
      raise_baby(duck, duck)
    raise_baby(duck, swan)
  raise_baby(swan, swan)

[iacore]

I'm trying to have type classes that only work in a scope. raise_baby<duck,duck> is a different effect than raise_baby<duck,swan>, so I think they should have different handlers.

The imagined use case is that library A defines the effect only has duck, while some other library B has swan need to use raise_baby from library A.

[CaramelFur]

@locriacyber Hi, the github discussions tab is probably a better place for this question.

Right now koka has a gitter chatroom, and since some time this is compatible with matrix. It is pretty inactive, but you can join it here.

[CaramelFur]

Hi @locriacyber, polymorphic effects not working this way is an intended part of koka. It would be extremely difficult and slow to add this. Because polymorphic effects would require the type of the arguments to be known at runtime. This means runtime types would also need to be added, and that only slows things down and makes them more complicated.

[iacore]

I don't think runtime types are needed. Each val binding has one type, and the effects in the above example are all compile-time known.

The problem is that now handler of <raise_baby<swan,swan> will hide handler raise_baby<duck,swan>, even though they are two different effects.

[CaramelFur]

Yes, in this example it is indeed clear what side effect handler should be called. But these handlers could be completely unkown and/or different for the same function. And in that case you need the runtime type to call the correct function.

[iacore]

But these handlers could be completely unkown and/or different for the same function.

Can you give an example?

[daanx]

The restriction is indeed fundamental (and intended). The reasons are three-fold:

• First of all, we want Koka to have an "untyped dynamic semantics", that is, we can erase all types and still run the program (and it will be not wrong for a well-typed program). (Note, this is unlike Haskell for example where we cannot interpret show (read "") without knowing the intermediate result type of read)

• Secondly, we adhere strictly to the algebraic effect handler semantics as outlined for example in [1]. This gives us a firm basis in theory and has known good properties with respect to composition of effect handlers for example (unlike call/cc for example, or arbitrary monads).

• Thirdly, we want to have principal type inference where any well-typed program can be assigned automatically a most general type (i.e. the best type). To make this work, we need deterministic "row unification" where the effect rows can be unified in a principal way (so, type rules have only equality between types (easy) and never in-equalities between types (very hard; a common case are subtypes leading to co- and contra-variance etc).)

The third one means that when we have an effect row with different effects "labels", like <exn,div> we can treat this as equal to <div,exn> when doing type inference. It also means that we cannot have polymorphic labels, like <a,b> or otherwise we cannot decide the equivalence <div,exn> ~= <a,b> for example deterministically. (note: we can have polymorphic rows, like <div,exn | e> where e is polymorph as that is decidable [2]).

Moreover, we can have (polymorpic) type parameters to effect "labels", like <foo<int>,foo<bool> but these cannot be reordered, and <foo<int>, foo<bool> != <foo<bool>, foo<int>>. At runtime this means that the first one needs an outer f
foo<bool> handler, while the inner handler should be foo<int> and the other way around for the second one. The reason is that at runtime there is only the "foo" effect tag and the innermost handler always handles the effect (which is what gives us an untyped dynamic semantics). If you want to address another handler you need to use mask to skip the innermost handler.

Hope this helps :-) The references may contain more examples. Here is a short example that shows that we cannot be rely on type parameters to infer which handler should be invoked (as in your original example):

effect foo<a>
  fun foo( xs : list<a> ) : int

fun main()
  with fun foo( xs : list<int> ) 
    xs.sum
  with fun foo( xs )
    xs.length
  with fun foo( xs : list<bool> )
    if xs.all(id) then 1 else 0

  <expr>

Here we set up three handlers, so the inferred effect context for <expr> is < foo<bool>, foo<a>, foo<int> > -- in that order! So, if I write foo([True]) for <expr> it will be handler by the inner handler (and return 1). If I write foo([1,2]) I will get a type error as the effect of foo([1,2]) : <foo<int> | e> does not unify with < foo<bool> | <foo<a>, foo<int>> >. If I want to really use the outer hander, I need to write mask<foo>{ mask<foo>{ foo([1,2]) } } -- ouch :-).

You may argue that we could infer this automatically in this case, but consider writing foo([]) ... now any of the handlers can potentially match and there is no "best" choice. This is especially trouble some for type inference: what if I have an argument xs and see xs.length and infer it has type list<a> and then I see foo(xs) and make some choice, say the bool handler, but then later we see if True then xs else [1,2] and now it would have been better to have chosen the int handler earlier on. This is why determinism is important for type inference.

[1] Ningning Xie and Daan Leijen. “ Generalized Evidence Passing for Effect Handlers” In The 26th ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2021.
Also as MSR-TR-2021-5, Mar, 2021.
pdf

[2] Daan Leijen, "Extensible records with scoped labels" pdf

[iacore]

(I think Koka has implicit forall, and the semantic is the same as C++ template (Is this true?).)

What's the use case for this type of effect handler?

  with fun foo( xs )
    xs.length

In practice, foo will be used for finite number of types of xs. If we disallow "forall a: foo" handler, we can use foo<bool> as tag, not just foo, right? This would solve the problem of "extending a library's functionality without changing its code" (the duck-swan problem) without type information at runtime (unlike Julia).

[iacore]

@daanx can you move this issue to Github discussion?