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:
>
>    1. 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).
>    2. "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:
>
>    1. 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.
>    2. 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.
>
> Monomorphism restrictions aside, wouldn't a re-writing pass that removed
all mutability constraints on local variables be correctness-preserving?
Or did you have a way to express the difference between "not mutable
through this alias" and "not mutable by any alias" for function arguments,
which would force callsites to have mutability restrictions for
compatibility with callee's signatures?

In C++11's "auto" type inference for local variables is terrifically
useful, and the burden of writing

const auto x = ...
  vs
auto x = ...

seems minimal relative to the benefits to human readers.  Enough so that
C++ code style reviewers at Google will ask for the "const" to be added in
if the original author neglected it.  Google's C++ style guide, though,
does prefer for much more verbosity about spelling out type names etc than
scripting languages, so it may not be your preferred design point.


Multiple languages have added local type inference recently, seemingly
without much disruption to their semantics.  That suggests that BitC could
start out with requiring the explicit annotations and then later gain
inference (if motivated by experience) off the critical path of developing
the language.


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.
>
>
> shap
>
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
>

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:
>
>    1. 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).
>    2. "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:
>
>    1. 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.
>    2. 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.
>
>
> shap
>
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to