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.