It occurs to me that the problem with my length example isn't really about mutability or purity at all. It's about the fact that the type system is insufficiently precise about lifetime analysis. Let's see if I can explain what I mean by that:
We had our structure, and a length computation that depended on the "next" field, which was init-only, and then an operation that overwrote the structure as a whole, following which the length computation was stale. The problem isn't the overwrite *per se*, nor it is the staleness *per se*. It's that we aren't able to say anything about the relationship between the two. Which leads me to notice that purity is just an extreme case of effect analysis. We have a computation (length) that sources (reads) certain regions. We have an action (the mutation) that sinks (writes) one of the regions sourced by the length computation. We have a flow of control on which that update can cause the value computed by length() to become stale. In this orientation, we can take the view that a pure structure is simply a region that we know (structurally) will never be mutated on a dependent control path. The advantage to making purity part of the type system is that it absolves us of some very complicated (and ultimately conservative) flow analysis. Now this mostly doesn't get us anywhere, except that it *may* let us justify the observation that the "pure" annotation falls more in the style of a region type than a data type, and in consequence purity is something that is bound at allocation time rather than at type definition time. That may or may not turn out to be relevant and helpful. Sigh. I think that in the end I'm mostly drowning in the presence of too many options where mutability is concerned: - shallow/deep - partial/complete (mutability type variables) - by-type/by-lifetime Something is clearly going to have to give, and soon.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
