Mutable Value Semantics Trend vs Immutability

#1

In functional programming, purity immutability is one of the concepts that people usually emphasize on. By purity, I understand as enforcing values in the program to be immutable, at least as a specification for the language user (this includes languages such as Koka-lang where as a backend optimization their values might get mutated once it is statically knowable that the reference is unique)

However, as I observe, in these recent years, a new trend (not that the idea is new, but it is the first time the idea gains significant attention from the public outside of academic I suppose) that I would conveniently label as mutable value semantics (MVS for short), as borrowed from Native Implementation of Mutable Value Semantics has occurred. The most noticeable events would be the rising of Rust, with its ownership and borrowing system. Also, Hylo | The Hylo Programming Language (hylo-lang.org) also catches my attention.

To be self-contained, here is what I mean by my umbrella term MVS:
When calling functions on variables, the compiler does things more intelligently and tracks the change of state of the variables being used, instead of being overly optimistic like Haskell where variables are supposed to be unchanged, thus purity has to be enforced, or being overly pessimistic like usual imperative languages where statically analyzing the states is deemed infeasible in general.

Here is a simplest example, in Rust,

fn use_it_up(x:String) {
    println!("I consume the {:?} now, you cannot use it any more!", x)
}

fn main() {
    let x = "123".to_string();
    use_it_up(x);
    use_it_up(x);  // again
          //  ^   
          //compiler would decide the x here 
          //is no longer usable, and complains
}

This code results in an error saying that I am attempting to use a moved value. (Well strictly speaking it is not mutating values so my usage of the term MVS is bad but I emphasize on the fact that the state of the used variables in the expression is semantically changed after the function call, i.e., in this case, the value of x becomes moved).

In other more complex examples, the compiler might track whether the variables are getting referenced (borrow checker in Rust), or whether the variables will be put back, like inout.

If one has to get into a holy war between programming paradigms, I might say this feels like a comeback for imperative programming. But eventually, FP or IP, in terms of semantics (as opposed to syntax), I personally only care about how I communicate with the compiler, the library and the user. And MVS feels a much more nuanced way to do so compared to both worlds of the past (just assume it is impure mutability or just enforce purity immutability).

In fact, this line of trend totally moves me out of the purity immutability camp (never in tbh). It is probably better, instead of saying we should ban mutation because it causes all sorts of problems, to say that we should communicate our intention as clearly as possible to the compiler, the caller, and the callee so that when I mutate or want to keep a reference to a value, they can be noticed, so that they can leverage their tools to optimize, verify and modularize.

But in Haskell, the fundamental of it seems to prevent such addition? I want to know what the Haskell community thinks of these kinds of language features(?), whether it is actually good or bad compared to alternatives, its desirability and feasibility in Haskell.

3 Likes
Introducing NeoHaskell: A beacon of joy in a greyed tech world
#2

I think that the recent developments with Linear Types might be up your alley.

x %1 -> ... means x has to be used exactly once inside the function. (Parts of it) cannot be discarded nor duplicated (unless they implement the Consumable resp. Dupable traits).

Because the compiler knows for certain that inside the function there will only be a single x, extra copies/memory allocation is prevented. In a sense, this makes x similar to an inout parameter from the paper except in a way that fits better with the rest of Haskell’s pure functional type system.

One disadvantage of linear types in Haskell (compared to e.g. Rust’s borrow checking) is that they are ‘opt in’, in the sense that they restrict the callee (the contents of a function) but not the caller from holding on to a copy of the data.

Thus, some slightly less beginner-friendly ‘callback style’ APIs have to be used to fully restric values to uniqueness. (example: Data.Array.Mutable.Linear.alloc) and also if you want to use linear types to their full extent, you want to ‘enter linear land’ very early in your program.

But while the ecosystem around linear types is still very young/small, it is very promising!

4 Likes
#3

Yes. I see nothing wrong with using a value more than once.

And I’m not sure you’re understanding ‘purity’ in a Haskell context: it means making the result of a function dependent only on its arguments. (Not, for example running some IO in the middle of a calculation to grab some value from ‘the world’ – as you can do in C.)

The other gotcha Haskell avoids is call-by-reference, where some innocent-looking function can update a global variable (‘Jensen’s Device’ from the ALGOL 60 report nowadays considered harmful). So the result of the function does depend only on the arguments passed; but the value of the rest of the program depends on what evil the function perpetrated in passing.

Well, no. All of the above trickery was commonplace in machine-level programming in the 1950’s. ALGOL was a serious attempt to control/discipline the resulting confusion. ‘Structured Programming’ 1968 went further, leading on to functional programming.

2 Likes
#4

Thank you. The mutable structure looks nice. (One nit-pick might be why throwing errors instead of returning a Either type in the safe version of APIs. :slight_smile: because we already paid the cost of runtime check already)

If I understand it correctly, by restricting the surface area of my APIs to my dependency (for example, I could decide the only entry of certain library types to be in some restricted files, where I instantly wrap the library type into a linear type, exporting only linear interface), I could be in a fully linear world built upon these wrappers? That is a not bad partial approach to the problem (of resource management).

But again, MVS seems to be a bit richer than just linearity and uniqueness. Other aspects include whether a variable is write-only (which is not in Rust (not built-in at least), but in the passing convention set in Hylo, (at least as they (Hylo) claims)), whether some reference(s) is held by others. Maybe Haskell can also (but also has to if want to) add some constructs to allow such feedback to the compiler. The problem though would be that code might be obscured by over-annotation (which Rust kind of already suffers).

Maybe a last side node is that syntax-wise, there is something more intuitive when
calling close door could change the door's type from OpenedDoor to ClosedDoor. One might instantly argue against this as this complicates reasoning. My thought is that, as long as the compiler work it out, and the behaviour of the called function is well-labled by its type signature, I would prefer this unorthodox solution.

#5

I’m not sure you’re understanding ‘purity’ in a Haskell context.

Thank you for correcting my misuse of the term purity. I have gone over my head. I should have used the term immutability.

I see nothing wrong with using a value more than once.

For me, it is wrong in Rust because Rust has a finer-grained semantics on the underlying resources and there is no value more than a value represented at certain computational resources. Then by default, using is really claiming that from now on nobody but me got to touch it, until I give it away or borrow it to someone else. In contrast, since in Haskell, a value is Just a value agnostic of its underlying representation, it is ok in Haskell to use a value more than once.

#6

Haskell also has this “hybrid” ability (to an extent) - by using the monadic ST type, a function can have an imperative implementation but without imposing an imperative interface on its callers, by using runST. Others have also mention more recent developments e.g. linear types.

No. And in fact, your prior observation:

…is a reasonable description of what usually happens in Haskell: by using types, we can indeed “communicate our intention as clearly as possible to the compiler, the caller, and the callee so that when I mutate or want to keep a reference to a value, they can be noticed, so that they can leverage their tools to optimize, verify and modularize.”

But this approach just isn’t to everyone’s liking:

…or as I described it here:

[…] the siren call of pervasive imperativity is still just as beguiling […]

…a recent case in point:

Mutation: it remains just as troublesome, but we still can’t seem to get rid of it entirely! This seems promising:

…but there doesn’t appear to be a great interest in making Haskell parallel by default (at least for now), which would help greatly to show the advantages of keeping things immutable as much as possible. And so in the absence of progress towards eliminating mutability entirely, new “not-as-imperative” languages have appeared, with each promising to simplify “the great mutability divide” in one form or another…and here we all are.

2 Likes
#7

This is possible with GADTs!

data DoorStatus = Open | Closed

data Door (status :: DoorStatus) where
    OpenDoor :: Door Open
    ClosedDoor :: Door Closed

newDoor :: Door Open
newDoor = OpenDoor

-- This is exhaustive, because the compiler knows
-- OpenDoor is the only constructor that can have
-- the type Door Open
closeDoor :: Door Open -> Door Closed
closeDoor OpenDoor = ClosedDoor

IIRC I don’t think Rust could do this

#8

Yes, but unfortunately the open door is still in scope!

1 Like
#9

ah I didn’t see the ask was to mutate the type of door… yes that’s quite different.

Possibly some combination of my snippet + linear types + allow name shadowing?

#10

I remember the 90s, when my computer was running on a PowerPC CPU, and there was this functional language, called Clean, which was essentially a dialect of Miranda / Haskell, but with some kind of linear types. Instead of writing :: IO a, people would write :: *World → (*World, a), a function type where the World argument could be used only once.

So, yes, mutability is possible in a Haskell-like language using linear logic.

The real question is: Why would you want to do that? Does it make your code faster to write, easier to prove correct, or faster at running?

#11

The real question is: Why would you want to do that? Does it make your code […] easier to prove correct?

Possibly, yes:

…I only say “possibly” because advances in proof techniques and tool may now have simplified the use of abstract monadic state in correctness proving. But I will defer to the experts here on that topic!

Other work by those and associated authors include:

1 Like
#12

What I meant was more “why mutability in the first place” rather than the more specific question of “why linear logic for mutability”. It seems clear to me that a Haskell program which does not mutate explicitly is easier to reason about than a program which does.

#13

From the abstract of State in Haskell (1995):

  • …with the caveat that some of those algorithms have now been superseded by “mutability-free” alternatives - otherwise, there’s still the type ST s a, and most importantly:

    runST :: (forall s . ST s a) -> a

  • …with the caveat that:

    …oh, that’s right - they didn’t. But they’re not the only ones wanting Haskell to be rid of IO a:

    Denotative programming timeline - HaskellWiki

#14

A slight correction: a set parameter in Hylo is not write-only, but must be written before it can be read, because it enters the function in an uninitialized state.

#15

The premise of Mutable Value Semantics is that mutation itself is not troublesome; instead the problem is the mutation of shared state. Obviously, the global variables mentioned in the article you cite are extremely shared.

1 Like
#16

But mutation by itself is troublesome:

…and mutation is the epitome of side effects! As I mentioned in this post on a related topic:

#17

If I were to design a new language, I’d definitely try to have mutable value semantics (in the pure fragment of the language, of course). More recent languages like Lean or Koka do that very successfully. If we had a good macro system, we could just copy the Lean approach, which desugars to simple, pure state passing, just like what the State monad would do, but less clumsy. It is the obvious idiom to apply for many kinds of algorithms.

2 Likes
#18

[…] simple, pure state passing, just like what the State monad would do, but less clumsy. It is the obvious idiom to apply for many kinds of algorithms.

Sure, the macro system would be dealing with the extra state parameters and arguments…but the code will still look imperative. So either approach isn’t really going to make that much of a difference with regards to aesthetics.

#19

The significant increase in complexity caused by mutation is almost entirely due to sharing.

There is nothing intrinsically more complex about this program compared to its “pure” counterpart:

var p = (x: 1, y: 2)
p.x = g(p.y)
p.y = g(p.x)
print(p)

Without even mentioning a specific programming language, I strongly suspect that everyone reading this thread knows what the intent of this program is and can predict its outcome. Therefore, renaming each intermediate value of p for the sake of immutability would arguably just add noise to this particular program, while collapsing everything into a single expression would make it harder to read. And if = offends, one can always pick another symbol.

This program is not only obvious to humans but also to compilers. While smart developers and optimizers can understand that p' = (x: g(p.y), y: p.y) is actually equivalent to a partwise in-place update of p, it is actually not an easy guess. To the best of my knowledge, a general procedure for all functional updates has yet to be discovered. In contrast, p.x = g(p.y) is concise and straightforward.

To me, these observations suggest that there’s an intrinsic value to mutation that is worth preserving and goes beyond convenience. Instead, it relates to some “truth” about the act of computing anything, especially if that computation takes place in the real world. Not everything is better expressed as a declarative relation (O’Neill 2009, The Genuine Sieve of Erathosthenes); I prefer baking using imperative recipes.

Losing confluence does indeed increases complexity. But again, when sharing off the table, the only issue is to define a precise evaluation order so that people (and machines) can reason about it. That is not as troublesome as it may sound. One can pick innermost, left-to-right and then an expression like f(p)(g(p.x), g(p.y)) is deterministic and unambiguous.

#20

I don’t think I can understand it! Let me try. First p.x is set to g(p.y). Then p.y is set to g applied to the (presumably) new value of p.x, that is g of the original p.y? So the final value of p.y is g applied to g applied to the original value of p.y?

If that’s really the intention then I think I’d prefer to see

p' = (x : g(p.y), y : g(g(p.y)))

Isn’t that the “pure counterpart” you’re referring to? I certainly see it as less complex.

2 Likes