Module theory

Modal double theories.

A modal double theory is a unital VDC equipped a family of modalities. A modality is minimally an endomorphism, and is usually a monad or comonad, in the 2-category of unital VDCs, normal functors, and natural transformations. In a model of a modal double theory, each endomorphism on the theory is interpreted as a endofunctor on the VDC of sets, i.e., as a lax double endofunctor on the double category of sets. The modalities on the semantics side are fixed across all models and include the double list monads and its many variants.

The various modalities are implicitly organized by a mode theory (Licata & Shulman 2015), a 2-category whose objects are called modes, morphisms are called modalities, and cells are sometimes called laws. Our mode theory has only one mode, corresponding to the fact our semantics is currently fixed to be the double category of sets and spans. Thus, our mode theory is actually a monoidal category. It seems excessively meta at this stage to reify the mode theory as the data of a finitely presented 2-category or monoidal category. Instead, the mode theory is implicit and baked in at the type level.

Structs

ModalDblTheory

A modal double theory.

ModeApp

Application of modalities.

Enums

List

List modalities available in a modal double theory.

ModalNode

A node in a morphism operation of a modal double theory.

ModalOp

A basic operation in a modal double theory.

Modality

Modalities available in a modal double theory.

Type Aliases

ModalMorOp

A morphism operation in a modal double theory.

ModalMorType

A morphism type in a modal double theory.

ModalObOp

An object operation in a modal double theory.

ModalObType

An object type in a modal double theory.

UstrModalDblTheory

A modal double theory with identifiers of type Ustr.