Only allow maximally divergent functions for in-place update of local vector variables

Author: TimWhiting

doc/spec/tour.kk.md

@@ -677,7 +677,7 @@ Koka can even [reuse][#sec-fbip] the memory of the elements of the vector if the
 ```
 fun reuse()
   var myvec := vector-init(10, fn(i) [i - 1, i, i + 1])
-  myvec.update(0, fn(l) l.map(fn(x) x + 1))
+  std/core/types/@byref(myvec).update(0, fn(l) l.map(fn(x) x + 1))
 ```
 
 Because the `myvec` is unique and the value at that position is also unique, the memory of both the old vector and the old value can be used in place thanks to Perceus reference counting.

lib/std/core/vector.kk

@@ -80,21 +80,23 @@ pub inline extern copy(v: vector<a>): vector<a>
 // var v[0] := 1 // updates v in place
 // ```
 // TODO: Is this safe in cs / js? I think we might need to conservatively copy?
-pub inline extern assign/@index( ^self : local-var<s,vector<a>>, ^index : int, assigned : a ) : <local<s>,exn> ()
+pub inline extern assign/@index( ^self : local-var<h,vector<a>>, ^index : int, assigned : a ) : <local<h>> ()
   c  "kk_ref_vector_assign_borrow"
   cs inline "(#1)[(int)#2] = #3"  // check bounds?
   js inline "(#1)[#2] = #3"       // todo: check bounds!
 
 // Assign to an entry in a local `:vector` variable.
-pub inline fun assign/update( ^self : local-var<s,vector<a>>, ^index : int, f : a -> <local<s>,exn,div|e> a ) : <local<s>,exn,div|e> ()
+pub inline fun assign/update( ^self : local-var<h,vector<a>>, ^index : int, f : a -> <local<h>,div> a ) : <local<h>,div> ()
   val i = index.ssize_t
+  // TODO: Somehow get rid of div & allow linear effects
   ensure-unique(std/core/types/@byref(self))
   val x = self.unsafe-extract(i)
   val res = f(x)
   self[index] := res
 
 // Ensures that a vector in a local variable is unique
-pub inline fun local/ensure-unique(^v: local-var<s,vector<a>>): <local<s>,exn,div|e> ()
+// TODO: Remove div (need hdiv constraint)
+pub inline fun local/ensure-unique(^v: local-var<h,vector<a>>): <local<h>,div> ()
   if v.unsafe-is-unique then () else v := unsafe-copy(v)
 
 // Length of a vector.

test/cgen/vec-unique.kk

@@ -3,6 +3,11 @@ fun update(xs: list<int>): console list<int>
   println(if xs.unsafe-is-unique then "unique a" else "not unique a")
   xs.map fn(x)
     x + 1
+
+fun update-trace(xs: list<int>): list<int>
+  trace(if xs.unsafe-is-unique then "unique a" else "not unique a")
+  xs.map fn(x)
+    x + 1
 
 // This is unsafe, since the behavior that depends on this check needs to be observationally equivalent
 inline fip extern unsafe-is-unique( ^v : list<a> ) : bool
@@ -51,13 +56,13 @@ fun main()
   println("Fip update to item in local vector variable")
   var a1 := vector-init-total(3, fn(i) [i])
   a1[1] := [5]
-  update(std/core/types/@byref(a1), 2, update)
+  std/core/types/@byref(a1).update(2, update-trace)
   a1.map(fn(x) x.show).join("").println
 
   println("Non-fip update to item in local vector variable")
   var a2 := vector-init-total(3, fn(i) [i])
   val a3 = a2
-  update(std/core/types/@byref(a2), 2, update)
+  std/core/types/@byref(a2).update(2, update-trace)
   a2.map(fn(x) x.show).join("").println
   a3.map(fn(x) x.show).join("").println
 
@@ -77,48 +82,48 @@ fun update-throw2(x: list<int>)
 // The nice thing about multiple references is that it will always be copied - so there is no issue
 // The problem with exceptions, is the reference count is too low
 // 
-fun test-error1()
-  println("Non-fip update to item in local vector variable")
-  var a2 := vector-init-total(3, fn(i) [i])
-  val a3 = a2
-  try {
-    update(std/core/types/@byref(a2), 2, update-throw)
-    a2.map(fn(x) x.show).join("").println
-  } fn(err) {
-      match err.info 
-        ExnL(l) -> println(if l.unsafe-is-unique then "unique a" else "not unique a")
-      a2.foreach(fn(x) x.show.trace)
-  }
+// fun test-error1()
+//   println("Non-fip update to item in local vector variable")
+//   var a2 := vector-init-total(3, fn(i) [i])
+//   val a3 = a2
+//   try {
+//     update(std/core/types/@byref(a2), 2, update-throw)
+//     a2.map(fn(x) x.show).join("").println
+//   } fn(err) {
+//       match err.info 
+//         ExnL(l) -> println(if l.unsafe-is-unique then "unique a" else "not unique a")
+//       a2.foreach(fn(x) x.show.trace)
+//   }
 
-fun test-error2()
-  println("Non-fip update to item in local vector variable")
-  val a4 = vector-init-total(3, fn(i) [i])
-  var a5 := a4
-  try {
-    update(std/core/types/@byref(a5), 2, update-throw)
-    a5.map(fn(x) x.show).join("").println
-  } fn(err) {
-      match err.info
-        ExnL(l) -> println(if l.unsafe-is-unique then "unique a" else "not unique a")
-      a5.foreach(fn(x) x.show.trace)
-  }
+// fun test-error2()
+//   println("Non-fip update to item in local vector variable")
+//   val a4 = vector-init-total(3, fn(i) [i])
+//   var a5 := a4
+//   try {
+//     update(std/core/types/@byref(a5), 2, update-throw)
+//     a5.map(fn(x) x.show).join("").println
+//   } fn(err) {
+//       match err.info
+//         ExnL(l) -> println(if l.unsafe-is-unique then "unique a" else "not unique a")
+//       a5.foreach(fn(x) x.show.trace)
+//   }
 
-fun test-error3()
-  println("Non-fip update to item in local vector variable")
-  val a6 = vector-init-total(3, fn(i) [i])
-  var a7 := a6
-  try {
-    update(std/core/types/@byref(a7), 2, update-throw)
-    a7.map(fn(x) x.show).join("").println
-  } fn(err) {
-      match err.info
-        ExnL(l) -> println(if l.unsafe-is-unique then "unique a" else "not unique a")
-      a7.foreach(fn(x) x.show.trace)
-  }
+// fun test-error3()
+//   println("Non-fip update to item in local vector variable")
+//   val a6 = vector-init-total(3, fn(i) [i])
+//   var a7 := a6
+//   try {
+//     update(std/core/types/@byref(a7), 2, update-throw)
+//     a7.map(fn(x) x.show).join("").println
+//   } fn(err) {
+//       match err.info
+//         ExnL(l) -> println(if l.unsafe-is-unique then "unique a" else "not unique a")
+//       a7.foreach(fn(x) x.show.trace)
+//   }
 
 // This works for some reason?
-fun test-error4()
-  println("Non-fip update to item in local vector variable")
-  val a6 = vector-init-total(3, fn(i) [i])
-  var a7 := a6
-  update(std/core/types/@byref(a7), 2, update-throw)
+// fun test-error4()
+//   println("Non-fip update to item in local vector variable")
+//   val a6 = vector-init-total(3, fn(i) [i])
+//   var a7 := a6
+//   update(std/core/types/@byref(a7), 2, update-throw)

test/cgen/vec-unique.kk.out

@@ -17,9 +17,7 @@ unique a
 Non-fip copies of vector in multiple resumptions
 ["0,1,0","0,1,1","0,0,0","0,0,1","1,1,0","1,1,1","1,0,0","1,0,1"]
 Fip update to item in local vector variable
-unique a
 [0][5][3]
 Non-fip update to item in local vector variable
-not unique a
 [0][1][3]
 [0][1][2]