Type refinement and monoidal closed bifibrations

Reference. Type refinement and monoidal closed bifibrations

The concept of refinement in type theory is a way of reconciling the “intrinsic” and the “extrinsic” meanings of types. We begin with a rigorous analysis of this concept, settling on the simple conclusion that the type-theoretic notion of “type refinement system” may be identified with the category-theoretic notion of “functor”. We then use this correspondence to give an equivalent type-theoretic formulation of Grothendieck’s definition of (bi)fibration, and extend this to a definition of monoidal closed bifibrations, which we see as a natural space in which to study the properties of proofs and programs. Our main result is a representation theorem for strong monads on a monoidal closed fibration, describing sufficient conditions for a monad to be isomorphic to a continuations monad “up to pullback”.

Cite

Cite as @mellies_zeilberger_2013 (helia, typst) · \cite{mellies_zeilberger_2013} (LaTeX)

BibTeX

bibtex · 7 lines

@misc{mellies_zeilberger_2013,
 title = {Type refinement and monoidal closed bifibrations},
 author = {Melli\`es, Paul-Andr\'e and Zeilberger, Noam},
 year = {2013},
 url = {https://arxiv.org/abs/1310.0263},
 note = {arXiv:1310.0263}
}

hayagriva YAML (typst)

yaml · 9 lines

mellies_zeilberger_2013:
  type: misc
  title: Type refinement and monoidal closed bifibrations
  author:
  - Melliès, Paul-André
  - Zeilberger, Noam
  date: 2013
  url: https://arxiv.org/abs/1310.0263
  note: arXiv:1310.0263

Download: mellies_zeilberger_2013.bib · mellies_zeilberger_2013.yml

Cited by (2)

The categorical contours of the Chomsky-Schützenberger representation theorem mellies-2025-theLMCS · 2025

We develop fibrational perspectives on context-free grammars and on nondeterministic finite-state automata over categories and operads. A generalized CFG is a functor from a free colored operad (aka multicategory) generated by a pointed finite species into an arbitrary base operad: this encompasses classical CFGs by taking the base to be a certain operad constructed from a free monoid, as an instance of a more general construction of an operad of spliced arrows

𝒲︀ 𝒞︀

for any category

𝒞︀

. A generalized NFA is a functor from an arbitrary bipointed category or pointed operad satisfying the unique lifting of factorizations and finite fiber properties: this encompasses classical word automata and tree automata without

𝜖

-transitions, but also automata over non-free categories and operads. We show that generalized context-free and regular languages satisfy suitable generalizations of many of the usual closure properties, and in particular we give a simple conceptual proof that context-free languages are closed under intersection with regular languages. Finally, we observe that the splicing functor

𝒲︀ : Cat \to Oper

admits a left adjoint

𝒞︀ : Oper \to Cat

, which we call the contour category construction since the arrows of

𝒞︀ 𝒪︀

have a geometric interpretation as oriented contours of operations of

𝒪︀

. A direct consequence of the contour / splicing adjunction is that every pointed finite species induces a universal CFG generating a language of tree contour words. This leads us to a generalization of the Chomsky-Schützenberger Representation Theorem, establishing that a subset of a homset

𝐿 \subseteq 𝒞︀ (𝐴, 𝐵)

is a CFL of arrows if and only if it is a functorial image of the intersection of a

𝒞︀

-chromatic tree contour language with a regular language.

DOI · arXiv

An Isbell duality theorem for type refinement systems mellies-2017-anMSCS · 2017

Any refinement system (= functor) has a fully faithful representation in the refinement system of presheaves, by interpreting types as relative slice categories, and refinement types as presheaves over those categories. Motivated by an analogy between side effects in programming and context effects in linear logic, we study logical aspects of this ‘positive’ (covariant) representation, as well as of an associated ‘negative’ (contravariant) representation. We establish several preservation properties for these representations, including a generalization of Day’s embedding theorem for monoidal closed categories. Then, we establish that the positive and negative representations satisfy an Isbell-style duality. As corollaries, we derive two different formulas for the positive representation of a pushforward (inspired by the classical negative translations of proof theory), which express it either as the dual of a pullback of a dual or as the double dual of a pushforward. Besides explaining how these constructions on refinement systems generalize familiar category-theoretic ones (by viewing categories as special refinement systems), our main running examples involve representations of Hoare logic and linear sequent calculus.

DOI · arXiv

Cites 12 works (4 here)

With notes (4)

Framed bicategories and monoidal fibrations shulman_2008TAC · 2008

In some bicategories, the 1-cells are ‘morphisms’ between the 0-cells, such as functors between categories, but in others they are ‘objects’ over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the ‘morphisms between 0-cells’, such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change ‘nonalgebraically’, using categorical fibrations. The resulting ‘framed bicategories’ assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones.

We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a ‘monoidal fibration’, meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.

Web

Separation logic: A logic for shared mutable data structures reynolds_separation_2002LICS · 2002

In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.

DOI

Introduction to Higher-Order Categorical Logic lambek_scott_19861986

Web

Adjointness in Foundations lawvere_1969Dialectica · 1969

DOI

External (8)

Codensity and the Ultrafilter Monad (2013)
Church and Curry: Combining Intrinsic and Extrinsic Typing (2008)
The Meaning of Types: from Intrinsic to Extrinsic Semantics (2000)
Representing Layered Monads (1999)
Higher-Dimensional Algebra III: n-Categories and the Algebra of Opetopes (1998)
On the meanings of the logical constants and the justification of the logical laws (1996)
Refinement Types for ML (1991)
Continuous Yoneda representation of a small category (1966)