Using scope kind to prevent values to escape

[timjs]

Do I understand correctly that Scope kind S keeps track of a local scope and makes sure a value doesn’t escape its surroundings? But how does it work? I’d like to create a data type that has a similar escape analysis as local-var, but I don’t seem to succes. Say something with an interface like the code below.

pub fun ptr(v: a): scope<s> ptr<s,a>
pub fun deref(p: ptr<s,a>): a
pub fun set(p: ptr<s,a>, v: a): ()

fun main()
  // This is all fine
  val p = ptr(32)
  println(p.deref)
  p.set(57)
  println(p.deref)

  val c = counter()
  println(c())
  println(c())

fun counter()
  val c = ptr(0)
  return fn() // ERROR: this shouldn't work! (Like with var).
    c.set(c.deref + 1)
    return c.deref

Hope anyone can help.

[TimWhiting]

Here is one solution: create your own abstract (non-handled) effect type, and mimic the reference / local-var.

struct ptr<s::H,h::H,a>
  v: ref<h,a>

pub type scoped<s::H> :: H -> X

pub inline extern unsafe-add-scope(f: () -> e a): (() -> <scoped<s>|e> a)
  inline "#1"
pub inline extern unsafe-remove-scope(f: () -> <scoped<s>|e> a): (() -> e a)
  inline "#1"

pub fun scoped<a,e>(f: forall<s> () -> <scoped<s>|e> a): e a
  unsafe-remove-scope(f)()

pub fun ptr<s,h,a>(v: a): <scoped<s>,alloc<h>> ptr<s,h,a>
  val r = ref(v)
  unsafe-add-scope(fn() Ptr(r))()

// Or scoped + ptr 
pub fun scoped-ptr(v: a, act: forall<s> (ptr<s,h,a>) -> <scoped<s>,alloc<h>|e> b): <alloc<h>|e> b
  with scoped
  act(ptr(v))

pub fun deref<s,h,a>(p: ptr<s,h,a>): <scoped<s>,read<h>,div|e> a
  !(p.v)

pub fun set<s,h,a>(p: ptr<s,h,a>, v': a): <scoped<s>,write<h>> () 
  val ptr = p.v
  ptr := v'
  ()

fun main(): <console,div> ()
  with scoped
  // This is all fine
  val p = ptr(32)
  println(p.deref)
  p.set(57)
  println(p.deref)

  val c = counter()
  c.println
  // println(c())
  // println(c())

fun counter(): div int
  with c <- scoped-ptr(0) // or: with scoped; val c = ptr(0)
  // ERROR: this shouldn't work! (Like with var).
  fn()
    c.set(c.deref + 1)
    c.deref

I think the scoped<s> is specifically intended for named effects within effect scopes. I don't think it is intended to do what you expect here.

You'll notice in my example I add scoped-ptr which is not necessary with local vars, because Koka automatically attempts to insert something equivalent of scoped above variable introductions.