You're viewing the readable version of this site. The interactive extras (search, diagrams, read-aloud) need JavaScript and a current browser. Enable JavaScript; if it is already enabled, update your browser.

Learn · Hidden Machines · Part VI

budding

The Conversation Has a Grammar

Scopes, typestate, and protocol automata.

scopes, typestate, protocols, automata, learn

You will model name resolution through scoped environments and recover a protocol automaton from guarded method calls.

A name needs an address

Two buildings may both contain room 204. The number resolves only inside a building. Identifiers likewise resolve through an environment chain whose shape and lifetime matter. Entering a scope extends the environment; leaving restores the prior one. Shadowing changes the nearest binding without mutating an unrelated global bag.

Protocol — choose the call permitted by the current state.

An API whose methods contain if (!started) and if (closed) guards is an automaton divided between caller and callee. Typestate represents the current protocol state in the value's type, so commit is available only after begin. A session type extends the idea across participants, relating sends and receives into one conversation grammar.

The laws include protocol fidelity—no admitted trace contains an invalid message—and terminality—after close, no operational message is accepted. Test the transition model with generated traces, then ensure adapters follow it.

Where the model stops

Dynamic peers, recovery, and network partitions may require runtime protocol checks even when local typestate helps. Do not encode every incidental phase in public generic types when a small runtime machine communicates more clearly.

Lessons

  • Names resolve inside environments with shape and lifetime.
  • APIs with lifecycle guards already imply protocol state.
  • Typestate moves legal next operations into the type surface.
  • Distributed conversations still need runtime settlement rules.

Practice

  1. Resolve a shadowed identifier through three nested scopes.
  2. Draw the legal traces of open, write, flush, and close.
  3. Transfer the protocol model to authentication or file upload.

Some programs encode not a sequence but many simultaneous relationships. The next chapter lets those relationships solve together.

References

  1. Robert Strom and Shaula Yemini, “Typestate: A Programming Language Concept for Enhancing Software Reliability”.” — state-indexed operation legality.
  2. Kohei Honda, “Types for Dyadic Interaction”.” — foundational session typing for conversations.