Theories as Types

Abstract

Theories are an essential structuring principle that enable modularity, encapsulation, and reuse in formal libraries and programs (called classes there). Similar effects can be achieved by dependent record types. While the former form a separate language layer, the latter are a normal part of the type theory. This overlap in functionality can render different systems non-interoperable and lead to duplication of work.

We present a type-theoretic calculus and implementation of a variant of record types that for a wide class of formal languages naturally corresponds to theories. Moreover, we can now elegantly obtain a contravariant functor that reflects the theory level into the object level: for each theory we obtain the type of its models and for every theory morphism a function between the corresponding types. In particular this allows shallow – and thus structure-preserving – encodings of mathematical knowledge and program specifications while allowing the use of object-level features on models, e.g. equality and quantification.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In the area of formal systems like type theories, logics, and specification and programming languages, various language features have been studied that allow for inheritance and modularity, e.g., theories, classes, contexts, and records. They all share the motivation of grouping a list of declarations into a new entity such as in . The basic intuition behind it is that R behaves like a product type whose values are of the form . Such constructs are indispensable already for elementary applications such as defining the algebraic structure of Semilattices (as in Fig. 1), which we will use as a running example.

Fig. 1.

A grouping of declarations for semilattices

System	Name of feature
	Stratified	Integrated
ML	Signature/module	Record
C++	Class	Class, struct
Java	Class	Class
Idris [Bra13]	Module	Record
Coq [Coq15]	Module	Record
HOL Light [Har96]	ML signatures	Records
Isabelle [Wen09]	Theory, locale	Record
Mizar [TB85]	Article	Structure
PVS [ORS92]	Theory	Record
OBJ [Gog+93]	Theory
FoCaLiZe [Har+12]	Species	Record

Many systems support stratified grouping (where the language is divided into a lower level for the base language and a higher level that introduces the grouping constructs) or integrated grouping (where the grouping construct is one out of many type-forming operations without distinguished ontological status), or both. The names of the grouping constructs vary between systems, and we will call them theories and records in the sequel. An overview of some representative examples is given in the table on the right. For a discussion of these concepts and a comprehensive review of the related work we refer the reader to [MRK].

The two approaches have different advantages. Stratified grouping permits a separation of concerns between the core language and the module system. It also captures high-level structure well in a way that is easy to manage and discover in large libraries, closely related to the advantages of the little theories approach [FGT92]. But integrated grouping allows applying base language operations (such as quantification or tactics) to the grouping constructs. For this reason, the (relatively simple) stratified Coq module system is disregarded in favor of records in major developments such as [Mat].

Allowing both features can lead to a duplication of work where the same hierarchy is formalized once using theories and once using records. A compromise solution is common in object-oriented programming languages, where classes behave very much like stratified grouping but are at the same time normal types of the type system. We call this internalizing the higher level features. While combining advantages of stratified and integrated grouping, internalizing is a very heavyweight type system feature: stratified grouping does not change the type system at all, and integrated grouping can be easily added to or removed from a type system, but internalization adds a very complex type system feature from the get-go. It has not been applied much to logics and similar formal systems: the only example we are aware of is the FoCaLiZe [Har+12] system. A much weaker form of internalization is used in OBJ and related systems based on stratified grouping: here theories may be used as (and only as) the types of parameters of parametric theories. Most similarly to our approach, OCaml’s first-class modules internalize the theory (called module type in OCaml) M as the type $\mathtt {module}\,M$; contrary to both OO-languages and our approach, this kind of internalization is in addition and unrelated to integrated grouping.

In any case, because theories usually allow for advanced declarations like imports, definitions, and notations, as well as extra-logical declarations, systematically internalizing theories requires a correspondingly expressive integrated grouping construct. Records with defined fields are comparatively rare; e.g., present in [Luo09] and OO-languages. Similarly, imports between record types and/or record terms are featured only sporadically, e.g., in Nuprl [Con+86], maybe even as an afterthought only.

Finally, we point out a closely related trade-off that is orthogonal to our development: even after choosing either a theory or a record to define grouping, many systems still offer a choice whether a declaration becomes a parameter or a field. See [SW11] for a discussion.

Contribution. We present the first formal system that systematically internalizes theories into record types. The central idea is to use an operator $\mathtt {Mod}$ that turns the theory T into the type $\mathtt {Mod}\left( T\right)$, which behaves like a record type. We take special care not to naively compute this record type, which would not scale well to the common situations where theories with hundreds of declarations or more are used. Instead, we introduce record types that allow for defined fields and merging so that $\mathtt {Mod}\left( T\right)$ preserves the structure of T.

Our approach combines the advantages of stratified and integrated grouping in a lightweight language feature that is orthogonal to and can be easily combined with other foundational language features. Concretely, it is realized as a module in the Mmt framework [Rab14], which allows for the modular design of foundational languages. By combining our new modules with existing ones, we obtain many formal systems with internalized theories. In particular, our typing rules conform to the abstractions of Mmt so that Mmt ’s type reconstruction [Rab17] is immediately applicable to our features. We showcase the potential in a case study based on this implementation, and which is interesting in its own right: A formal library of elementary mathematical concepts that systematically utilizes $\mathtt {Mod}\left( \cdot \right)$ throughout for algebraic structures, topological spaces etc.

Overview. We formulate our approach in the setting of a dependently-typed $\lambda$-calculus, which we recall in Sect. 2. This section also serves as a gentle primer for defining language features in Mmt. Section 3 introduces our notion of record types, based on which we introduce the model-operator in Sect. 4. Section 5 presents our implementation and a major case study on elementary mathematics. This paper is a shortened version of [MRK], which also contains all the proofs.

2 Preliminaries

We introduce the well-known dependently-typed lambda calculus as the starting point of our development. The grammar is given in Fig. 2. The only surprise here is that we allow optional definitions in contexts; this is a harmless convenience at this point but will be critical later on when we introduce records with defined fields. As usual, we write $T\rightarrow T'$ instead of $\prod _{x:T}T'$ when possible. We also write $T[x/T']$ for the usual capture-avoiding substitution of $T'$ for x in T.

Fig. 2.

Grammar for contexts and expressions

Mmt uses a bidirectional type system, i.e., we have two separate judgments for type inference and type checking. Similarly, we have two equality judgments: one for checking equality of two given terms and one for reducing a term to another one. Our judgments are given in Fig. 3.

Adding record types in Sect. 3 will introduce non-trivial subtyping, e.g., is a subtype of .¹ Therefore, we already introduce a subtyping judgment here even though it is not needed for dependent function types yet. For our purposes, it is sufficient (and desirable) to consider subtyping to be an abbreviation: $\varGamma \vdash T_1 <: T_2 \;\mathrm {iff}\;\;\mathrm {for}\;\mathrm {all}\;t \;\varGamma \vdash t \Leftarrow T_1 \;\mathrm {implies}\;\varGamma \vdash t \Leftarrow T_2$.

Fig. 3.

Judgments

The pre/postconditions of these judgments are as follows: $\varGamma \vdash t \Leftarrow T$ assumes that T is well-typed and implies that t is well-typed. $\varGamma \vdash t \Rightarrow T$ implies that both t and T are well-typed. $\varGamma \vdash t_1 \rightsquigarrow t_2$ implies that $t_2$ is well-typed iff $t_1$ is (which puts additional burden on computation rules that are called on not-yet-type-checked terms). Equality and subtyping are only used for expressions that are assumed to be well-typed, i.e., $\varGamma \vdash t_1 \equiv t_2:T$ implies $\varGamma \vdash t_i \Leftarrow T$, and $\varGamma \vdash T_1 <: T_2$ implies that $T_i$ is a type/kind.

Remark 1

(Horizontal Subtyping and Equality). The equality judgment could alternatively be formulated as an untyped equality $t\equiv t'$. That would require some technical changes to the rules but would usually not be a huge difference. In our case, however, the use of typed equality is critical.

For example, consider record values and as well as record types and . Due to horizontal subtyping, we have $S <: R$ and thus both $r_i \Leftarrow S$ and $r_i \Leftarrow R$. This has the advantage that the function $S\rightarrow R$ that throws away the field b becomes the identity operation. Now our equality at record types behaves accordingly and checks only for the equality of those fields required by the type. Thus, $r_1 \equiv r_2:R$ is true whereas $r_1 \equiv r_2:S$ is false, i.e., the equality of two terms may depend on the type at which they are compared. While seemingly dangerous, this makes sense intuitively: $r_1$ can be replaced with $r_2$ in any context that expects an object of type R because in such a context the field b, where $r_1$ and $r_2$ differ, is inaccessible.

Of course, this treatment of equality precludes downcasts: an operation that casts the equal terms $r_1:R$ and $r_2:R$ into the corresponding unequal terms of type S would be inconsistent. But such downcasts are still possible (and valuable) at the meta-level. For example, a tactic GroupSimp(G, x) that simplifies terms x in a group G can check if G is commutative and in that case apply more simplification operations.

The full rules of a lambda calculus can be found in the long version [MRK].

We can now show that the usual variance rule for function types is derivable.

Theorem 1

The following subtyping rule is derivable:

$$ \frac{\varGamma \vdash A<: A'\quad \varGamma ,x:A \vdash B'<: B}{\varGamma \vdash \prod _{x:A'}B' <: \prod _{x:A}B} $$

Moreover, we can show that every well-typed term t has a principal type T in the sense that (i) $\varGamma \vdash t \Leftarrow T$ and (ii) whenever $\varGamma \vdash t \Leftarrow T'$, then also $\varGamma \vdash T <: T'$. The principal type is exactly the one inferred by our rules (see Theorem 2).

3 Record Types with Defined Fields

We now introduce record types as an additional module of our framework by extending the grammar and the rules. The basic intuition is that and construct record types and terms. We call a context fully typed resp. defined if all fields have a type resp. a definition. In , $\varGamma$ must be fully typed and may additionally contain defined fields. In , $\varGamma$ must be fully defined; the types are optional and usually omitted in practice.

Because we frequently need fully defined contexts, we introduce a notational convention for them: a context denoted by a lower case letters like $\gamma$ is always fully defined. In contrast, a context denoted by an upper case letter like $\varGamma$ may have any number of types or definitions.

3.1 Records

We extend our grammar as in Fig. 4, where the previously existing parts are grayed out.

Fig. 4.

Grammar for records

Remark 2

(Field Names and Substitution in Records). Note that we use the same identifiers for variables in contexts and fields in records. This allows reusing results about contexts when reasoning about and implementing records. In particular, it immediately makes our records dependent, i.e., both in a record type and — maybe surprisingly — in a record term every variable x may occur in subsequent fields. In some sense, this makes x bound in those fields. However, record types are critically different from $\varSigma$-types: we must be able to use x in record projections, i.e., x can not be subject to $\alpha$-renaming.

As a consequence, capture-avoiding substitution is not always possible. This is a well-known problem that is usually remedied by allowing every record to declare a name for itself (e.g., the keyword $\mathtt {this}$ in many object-oriented languages), which is used to disambiguates between record fields and a variable in the surrounding context (or fields in a surrounding record). We gloss over this complication here and simply make substitution a partial function.

Before stating the rules, we introduce a few critical auxiliary definition:

Definition 1

(Substituting in a Record). We extend substitution $t[x/t']$ to records:

Definition 2

(Substituting with a Record). We write $t [r / \varDelta ]$ for the result of substituting any occurrence of a variable x declared in $\varDelta$ with r.x

In the special case where , we simply write $t[\delta ]$ for , i.e., we have $t[x_1:=t_1,\ldots ,x_n:=t_n]=t[x_n/t_n]\ldots [x_1/t_1]$.

Fig. 5.

Rules for records

Our rules for records are given in Fig. 5. Their roles are systematically similar to the rules for functions: three inference rules for the three constructors followed by a type and an equality checking rule for record types and the (in this case: two) computation rules. We remark on a few subtleties below.

The formation rule is partial in the sense that not every context defines a record type or kind. This is because the universe of a record type must be as high as the universe of any undefined field to avoid inconsistencies. For example, $\max (a:\mathtt {nat})=\mathtt {type}$, $\max (a:\mathtt {type})=\mathtt {kind}$ and $\max (a:\mathtt {kind})$ is not defined. If we switched to a countable hierarchy of universes (which we avoid for simplicity), we could turn every context into a record type.

The introduction rule infers the principal type of every record term. Because we allow record types with defined fields, this is the singleton type containing only that record term. This may seem awkward but does not present a problem in practice, where type checking is preferred over type inference anyway.

The elimination rule is straightforward, but it is worth noting that it is entirely parallel to the second computation rule.²

The type checking rule has a surprising premise that r must already be well-typed (against some type R). Semantically, this assumption is necessary because we only check the presence of the fields required by — without the extra assumption, typing errors in any additional fields that r might have could go undetected. In practice, we implement the rule with an optimization: If r is a variable or a function application, we can efficiently infer some type for it. Otherwise, if , some fields of $\delta$ have already been checked by the first premise, and we only need to check the remaining fields. The order of premises matters in this case: we want to first use type checking for all fields for which provides an expected type before resorting to type inference on the remaining fields.

In the equality checking rule, note that we only have to check equality at undefined fields — the other fields are guaranteed to be equal by the assumption that $r_1$ and $r_2$ have type .

Like the type checking rule, the first computation rule needs the premise that r is well-typed to avoid reducing an ill-typed into a well-typed term. In practice, our framework implements computation with a boolean flag that tracks whether the term to be simplified can be assumed to be well-typed or not; in the former case, this assumption can be skipped.

The second computation rule looks up the definition of a field in the type of the record. Both computation rules can be seen uniformly as definition lookup rules — in the first case the definition is given in the record, in the second case in its type.

Example 1

Figure 6 shows a record type of Semilattices (actually, this is a kind because it contains a type field) analogous to the grouping in Fig. 1 (using the usual encoding of axioms via judgments-as-types and higher-order abstract syntax for first-order logic).

Fig. 6.

The (record-)kind of semilattices

Then, given a record $r : \mathtt {Semilattice}$, we can form the record projection $r.\wedge$, which has type $r.U\rightarrow r.U\rightarrow r.U$ and $r.\mathtt {assoc}$ yields a proof that $r.\wedge$ is associative. The intersection on sets forms a semilattice so (assuming we have proofs $\cap -\mathtt {assoc}$, $\cap \mathtt {-comm}$, $\cap \mathtt {-idem}$ with the corresponding types) we can give an instance of that type as

Theorem 2

(Principal Types). Our inference rules infer a principal type for each well-typed normal term.

In analogy to function types, we can derive the subtyping properties of record types. We introduce context subsumption and then combine horizontal and vertical subtyping in a single statement.

Definition 3

(Context Subsumption). For two fully typed contexts $\varDelta _i$ we write $\varGamma \vdash \varDelta _1 \hookrightarrow \varDelta _2$ iff for every declaration $x:T[:=t]$ in $\varDelta _1$ there is a declaration $x:T'[:=t']$ in $\varDelta _2$ such that

• $\varGamma \vdash T' <: T$ and

• if t is present, then so is $t'$ and $\varGamma \vdash t \equiv t':T$

Intuitively, $\varDelta _1 \hookrightarrow \varDelta _2$ means that everything of $\varDelta _1$ is also in $\varDelta _2$. That yields:

Theorem 3

(Record Subtyping). The following rule is derivable:

3.2 Merging Records

We introduce an advanced operation on records, which proves critical for both convenience and performance: Theories can easily become very large containing hundreds or even thousands of declarations. If we want to treat theories as record types, we need to be able to build big records from smaller ones without exploding them into long lists. Therefore, we introduce an explicit merge operator $+$ on both record types and terms.

In the grammar, this is a single production for terms:

$$ T :\,\!:= T+T $$

The intended meaning of $+$ is given by the following definition:

Definition 4

(Merging Contexts). Given a context $\varDelta$ and a (not necessarily well-typed) context E, we define a partial function $\varDelta \oplus E$ as follows:

• $\cdot \;\oplus \;E \;=\; E$

• If $\varDelta =d,\varDelta _0$ where d is a single declaration for a variable x:

  • if x is not declared in E: $(d,\varDelta _0)\;\oplus \;E \;=\; d,\;(\varDelta _0 \oplus E)$

  • if $E\;=\;E_0,e,E_1$ where e is a single declaration for a variable x:

    • $*$ if a variable in $E_0$ is also declared in $\varDelta _0$: $\varDelta \oplus E$ is undefined,

    • $*$ if d and e have unequal types or unequal definitions: $\varDelta \oplus E$ is undefined³,

    • $*$ otherwise, $(d,\varDelta _0)\;\oplus \;(E_0,e,E_1)=E_0,m,(\varDelta _0,E_1)$ where m arises by merging d and e.

Note that $\oplus$ is an asymmetric operator: While $\varDelta$ must be well-typed (relative to some ambient context), E may refer to the names of $\varDelta$ and is therefore not necessarily well-typed on its own.

We do not define the semantics of $+$ via inference and checking rules. Instead, we give equality rules that directly expand $+$ into $\oplus$ when possible:

In implementations some straightforward optimizations are needed to verify the premises of these rules efficiently; we omit that here for simplicity. For example, merges of well-typed records with disjoint field names are always well-typed, but e.g., is not well-typed even though both arguments are.

In practice, we want to avoid using the computation rules for $+$ whenever possible. Therefore, we prove admissible rules (i.e., rules that can be added without changing the set of derivable judgments) that we use preferentially:

Theorem 4

If $R_1$, $R_2$, and $R_1+R_2$ are well-typed record types, then $R_1+R_2$ is the greatest lower bound with respect to subtyping of $R_1$ and $R_2$. In particular, $\varGamma \vdash r \Leftarrow R_1+R_2$ iff $\varGamma \vdash r \Leftarrow R_1$ and $\varGamma \vdash r \Leftarrow R_2$.

If $\varGamma \vdash r_i \Leftarrow R_i$ and $r_1+r_2$ is well-typed, then $\varGamma \vdash r_1+r_2 \Leftarrow R_1+R_2$.

Inspecting the type checking rule in Fig. 5, we see that a record r of type must repeat all defined fields of $\varDelta$. This makes sense conceptually but would be a major inconvenience in practice. The merging operator solves this problem elegantly as we see in the following example:

Example 2

Continuing our running example, we can now define a type of semilattices with order (and all associated axioms) as in Fig. 7.

Fig. 7.

Running example

Now the explicit merging in the type $\mathtt {SemilatticeOrder}$ allows the projection $\mathtt {interSLO}.\le$, which is equal to $\lambda x,y:(\mathtt {interSLO}.U)\;.\;(x \doteq x (\mathtt {interSLO}.\wedge ) y)$ and $\mathtt {interSLO}.\mathtt {refl}$ yields a proof that this order is reflexive – without needing to define the order or prove the axiom anew for the specific instance $\mathtt {interSL}$.

4 Internalizing Theories

4.1 Preliminaries: Theories

We introduce a minimal definition of stratified theories and theory morphisms, which can be seen as a very simple fragment of the MMT language [RK13]. The grammar is given in Fig. 8, again graying out the previously introduced parts.

Fig. 8.

A simple stratified language

Each of the two levels has its own context: Firstly, the theory level context $\varTheta$ introduces names X, which can be either theories $X=\{\varGamma \}$ or morphisms $X:P\rightarrow Q=\{\varGamma \}$, where P and Q are the names of previously defined theories. Secondly, the expression level context $\varGamma$ is as before but may additionally contain includes $\mathtt {include}\,X$ of other theories resp. morphisms X. We call a context flat if it does not contain includes.

All judgments are as before except that they acquire a second context, e.g., the typing judgment now becomes $\varTheta ;\varGamma \vdash t \Leftarrow T$. With this modification, all rules for function and record types remain unchanged. However, we add the restriction that $\varGamma$ in and must be flat.

We omit the rules for theories and morphisms for brevity and only sketch their intuitions. We think of theories as named contexts and of morphisms as named substitutions between contexts. Includes allow forming both modularly by copying over the declarations of a previously named object. While theories may contain arbitrary declarations, morphisms are restricted: Let $\varTheta$ contain $P=\{\varGamma \}$ and $Q=\{\varDelta \}$. Then a morphism $V:P\rightarrow Q=\{\delta \}$ is well-typed if $\delta$ is fully defined (akin to record terms) and contains for each declaration x : T of P a declaration $x=t$ where t may refer to all names declared in Q. V induces a homomorphic extension $\overline{V}$ that maps P-expressions to Q-expressions. The key property of morphisms is that, if V is well-typed, then $\varTheta ;P \vdash t \Leftarrow T$ implies $\varTheta ;Q \vdash \overline{V}(t) \Leftarrow \overline{V}(T)$ and accordingly for equality checking and subtyping. Thus, theory morphisms preserve judgments and (via propositions-as-types representations) truth. Moreover, it is straightforward to extend the above with identity and composition so that theories and morphisms form a category. We refer to [Rab14] for details.

4.2 Internalization

We can now add the internalization operator, for which everything so far was preparation. We add one production to the grammar:

$$ T :\,\!:= \mathtt {Mod}\left( X\right) $$

The intended meaning of $\mathtt {Mod}\left( X\right)$ is that it turns a theory X into a record type and a morphism $X:P\rightarrow Q$ into a function $\mathtt {Mod}\left( Q\right) \rightarrow \mathtt {Mod}\left( P\right)$. For simplicity, we only state the rules for the case where all include declarations are at the beginning of theory/morphism:

where we use the following abbreviations:

• In the rule for theories, $\max P$ is the biggest universe occurring in any declaration transitively included into P, i.e., $\max P = \max \{\max P_1,\ldots , \max P_n,\max \varDelta \}$ (undefined if any argument is).

• In the rule for morphisms, $\delta [r]$ is the result of substituting in $\delta$ every reference to a declaration of x in Q with r.x.

In the rule for morphisms, the occurrence of $\mathtt {Mod}\left( P\right)$ may appear redundant; but it is critical to (i) make sure all defined declarations of P are part of the record and (ii) provide the expected types for checking the declarations in $\delta$.

Example 3

Consider the theories in Fig. 9. Applying $\mathtt {Mod}\left( \cdot \right)$ to these theories yields exactly the record types of the same name introduced in Sect. 3 (Figs. 6 and 7), i.e., we have $\mathtt {interSL} \Leftarrow \mathtt {Mod}\left( \mathtt {Semilattice}\right)$ and $\mathtt {interSLO} \Leftarrow \mathtt {Mod}\left( \mathtt {SemilatticeOrder}\right)$. In particularly, $\mathtt {Mod}$ preserves the modular structure of the theory.

Fig. 9.

A theory of semilattices

The basic properties of $\mathtt {Mod}\left( X\right)$ are collected in the following theorem:

Theorem 5

(Functoriality). $\mathtt {Mod}\left( \cdot \right)$ is a monotonic contravariant functor from the category of theories and morphisms ordered by inclusion to the category of types (of any universe) and functions ordered by subtyping. In particular,

• if P is a theory in $\varTheta$ and $\max P\in \{\mathtt {type},\mathtt {kind}\}$, then $\varTheta ;\varGamma \vdash \mathtt {Mod}\left( P\right) \Leftarrow \max P$

• if $V:P\rightarrow Q$ is a theory morphism in $\varTheta ;\varGamma \vdash \mathtt {Mod}\left( V\right) \Leftarrow \mathtt {Mod}\left( Q\right) \rightarrow \mathtt {Mod}\left( P\right)$

• if P is transitively included into Q, then $\varTheta ;\varGamma \vdash \mathtt {Mod}\left( Q\right) <: \mathtt {Mod}\left( P\right)$.

An immediate advantage of $\mathtt {Mod}\left( \cdot \right)$ is that we can now use the expression level to define expression-like theory level operations. As an example, we consider the intersection $P\cap P'$ of two theories, i.e., the theory that includes all theories included by both P and $P'$. Instead of defining it at the theory level, which would begin a slippery slope of adding more and more theory level operations, we can simply build it at the expression level:

$$ P\cap P':=\mathtt {Mod}\left( Q_1\right) +\ldots +\mathtt {Mod}\left( Q_n\right) $$

where the $Q_i$ are all theories included into both P and $P'$.⁴

Note that the computation rules for $\mathtt {Mod}$ are efficient in the sense that the structure of the theory level is preserved. In particular, we do not flatten theories and morphisms into flat contexts, which would be a huge blow-up for big theories.⁵

However, efficiently creating the internalization is not enough. $\mathtt {Mod}\left( X\right)$ is defined via $+$, which is itself only an abbreviation whose expansion amounts to flattening. Therefore, we establish admissible rules that allow working with internalizations efficiently, i.e., without computing the expansion of $+$:

Theorem 6

Fix well-typed $\varTheta$, $\varGamma$ and $P=\{\mathtt {include}\,P_1,\ldots ,\mathtt {include}\,P_n,\varDelta \}$ in $\varTheta$. Then the following rules are admissible:

$$\begin{aligned} \frac{ \overbrace{\varTheta ;\varGamma \vdash r \Leftarrow \mathtt {Mod}\left( P_i\right) }^{1\le i\le n} \quad \overbrace{\varTheta ;\varGamma \vdash r.x \Leftarrow T[r / P] }^{x:T\in \varDelta } \quad \overbrace{\varTheta ;\varGamma \vdash r.x \equiv t[r / P]:T[r / P]}^{x:T:=t\in \varDelta }\quad \varGamma \vdash r \Rightarrow R }{\varTheta ;\varGamma \vdash r \Leftarrow \mathtt {Mod}\left( P\right) } \end{aligned}$$

where $[r / P]$ abbreviates the substitution that replaces every x declared in a theory transitively-included into P with r.x.⁶

The first rule in Theorem 6 uses the modular structure of P to check r at type $\mathtt {Mod}\left( P\right)$. If r is of the form , this is no faster than flattening $\mathtt {Mod}\left( P\right)$ all the way. But in the typical case where r is also formed modularly using a similar structure as P, this can be much faster. The second rule performs the corresponding type inference for an element of $\mathtt {Mod}\left( P\right)$ that is formed following the modular structure of P. In both cases, the last premise is again only needed to make sure that r does not contain ill-typed fields not required by $\mathtt {Mod}\left( P\right)$. Also note that if we think of $\mathtt {Mod}\left( P\right)$ as a colimit and of elements of $\mathtt {Mod}\left( P\right)$ as morphisms out of P, then the second rule corresponds to the construction of the universal morphisms out of the colimit.

Example 4

We continue Example 3 and assume we have already checked $\mathtt {interSL} \Leftarrow \mathtt {Mod}\left( \mathtt {Semilattice}\right)$ (*).

We want to check . Applying the first rule of Theorem 6 reduces this to multiple premises, the first one of which is (*) and can thus be discharged without inspecting $\mathtt {interSL}$.

Fig. 10.

Theories for R-modules and vector spaces

Example 4 is still somewhat artificial because the involved theories are so small. But the effect pays off enormously on larger theories.

5 Implementation and Case Study

We have implemented a variant of the record types and the $\mathtt {Mod}\left( \cdot \right)$-operator described here in the MMT-system (as part of [LFX]). They are used extensively in the Math-in-the-Middle archive (MitM), which forms an integral part in the OpenDreamKit [Deh+16] and MaMoRed [Koh+17] projects. In particular the formalizations of algebra and topology are systematically built on top of the concepts presented in this paper.

The archive sources can be found at [Mit], and its contents can be inspected and browsed online at https://mmt.mathhub.info under MitM/smglom. Note that the $\mathtt {Mod}\left( \cdot \right)$ operator is called $\mathtt {ModelsOf}$ here.

For a particularly interesting example that occurs in MitM, consider the theories for modules and vector spaces (over some ring/field) given in Fig. 10, which elegantly follow informal mathematical practice. Going beyond the syntax introduced so far, these use parametric theories. Our implementation extends $\mathtt {Mod}$ to parametric theories as well, namely in such a way that $\mathtt {Mod}\left( \mathtt {Module}\right) :\prod _{R:\mathtt {Mod}\left( \mathtt {Ring}\right) }\mathtt {Mod}\left( \mathtt {Module}(R)\right)$ and correspondingly for fields. Thus, we obtain

$$ \mathtt {Mod}\left( \mathtt {VSpace}\right) =\lambda F : \mathtt {Mod}\left( \mathtt {Field}\right) .((\mathtt {Mod}\left( \mathtt {Module}\right) \,F) + \ldots ) $$

and, e.g., $\mathtt {Mod}\left( \mathtt {VSpace}\right) \,\mathbb {R} <: \mathtt {Mod}\left( \mathtt {Module}\right) \,\mathbb {R}$. Because of type-level parameters, this requires some kind of parametric polymorphism in the type system. For our approach, the shallow polymorphism module that is available in Mmt is sufficient.

6 Conclusion

We have presented a formal system that allows to systematically combine the advantages of stratified and integrated grouping mechanisms found in type theories, logics, and specification/programming languages. Concretely, our system allows internalizing theories into record types in a way that preserves their defined fields and modular structure.

Our MitM case study shows that theory internalization is an important feature of any foundation; especially if it interfaces to differing mathematical software systems. Our experiments have also shown that (predicate) subtyping makes internalization even stronger in practice. But type-inference in the combined system induces non-trivial trade-offs; which we leave to future work.