Allow stored properties in extensions

When I talk about "auxiliary" properties I'm thinking about things like Array.capacity. It's certainly not just a function of other properties (it's a function of the entire history of that value at a minimum), but I also wouldn't really argue that knowledge of capacity is essential to reasoning correctly about Array in many cases. Indeed, Equatable and Codable ignore capacity, and for the vast majority of algorithms written over Array it likely wouldn't matter one bit if capacity were an inaccessible implementation detail.

That said, there are of course many different levels at which you can "reason... about the type," and so yes, if your goal is to properly grasp every single state that the type can be in, then an important part of that is getting a complete picture of all the stored properties. But I don't think it's incorrect to say that some stored properties are more important to understand than others. And even if you do get a complete picture of all the stored properties and their types, you may not have a complete picture of the invariants maintained by the implementation (e.g., that Array.count <= Array.capacity). I think this also intersects with Xiaodi's point that understanding the list of all stored properties and their types is not necessarily the end-all-be-all of reasoning correctly about a type, so it's not obvious that prioritizing this type of inspection above all others is the correct call.

2 Likes

The vast majority of algorithms written over Array use the public API of the type, and so yes, to them it doesn’t really matter where in the source file a property is defined. But to the person implementing Array, as one does in the source file for a type, knowing that capacity exists and that there are important invariants that must hold is precisely the type of thing that’s important!

2 Likes

To be clear, I'm in agreement here. Just wanted to provide a bit more clarity as to the line I was drawing in my head between "auxiliary" and "core" properties of a type.

3 Likes