3
$\begingroup$

Question

My use case for what is described below is not a language or compiler implementation, but finding a reasonable semantics for this feature in a an abstract calculus.

Ideally, you give me a name for this concept, with references to a language that implements it and how that is done, or a theoretical exposition of how it could be done. Of course an original idea is highly appreciated, too.

A solution combining metaprogramming with an existing language feature is fine as well.

Detailed examples

I don't really know whether the concept I have in mind already has a name. I'm looking for a language feature by which you can declare variables referring to complex data types from their parts, as they were mutable, without them actually being mutable.

The essential part of what I imagine is not the controlled immutability, though, but the ability to "synthesize" an immutable structure implicitely from "assignment-like" forms.

Let's assume for now that such special variables are written as <x>. As an example, take a Markov chain:

<x[1]> = 0
for n in 1:N {
    <x[n]> = <x[n-1]> + rand()
}
print(<x[2]>) # OK
print(<x>)    # OK (but I never wrote `<x> = ...`!
<x[2]> = 2    # ERROR (mutation)
<x[N+1]> = 3  # ERROR (usage after completion)

Note that:

  • x is not needed to be "initialized", to an empty or uninitialized sequence or otherwise.
  • When the whole <x> is used, it is "unified" from all the individual <x[i]>.
  • I'd like the <x[i]> to behave just like single variables, as if the loop were completely unrolled to scalars x_i.
  • As soon as <x> has been "unified", it can no more be updated. At that point, <x> is assumed to be "complete".
  • The errors should not occur just at runtime, but be statically detectable -- either as a type error, or after some other kind of analysis.
  • Arrays are just an example. In principle, the same concept should also work for <x> being a struct, and several fields of it (<x.foo>) assigned after each other.

The code above is not trivially transformable to an initializer; it is expressible as an unfold, but I want this to work generally. I can imagine that a system of this kind could more easily be designed when the components are statically known:

<x[1]> = 1
<x[2]> = <x[1]> + 1
sum(<x>)

can be simply rewritten as

<x> = (1, 1 + 1)
sum(<x>)

but that's not enough flexibility.

And I'm not doing Prolog, so only "unification" is not enough of an answer. This is unification of mutation statements in imperative syntax.

Ideas for realization

Syntax

I can imagine something like a VB with statement, as follows:

with <x> {
  <x[1]> = 1
  <x[2]> = <x[1]> + 1
}
print(<x>)

but that's not quite as implicit as I want. Also, at least it would have to allow arbitrary statements within its body, without imposing restriction on interdependencies. And once that's possible, you could probably just infer the boundaries of the "with block" automatically as the largest range of expressions from the first mention of any <x[i]> to the first usage of <x>.

That could also be implemented by making <x> transient within the block, and persisting it at the end, but the thing I'm after is not to control mutability, but the implicit unification. At least one would need a way to statically detect modification after persistification -- unlike how this works in Clojure.

Special types

The direction I see most hope in is a special type system. In that case, x might be needed to be "declared" at the beginning somehow.

I resarched substructural type system a bit, but think that none of them really does what I want: the restriction is not to use the components of <x> only a certain number of times, but to build up a thing by parts. After that, the parts should be able to be used as much as one likes with immutable access.

However I could just be wrong, and there is a way to use some substructural system for this purpose.

$\endgroup$
2
  • 2
    $\begingroup$ Not an answer, but some relevant search terms to look into if you haven't already: definite assignment analysis, exhaustive pattern matching, copatterns. $\endgroup$ – Aaron Rotenberg Aug 31 '20 at 8:37
  • $\begingroup$ At least 1.5 new ideas for me. Copatterns look like a hot candidate! $\endgroup$ – phipsgabler Aug 31 '20 at 8:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.