Learn · Hidden Machines · Part VI
budding
The Conversation Has a Grammar
Scopes, typestate, and protocol automata.
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.
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
- Resolve a shadowed identifier through three nested scopes.
- Draw the legal traces of open, write, flush, and close.
- 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
- “Robert Strom and Shaula Yemini, “Typestate: A Programming Language Concept for Enhancing Software Reliability”.” — state-indexed operation legality.
- “Kohei Honda, “Types for Dyadic Interaction”.” — foundational session typing for conversations.