[Grace-core] Personal Freshness and Constant Immutability

[James Noble]

As per the "Concern" message, there seem to be a range of invariants about programs or objects that it can be useful to state and check. These invariants are typically "interprocedural" either because an object itself moves around a program, or it requests messages from other objects. 

Three of these invariants to be going on with include:

 * immutable - requests on this object do not (logically) depend on mutable state. The objects (public) methods must be "pure functions" with results depending only upon the receiver and argument values.
 * read only - requests may depend on mutable values but do not (logically) change any mutable state
 * fresh - an object is logically newly allocated - Grace is supposed to permit inheritance/concatenation only from fresh objects. 

and there will no doubt be lots more, especially as concurrency gets involved - look at X10 for example.

How can we support this in a Graceful manner? 

While James (in particular) has some ideas here, they're not worked out and he thinks there is design work and probably research still to be done. 

Semantically, we may be able to have a (meta-) model based on logical annotations to objects - an immutable object is somehow annotated with the "immutable" property.  Syntactically, it seems we need several small things, such as:

 * a way to create an object with a particular property (e.g. immutable) - presumably that should fail if the object doesn't have the property
 * qualifying a type or variable to say an object must have some (meta-)property - an object must be fresh, or unique, or immutable
 * testing an object to ensure it has a meta-property (given types, can this just be a match/case?)
 * "insisting" that a particular object has a meta-property - even if an object isn't actually fresh or immutable, sometimes we need to treat it as if it was --- an object can be "logically" immutable, but "physically" mutable e.g. with an internal cache
 * propagating and checking these meta-properties through expressions via the type system.
 * potentially a way to remove a property from an object.

It seems particularly difficult, in a general framework, to handle cases where these meta-properties themselves are removable, or mutable.  Freshness, for example, is a mutable or (automatically) removable meta-property: an object is fresh so long as there is only one reference to that object.

We have the annotation syntax for variables - extending that to types and objects would seem to be the first step.   I do think there could be a nice solution here, but we don't have it yet.