docs/proposals/TypeState.rst

:orphan:

General Type State Notes
========================

Immutability
------------

Using Typestate to control immutability requires recursive immutability
propagation (just like sending a value in a message does a recursive deep copy).
This brings up interesting questions:

1. should types be able to opt-in or out of Immutabilizability?

2. It seems that 'int' shouldn't be bloated by tracking the possibility of
   immutabilizability.

3. We can reserve a bit in the object header for reference types to indicate
   "has become immutable".

4. If a type opts-out of immutabilization (either explicitly or implicitly) then
   a recursive type derived from it can only be immutabilized if the type is
   explicitly marked immutable.  For example, you could only turn a struct
   immutable if it contained "const int's"?  Or is this really only true for
   reference types?  It seems that the immutability of a value-type element can
   follow the immutability of the containing object.  Array slices need a
   pointer to the containing object for more than just the refcount it seems.

Typestate + GC + ARC
--------------------

A random email from Mike Ferris.  DVTInvalidation models a type state, one which
requires recursive transitive propagation just like immutable does:

"For what it is worth, Xcode 4 has a general DVTInvalidation protocol that many
of our objects adopt.  This was a hard-won lesson dealing with GC where just
because something is ready to be collected does not mean it will be immediately.

We use this to clean up held resources and as a statement of intent that this
object is now "done".  Many of our objects that conform to this protocol also
assert validity in key external entry points to attempt to enforce that once
they're invalid, no one should be talking to them.

In a couple cases we have found single-ownership to be insufficient and, in
those cases, we do have, essentially, ref-counting of validity.  But in the vast
majority of cases, there is a single owner who _should_ be controlling the
useful lifetime of these objects.  And anyone else keeping them alive after that
useful lifetime is basically in error (and is in a position to be caught by our
validity assertions.)

At some point I am sure we'll be switching to ARC and, as we do, the forcing
function that caused us to adopt the DVTInvalidation pattern may fall by the
wayside (i.e. the arbitrary latency between ready to be collected and
collected).  But I doubt we would consider not having the protocol as we do
this.  It has been useful in many ways to formalize this notion if only because
it forces more rigorous consideration of ownership models and gives us a
pragmatic way to enforce them.

The one thing that has been a challenge is that adoption of DVTInvalidation is
somewhat viral.  If you own an object that in invalidate-able, then you pretty
much have to be invalidate-able yourself (or have an equivalent guaranteed
trigger to be sure you'll eventually invalidate the object)...  Over time, more
and more of our classes wind up adopting this protocol.  I am not sure that's a
bad thing, but it has been an observed effect of having this pattern."

Plaid Language notes
--------------------

http://plaid-lang.org/ aka http://www.cs.cmu.edu/~aldrich/plaid/

This paper uses the hybrid dynamic/static approach I chatted to Ted about (which
attaches dynamic tags to values, which the optimizer then tries to remove). This
moves the approach from "crazy theory" to "has at least been implemented
somewhere once": http://www.cs.cmu.edu/~aldrich/papers/plaid-oopsla11.pdf

It allows typestate changes to change representation.  It sounds to me like
conjoined discriminated unions + type state.

Cute typestate example: the state transition from egg, to caterpillar, to pupae,
to butterfly.

It only allows data types with finite/enumerable typestates.

It defines typestates with syntax that looks like it is defining types::

  state File {
    val filename;
  }

  state OpenFile case of File = {
    val filePtr;
    method read() { ... }
    method close() { this <- ClosedFile; }
  }

  state ClosedFile case of File {
    method open() { this <- OpenFile; }
  }

Makes it really seem like a discriminated union.  The stated reason to do this
is to avoid having "null pointers" and other invalid data around when in a state
where it is not valid.  It seems that another reasonable approach would be to
tag data members as only being valid in some states.  Both have tradeoffs.
Doing either of them would be a great way to avoid having to declare stuff
"optional/?" just because of typestate, and even permits other types that don't
have a handy sentinel.  It is still useful to define unconditional data, and
still useful to allow size-optimization by deriving state from a field ("-1 is a
closed file state" - at least if we don't have good integer size bounds, which
we do want anyway).

It strikes me that typestate declarations themselves (e.g. a type can be in the
"open" or "closed" state) should be independently declared from types and should
have the same sort of visibility controls as types.  I should be able to declare
a protocol/java interface along the lines of::

  protocol fileproto {
    open(...) closed;
    close(...) opened;
  }

using "public" closed/opened states.  Insert fragility concerns here.

It supports multidimensional typestate, where a class can transition in multiple
dimensions without having to manually manage a matrix of states.  This seems
particularly useful in cases where you have inheritance.  A base class may
define its own set of states.  A derived class will have those states, plus
additional dimensions if they wanted.  For example, an NSView could be visible
or not, while an NSButton derived class could be Normal or Pressed Down, etc.

Generics: "mechanisms like type parameterization need to be duplicated for
typestate, so that we can talk not only about a list of files, but also about a
list of *open* files".


You should be allowed to declare typestate transitions on "self" any any by-ref
arguments/ret values on functions.  In Plaid syntax::

  public void open() [ClosedFile>>OpenFile]

should be a precondition that 'self' starts out in the ClosedFile state and a
postcondition that it ends up in the OpenFile state.  The implementation could
be checked against this contract.

Their onward2009 paper contains the usual set of aliasing restrictions and
conflation of immutable with something-not-typestate that I come to expect from
the field.

Their examples remind me that discriminated unions should be allowed to have a
'base class': data that is common and available across all the slices.  Changing
to another slice should not change this stuff.

'instate' is the keyword they choose to use for a dynamic state test.