Fully transitive const is not necessary

[guslay]

Just a quick reply, I still this it should be discussed elsewhere...

> If we say that the mutable part of invariant A is not accessible during pure
> functions, then (A = B = C) holds true.  In fact, I would argue that for
> logical const, the mutable part is not part of the invariant A instance, but
> is an 'associated' or 'tacked-on' piece that happens to be carried around
> with A.  It is used by A to help for various tools such as syncrhonization,
> memoization, etc, but it is not part of A's state.  Think of it as living in
> A's namespace, but not in the instance, and so it is inaccessible to pure
> functions.
> 
> -Steve 

My idea was that you cannot prove A = B = C if pure functions can access mutable members of an invariant object.

- Class A has a mutable _lock member
- f = isLocked() pure
- g = unlock() unpure


But now that I think of it, you are right, the same constraints also applies to global state. So tho make purity works, you would need to applies the same rules to mutable members as to global states:

Minimally,
- Forbid pure functions to call non-pure functions or to access mutable members directly.
- Forbid pure functions to call non-pure functions or to access mutable global state directly.

More drastically,
- Forbid invariant object with mutable members to take any part in pure expressions.
- Forbid invariant object with accessing mutable global states to take any part in pure expressions.


To only things I see that can break a pure method are:

- If A is abstract type, can the concrete type of the object subvert the purity analysis.
- Casting inside the pure function.
- Invariant parameter not really invariant.
- Aliasing.

All those things are some sort of cheating, and those have nothing to do with mutable members.


I still believe!