Draft: Design of Mutable State (WIP)

[b-studios]

At the moment, mutable state in Effekt is modelled with instances of the Region interface:

• global mutable state is a global, toplevel capability of type Region that we can allocate global variables into
• local mutable state (within functions) create a new region this: Region that we use to allocate local variables into
• region-based memory management is achieved by the term-level construct region r { STMT } which brings a region r: Region into scope that can be used to allocate fresh cells into.

It is very appealing that all of these variants of mutable state can be expressed with the same concept. However, backends implement some of these variants differently. For example global mutable state is typically special-cased.

In the lifted setting (especially in the context of recent work on monomorphization), it becomes more and more clear that we want to distinguish different use cases in order to implement them more efficiently. Talking to @phischu we made the following assumptions:

1. Local mutable state will almost never allocate cells dynamically – i.e., we almost never see code like:

   def foo() = {
     var x in this = 0;
     bar {this} // where bar allocates into `this`
   } 
   

2. A lot of allocations into dynamic regions are monomorphic – i.e., we expect to see code like

   region r { var x in r = 0; var y in r = 1; ... }
   

   but not code like

   region r { var x in r = 0; var y in r = Tuple(true, ""); ... }
   

Alternative Design

Under these assumptions, we might sketch the following alternative design. Internally, we have two interface types Local and Region[T].

• Local is never user-facing. Function local, mutable variables will be automatically desugared into usages of Local. For example

  def foo() = {
    var x = 47;
    var y = true:
    ...
  }
  

  may result in

  interface Local$foo { def x$get(): Int; def x$set(n: Int): Unit; def y$get(): Boolean; def y$set(b: Boolean): Unit }
  
  def foo() = local$foo { {frame:Local$foo} =>
    frame.x$set(47);
    frame.y$set(true);
    ...
  }
  

  Technical note: In the lifted setting (iterated CPS), these locals could be implemented in cont-over-reader (k1 => s: (Int, Boolean) => k2 => ...). Either each local introduces an additional component and lift is "jump over one component", or we structure lifts as (van Laarhoven) lenses. In the latter case, multiple subsequent mutable frames could lead to evidence that corresponds to lense-composition.

• Region[T] is monomorphic in its type T.

  def foo() = region r: Int { 
    var x in r = 0;
    otherFunction {r} // can allocate into r
    ...
  }
  

Technical note: Again, this way we can model regions as k1 => r: Arena[T] => k2 => ... in iterated CPS. Allocating (and potentially reading and writing) would require evidence to find the position to allocate into the stack.

Everything here is still up to discussion. Especially the design of Local as a specialized interface is very premature.

Other open questions: How should we model global mutable state in this light? Do we need to know all global mutable references up front (by "declaring them" at the toplevel -- very much like Local) or do we want to support dynamic allocation? Right now, I very much are in favor of the former option.

[b-studios]

In #231 you can see what is necessary to pass evidence to get, put, and fresh.