effect type problem

[choltreppe]

Hallo there, I just stumbled upon koka and really like it.
So I just started trying out some stuff, now I wanted to write this little function for updating the value at an index of a list:

pub fun update (l: list<t>, i: int, f: (t) -> e t) : <exn|e> list<t> {
  fun traverse (l, i) : <exn|e> list<t> {
    match l {
      [] -> throw("index out of bound")
      Cons(x, xs) -> if i == 0
                      then Cons(f(x), xs)
                      else Cons(x, traverse(xs, i - 1))
    }
  }
  if i < 0
    then throw("index out of bound")
    else traverse(l, i)
}

and get this error:

error: effects do not match
  context        :                            Cons(x, traverse(xs, i - 1))
  term           :                            Cons(x, traverse(xs, i - 1))
  inferred effect: $e
  expected effect: <exn|_e1>
  because        : effect cannot be subsumed

This doenst happen if I leave out the polymorphic effect in the update-function type. So its maybe about the compiler not knowing f can just be called once and thinking its an infinite effect type?

thanks in advance
chol

[chtenb]

This aspect of programming with effects is a little underdocumented in Koka. As far as I understand it, all effects that are polymorphic should have the same row of concrete effects. So in your case that means you should add exn to the effects of f. Like this

pub fun update (l: list<t>, i: int, f: t -> <exn|e> t) : <exn|e> list<t> {
  fun traverse (l, j) {
    match l {
      [] -> Nil
      Cons(x, xs) -> 
        if j == 0
        then Cons(f(x), xs)
        else Cons(x, traverse(xs, j - 1))
    }
  }
  if i < 0
    then throw("index out of bound")
    else traverse(l, i)
}

You can do this because you exhibit the exn effect anyways, so there is no harm in allowing this effect in f as well.

[anfelor]

In this case, you can also fix the problem by just removing the type signatures and letting Koka do the work:

pub fun update (l, i, f)
  fun traverse (l, i)
    match l
      [] -> throw("index out of bound")
      Cons(x, xs) -> if i == 0
                      then Cons(f(x), xs)
                      else Cons(x, traverse(xs, i - 1))
  if i < 0
    then throw("index out of bound")
    else traverse(l, i)

where Koka infers:

pub fun update (l : list<a>, i : int, f : a -> <exn|e> a) : <exn|e> list<a>

[fredrikroos]

You can also mask exn when calling f. Then Koka will infer the closure to have the e effect, without exn so it will match the signature. Doing it that way means you don't get any unwanted exceptions so I think that's preferable to just allowing exceptions.

[mccraigmccraig]

I think I've been seeing the same thing... I had

module err

pub effect logger
  fun log-enter(name: string, input-str: string) : void
  fun log-leave(name: string, output-str: string) : void

pub type step<i,o,e>
  Pure(name: string, f: (i) -> pure o)
  Fx(name: string, f: (i) -> <pure|e> o)

pub fun run-step<i,o,e>(s: step<i,o,e>, i: i): <pure,logger|e> o
  match s
    Pure(n, f) ->
      log-enter(n, "")
      val r = f(i) 
      log-leave(n, "") 
      r
    Fx(n, f) ->
      log-enter(n, "") 
      val r = f(i) 
      log-leave(n, "") 
      r

which gives me this error in the Fx match clause:

effects do not match
context        :       val r = f(i) 
                       log-leave(n, "")
term           :       val r = f(i) 
                       log-leave(n, "")
inferred effect: <logger|_e1>
expected effect: <div,exn|$e>

Making the effects for the Pure and Fx functions line up, thus:

module err

pub effect logger
  fun log-enter(name: string, input-str: string) : void
  fun log-leave(name: string, output-str: string) : void

pub type step<i,o,e>
  Pure(name: string, f: (i) -> <pure,logger|e> o)
  Fx(name: string, f: (i) -> <pure,logger|e> o)

pub fun run-step<i,o,e>(s: step<i,o,e>, i: i): <pure,logger|e> o
  match s
    Pure(n, f) ->
      log-enter(n, "")
      val r = f(i) 
      log-leave(n, "") 
      r
    Fx(n, f) ->
      log-enter(n, "") 
      val r = f(i) 
      log-leave(n, "") 
      r

makes the type error go away...

there's something odd going on with inference though... If i remove the run-step result annotation i get another type error

abstract types do not match
context      : pub fun run-step<i,o,e>(s: step<i,o,e>, i: i)
               ...
                     r
term         : pub fun run-step<i,o,e>(s: step<i,o,e>, i: i)
               ...
                     r
inferred type: forall<b,c,e1> (s : step<b,c,e1>, i : b) -> <pure,logger|e1> c
expected type: forall<b,c,e1> (s : step<b,c,e1>, i : b) -> <pure,logger|$e> $a
because      : type cannot be instantiated to match the annotation

which indicates that koka is inferring the wrong type for the results of f(i)

When i add the run-step result annotation back, the type error goes away, but hovering for IntelliSense in VSCode still shows the wrong result type for f(i) (the result is shown as the same type as the parameter in IntelliSense). But - the program compiles and runs ok 🤷‍♂️

[TimWhiting]

This is related to this issue: #477. You cannot partially annotate part of a signature that is related to a polymorphic variable in the return type without also annotating the return type. I'm still not sure if this is a regression or whether this was always the behavior.

[hflsmax]

This aspect of programming with effects is a little underdocumented in Koka. As far as I understand it, all effects that are polymorphic should have the same row of concrete effects. So in your case that means you should add exn to the effects of f. Like this

Does anyone know if this is a type-theoretic limitation or if it's just that type inference in this case is not implemented.

[TimWhiting]

It is not a limitation, nor a problem with inference.

Rather, this is totally expected, but the error message and hints could be improved.

pub fun update (l: list<t>, i: int, f: (t) -> e t) : <exn|e> list<t> {
  fun traverse (l, i) : <exn|e> list<t> {
    match l {
      [] -> throw("index out of bound")
      Cons(x, xs) -> if i == 0
                      then Cons(f(x), xs)
                      else Cons(x, traverse(xs, i - 1))
    }
  }
  if i < 0
    then throw("index out of bound")
    else traverse(l, i)
}

// Should be
pub fun update (l: list<t>, i: int, f: (t) -> <exn|e> t) : <exn|e> list<t>

Because there is an exception thrown in update, thus requiring exn and since f is called under the same handlers as update (no new handlers are added or masked), then f must be called under the same handlers. Note that it doesn't mean that the function passed in as f has to throw exceptions, only that it may if it needs to. Any function can be passed in as f if the effects can unify and be subsumed by the effects mentioned in the signature. An f that uses no effects i.e. <> will be first opened to a polymorphic effect e prior to being unified with <exn|e>: making the type variables clear this means that the following constraint must hold during type inference e1=<exn|e2>. A function that uses fewer effects can easily be opened to allow for usage in places that more effect handlers are available than strictly needed.

[chtenb]

Apart from the error message, I also don't think it's explained in the book. The whole concept of unification is probably a little alien to most programmers, as you would naturally rather think in terms of subtypes, i.e. f should be able to run in update since it requires no effects that update does not have. The fact that the type system doesn't work that way is something unintuitive.

[hflsmax]

@TimWhiting Thanks for your explanation. I understand that adding concretes effect to the function argument's type doesn't impose restriction on the call-site, but I still don't get why it is needed at the first place.

Can you help me understand why the function higher-order1 type-checks, but not higher-order2?

effect eff1
  fun eff1(): ()
effect eff2
  fun eff2(): ()

fun higher-order1(f: (int) -> <eff1> int, x: int): <eff1, eff2> int 
    f(x)

fun higher-order2(f: (int) -> <eff1|e> int, x: int): <eff1, eff2|e> int
    f(x)

[TimWhiting]

Okay, how about this explanation:
Your higher-order1 function f only accesses eff1, so it's completely safe to run it in a context that has eff1 and eff2.

However, your higher-order2 function f accesses eff1, plus potentially multiple other effects in e.
Most of those effects should be fine.

However, let's assume there is a call site where f is a function that accesses eff1 and eff2 i.e. <eff1,eff2>.
So e=eff2.
That means that the return effect type must be <eff1,eff2,eff2>.

When f calls an operation of eff2 which instance of eff2 should it access, and what order are the handlers in?
Since effects with the same effect label cannot be reordered, the order matters.

However, looking at the two rows: <eff1|e=eff2> and <eff1,eff2,e=eff2> you can see that the eff2 associated with e got swapped inwards. So they should not access the same effect handler.

Koka makes you opt into those semantics (to skip the innermost handler), by forcing you to mask the effect.

fun higher-order2(f: (int) -> <eff1|e> int, x: int): <eff1, eff2|e> int
  mask<eff2>
    f(x)

This means that you expect there to be two handlers of eff2 above this point if f accesses eff2, if f doesn't access eff2 then it doesn't matter.

However, in the normal case, you want it to reach the innermost handler and not skip it.
Then you need the effect row to have the same effects as the return type.

fun higher-order2(f: (int) -> <eff1, eff2|e> int, x: int): <eff1, eff2|e> int
    f(x)

In other words those eff2 instances will correspond the same handler, since assuming e=<eff2...> will not change the fact that the body of higher-order2 and f will both access the innermost handler first.