On Thu, Aug 8, 2013 at 10:15 AM, David Jeske <[email protected]> wrote:
> i propose (deep) const and shallow const effects.... You're about five years late to be proposing these, since this was the major underlying thrust of Swaroop Sridhar'ss Ph.D. dissertation. Also, effects aren't really the right way to think about this. Where C# *readonly* can be used, it has the same implications and deficiencies as C/C++ *const*. It can't be used in all of the places we need it, and it doesn't cover a lot of cases we want (and neither does const). But let's start this discussion with a reminder of BitC terminology, and why some of what you want cannot (in principle) be inferred. First, I'm going to ignore unboxed types here. For purposes of this discussion, the issues and challenges with unboxed types are a pure subset of those for boxed types. Stated a different way: the difference between boxed and unboxed types in this discussion is that boxed types have one more case to deal with. So if we can get clear about this for boxed types, it will be clear for unboxed types as well. *Naively Understood Terms* *Const vs. Immutable* * * What we intend by *const* is a statement about a "view" on a (possibly transitive) data structure. The holder of a const something cannot modify the something. That is: *we* cannot change that something. What we intend by *immutable* is a statement about *all* views on a (possibly transitive) data structure. The holder of an immutable something knows that *nobody* can modify the something. This is true if *all* live reachability to the something is *const*. Note that in most cases, deep const is a lot less useful than you might think, and what we actually wanted was deep immutable. *Shallow vs. Deep* * * In graph structures, we often talk about shallow vs. deep properties. In a language with "mostly boxed" objects this isn't quite enough, because making a *reference* constant isn't all that helpful. This problem exists in C/C++ as well: const char * -- pointer to constant characters const char * const -- constant pointer to constant characters This approach is so easy to understand that there are *hundreds* of web pages about it and command line tools have been written to re-play C types in quasi english so that people can remember what the heck they mean. The syntax of C# doesn't admit the ability to do the second declaration, and it isn't clear how "readonly" should be understood for reference types. I know what C# thinks the answer is, but which understanding is more sensible: readonly T m_t; // [immutable] reference to [mutable] T, as in C# readonly T m_t; // [potentially mutable] reference to [shallow] constant T C# takes the first interpretation. In the C# syntax it is even more awkward to apply the C/C++ approach, but here is what it would look like: readonly T m_t; // [mutable] reference to [shallow] readonly T readonly T readonly m_t; // [immutable] reference to [shallow] readonly T In this view, "readonly T" should be understood as a type meta-constructor, which is how Swaroop's thesis handled it. One reason that C# doesn't have a notion of "reference to readonly object" is that it avoids all the mess that goes with const methods and so forth. And now if we introduce a notion of "deep readonly", we get the following somewhat odd syntax: deep readonly T m_t; // [mutable] reference to [transitively] readonly T T deep readonly m_t; // [transitively] readonly reference to T a bit weird, syntactically, but consistent. Unfortunately, as I'll illustrate in my next note, deep and shallow aren't good enough for a lot of things. Also, it turns out that immutability requires non-local inference, and therefore cannot be inferred. But note that in all cases the object is only readonly to us. In keeping with the notion that we generally want to be able to downgrade authority on references, we want to allow a mutate-permitting reference to be copied into a mutate-prohibiting reference cell. Now it's very tempting to try to imagine that these annotations are about the containing memory cell of the object, but that turns out not to be a good intuition, because it has very unfortunate consequences for field types. A more semantically sensible view is that *mutability restrictions on sub-parts of an object remain in effect until the containing object is no longer live*. Unfortunately, that definition introduces its own problems. What does a copy constructor mean in this case? How about an assignment? Is liveness a property of the memory cell containing the object, or a property of the object itself? All of these questions have internally consistent answers in terms of the underlying type theory, but they all entail surprises for the programmer. > these could be inferred within a module for convenience, but would need to > be declared at module boundaries, to avoid thebinference hamstringing > someone's module contract. > So we all thought. But it turned out that inferring this required inventing some new entirely new type theory: Sound and Complete Type Inference in BitC<http://www.bitc-lang.org/docs/papers/complete.pdf> shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
