Can the idea of Affine (relaxed Linear) Types be implemented in an untyped setting to enable safe mutations?

129 views Asked by At

It'd be useful if I could use safe in-place destructive updates on Arrays and Maps every now and then. Linear types are a technique to allow safe mutations by restricting the consumption of values to an exactly once semantics. While it seems not possible to implement exactly once in Javascript, here is an implementation of the relaxed at most once variant, which corresponds to affine types:

class LinearProxy {
  constructor() {
    this.once = false;
  }

  get(o, k) {
    if (this.once)
      throw new TypeError("non-linear type usage");

    else this.once = true;

    if (k === "run")
      return once(f => {
        const r = f(o);

        if (r === o)
          throw new TypeError("non-linear type usage");

        else return r;
      });

    return o[k];
  }

  set(o, k, v) {
    if (this.once)
      throw new TypeError("non-linear type usage");

    o[k] = v;
    return true;
  }
}

const linear = o => new Proxy(o, new LinearProxy());

const once = f => {
  let called = false;

  return x => {
    if (called)
      throw new TypeError("non-linear type usage");

    else {
      called = true;
      return f(x);
    }
  };
};

const run = f => tx =>
  tx["run"] (f);
  
const id = x => x;
const last = xs => xs[xs.length - 1];
const dup = xs => [...xs, ...xs];

const xs = linear([1,2,3]),
  ys = linear([1,2,3]),
  zs = linear([1,2,3]);

xs[3] = 4;
xs[4] = 5;

console.log(
  "run(last) (xs):",
  run(last) (xs)); // 5

try {run(last) (xs)}
catch(e) {console.log("run(last) (xs):", e.message)} // type error (A)

try {const x = xs[4]}
catch(e) {console.log("x = xs[4]:", e.message)} // type error (A)

try {xs[0] = 11}
catch(e) {console.log("xs[0] = 11:", e.message)} // type error (B)

try {run(id) (ys)}
catch(e) {console.log("run(id) (ys):", e.message)} // type error (C)

console.log(run(dup) (zs)); // [1,2,3,1,2,3] (D)

Subsequent read access (A) and write access (B) of once consumed linear types throw a type error. The attempt to gain immediate access to the reference (C) of a linear type also throws a type error. The latter is just a naive check to prevent returning the reference by accident. One could easily bypass it, so we must rely on convention for this case.

However, D is not affine, because the argument is consumed twice. Does the fact that the non-linear use happens within a function scope means that it is still (relatively) safe? Is there a more clever way to implement linear types in Javascript?

0

There are 0 answers