Combining polymorphic effects

[aslakg]

effect semigroup<a> {
    fun mappend(x: a, y: a) : a
}

effect monoid<a> {
    val mempty : a
}

fun summarise(list) {
    match(list) {
        Cons(a,b) -> mappend(a, summarise(b))
        Nil -> mempty
    }
}

fun test() {
  val x = summarise([1,2,3])
  val y = summarise(["A","b","c"])
  42
}

I'm unable to get this to compile, because test uses both monoid<int> and monoid<string> , and is trying to unify them.
Is this a current limitation of koka/the type inferencer, or is there a way around this?
I assumed that with row types for effects, I could annotate test with <monoid<int>,semigroup<int>,console,monoid<string>,semigroup<string>> int
but this does not seem to work.

Any insights would be most appreciated!

The error given is this:

bugreport.kk(17, 3): error: effects do not match
  context        :   val x : int = summarise([1,2,3])
                     val y : string = summarise(["A","b","c"])
                     42
  term           :   val x : int = summarise([1,2,3])
                     val y : string = summarise(["A","b","c"])
                     42
  inferred effect: <monoid<string>,semigroup<string>|_e1>
  expected effect: <monoid<int>,semigroup<int>|_e>

[naoyafurudono]

I think the type system works well and it is not limitation of the type inference engine.

There are no handlers to handle test function in type safe way. For example, if a handler for monoid<int> is the inner most handler for monoid effect, mempty in summarise(["A", "b", "c"]) will get stuck, since the handler expect int while the argumet for mempty is string.

In Koka, < monoid<int>, monoid<string> > and < monoid<string>, monoid<int> > are incompatible (this limitation helps to detect the type error described above) so the unification was (successfully) failed.

[aslakg]

In my view monoid<int> and monoid<string> are two different types, and two different effects, and I'd use two handlers to handle them. I don't see why they should be unified... Surely list<string> and list<int> are treated as two different types, so it's reasonable to expect this.

[aslakg]

F.ex. if I have these function definitions:

fun test(l : list<string>) {
  println("This takes a list of strings")
}

fun test(l : list<int>) {
  println("This takes a list of ints")
}

then calling test([1,2,3]) will print "This takes a list of ints".
Similarly, therefore, I'd expect the effect to be monoid<int> and not just monoid. I know there are new developments with named effects - maybe that's the way around this?

[TimWhiting]

@aslakg
You have not implemented handlers for the effects

effect semigroup<a>
  fun mappend(x: a, y: a) : a

effect monoid<a>
  val mempty : a

fun summarise(list: list<a>): <monoid<a>, semigroup<a>> a
  match(list)
    Cons(a,b) -> mappend(a, summarise(b))
    Nil -> mempty

fun stringmonad(action)
  with handler<monoid<string>>
    val mempty = ""
  with handler<semigroup<string>>
    fun mappend(x: string, y: string) x ++ y
  action()

fun intmonad(action)
  with handler<monoid<int>>
    val mempty = 0
  with handler<semigroup<int>>
    fun mappend(x: int, y: int) x + y
  action()

fun main()
  with intmonad
  val a = summarise([1,2,3])
  with stringmonad
  val b = summarise(["A","b","c"])
  a.show.println()
  b.println()

However I would agree that this:

fun main()
  with intmonad
  with stringmonad
  val a = summarise([1,2,3])
  val b = summarise(["A","b","c"])
  a.show.println()
  b.println()

Should also work. I understand from the row types rules why this does not work, but I do not understand why the restriction for swap on row types is needed.

[AZMCode]

Oh God please this.
I want polymorphic effects instantiated with different types actually be different effects!

[chtenb]

Daan explains the issue with polymorphic effect handlers quite well in this post: #241 (comment)

[AZMCode]

Oh boy, just read it, and that is a bummer
Oh well then

[TimWhiting]

There is active work for designing a form of ad-hoc polymorphism or typeclasses in Koka. I've talked with Daan and it's the next thing that he plans to add to Koka. In talking with him, and considering changes to the effect system to support something like this we came to the conclusion that effects don't really fit as a replacement for ad-hoc polymorphism / typeclasses, at least in Koka - and maybe in general due to the fact they are dynamically scoped and interceptable (i.e. somewhat unpredictable). I don't want to state any design plans right now, since they are still subject to change and experimentation, but just wanted to say that it is probably the next thing coming for Koka. Stay tuned.

[AZMCode]

I'm back after toying around with implicit parameters, and let me tell you, they're absolutely great, and definitely the correct (and nevermind performance-conscious) way to do polymorphism in Koka to my eyes, yet this issue bugs me still.

This, among other things, if I'm correct, prevents koka from having a mininal-but-general 'yield' or 'generator' effect with proper type safety, implementing coroutines, instead preferring type-specific effects.

Hopefully this issue will eventually be revisited, but I can understand that there are technical concerns behind this desicion I'm honestly not yet capable of fully understanding yet.

[TimWhiting]

For now I'd recommend using named effects for use cases where you want multiple resumable computations with different types in the same scope.

See this example, or one of the others in this folder:
ask - a basic example of named handlers:
https://github.com/koka-lang/koka/blob/336bf9ba7cf0da2923f6547169bb708207bbcb80/samples/handlers/named/ask.kk

heap - an example of a polymorphic usage, as well as scoping - which prevents the handler from escaping it's creation scope - which would cause an error (every ref is created in the heap scope).
https://github.com/koka-lang/koka/blob/336bf9ba7cf0da2923f6547169bb708207bbcb80/samples/handlers/named/heap.kk