Design mutability semantics

[jfecher]

Right now, mutability is temporarily tied to the ref a type which isn't desirable since it ties mutability to lifetime inference. There are a few open questions and wants as to how mutability should be designed:

1. Mutation x := y should likely create a mutation effect of some kind (say Mutate t). This effect would need to be percolated up to a functions signature iff x is used as a parameter (or global). If x is local to the function, it is internal mutation so callers would not need to care and the constraint should not be propagated. Interestingly, these are actually the rules traits use for inference so perhaps it should be a built-in trait instead. Prior art here includes koka with its st<h, t> effect for a mutable state t in heap h. The heap parameter is used to determine if the state is local or not. Edit: The reasoning for this rule is so that we can disallow mutation in new threads via Thread.spawn: (unit -> unit can []) -> unit can IO which explicitly disallows any extra effects in the function to run in a new thread. Note that this won't solve the problem of the master thread mutating a reference it passes to a child, it only prevents the child from mutating it.

2. It is unclear whether mutation should be inside the type system as a mutable reference type, or outside of it as a variable modifier. We'll need to explore the tradeoffs of both.

3. Related is that assuming we have mut t for a mutable reference to a value and t for a value, we could construct a mutable value via a function t -> mut t. This doesn't seem to allow for immutable values if we can convert any t to a mutable one. Moreover, what are the semantics for this conversion? Do we shallow or deep copy? Do we move?

4. If we have a mut StructType we should be able to project the mutability to a field struct.foo := struct.bar where the lhs resolves to a mut FooType and the rhs resolves to a BarType (ie only struct.bar is dereferenced despite both being field accesses). Do we need field accesses to be polymorphic over mut-ness? The current compiler slaps a band aid on this by having a separate operator struct.&foo for getting a reference to a field.

5. Similarly, it'd be nice if mut T were implicitly convertible to an immutable version to pass to functions that don't require mutation. Rust allows an implicit &mut T to &T conversion for example. The current ante compiler only has T and ref T, and so does not allow this at all since you must explicitly deref T.

We should come up with a design that addresses all these points (and others?), and is ideally easy to use/understand for users. Feel free as well to address only parts of this design or leave opinions below.

I list this as "good first issue" but perhaps this isn't right since it can have a few more complex interactions with type inference, effects, and general usage/vision.

[PROMETHIA-27]

1. How exactly would this effect correlate to parameters? If I have the function

mutate (x: I32) (y: I32) can Mutate I32 = ...

does that mean it can mutate one, or both? Which one if only one?

2. As prior art, rust has both:

let mut = // a mutable place
let r = &mut // a mutable reference to something

3. As further prior art, rust sort of has this function represented via move semantics.

let s = "mutating".to_string();
// can't mutate an immutable place
// s.push('c');
let mut s2 = s;
// now we can
s2.push('c');

5. I think further consideration of this requires ironing out the previous issues, since it's not certain if there will even be a mutable reference type and/or mutable places

[jfecher]

@PROMETHIA-27 apologies for the late response, forgot about this comment!

does that mean it can mutate one, or both? Which one if only one?

Though it depends on the definition of the effect and the handler used, effects have no relation at all to parameters. There's nothing binding this Mutate effect to x or y in your example so one can only assume it is like a State effect which automatically threads through a mutable variable in your program like ST in haskell. This isn't the only design we could use though.

2. As prior art, rust has both:

Yep. And OCaml has only the mutable modifier which is only useable on struct fields. Then it uses this to implement the ref type. Haskell has IORef as a mutable variable type, where using/referencing it requires the IO monad. Koka also has local mutable variables where you cannot mutate them across functions.

3. As further prior art, rust sort of has this function represented via move semantics.

I think "move semantics" alone is not really a sufficient answer here because there are a lot of questions you have to answer before you can get them. The main one being that the language should not have every value be move only, so how should you convert between moveable and shared values? Rust has moveable everything by default and shared references. There are more formal systems however which rust is sometimes translated to for papers in which values are shared by default with a set of identifiers of what they are shared to. So x{y, b} is the variable/value x which is shared with the variables y and b. If ante adopts this system then we could have the somewhat easy answer of "you can make a value mutable as long as its not shared by anything else" while keeping sharing easy and somewhat sidestepping whether something is actually "moved."
This idea is called "reachability types" and here's one such paper for them: https://www.cs.purdue.edu/homes/rompf/papers/bao-oopsla21.pdf.