On Tue, Dec 23, 2014 at 8:14 AM, Jonathan S. Shapiro <[email protected]> wrote: > My son is off with his mom for a big chunk of the christmas school break, > and I'm using the time to work on BitC. One of the things we did in v0 was > infer mutability. My question now is: is this useful? > > The original impetus for that work is kind of embarrassing. I didn't want to > have to put mutability annotations on local variables when writing > imperative code. The very first implementation used an awful two-pass hack > that simply checked whether a local variable was assigned somewhere, and > didn't consider "deep" mutability at all. I kind of liked the outcome, > because it reduced the burden of distracting annotations in the program. > That was actually useful, so we started poking at deep mutability, and that > led to the inference work. > > My own thoughts are conflicted. Let's see whether I can gather them in some > sort of order: > > Mutability is definitely part of type. There are some things that humans are > very, very unlikely to annotate correctly. That seems like an argument in > favor of inference. I'm particularly interested, here, in subgraph > mutability at procedure calls (I call you wit a graph I can mutate, but we > can infer that you don't change it). > "mutable" and "const" are meta-constructors. That's not devilishly complex, > but it's not something that's really covered in the literature. I'm > concerned about maintenance issues arising from that. > > There is ironically an argument against doing the local mutability inference > that we did originally. It has the effect that a stray assignment statement > causes it's target location to become mutable. There are really two problems > hiding there: > > It promotes errors. By failing to require the programmer to state their > intent, it becomes possible to unintentionally modify something without > getting caught by a diagnostic. > In the BitC type system, mutation triggers monomorphism restrictions. These > propagate through unification to all sorts of places. It's possible (though > I don't recall ever seeing it) that an assignment here would manifest an > error diagnostic about type unification somewhere else. This sort of > "traveling error syndrome" is inherent in type inference. > > The reason to keep local mutability inference is that it helps to preserve > the relatively low annotation burden of BitC, making it feel a lot more like > a scripting language or an interactive language. > > One side note: we got the mutability contagion rules wrong in v0, which led > to some awkwardness. It's now clear what they should have been, and it's not > problem to correct that.
Could you give a brief description of what the mutability inference or lack of it would look like? In particular, what would variable declarations and assignments look like? Here are a few somewhat unorganized points, but I realized after writing them that they may not be very coherent given my lack of understanding of what the inference would do. In languages where mutability is the default, but an annotation is possible, I generally find myself adding const / final / similar in front of every single variable declaration to catch errors. I think there may be a distinction between simple variable mutability and deep data structure mutability, though. In imperative languages I often find myself wanting to write routines which are as generic over mutability as possible (e.g., take three arrays, one of which has to be mutable, one of which has to be deep immutable (because we store it in a lazy closure, say), one of which can and should be either one). Here mutability inference sounds lovely. In contrast, I'd personally be fine without a notation of mutability of simple variables, as long as the unboxing support is good enough that a mutable cell is as fast as a mutable language variable would be. I.e., use ocaml's ref type, but unbox it. Mutability of simple variables is fragile in the presence of closures: Python just gets in wrong, Java disallows it entirely, and I spent half an hour on Friday tracking on a bug in some Scala code that tied a var into a closure. Geoffrey _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
