Can't use CPS with extern functions

[Pauan]

Consider this Koka module foo.kk:

module foo

extern include {
  js file "foo-inline.js"
}

public extern foo(fn: () -> e a): e a {
  js "foo_inline"
}

fun main() {
  foo { 1 }
}

And this JavaScript file foo-inline.js:

function foo_inline(f) {
  return f();
}

---

When compiling, I get this output:

function foo_inline(f) {
  return f();
}

function _cps_foo(fn, _k) /* forall<a,e> (fn : () -> e a) -> e a */  {
  return foo_inline(fn);
}

function _fast_foo(fn) /* forall<a,e> (fn : () -> e a) -> e a */  {
  return foo_inline(fn);
}

function foo(fn, _k) /* forall<a,e> (fn : () -> e a) -> e a */  {
  return ((_k !== undefined)) ? _cps_foo(fn, _k) : _fast_foo(fn);
}

function main() /* () -> int */  {
  return foo(function() {
    return 1;
  });
}

Depending on whether the effect is CPS or not, it will call either _fast_foo or _cps_foo.

However, there is a problem: _cps_foo calls foo_inline, but it doesn't pass in the _k CPS argument. This means that foo_inline cannot work for CPS effects.

This can be solved by changing _cps_foo to pass in the _k parameter.

Or alternatively it could be solved by adding in a new mechanism to specify different behavior for CPS vs non-CPS:

public extern foo(fn: () -> e a): e a {
  js "foo_inline"
  js cps "foo_inline_cps"
}

This would also work with inline:

public extern foo(fn: () -> e a): e a {
  js inline "foo_inline(#1)"
  js inline cps "foo_inline_cps(#1, #2)"
}

Personally, I prefer this solution.

[anfelor]

Closing this issue since Koka now uses a different translation of effect handlers which allows this kind of code by explicit calls to kk_yielding.