Trouble with Typestate

If you are unfamiliar with it, typestate is a property explored by several new general purpose programming languages such as Plaid and Rust. The idea is to lift object states into the type system – i.e. initialization status, or whether a file is open. This feature promises to catch various unnecessary mistakes, such as trying to write a file after closing it.There are three basic problems with typestate.

First, typestate is an abstraction inversion. To avoid TOCTTOU errors in a concurrent system, one must use linear types to guarantee uniqueness of a reference (any shared reference must share typestate). However, if one has linearity, one doesn’t need typestate as a concept, since linear (single-use) references can simply return a new object.

Second, we want a certain form of object transparency to support testing and integration: simulated resources must have the same type model as external resources, and follow the same code paths. However, we do not have linearity for external resources, nor any guarantee of typestate in a concurrency scenario. Resources such as cameras, frame buffers, mice, keyboards, databases, foreign services, et cetera are not suitable domains typestate. Typestate seems more appropriate for ‘relationships’ than resources – i.e. connections, protocols, handshakes, stages in a process – and linearity is just as effective for these purposes.

Third, typestate does not scale or compose well. By nature, states have combinatorial complexity, but developers cannot handle that much. To scale, we must ‘lose information’, reduce typestates as we abstract vertically. Unfortunately, we must still work with typestate, so this usually means downcasting and results in a more dynamic type model, which undermines many benefits of static analysis.

A reasonable option, though, might be linear semantics with typestate as some syntactic sugar.

Advertisements
This entry was posted in Language Design, Types. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s