  The theory of program modules is of interest to language designers not only
for its practical importance to programming, but also because it lies at the
nexus of three fundamental concerns in language design: the phase distinction,
computational effects, and type abstraction. We contribute a fresh "synthetic"
take on program modules that treats modules as the fundamental constructs, in
which the usual suspects of prior module calculi (kinds, constructors, dynamic
programs) are rendered as derived notions in terms of a modal type-theoretic
account of the phase distinction. We simplify the account of type abstraction
(embodied in the generativity of module functors) through a lax modality that
encapsulates computational effects. Our main result is a (significant)
proof-relevant and phase-sensitive generalization of the Reynolds abstraction
theorem for a calculus of program modules, based on a new kind of logical
relation called a parametricity structure. Parametricity structures generalize
the proof-irrelevant relations of classical parametricity to proof-relevant
families, where there may be non-trivial evidence witnessing the relatedness of
two programs -- simplifying the metatheory of strong sums over the collection
of types, for although there can be no "relation classifying relations", one
easily accommodates a "family classifying small families". Using the insight
that logical relations/parametricity is itself a form of phase distinction
between the syntactic and the semantic, we contribute a new synthetic approach
to phase separated parametricity based on the slogan "logical relations as
types", iterating our modal account of the phase distinction. Then, to
construct a simulation between two implementations of an abstract type, one
simply programs a third implementation whose type component carries the
representation invariant.
