What is typestate?

Question

What does TypeState refer to in respect to language design? I saw it mentioned in some discussions regarding a new language by mozilla called Rust.

Disembroil

Answer 1

Note: Typestate was dropped from Rust, only a limited version (tracking uninitialized and moved from variables) is left. See my note at the end.

The motivation behind TypeState is that types are immutable, however some of their properties are dynamic, on a per variable basis.

The idea is therefore to create simple predicates about a type, and use the Control-Flow analysis that the compiler execute for many other reasons to statically decorate the type with those predicates.

Those predicates are not actually checked by the compiler itself, it could be too onerous, instead the compiler will simply reasons in terms of graph.

As a simple example, you create a predicate even, which returns true if a number is even.

Now, you create two functions:

• halve, which only acts on even numbers
• double, which take any number, and return an even number.

Note that the type number is not changed, you do not create a evennumber type and duplicate all those functions that previously acted on number. You just compose number with a predicate called even.

Now, let's build some graphs:

a: number -> halve(a)  #! error: `a` is not `even`

a: number, even -> halve(a)  # ok

a: number -> b = double(a) -> b: number, even

Simple, isn't it ?

Of course it gets a bit more complicated when you have several possible paths:

a: number -> a = double(a) -> a: number, even -> halve(a) #! error: `a` is not `even`
          \___________________________________/

This shows that you reason in terms of sets of predicates:

• when joining two paths, the new set of predicates is the intersection of the sets of predicates given by those two paths

This can be augmented by the generic rule of a function:

• to call a function, the set of predicates it requires must be satisfied
• after a function is called, only the set of predicates it established is satisfied (note: arguments taken by value are not affected)

And thus the building block of TypeState in Rust:

• check: checks that the predicate holds, if it does not fail, otherwise adds the predicate to set of predicates

Note that since Rust requires that predicates are pure functions, it can eliminate redundant check calls if it can prove that the predicate already holds at this point.

---

What Typestate lack is simple: composability.

If you read the description carefully, you will note this:

• after a function is called, only the set of predicates it established is satisfied (note: arguments taken by value are not affected)

This means that predicates for a types are useless in themselves, the utility comes from annotating functions. Therefore, introducing a new predicate in an existing codebase is a bore, as the existing functions need be reviewed and tweaked to cater to explain whether or not they need/preserve the invariant.

And this may lead to duplicating functions at an exponential rate when new predicates pop up: predicates are not, unfortunately, composable. The very design issue they were meant to address (proliferation of types, thus functions), does not seem to be addressed.

Centrifuge

Answer 2

It's basically an extension of types, where you don't just check whether some operation is allowed in general, but in this specific context. All that at compile time.

The original paper is actually quite readable.

Introduction

There is some discussion of this paper in the LtU thread on Rust: lambda-the-ultimate.org/node/4009 – Ravishment

Answer 3

There's a typestate checker written for Java, and Adam Warski's explanatory page gives some useful information. I'm only just figuring this material out myself, but if you are familiar with QuickCheck for Haskell, the application of QuickCheck to monadic state seems similar: categorise the states and explain how they change when they are mutated through the interface.

Ravishment

Answer 4

Typestate is explained as:

• leverage type system to encode state changes
• Implemented by creating a type for each state
  • Use move semantics to invalidate a state
  • Return the next state from the previous state
  • Optionally drop the state(close file, connections,...)
• Compile time enforcement of logic

struct Data;
struct Signed;

impl Data {
  fn sign(self) -> Signed {
    Signed
  }
}

let data = Data;
let singed = data.sign();

data.sign() // Compile error

Combe