Open evincarofautumn opened 9 years ago
We can add a mut
operator with a special typing rule:
Γ ⊢ e : ∀H. (R… → S… +Mut<H> +P), H ∉ free(R… → S… +P)
------------------------------------------------------
Γ ⊢ e mut : R… → S… +P
This is basically Haskell’s runST
, adapted to permissions rather than monads, and without an existential (or rank-2 universal) type. Then { … } mut
or do (mut) { … }
enables local mutation of non-escaping variables:
type Var<A, H>
define var<A, H> (A -> Var<A, H> +Mut<H>)
define load<A, H> (Var<A, H> -> A +Mut<H>)
define store<A, H> (A, Var<A, H> -> +Mut<H>)
// -> Int32 +IO
do (mut):
1 var -> x;
x load say
2 x store
x load dup say
// -> Var<Int32, H>
// error: mutable variable would escape its scope
do (mut):
1 var
With an operator like addr(lvalue)
, this could let you take the address of a local value or field and safely pass it down the call stack. There would need to be some operators or other sugar for load
and store
, such as Forth’s @
and !
. The aforementioned fat-arrow syntax a => b;
could be sugar for a addr(b) store
.
The arrow syntax introduces a local variable.
Introducing another local by the same name doesn’t mutate it in place. Rather, the new variable shadows the original one.
I propose a fat-arrow syntax for mutating local variables in place.
The right hand side of a fat arrow is (ironically) an lvalue, not an expression—it can be extended to mutate fields of structures by index.
Or by name, if we introduce notation for named fields in type definitions.
Array indexers should also serve as lvalues.