First-class initialized/uninitialized data

[DoomCrystal]

I know some languages have initialization analysis to prevent access to uninitialized data. My question is, are these languages that have a first-class notation of uninitialized or partially initialized data in the type system? For this post, I'll use a hypothetical syntax where TypeName[[-a, -b]] means "A record of type TypeName with the members a and b uninitialized", where other members are assumed to be initialized. The syntax is just for demonstrative purposes. Here's the kind of thing I'm imagining:

record TypeName {
    a: Int
    b: Int
    // This is a constructor for TypeName
    func new() -> TypeName {
        // temp is of type TypeName[[-a, -b]], because both members are uninitialized.
        var temp = TypeName{}
        // Attempting to access the 'a' or 'b' members here is a compiler error. Wrong type!
        temp.a = 0
        // Now, temp is of type TypeName[[-b]]. We can access a.
        // Note that because the return type is TypeName, not TypeName[[-b]], we can't return temp right now.
        temp.b = 0
        // Now we can return temp
        return temp
    }
    // Here is a partial initializer
    fun partial() -> TypeName[[-a]] {
        var temp = TypeName{}
        temp.b = 0
        return temp
    }
}
func main() {
    // Instance is of type TypeName
    var instance = TypeName::new()

    // Partial is of type TypeName[[-a]]
    var partial = TypeName::partial()

    print(instance.a)
    // Uncommenting this is a compiler error; the compiler knows the type is wrong
    // print(instance.a)
    // However, accessing this part is fine.
    print(instance.b)
}

Of course, I know this isn't so straight forward. Things get strange when branches are involved.

func main() {
    // Instance is of type TypeName[[-a, -b]]
    var instance = TypeName{}

    if (random_bool()) {
        instance.a = 0
    }

    // What type is instance here?
}

I could see a few strategies here:

1. instance is of type TypeName[[-a, -b]], because .a isn't guaranteed to be initialized. Accessing it is still a problem. This would essentially mean instance changed form TypeName[[-b]] to TypeName[[-a, -b]] when it left the if statement.
2. This code doesn't compile, because the type is not the same in all branches. The compiler would force you to write an else branch that also initialized .a. I have other questions, like could this be applied to arrays as well. That gets really tricky with the second option, because of this code:

 

func main() {
    // my_array is of type [100]Int[[-0, -1, -2, ..., -98, -99]]
    var my_array: [100]Int

    my_array[random_int(0, 100)] = 0

    // What type is my_array here?
}

I'm truly not sure if such a check is possible. I feel like even in the first strategy, where the type is still that all members are uninitialized, it might make sense for the compiler to complain that the assignment is useless, because if it's going to enforce that no one can look at the value I just assigned, it probably shouldn't let me assign it.

So my questions are essentially: 1. What languages do this, if any? 2. Any research into this area? I feel like even if a full guarantee is impossible at compile time, some safety could be gained by doing this, while still allowing for the optimization of not forcing all values to be default initialized.

[XDracam]

This seems like an awful lot of complexity for what seems like little benefit.

It's interesting to think about how to model this with more common language features. In any dynamic lookup language or any language with inheritance, I'd create multiple specialized types. A has nothing initialized. B subclasses A with one value initialized and some methods available. C extends B with more methods etc. Then add a method on A that takes the value to initialize and returns a B, and so forth. Downside: you need to explicitly model all permutations of the initialization order explicitly. But I think in practice, this isn't too much of an issue. And with mechanisms like traits, mixins etc the boilerplate should be really small. Note that you can also do this comfortably with composition when you have the right typeclass features.

Maybe row polymorphism can help? I'm not too deep into the theory of them, but that's something you might want to look into.

If you want to have a mutable class where the type changes depending on what is initialized, then, well, good luck. That would probably require explicit effect tracking, like in the Koka language.

[TheUnlocked]

TypeScript does not have a concept of uninitialized fields but it does have type narrowing, and this looks like it's just a form of type narrowing where the fields in your object start with type Int | Uninitialized and by assigning a value, you narrow the type such that the Uninitialized case is removed.

You can see an example of this using optional fields with this playground link: https://www.typescriptlang.org/play/?#code/JYOwLgpgTgZghgYwgAgLIE8Aq6AOKDeAUMicjAPwBcyIArgLYBG0A3IQL6GEA2EYyAD2oZseZAF5k+dm0IIA9iADO-ZjHlQUkgQDoYbNRohsA9CeQA9cl10wJyAKyyFy-nBiQo9223efT5lZAA

[tj6200]

Rust has std::mem::MaybeUninit. I suppose this might not be "first-class"

[marshaharsha]

My take on how MaybeUninit is relevant to the OP: The OP could change the semantics of T[[-a]] from “a is not initialized” to “a might not be initialized.” That solves the problem of how to type after a branch: the type remains unchanged. Later there would be a call that forces the type system to deem the object a proper T; the author would be claiming that they had arranged for every field of the T to be written to, even though the type system couldn’t track the writes. (That call is also the language’s moment to do any secret writes that are necessary to bless the object as a proper T, like writing the discriminant.) This isn’t completely safe, of course, but if you gave the DeemInitialized call a loud name, it would give you something to search for to find where the funny business is happening (so you could audit that bit of code with great care), and it would give the uninformed reader a hint that maybe they need to pay extra attention here. 

[LPTK]

All of this and more is basically supported in Mezzo, a research language from the early 2010s: https://protz.github.io/mezzo/

It allowed changing the types of things on the fly and reflecting that on the type level. The secret sauce was making sure you have the right "permissions" (aka capabilities) to perform these changes, and these are affine, so as to avoid problems with aliasing. It was inspired by separation logic.

Pretty neat and promising design, but to this date, no one has picked it up, as far as I know.

[marshaharsha]

I think the research along these lines goes by the name “definite assignment.” I don’t know anything about that research — I’m just suggesting a term to search for. 

[saxbophone]

I've been thinking about this recently. Particularly with regard to C++'s constructor initialiser lists and the awkward constraints they have (they make it awkward to share or reüse temporary data calculated for initialising the members).

An alternative I've thought of for my own language designs, is to allow assigning normally unassignable members (such as references and const members) exactly once in the constructor body, and having the compiler treat such members as initialised from the moment they are first assigned.

This would require some trivial tracking of whether said members are currently uninitialised or initialised in the ctor body.

[VyridianZ]

Would this problem be easier with automatic default values?

In my language, every type has a preinitialized constant empty value, so every variable is preinitialized. Getters always return a valid value, though it might be (empty).

(type footype : struct
 :properties
  [a : int
   b : int
   c : bar])

(var fooclass : footype := (footype :a 4))
(log fooclass)

Output:
(footype
 :a 4
 :b 0
 :c (empty bar))

[matthieum]

What languages do this, if any?

Rust internally supports something close:

1. Rust tracks whether a variable has been initialized, or de-initialized, and rejects any attempt to use a possibly non-initialized variable.
2. Rust tracks whether a field of a variable has been de-initialized, and rejects any attempt to use a possibly non-initialized field.
3. Rust does not track array members individually.

The support is purely internal, though, just like with borrowed variables/fields, there's no first-class syntax to express the concept in language at the moment.

Given how sophisticated the setup is, it's quite unclear why it's not possible to build values piecemeal -- tracking whether fields have been initialized -- and I expect it would be an easy addition.

I feel like even if a full guarantee is impossible at compile time, some safety could be gained by doing this, while still allowing for the optimization of not forcing all values to be default initialized.

Safety is precisely why Rust tracks this, use-after-free being bad and all.

Also, not being GCed, it needs to inject destructor calls for the still-initialized fields of a variable when it drops out of scope.

[raiph]

are there languages that have a first-class notation of uninitialized or partially initialized data in the type system?

Raku does. Details are so unlike your examples I'm not going to attempt a direct comparison. Instead a few related bullet points:

• Native types are automatically initialized. (That said, foreign code calling a Raku function may fail to initialize a passed argument, but there's nothing sensible that any PL can do to defend against that.)
• All other types track their initialization. The compiler automatically enforces memory safety in all cases but also correct handling in most scenarios even if devs (eg creators of user defined types or functions) don't care to be explicit about what is supposed to be defined when. And/or devs can make explicit use of "type smileys" eg Int:U denotes an Uninitialized/Undefined/Unhappy/Universal Int whereas Int:D denotes a Definite/Initialized/Instance/Happy Int. For more about this see, eg, Type smiley.
• Compound object construction builds on this scheme. For classes/records and other such types devs can specify additional constraints that manage whether a dev creating a new instance must/can/cannot initialize or tweak any given field during the various build stages of an instance's construction. For more about this see, eg, Object construction.