koka-lang / koka

Koka language compiler and interpreter
http://koka-lang.org
Other
3.16k stars 151 forks source link

Suggestion: Generalize type variables in mask behind #519

Open anfelor opened 1 month ago

anfelor commented 1 month ago

In Koka, we can use mask behind to override a handler as such:

effect eff<a>
  ctl op() : ()

fun test(comp : () -> <eff<a>|e> ()) : <eff<a>|e> ()
  with ctl op() -> {op(); resume(())}
  with mask behind<eff>
  comp()

However, this currently only allows us to override an effect with exactly the same effect, including type variables. Thus, we can not write: fun test(comp : () -> <eff<a>|e> ()) : <eff<b>|e> () (notice the b in the last effect row).

Is there anything stopping us from allowing a different type variable on the masked effect? Concretely, I am suggesting to change the type signature of mask behind from:

mask behind<eff> : forall<a,b,e> () -> ((() -> <eff<a>|e> b) -> <eff<a>,eff<a>|e> b)

to:

mask behind<eff> : forall<a,a1,b,e> () -> ((() -> <eff<a>|e> b) -> <eff<a>,eff<a1>|e> b)

where all type variables in the masked effect are now generalized (as a1 here). @jasigal has a larger example where this functionality would be useful.

jasigal commented 1 month ago

In general, I find this useful when there's a purely local need to handle an effect using a different version of it, meaning named handlers aren't really needed.