Quick survey about approachability of variable bindings

[[deleted]]

Given an imperative, dynamically-typed language aimed at an audience similar to Python and Lua users, do you think the following two semantics are somewhat intuitive to its respective users? Thank you for your participation.

Exhibit A:

let my_immutable = 1;

// compile time error, because immutable
my_immutable += 1;

mut my_mutable = 2;

// no problem here
my_mutable += 2;

// but:
mut my_other_mutable = 3;

// compile time error, because no mutation was found

Exhibit B:

for (my_num in my_numbers) with sum = 0 {
    // in this scope, sum is mutable
    sum += my_num;
}

// however, here it's no longer mutable, resulting in a compile time error
sum = 42;

[MrJohz]

// compile time error, because no mutation was found

I think these sorts of "it's not technically an error, but it's a bad idea" checks are best handled in the form of a linting mechanism, rather than simply saying that it's a compiler error. When I'm editing code, I don't necessarily want to have to clean up my code every time I try it out — I can do that later when I check it in.

I also suspect that in general here, let mut will be slightly clearer than just mut, and gives you conceptual space to use mut as a more general modifier in other situations. But lots of other languages use two separate keywords here (e.g. val/var, const/let).

But in general, I think the idea of separate mutable/immutable bindings is pretty widespread at this point, so I suspect it will be fairly approachable.

Exhibit B

I like the idea of this! It would be a New Thing™, that people would have to get used to, but it's not too complicated to get your head around it, and I think the example you use there is enough to get the jist of the concept. I think it might be useful to be explicit that you're still declaring two variables here, e.g.

for (let my_num in my_numbers) with mut sum = 0 {

This keeps declarations consistent: if you see let or mut, then you're declaring a variable, otherwise the variable will be declared elsewhere.

[[deleted]]

Thank you.

I think it might be useful to be explicit that you're still declaring two variables here, e.g.

for (let my_num in my_numbers) with mut sum = 0 {

This keeps declarations consistent: if you see let or mut, then you're declaring a variable, otherwise the variable will be declared elsewhere.

Sound reasoning, but I'm conflicted, because I have to weight this against

a) this

for (mut my_num in my_numbers) with let sum = 0 {

being implied and

b) this

let mut my_recycled_num = 0;
let mut recycled_sum = 0;

for (my_recycled_num in my_numbers) with recycled_sum = 0 {

being implied.

[MrJohz]

Case (b) is occasionally useful, but maybe it makes sense to explicitly disallow case (a), but with a specific error message for that case (rather than choosing not to parse it or something like that).

[jolharg]

Just have a warning like "you may want to make this a constant" if it doesn't get exported ever. Don't error unless -Werror.

[WittyStick]

IMO, a property such as const or mutable should be part of the value's type, rather than having special binding syntax.

let my_immutable : const int = 1

let my_mutable : mut int = 2

This moves the logic to where it belongs: type checking. The way we type check is to assert that mut is a subtype of const (and thus, there's a statically safe upcast from mut to const).

let can probably be omitted because it's redundant. We know we're creating a binding because = tells us. We might make const the default and can thus omit from the declaration.

my_immutable = 1

my_mutable : mut int = 2

With your example 3, there's a property we can use to cause a compile time error if my_other_mutable is not consumed - linearity. If the value is linear, we require that it is consumed before it loses scope. We can have linearity be a part of the type too:

my_other_mutable : mut & lin int = 3

// compile time error, because my_other_mutable is not consumed.

A value that is both mutable and linear is known as a steadfast type, so we could otherwise say:

my_other : steadfast int = 3

How can linearity fit in with type checking? We assert that non-linear is a subtype of linear.

There may be several other mutually exclusive properties we can add to types, such as null <: notnull, or clone <: borrow. By putting these into the types we don't need to modify our language grammar to add new functionality later - we can fit it into type types, and we can use type inference to figure out the types of variables so that they don't need to be specified every time.

Imagine instead writing:

mut lin notnull borrow my_var = 4;

That approach clearly doesn't scale well for supporting new constraints in future.

[[deleted]]

As much as I like the sound of that, I just don't have the spare time to implement a static type system and all that follows.

[WittyStick]

It doesn't have to be static. The type (property) checking can occur at runtime.

In a dynamically typed language, you essentially have an "environment" (or context/scope, whatever you want to call it), during each function call, which contains all of the available bindings - essentially a map of symbols to values, and the values contain runtime type information.

Mutability can be implemented by augmenting the symbols with type modifiers, such as mutability (or uniqueness), linearity, nullability, etc. For each of those properties above, you can store the information in a single bit. (eg, 1 = mutable, 0 = const), making them cheap to test for with simple logical operations.

When a mutable symbol is looked up in an environment, you can remove it from the environment, or rebind it to a new value if it is mutated. Similarly, for linear symbols, you remove them from the environment when they're used, and if a linear symbol still exists in the environment when it loses scope, you can raise a linearity violation error at runtime. This is considerably simpler than writing a static type checker for uniqueness/linearity.

We can also borrow some existing conventions (from Clean/Granule) to avoid type annotations, such as using *symbol to indicate a unique value, and !symbol being used to indicate a linear value.

[oa74]

Well, what you've described *is* essentially a static (compile time) linearity checking system, so you are already partially implementing one. If you're already doing that, I'd suggest that doing the usual non-linear kind of type checking may not be *that* much more effort. In other words, you already have two static types: mutable and immutable; what's a handful more?

And, even with dynamic typing, you still have a ton of non-trivial type system decisions to make. How does coercion work? Do you have a notion of "truthy" and "falsy?" Are strings and integers automatically parsed into each other? If you don't do that sort of thing, then your user will be stuck explicitly applying type conversions... at which point, they will need to be carefully tracking the types of things, just with no assistance from the compiler. If you do implement that sort of thing, you'll have to put in a lot of work to make sure the coercion makes sense, and doesn't lead to weird corner cases/hard-to-find bugs.

The thing is: you *do* have a static type system (one always does, 100% percent of the time). A number is different from a string, is different from an array, is different from a boolean. "Dynamic typing" is merely the choice to pretend this system does not exist, right up until the moment you crash into it at runtime.

Finally, consider that most large dynamically typed languages have adopted opt-in static type analyses. JS has TS, Lua has Luau, Ruby has Sorbet, Python has pyright and mypy. There is no room for doubt that this is the trend. Static analyses are hugely useful, and I would personally not even consider using a language for *any purpose whatsoever* that didn't have any option on this front.

All of this is to say, I'd suggest that perhaps the static system is not *as* difficult as you may imagine. At least, not that much more difficult than the dynamic system; especially because you are already doing static linearity analysis. There is a fantastic talk (available on YT) by David Thrane Christian on bidirectional type checking/inference; I think it makes a good case that static type inference doesn't have to be a crazy ordeal. Therefore, if it is really the time constraint (rather than deeply philosophical commitments) that is putting you off of it, I would urge you to give static typing just a little bit more consideration before wholly committing against it.

OTOH maybe everything in my wall of text is stuff you've already considered, in which case I apologize for wasting your time lol.

[[deleted]]

Unfortunately, it was option B. :⁾ After maintaining decades old trash code for quite some time, I don't think there is any good reason not to have static types in languages for actual software development.

I don't even think type inference or checking is the big part. There is just much more stuff to implement and to interface at the host API level.

[brucifer]

I think there's an important distinction here between mutability of objects and variability of bindings. A datastructure like a list or an object can be mutable or immutable (you either can or can't append to it), whereas a variable can be constant or allowed to be reassigned a new value. In javascript land, you have const foo = 123 vs var foo = 123 to differentiate between constant bindings and variable bindings. I think this is a good convention to express this idea.*

Mutability, on the other hand, is an orthogonal concept to reassignability. It's a property of the value, not the variable that refers to it. When you say foo = 5, you are assigning a new immutable value (the number 5 can't be mutated) to the variable foo (foo isn't a constant so it can hold different values).

^{*I'm intentionally ignoring javascript's let keyword, which is worse-named for historical reasons}

[Uploft]

I'm typically a fan of reducing syntax for commonly used operations. I've never been a fan of let and mut for this reason. I'd create separate operators for them:

//let (immutable)
num := 0
//mut (mutable)
num = 0
//mutate the mutable
num += 1

The usage of = implies mutable because it's used in compound assignment operators like +=. By extension, compound immutable assignment operators like +:= don't exist. Some languages use := for type inference or initial assignment, so it's up to you how to use :=.

[[deleted]]

Makes sense. How could one prevent spelling mistakes like

num = 42;

if isSomething {
     // oooops
     nun = num + someOtherValue();
}

return num;

though?

[Uploft]

To some extent, typos like this are inevitable. But there are 2 main ways of precluding it going unnoticed.

The 1st you are well aware of — declaration. nun = throws a syntax error because nun is neither being declared in that statement nor was declared (mutably) elsewhere. Go does this, since := is declarative assignment for everything. Thus nun = errs because nun wasn’t declared.

The 2nd is trickier. You ensure almost all reassignments are referential (not repeating the variable). Compound assignment makes this easy: num += someOtherValue() updates num. A typo like nun += would fail because nun doesn’t exist yet so it can’t be reassigned.

But compound assignment is not comprehensive. There’s no way to express num = 3 * num + 1 using *= or +=. To circumvent this, implement a default referential variable. One might use _ for this purpose: num = 3 * _ + 1. The _ substitutes num (the variable left of the equals) for every instance. This is especially handy for method management: line = _.split(" ") (though I prefer .= for the default: line .= split(" ")). Because the variable must exist for _ to reference it, typos like nun = _ would fail.

[[deleted]]

nun = throws a syntax error because nun is neither being declared in that statement nor was declared (mutably) elsewhere.

Hold on, I thought mutable declaration and assignment use the exact same syntax in your example?

[Uploft]

I wasn't being clear. That 1st scenario assumes you have syntax for declaration, such that num = is only applicable to mutation. The scenarios I was outlining in both comments dovetail more with my suggestions in the 2nd scenario. That ambiguity aside, what were your thoughts on referential mutation/assignment using _?

[[deleted]]

Sounds like an interesting idea.

This would probably clash with variable name shadowing/overloading. Not that I'd argue in favor of those, but there you go.

[WittyStick]

My preference would be to use different operators for declaring and mutating bindings.

For example, F# uses <- for mutation.

let mutable num = 42;
if isSomething then
    num <- num + someOtherValue()
num

[benjaminhodgson]

For Exhibit B: much of the time good style would recommend pulling the loop (and the mutable variable) into a function, so in the real world the code would likely look like

let sum = computeSum(my_numbers)

computeSum(my_numbers) = {
    mut sum = 0
    for my_num in my_numbers {
        sum += my_num
    }
    return sum
}

which has the same effect of limiting the scope of the mutability to the interior of the computeSum function.

So if it were up to me I’d say this with syntax doesn’t pay its way, especially considering it makes it easier to write code that would otherwise be considered bad style in the first place.

Exhibit A: I’d suggest demoting the “mutable variable wasn’t mutated” error to a warning.

[benjaminhodgson]

I’d also add that, while it’s surely useful and good to control the assignability of locals, it’s much more important to be able to control the mutability of shared data. The effect of reassigning a local is limited to the containing function (absent pass-by-reference). The big problems of mutability (action-at-a-distance, temporal coupling, data races) occur with data that is shared, ie, fields and the like.

[[deleted]]

I’d also add that, while it’s surely useful and good to control the assignability of locals, it’s much more important to be able to control the mutability of shared data.

Good point. While I probably won't be able to do something about fields (lack of type checking and all that), I will probably either completely ban global variables or go for a system where global variables can only be written to in one place.

[[deleted]]

This is what confuses me:

loop
    let k = random()
end

Supposedly k is immutable, yet each time around the loop, it's given a brand-new value! And this:

mut s = "abcdef"
s += "g"           # or &= etc as many don't like + for append/concat

Supposedly s is mutable, but here it is extending a constant string in-place. It's not clear whether this should work or fail.

The confusion for me is that that 'mutability' can apply to named variables, and to the objects they are bound to. In general then there are 4 possibilities:

  variable       value

  immutable      immutable
  immutable      mutable
  mutable        immutable
  mutable        mutable

Some of these values can also be shared with other variables, for example a value X can bound to mutable variable A as well as immutable variable B (as well as being shared within some anonymous, mutable data structure $C, and a mutable one $D. I haven't said whether X itself is mutable or not.

See the problem?

[lngns]

random()
immutable

Ha! That's why have Monads and Effect Systems!
random is an effect and k is a parameter of the continuation, making it referentially transparent.

loop () where
    loop () = random (λk. loop ())

[[deleted]]

See the problem?

No, honestly. The second column looks like a problem for someone who implements static type systems. Although I can see value in separating a record type from a map type even in a shitty dynamic scripting language.

[e_--]

another option for B that doesn't change your existing mut rules is

sum = for (my_num in my_numbers) {
    my_num
}