It is informally understood that the purpose of modal type constructors in programming calculi is to control the flow of information between types. In order to lend rigorous support to this idea, we ...study the category of classified sets, a variant of a denotational semantics for information flow proposed by Abadi et al. We use classified sets to prove multiple noninterference theorems for modalities of a monadic and comonadic flavour. The common machinery behind our theorems stems from the the fact that classified sets are a (weak) model of Lawvere's theory of axiomatic cohesion. In the process, we show how cohesion can be used for reasoning about multi-modal settings. This leads to the conclusion that cohesion is a particularly useful setting for the study of both information flow, but also modalities in type theory and programming languages at large.
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, placing
projectibility
of module expressions on a type-theoretic basis.
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
, by iterating our modal account of the phase distinction. We axiomatize a dependent type theory of parametricity structures using two pairs of complementary modalities (syntactic, semantic) and (static, dynamic), substantiated using the topos theoretic
Artin gluing
construction. 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.
Live functional programming with typed holes Omar, Cyrus; Voysey, Ian; Chugh, Ravi ...
Proceedings of ACM on programming languages,
01/2019, Volume:
3, Issue:
POPL
Journal Article
Peer reviewed
Open access
Live programming environments aim to provide programmers (and sometimes audiences) with continuous feedback about a program's dynamic behavior as it is being edited. The problem is that programming ...languages typically assign dynamic meaning only to programs that are complete, i.e. syntactically well-formed and free of type errors. Consequently, live feedback presented to the programmer exhibits temporal or perceptive gaps.
This paper confronts this "gap problem" from type-theoretic first principles by developing a dynamic semantics for incomplete functional programs, starting from the static semantics for incomplete functional programs developed in recent work on Hazelnut. We model incomplete functional programs as expressions with holes, with empty holes standing for missing expressions or types, and non-empty holes operating as membranes around static and dynamic type inconsistencies. Rather than aborting when evaluation encounters any of these holes as in some existing systems, evaluation proceeds around holes, tracking the closure around each hole instance as it flows through the remainder of the program. Editor services can use the information in these hole closures to help the programmer develop and confirm their mental model of the behavior of the complete portions of the program as they decide how to fill the remaining holes. Hole closures also enable a fill-and-resume operation that avoids the need to restart evaluation after edits that amount to hole filling. Formally, the semantics borrows machinery from both gradual type theory (which supplies the basis for handling unfilled type holes) and contextual modal type theory (which supplies a logical basis for hole closures), combining these and developing additional machinery necessary to continue evaluation past holes while maintaining type safety. We have mechanized the metatheory of the core calculus, called Hazelnut Live, using the Agda proof assistant.
We have also implemented these ideas into the Hazel programming environment. The implementation inserts holes automatically, following the Hazelnut edit action calculus, to guarantee that every editor state has some (possibly incomplete) type. Taken together with this paper's type safety property, the result is a proof-of-concept live programming environment where rich dynamic feedback is truly available without gaps, i.e. for every reachable editor state.
Multimodal Dependent Type Theory Gratzer, Daniel; Kavvos, G. A.; Nuyts, Andreas ...
Logical methods in computer science,
01/2021, Volume:
17, Issue 3
Journal Article
Peer reviewed
Open access
We introduce MTT, a dependent type theory which supports multiple modalities.
MTT is parametrized by a mode theory which specifies a collection of modes,
modalities, and transformations between them. ...We show that different choices of
mode theory allow us to use the same type theory to compute and reason in many
modal situations, including guarded recursion, axiomatic cohesion, and
parametric quantification. We reproduce examples from prior work in guarded
recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a
simple and usable syntax whose instantiations intuitively correspond to
previous handcrafted modal type theories. In some cases, instantiating MTT to a
particular situation unearths a previously unknown type theory that improves
upon prior systems. Finally, we investigate the metatheory of MTT. We prove the
consistency of MTT and establish canonicity through an extension of recent
type-theoretic gluing techniques. These results hold irrespective of the choice
of mode theory, and thus apply to a wide variety of modal situations.
We present a graded modal type theory, a dependent type theory with grades that can be used to enforce various properties of the code. The theory has Π-types, weak and strong Σ-types, natural ...numbers, an empty type, and a universe, and we also extend the theory with a unit type and graded Σ-types. The theory is parameterized by a modality, a kind of partially ordered semiring, whose elements (grades) are used to track the usage of variables in terms and types. Different modalities are possible. We focus mainly on quantitative properties, in particular erasure: with the erasure modality one can mark function arguments as erasable. The theory is fully formalized in Agda. The formalization, which uses a syntactic Kripke logical relation at its core and is based on earlier work, establishes major meta-theoretic properties such as subject reduction, consistency, normalization, and decidability of definitional equality. We also prove a substitution theorem for grade assignment, and preservation of grades under reduction. Furthermore we study an extraction function that translates terms to an untyped λ-calculus and removes erasable content, in particular function arguments with the “erasable” grade. For a certain class of modalities we prove that extraction is sound, in the sense that programs of natural number type have the same value before and after extraction. Soundness of extraction holds also for open programs, as long as all variables in the context are erasable, the context is consistent, and erased matches are not allowed for weak Σ-types.
A cost-aware logical framework Niu, Yue; Sterling, Jonathan; Grodin, Harrison ...
Proceedings of ACM on programming languages,
01/2022, Volume:
6, Issue:
POPL
Journal Article
Peer reviewed
Open access
We present
calf
, a
c
ost-
a
ware
l
ogical
f
ramework for studying quantitative aspects of functional programs. Taking inspiration from recent work that reconstructs traditional aspects of ...programming languages in terms of a modal account of
phase distinctions
, we argue that the cost structure of programs motivates a phase distinction between
intension
and
extension
. Armed with this technology, we contribute a synthetic account of cost structure as a computational effect in which cost-aware programs enjoy an internal noninterference property: input/output behavior cannot depend on cost. As a full-spectrum dependent type theory,
calf
presents a unified language for programming and specification of both cost and behavior that can be integrated smoothly with existing mathematical libraries available in type theoretic proof assistants.
We evaluate
calf
as a general framework for cost analysis by implementing two fundamental techniques for algorithm analysis: the
method of recurrence relations
and
physicist’s method for amortized analysis
. We deploy these techniques on a variety of case studies: we prove a tight, closed bound for Euclid’s algorithm, verify the amortized complexity of batched queues, and derive tight, closed bounds for the sequential and
parallel
complexity of merge sort, all fully mechanized in the Agda proof assistant. Lastly we substantiate the soundness of quantitative reasoning in
calf
by means of a model construction.
In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to
extend
it to permit capturing pure expressions with types. Our key observation is that, just ...as the pure simply-typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a
comonadic
type discipline.
We establish the correctness of our type system via a simple denotational model, which we call the
capability space
model. Our model formalises the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is
capability-safe
if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the call-by-value β and η laws) for the imperative lambda calculus, and show its soundness relative to this semantics.
Finally, we give a translation of the pure simply-typed lambda calculus into our comonadic imperative calculus, and show that any two terms which are βη-equal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equation-preserving way into our imperative calculus.
PDF
