It seems like whether this represents a mutable or immutable data structure depends on the operations you allow. If polling with nonvar() is allowed, couldn’t you see variables mutate as you do more unification? But if it’s not allowed, I guess you get a variable to be defined later?
Compare with a Promise. If you can check whether it resolved, you can see it mutate. If the only operation allowed is to await it then from the code’s point of view, it might be considered an immutable reference to the pending result.
Yes, `nonvar/1` is considered "extralogical", in that it can be used to observe these side effects. If one sticks to "pure" logical operations (which unintuitively excludes `\+` negation) they are not observable.