> > One other point while I'm stirring the pot here: a non-mutable vector is an > example of a mutability constraint that is neither fully shallow nor fully > transitive. The elements may be immutable, but they may be references to > objects that *are* in turn mutable. This takes us head on into challenging > territory that we have visited (unsatisfactorily) before: how to state the > scope (coverage?) of contract in an object graph? Alternatively, how to > capture the relationship between the programmer notion of "object" as a > coherent functional unit, and the runtime notion of object as a collection > of primitive data structures. >
>From what I've read of the literature so far, the most well-known approaches are regions, ownership, and separation logic. Disciple, for example, tracks laziness as well as mutability via type class constraints, and provides syntactic sugar to approximate using mutable as a type qualifier. The notion of spine-lazy vs element-lazy lists is exactly analogous to distinguishing between a mutable list of immutable elements and an immutable list of mutable elements. DPJ allows globbing over hierarchical region subtrees with their Region Path Lists. JOE's under(region) provides a simpler, more restrictive notation for the same basic idea. If region globs can be used to demarcate mutability, then pointer-to-mutable-object, pointer-to-shallow-immutable-object, and pointer-to-deep-immutable-object-graph are special cases of expressible possibilities. The papers I've seen have presented ownership systems to enforce encapsulation and not mutability. But ownership systems have been used to express uniqueness and locking constraints (monitor/owned/lockfree), which seem structurally similar to mutability constraints -- uniqueness in particular. Separation logic I don't know much about, but my impression is that it optimizes for mathematical tractability over human comprehensibility.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
