[bitc-dev] Mutability, Copies, and Surprises

Jonathan S. Shapiro shap at eros-os.org
Tue Jul 25 01:53:27 EDT 2006


Swaroop and I have just gotten off the phone, wrapping up a discussion
that has taken several weeks. It seems to be a pattern in these
discussions that (a) the answers always turn out to be simple, and (b)
they often have counter-intuitive consequences.

Our current conversation got started because of a glitch that I noticed.
I was writing the implementation of vector->string, and I realized that
no single implementation is possible. We need to have:

  immutable-vector->string : (fn ((vector char)) string)
  mutable-vector->string   : (fn ((vector (mutable char))) string)

This seemed really stupid to me, so I asked myself why it should not be
possible to pass (vector (mutable char)) wherever (vector char) is
expected. A long discussion ensued, and the answer is: no, we really
don't want to do this. While the vector->string case will work, it works
for weird reasons that do not generalize. Let me first give the general
rule, and then illustrate the problem.

   Rule: no *location* can ever have more than one type.

     [Recall that BitC does not have subtyping or subclassing]

The definition of "location" is simultaneously straightforward and
complicated, and I will come back to that in a subsequent note. For the
moment, assume that we are polyinstantiating all cases of polymorphism
so that each instantiation will end up having distinct run-time
locations. This should be enough to let you mentally apply the rule
above.

Why?

To see the problem, consider the procedure:

  (define (vector-return vec:(vector char)) vec)
  => (fn ((vector char)) (vector char))

and the application

  (let ((mv (vector (mutable 10) (mutable 20))))
    (let ((imv (vector->return mv)))
      (== (vector-nth imv 0)
          (begin (set! (vector-nth mv 0) 5)
                 (vector-nth imv 0)))))
  => false

Note that this application of vector->return is illegal under the "one
location, one type" rule. It needs to be. Here is the problem.

First, note that "vector" is a reference type, so if we were to allow
this use of vector-return, we would end up with imv and mv pointing to
identical content, but disagreeing about the types of the cells. If this
were allowed, the compiler would never be entitled to believe that
vector cells (or more generally, fields of alpha type within value
types) are constant! In particular, the compiler cannot safely eliminate
the extra index into imv in this example unless it can determine that
the first expression of the begin form cannot mutate it -- the
"constness" of imv is merely a local aberration rather than a statement
of true immutability.

Thus the rule: no location can ever be allowed to have more than one
type.

HOWEVER:

This rule is not triggered at copy boundaries. We already have the idea
in BitC that a mutable char can be passed to a function expecting char.
This is legal because the char is passed by value.

In principle, we could extend this up to the reference boundary for
value types. That is, if we have:

  (defstruct (S 'a 'b):val a:'a b:'b)
  (define (f s:(S int32 int32)) s)

we can allow:

  (f (S (mutable 10) (mutable 20)))

because a *copy* of S is being made at the procedure call boundary.

So there is now a design question: how far should copy-compatibility
across mutability extend, and how far should it be inferred? Which
overloads should be permitted?

Let me describe the behavior today, and then send out two more emails to
establish framework for this question.


BEHAVIOR TODAY

Today, the rule in the compiler is that two types T1, T2 are copy
(therefore binding) compatible if the types

  (mutable T1)   (mutable T2)

are the same type [recall that (mutable (mutable X)) == (mutable X)].
The current rule for these is to strip mutability at a copy boundary (a
LET binding, argument passing, and return). The problem then became
"what to do for internal-only types?"

For local bindings, the inference engine currently maintains a tri-state
setting on every type:

  definitely mutable (therefore not polymorphic)
  definitely immutable
  undecided (so-called "maybe-mutable")

There are well-defined points where an "undecided" type will be set to
"immutable": primarily at the let-binding boundary. This has the effect
of maximizing polymorphism and discouraging immutability, but it also
has the somewhat strange effect that:

  (let ((i 0:int32))
    (set! i 1))

would not work, because "i" was frozen to immutable at the end of the
let bindings and before the let body. As a result, the set! is
ill-typed.

I (shap) kept tripping on this, and the compiler now implements the
following hack as a workaround:

  if, during symbol resolution, the compiler observes an expression
  of the form

    (set! ID EXPR)

  it marks the ID as mutated. If such a mark is present, the type
  checker will later type this ID as "definitely mutable"

Note that this rule does NOT cover things like:

   (set! (vector-nth ID 0) EXPR)

because it has to be run at symbol resolution time (i.e. before type
records have been built) so there is really nothing to hang the element
mutability off of. It's unquestionably a hack, but it's good enough to
deal with induction variable sorts of things, which covers most cases in
practice.

Finally, if an identifier is still undecided at the end of the top-level
form, we fix it to "not mutable"

  [The real rule is more complex than this, because I haven't taken into
   account the issue of alpha variable scoping. Swaroop should send out
   a note explaining how alpha variables are handled.]

I re-visit this case mainly to point out that (a) inference of
mutability raises some non-trivial problems, and (b) the more we extend
copy flexibility, the harder the inference will become.


On to internal and external function types in my next note.


shap



More information about the bitc-dev mailing list