Overview and explanation of the various mutation effects, local, local-var, st

[chtenb]

There seem to be several effects in use for modelling mutation in Koka. E.g. local<h>, local-var<s,a>, st<h>.
Apart from an explanation of st<h> in the book, I'm unable to find an explanation of what these different effects are for.
The compiler sometimes complains about errors related to local<h>

  inferred effect: $e
  expected effect: <local<_h>|_e1>
  because        : effect cannot be subsumed

I'm currently unable to understand what this error message means, since I don't know where local comes from and why it is there.

[TimWhiting]

st<h> models state of ref variables in some heap.

In contrast, local<h> models state of var variables in a local heap. The compiler tries to verify that references to the local variable don't escape the dynamic scope of the declaration of the variable.

I believe the compiler might be able to dismiss st<h> as well if it can determine references to the ref don't escape the scope of its declaration, but that is much more rare.

local-var<s,a> is the actual "reference" to a local variable which can be used to build generic utility functions to work with local variables.

[chtenb]

According to the book, it can:

it turns out that we can safely discard the st<h> effect whenever the heap type h cannot be referenced outside this function, i.e. it is not part of an argument or return type. More formally, the Koka compiler proves this by showing that a function is fully polymorphic in the heap type h and applies the run function (corresponding to runST in Haskell) to discard the st<h> effect."

Would you ever have to refer to a local<h> effect in your code, or is this rather something that only the compiler uses?

[TimWhiting]

Very rarely if ever you would have to use local<h> in an effect row I believe, and only in connection with using local-var<s,a>.

If you see it as an error in the compiler, it means that the compiler is having trouble figuring out how the local variable won't escape.
Two solutions to that:

1. Insert a mask<local>{expression} where you are using a polymorphic function that doesn't use the local variable, but in a context that does (and make sure if expression uses the local variable that you dereference it outside the mask and use the local val instead.
   Here are two examples from the standard library:
   

   koka/lib/std/core/list.kk

   Line 402 in 70f5609

   mask<local>{ action(j,x) }

   
   

   koka/lib/std/core/sslice.kk

   Line 256 in 70f5609

   if (mask<local>{pred(c)}) then cnt := cnt+1

2. If that still fails, try using ref instead, maybe the error messages will help you better figure out where the problem is to apply the earlier solution.

[chtenb]

Thanks, that is very helpful advice. If you have multiple local variables in a scope, how many local effects are involved with that? Just one, or one for each variable?

[chtenb]

Looks like I'm running into #154 a lot when applying your suggested strategies

[daanx]

Ah interesting -- I'll try to fix #154.
So, the local is still a bit experimental.. I added it as a variant of st specifically for local variables. There is one local-scope inserted as a runST equivalent for all local variables (to prevent escaping). Each local variable uses std/core/hnd/local-var to create a local variable that has a mini-handler so the state is correctly preserved on multiple resumptions. (This is not ideal as it makes them quite expensive and it would be nice to do this on-demand and actually use mutable stack slots instead).
I am still looking for a better way to do this though and prevent escaping using other methods (like modal types) but for now this is the best solution I think. A problem occurs though with handlers that access the local state from their action though as that would add the local<s> effect -- if the action calls some parameter f then that gets unified with the local<s> and we get an error (due to the escaping s). In such cases we need to mask the local effect which now exposes the mechanics to the user... not great. Maybe there are better ways around this issue...