Lambda the Ultimate

I am struggling with the semantics and implementation of abstract state in my language dodo and I am looking for relevant papers or prior art.

These are the desired properties of abstract state I am after:

- A type can have different sets of attributes and methods depending on the abstract state of the object
- State transition can be ruled by an expression based on attributes of the object
- If the type is composed with mixin Tagged, then abstract state is stored in the tag
- A tagged type can define transition functions to go from one specific state to the other
- The abstract state cannot be set by other means than previously listed

The first property means that state transition basically changes the type of the object. I think of unions in C, or case classes in functional languages. The compiler needs to check the abstract state of the object to see if an operation on it is valid.

The second property defines a way to transition to a new state. In dodo, rules are enforced during validation of changes. Validation can be explicit (mutable object) or implicit.

The third property allows abstract state to be encoded in a variable. For polymorphic types, the type attribute and the abstract state tag are the same. The type of an object establishes its abstract state.

The last two properties ensure that state transitions occur in a controlled fashion. A transition function can either return an object in the new state (notably for immutable objects) or mutate the object, allowing it to assume the form required for the new state.

I am having trouble with the notion of an object changing its set of attributes and operations in the middle of a method, I don't know what would be a reasonable solution.