  Session types provide a principled approach to typed communication protocols
that guarantee type safety and protocol fidelity. Formalizations of
session-typed communication are typically based on process calculi, concurrent
lambda calculi, or linear logic. An alternative model based on
context-sensitive typing and typestate has not received much attention due to
its apparent restrictions. However, this model is attractive because it does
not force programmers into particular patterns like continuation-passing style
or channel-passing style, but rather enables them to treat communication
channels like mutable variables. Polymorphic typestate is the key that enables
a full treatment of session-typed communication. Previous work in this
direction was hampered by its setting in a simply-typed lambda calculus. We
show that higher-order polymorphism and existential types enable us to lift the
restrictions imposed by the previous work, thus bringing the expressivity of
the typestate-based approach on par with the competition. On this basis, we
define PolyVGR, the system of polymorphic typestate for session types,
establish its basic metatheory, type preservation and progress, and present a
prototype implementation.
