Towards the Type Safety of Pure Subtype Systems

Hutchins’ Pure Subtype Systems (PSS for short) [19, 18] have been proposed as a novel approach to type theory that enables a number of advanced language features for extensibility and genericity. Among other benefits, PSS (hereafter in the singular) harmoniously solves both the expression problem [30, 32] and the tag-elimination problem [18]. PSS’s expressivity allows one to implement extensible modules based on deep mixin composition, which is a key result for a type system [18]. By blurring the distinction between types and terms, PSS naturally combines dependent types and higher-order subtyping, which makes the approach very promising as a basis for generic, modular, and extensible programming. However, a proof of type safety for PSS is conspicuously lacking. This crucial property has only been shown to hold under the conjecture that two key reduction relations in the system, equivalence and subtyping, commute [18]. The commutativity of these two reductions is an instance of a recurrent problem in higher-order subtyping known as transitivity elimination. Consequently, the type safety of PSS has remained an open problem for more than a decade.

In this paper, we resolve this long-standing open problem by introducing a novel reformulation of Hutchins’ PSS. Our system is based on a mechanism reminiscent of the Krivine Abstract Machine, it allows more fine-grained reductions and exposes crucial intermediate reduction steps that were absent in the original PSS. This architectural change allows for a direct and elegant proof of transitivity elimination.

Contrary to traditional type systems, PSS harmoniously mixes terms and types. Consider the natural number $3$ and the type $\mathrm{𝑁𝑎𝑡}$ of natural numbers. In PSS one can have a term that encodes $\mathrm{𝑁𝑎𝑡}+3$ with the naive Church encoding of naturals, which type-checks to $\mathrm{𝑁𝑎𝑡}$. Terms can also be used instead of types: for instance the function $\lambda x\le \mathrm{\hspace{0.17em}3}.x$, whose subtype annotation is $3$ (we write $\le$ for the subtyping relation, that is, the substitute of typing in our calculus), is a valid expression. The latter example is an instance of bounded quantification [26] where the term $3$ is the singleton type $\{3\}$ and the subtyping relation is akin to the subset relation.

By replacing the typing relation with a more general subtyping relation, PSS greatly increases expressivity. Since terms and types belong to the same syntactic kind, PSS naturally subsumes dependent types and higher-order subtyping. This unification enables a host of advanced language features for extensibility, genericity, and efficiency, including virtual types, recursive types, deep mixin composition, feature-oriented programming, bounded quantification, and partial evaluation [19, 32, 18].

In the original work on PSS, Hutchins introduces a declarative system with two relations: one for equivalence (akin to $\beta$-equivalence) and another for subtyping, both of which are defined with transitive closure. The proof of type safety requires a type preservation property, which states that the type of a program is preserved under evaluation. This property, in turn, hinges on a critical inversion lemma: any two functions in the subtyping relation must have equivalent subtype annotations. This lemma cannot be proven directly in the declarative system due to the presence of transitivity, which introduces intermediate terms that may not be structurally related to the functions being compared. Proving type preservation thus amounts to showing that transitivity is an admissible rule in the system.

In order to prove transitivity elimination, Hutchins proposes an equivalent syntax-directed, algorithmic system with two different notions of reduction: an equivalence reduction that models $\beta$-reduction, and a subtyping reduction that models small-step subtyping, where subtyping reduction subsumes equivalence reduction. For short, we may write “reduction” for the $\beta$-reduction, and “promotion” for the subtyping reduction. The declarative subtyping relation is shown to be equivalent to the combination of subtyping and equivalence reduction sequences as depicted below.

$u\le t\text{iff}\text{exists}v\text{such that}$  $\begin{array}{c}\text{<object type="image/svg+xml" data="dagpub-standalone-combined-2026-01-06-12-07-01-page-1.pdf2svg.svg" id="S1.p6.m4.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="50" height="44" style="width: 100px; height: unset; max-width: 100\%"></object>}\end{array}$

In the algorithmic setting, transitivity can be shown to be admissible if these two notions of reduction commute. Diagrammatically, commutativity ensures that a transitive derivation which forms a “stair” of reduction and promotion steps can be flattened into a single angle.

Despite his efforts, Hutchins failed to prove that commutativity holds in his algorithmic system, which prevented him from proving transitivity elimination and type safety. The culprit of this failure is exemplified by a very elementary case (depicted below), which involves the reduction of a redex and the promotion of the formal parameter in the redex’s abstraction to its annotation.

The redex $(\lambda x\le t.x)v$ on the bottom-left corner of the diagram is reduced (in the horizontal) to $v$, and promoted (in the vertical) to $(\lambda x\le t.t)v$. It is then unclear how to complete the right edge of the diagram in a single step.

To tackle this problem, Hutchins resorted to simultaneous reduction and to the decreasing diagrams technique of [29], but he failed to assign depths to each reduction step so as to show that reduction decreases in the way prescribed by the decreasing diagrams technique, because $\beta$-reduction increases this depth. Hutchins himself explains this failure in detail in his PhD thesis (Section 2.7: Confluence and commutativity)[18].

We reformulate the PSS theory by providing an alternative version of the algorithmic system with a more fine-grained notion of subtyping, in which we can now prove the commutativity result. Our version, which we dub Machine-Based PSS (MPSS for short), uses a continuation stack mechanism, reminiscent of the Krivine Abstract Machine (KAM) [20, 1] to track operands passed to abstractions. This mechanism enables a direct proof of commutativity. Indeed, by explicitly managing operands on a stack, the subtyping relation in MPSS exposes all the intermediate terms that are needed to complete the commutativity diagram directly, without resorting to complex techniques like decreasing diagrams. For instance, in our system, the subtyping relation $(\lambda x\le t.x)v\stackrel{\le }{⟶}(\lambda x\le t.t)v$ doesn’t exist, instead the variable $x$ must first be promoted to the operand $v$, which later may be promoted to the annotation $t$. Exposing this intermediate step, essentially disallowing premature promotion that exists in Hutchins’ system, allows us to complete the above commutativity diagram:

Our detailed contributions are the following:

• $\mathrm{■}$

  We introduce MPSS, a reformulation of Hutchins’ PSS that, among other changes, keeps track of the operands that have been passed at a particular scope by using a mechanism reminiscent of the continuation stack of the KAM [20, 1]. MPSS is a more fine-grained system in the sense that the stack mechanism exposes intermediate terms that were absent in Hutchins’ system.

• $\mathrm{■}$

  We prove the commutativity of the subtyping and equivalence reductions of MPSS, which enables transitivity elimination and the inversion lemma. Our proof of commutativity is direct and proceeds by simple structural induction on terms.

• $\mathrm{■}$

  We sketch how a type system can be derived from our alternative system, thanks to transitivity being now admissible.

The remainder of this paper is organised as follows. Section 2 introduces MPSS. Our system is a reformulation of Hutchins’ algorithmic framework equipped with a stack mechanism inspired by the Krivine Abstract Machine (KAM) to track operands, alongside two reductions for subtyping and equivalence. Section 3 proves the commutativity of the two reduction relations in MPSS. Section 4 sketches the design of a type system built upon MPSS and discusses the path to proving its type safety. Section 5 and 6 discuss related and future work, and Section 7 concludes.

All the formal proofs of the lemmas and theorems stated in the paper are collected in the appendix of the full version of this paper accessible online at https://arxiv.org/abs/2407.13882.

Machine-Based PSS (MPSS for short) is a reformulation of PSS where the algorithmic reductions are instrumented with a stack mechanism reminiscent of the Krivine Abstract Machine (KAM) [20, 1].

MPSS is an extension of the pure lambda calculus with a constant symbol $\mathrm{𝖳𝗈𝗉}$ for the most general supertype and with subtype annotations in the formal parameters of abstractions. Assuming a countably infinite set of variables $\mathrm{V}$ ranged over by $x,y,\mathrm{\dots }$, the syntax of terms, contexts, and stacks is defined as follows:

A variable $x\in \mathrm{V}$ is a term. The term $\mathrm{𝖳𝗈𝗉}$ is the most general supertype, such that any other term is its subtype. An abstraction $(\lambda x\le t.u)$ has a parameter $x$, a subtype annotation $t$, and a body $u$. An application $(uv)$ has an operator $u$ and an operand $v$. The Greek letter $\alpha$ is a metavariable for terms that originate as operands from the stack.

We assume the usual notions of free and bound variables, and the usual capture-avoiding substitution function, denoted by $u[x\backslash v]$, that replaces the free occurrences of variable $x$ in $u$ by $v$, while avoiding the capture of any bound variable in $u$. We consider terms that result after the renaming of bound variables to be identical. When needed, we assume that $\alpha$-equivalence is applied at will to avoid clashing of free variables.

An application of the form $(\lambda x\le t.u)v$ is a redex. Contraction of a redex is modelled by $\beta$-reduction, which rewrites $(\lambda x\le t.u)v$ into $u[x\backslash v]$. Consider the following example of a redex involving the term $\lambda x\le \mathrm{𝖳𝗈𝗉}.x$ for universal identity. Since universal identity is a subtype of $\mathrm{𝖳𝗈𝗉}$, the self-application of universal identity, i.e. the redex $(\lambda x\le \mathrm{𝖳𝗈𝗉}.x)(\lambda x\le \mathrm{𝖳𝗈𝗉}.x)$, reduces to $x[x\backslash \lambda x\le \mathrm{𝖳𝗈𝗉}.x]$, which is equal to universal identity by the definition of the substitution function. We assume conventional parenthesis-dropping conventions where abstractions associate to the right and applications to the left, and applications bind stronger than abstractions. We define normal forms as terms that are either Top, functions that have a subtype annotation and a body in normal form, or a variable applied to any number of normal forms.

Our system uses logical contexts (contexts for short) $\mathrm{\Gamma }$ to store annotations from abstractions encountered within a given scope. A context $\mathrm{\Gamma }$ is a sequence of subtype annotations $x\le t$ and equivalence annotations $x\equiv \alpha$. We write $x\mathrm{⊲}t$ to denote either kind of annotation, and throughout this paper the metavariable $\mathrm{⊲}$ designates either $\le$ or $\equiv$. We use $\epsilon$ for the empty context and we write $\mathrm{\Gamma },x\mathrm{⊲}t$ for the operation that appends annotation $x\mathrm{⊲}t$ to the subtype annotations of $\mathrm{\Gamma }$. By abuse of notation, we write ${\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2$ for the concatenation of contexts ${\mathrm{\Gamma }}_1$ and ${\mathrm{\Gamma }}_2$. We say that $x$ has subtype $t$ in $\mathrm{\Gamma }$ (written $x\le t\in \mathrm{\Gamma }$) if $x\le t$ is the rightmost annotation for $x$ in $\mathrm{\Gamma }$. Respectively, we say that $x$ is equivalent to $\alpha$ in $\mathrm{\Gamma }$ (written $x\equiv \alpha \in \mathrm{\Gamma }$) under similar conditions.

In order to accommodate the stack mechanism, we introduce extended contexts $\mathrm{\Gamma };s$, which are logical contexts $\mathrm{\Gamma }$ coupled with a continuation stack $s$. Extended contexts adapt the algorithmic reduction relations to the stack mechanism of MPSS.

Figure 1 introduces the prevalidity condition on contexts that ensures each annotation in a context mentions a different variable, to avoid clashing of variable names. We say that $x$ is in the domain of $\mathrm{\Gamma }$ (written $x\in \mathrm{dom}(\mathrm{\Gamma })$) if and only if an annotation for variable $x$ occurs in $\mathrm{\Gamma }$, i.e., there exists a term $t$ (or a term $\alpha$) such that $x\le t\in \mathrm{\Gamma }$ (or $x\equiv \alpha \in \mathrm{\Gamma }$). The empty context $\epsilon$ is prevalid (Rule Pv-Emp in Figure 1). Adding a subtype annotation $x\le t$, or an equivalence annotation $x\equiv \alpha$ to a prevalid context $\mathrm{\Gamma }$ yields a prevalid context if the free variables of $t$ (respectively, $\alpha$) are in the domain of $\mathrm{\Gamma }$, and if $x$ is not already in the domain of $\mathrm{\Gamma }$ (Rules Pv-Ctx and Pv-EqA). Prevalidity for extended contexts (also defined in Figure 1) stipulates that a prevalid context coupled with an empty stack is prevalid (Rule Pv-Nil), and that an extended context $\mathrm{\Gamma };\alpha ::s$ is prevalid if the free variables of $\alpha$ are in the domain of $\mathrm{\Gamma }$ (Rule Pv-Sta). We now present our reduction relations.

Figure 2 presents our equivalence ($\stackrel{\equiv }{⟶}$) and subtyping ($\stackrel{\le }{⟶}$) reductions. We do away with a declarative system like Hutchins’ system, and our MPSS resembles his algorithmic system (p. 58 of [18]) where we adopt simultaneous reduction upfront in order to simplify the commutativity proofs (resembling p. 74 of [18]), and where contexts are coupled with a stack in order to accommodate the stack mechanism. The equivalence reduction $\stackrel{\equiv }{⟶}$ models a reflexive, small-step, simultaneous $\beta$-reduction. Rule Me-Bet performs $\beta$-reduction, while Rule Me-Pro replaces a variable by its equivalent operand from the context. Rules Me-Var and Me-Top allow the reduction relation to be reflexive. Rule Me-TAp is a technical device from Hutchins’ formulation in [18], whose objective is to accommodate terms with shape $\mathrm{𝖳𝗈𝗉}u$, which may pop up in reductions, and which cannot be $\beta$-reduced by Rule Me-Bet (see p. 59 of [18] for a further discussion on this issue). Me-App propagates promotion through unapplied applications by pushing the operand onto the stack and proceeding with the operator, mimicking KAM’s stack management. Rules Me-Fun and Me-FOp distinguish between unapplied and applied abstractions: Me-Fun propagates promotion by enlarging the context with the abstraction’s annotation and proceeding with the body, and Me-FOp promotes the body of an applied abstraction by taking the operand from the stack and enlarging the context with an equivalence annotation.

The subtyping reduction $\stackrel{\le }{⟶}$ defines promotion in a stack-aware manner. Rule Ms-Pro promotes a variable to its subtype annotation, and Rule Ms-Top promotes any term to $\mathrm{𝖳𝗈𝗉}$. Rule Ms-Equ subsumes equivalence reduction. Rules Ms-App, Ms-Fun and Ms-FOp are the counterparts of the equivalence reduction rules Me-App, Me-Fun and Me-FOp respectively. Because Hutchins’ declarative system is not contravariant, its algorithmic system, which we took inspiration from, does not change the type annotation of abstractions: in his system, there is no rule $\lambda x\le t.u\stackrel{\le }{⟶}\lambda x\le t^{\prime }.u$ with assumption $t^{\prime }\stackrel{\le }{⟶}t$. The main motivation for this design choice is to avoid the undecidability of the related typechecking, as described in [25], and to avoid complicating the meta-theory even more. Our system follows the same principle, both Rules Ms-Fun and Ms-FOp do not change the type annotation, and in general there is no reduction rule to change the type annotations, except from equivalence reductions that are allowed. Handling the interaction between the stack and the context is the cornerstone to prove the commutativity result, and to avoid the premature promotion issues that plagued Hutchins’ approach.

To illustrate our stack mechanism, consider the following subtyping reduction derivation

Rule Ms-App pushes the operand $v$ onto the stack. Inside the abstraction, the variable $x$ is not promoted to its type $t$ but is instead reduced to the operand $v$ retrieved from the context, which was placed there by Ms-FOp after popping from the stack. Keeping track of operands prevents the premature promotion that caused Hutchins’ commutativity proof to fail.

As in Hutchins’ PSS, we define a subtyping relation $\le$, on which we wish to prove that transitivity is admissible in the next section, as follows, with $\stackrel{}{⟶\to }$ being the transitive closure of $\stackrel{}{⟶}$:

$u\le t\text{iff}\text{exists}v\text{such that}$ $\begin{array}{c}\text{<object type="image/svg+xml" data="dagpub-standalone-combined-2026-01-06-12-07-01-page-4.pdf2svg.svg" id="S2.p11.m5.1.g1nest" class="ltx\_graphics ltx\_img\_square" width="50" height="44" style="width: 100px; height: unset; max-width: 100\%"></object>}\end{array}$

As explained in the introduction, proving transitivity elimination requires us to show that the equivalence ($\stackrel{\equiv }{⟶}$) and subtyping ($\stackrel{\le }{⟶}$) reductions commute, which we do below in this section. In order to state the commutativity result, we first define a reduction relation on extended contexts, which captures the evolution of annotations during reduction.

Reduction of extended context $\mathrm{\Gamma };s\rightarrowtail {\mathrm{\Gamma }}^{\prime };s^{\prime }$

With this definition, we can now state our main commutativity result.

The generalisation over all possible resulting contexts ${\mathrm{\Gamma }}^{\prime };s^{\prime }$ is crucial for the inductive proof. Indeed, consider the following commutation diagram, with context $\mathrm{\Gamma };\mathrm{nil}$:

The only possible arrow that could exist, apart from a promotion of the whole term to $\mathrm{𝖳𝗈𝗉}$, is a promotion of the variable $x$ to its subtype annotation $t^{\prime }$. Therefore, the top right term is $\lambda x\le t^{\prime }.t^{\prime }$, and the diagram is completed as follows:

However, in the proof of this theorem, everything works by induction on the terms. Therefore, starting from the original diagram, we apply the induction hypothesis on the following diagram, with context $\mathrm{\Gamma },x\le t;\mathrm{nil}$:

And as we have seen above, we must complete this diagram with $t^{\prime }$ being the top right term, as the only possible completion of the original diagram is the term $\lambda x\le t^{\prime }.t^{\prime }$. Therefore, the completed diagram by the induction hypothesis must be:

Hence the requirement that the context of the right arrow must be $\mathrm{\Gamma },x\le t^{\prime };\mathrm{nil}$, and therefore the formulation of the theorem with a generalisation over contexts.

Similarly, our equivalence reduction relation satisfies the diamond property, on which the result above rests. A similar generalisation over contexts is required, with two different reduced extended contexts however, as both the top and the right edge can now do variable promotions thanks to Rule Me-Pro. The pathological case is the following, with context $\mathrm{\Gamma };\mathrm{nil}$:

To solve this pathological case in the induction, one of the sub-induction calls is the following diagram:

And similarly as above, the top edge is completed with extended context $\mathrm{\Gamma },x\equiv {\alpha }_2;\mathrm{nil}$, whereas the right edge is completed with extended context $\mathrm{\Gamma },x\equiv {\alpha }_1;\mathrm{nil}$. Both these contexts satisfy the requirement of the theorem (that is, we have $\mathrm{\Gamma },x\equiv {\alpha }_0;\mathrm{nil}\rightarrowtail \mathrm{\Gamma },x\equiv {\alpha }_2;\mathrm{nil}$ and $\mathrm{\Gamma },x\equiv {\alpha }_0;\mathrm{nil}\rightarrowtail \mathrm{\Gamma },x\equiv {\alpha }_1;\mathrm{nil}$).

With commutativity and the diamond property established, we can prove that our system enjoys the transitivity elimination property.

In order to illustrate our result, and highlight the differences between PSS and MPSS, we detail below an example of an application of Theorem 3:

Thanks to the above commutative system, we can now sketch the design of a type-safe system. The static semantics for this system is defined by a well-formedness judgment, presented in Figure 4, which is the static condition for type safety. Rules Wf-PrS and Wf-PrE ensure that a variable is well-formed if and only if it occurs in a prevalid context (respectively, in a subtype or an equivalence annotation). Rule Wf-Top ensures that $\mathrm{𝖳𝗈𝗉}$ is universally well-formed. Rule Wf-Fun ensures that an abstraction is well-formed if and only if it has a well-formed annotation, and its body is well-formed in a context enlarged with the abstraction annotation. Finally, Rule Wf-App ensures that an application is well-formed if and only if it has an operator that is a well-subtype of a function, and an operand that is a well-subtype of the operator’s subtype annotation.

Well-formedness depends on the well-subtyping relation ${\le }_{\mathrm{wf}}$, which in turn subsumes well-equivalence ${\equiv }_{\mathrm{wf}}$. The rules for well-subtyping connect the static system to our dynamic reduction semantics. For example, Rule Ws-Lf2 states that $v$ is a well-subtype of $t$ if $v$ promotes to some $v^{\prime }$ that is itself a well-subtype of $t$.

We define type safety as progress (well-formed terms either are in normal form or can be reduced), and preservation (subtyping relations between terms are preserved under reduction by the operational semantics below). We define the operational semantics as a context-based reduction semantics [13]: the evaluation $\mapsto$ is defined as the congruence closure (Rule Os-Con and evaluation contexts $𝖢$) of $\beta$-reduction (Rule Os-Bet).

Operational Semantics $t\mapsto t^{\prime }$

Well-formedness depends on the well-subtyping relation defined in Figure 4. Well-subtyping (${\le }_{\mathrm{wf}}$) subsumes well-equivalence (${\equiv }_{\mathrm{wf}}$). We use the meta-variable $\mathrm{⊲}$ and define (${\mathrm{⊲}}_{\mathrm{wf}}$), which captures both relations, and similarly for their transitive closure (${\mathrm{⊲}}_{\mathrm{wf}}^{\ast }$). By a slight abuse of language, and to simplify the text, we write “well-subtyping” to refer to the meta-notation (${\mathrm{⊲}}_{\mathrm{wf}}$) in the paragraph that follows.

Figure 4 introduces transitive well-subtyping, the straightforward transitive closure of the well-subtyping relation (Rules Ws-Sub and Ws-Trs). Next in the figure is well-subtyping, which is defined similarly to the diagrammatic subtyping relation $\le$ defined in Section 2, but with extra requirements on the well-formedness of the terms involved. Rule Ws-Rfl states that well-subtyping is reflexive. Rule Ws-Lf1 ensures that $v$ is a well-subtype of $t$ if and only if $v^{\prime }$ is a well-subtype of $t$ and $v$ reduces to $v^{\prime }$. Rule Ws-Lf2 ensures that $v$ is a well-subtype of $t$ if and only if $v^{\prime }$ is a well-subtype of $t$ and $v$ promotes to $v^{\prime }$, but with the extra requirements that both $v$ and $v^{\prime }$ are well-formed, whose role is explained in a minute. Rule Ws-Rgh ensures that $v$ is a well-subtype of $t$ if and only if $v$ is a well-subtype of $t^{\prime }$ and $t$ reduces to $t^{\prime }$.

Thanks to these definitions, we may define type safety in our calculus as the following progress and preservation theorems.

The proof of type preservation (Theorem 5) rests on showing that reduction preserves term well-formedness. Lemma 6 establishes this fact.

A crucial case in the proof of Lemma 6 is $\beta$-reduction, where a well-formed application $(\lambda x\le t.u)\alpha$ reduces to $u[x\backslash \alpha ]$. To handle this case, we need to show that well-formedness is preserved by substitution. The following lemma provides this guarantee, where the premise $\mathrm{\Gamma }⊢\alpha {\le }_{\mathrm{wf}}^{\ast }t$ comes from the well-formedness of the original term.

Our subtyping relation in MPSS is context-dependent, unlike in PSS where it isn’t, which implies that Lemma 7 relies on the conjecture collected below, which states that the well-subtyping relation is independent of the surrounding program structure, on certain contexts named covariant contexts defined as follows:

We believe that the conjecture holds with the additional well-formedness requirements that both $v$ and $v^{\prime }$ are well-formed in Rule Ws-Lf2 above.

All in all, type safety, which is the combination of progress (Theorem 4) and preservation (Theorem 5), holds under the assumption that Conjecture 8 holds. The proof that both these theorems hold under the assumption that Conjecture 8 holds can be found in the appendix of the full version online at https://arxiv.org/abs/2407.13882.

Establishing this conjecture is the final step towards a complete proof of type safety. The sketch of a complete type system provided in this section demonstrates a path forward, built upon the solid foundation of our commutativity result. Future work could either adopt this sketch and complete the proof of type safety, or develop a different type system that leverages the commutativity result established in Section 3 to establish type safety in a different way.

PSS naturally subsumes dependent types and higher-order subtyping, so we comment on both ideas.

There are many works related to dependent types. For instance in Cayenne [4], Idris [7] or Haskell [21], dependent types are an extension of the language, in contrast to our case where dependent types are built-in as there is no distinction between terms and types.

Other languages mainly use dependent types for theorem proving, for instance Coq [12] or Agda [6]. Our language is not strongly normalising, and our main goal is not theorem proving as we cannot use the language as a proof system, since applying the Curry-Howard correspondence to PSS in a consistent way is still an open question.

To accommodate the Curry-Howard correspondence, one possible approach is to distinguish between potentially non-terminating terms and terminating terms, either with monads or via other means [23, 24]. ${\lambda }^{\theta }$ is a calculus that explores this idea [9, 10, 28]. It combines proofs and programs into a single language that distinguishes two fragments, a logical fragment where every term is strongly normalising that is suited to write proofs, and a programmatic fragment that is Turing complete and lacks termination. Such systems allow so-called freedom of speech, which is the ability to write (terminating) proofs about non-terminating terms.

Subtyping extensions of type systems have been considered. In 1997, Chen proposed ${\lambda }_{C_{\le }}$ [11], an extension of the calculus of constructions ${\lambda }_C$ with subtyping. However, Chen’s ${\lambda }_{C_{\le }}$ supports neither top types nor bounded quantification as we do in PSS.

Various extensions of System F, in order to equip it with subtyping, have also been considered in the literature. Within these we find System F_≤ [8] and System F${}_{}{}^{\omega }{}_{\le }{}^{}$ [26], which respectively add subtyping and higher-order subtyping capabilities. PSS subsumes the version of System F_≤ without contravariant arrow-types [18].

The origin of mixing terms and types goes back to the introduction of pure type systems [22], which generalises the seminal works on lambda calculi with types by [5]. These systems have the ability to unify types and terms under the same kind, but there is a typing relation instead of a subtyping one. Moreover, in some of these pure type systems, the type $\perp$ is inhabited. This gives rise to the well-known Girard’s paradox (see [17]). In our system, there is not a primitive $\perp$ subtype, but we could encode such a subtype to be inhabited by itself, and that would be unproblematic since our aim is not to use PSS as a theorem prover.

Systems where terms can be used in certain ways as types have been considered. Aspinall studied the combination of subtyping with singleton types [3]. Singleton types are close to what we study, as in our calculus, terms can be seen as singleton types of this unique value. We have for instance, for every term $t$, $\epsilon ⊢t\le t$, which would be translated to $⊢t:\{t\}$ in a system with singleton types.

Other attempts to unify typing and subtyping exist. A more conservative attempt that tries to unify typing and subtyping is [31]. This work has two major differences with our approach. First, in [31] the subtyping relation still tracks types (their unification of subtyping and typing is more conservative than ours). Second, in PSS functions and function (sub)types are defined with the same syntax, and therefore they are both instances of the same construct, which is not the case in [31].

Because many interesting features described in [18] are related to modules, other type systems especially related to objects have been studied. Our work shares foundational goals with the Dependent Object Types (DOT) calculus, the theoretical basis for Scala 3 [2, 27]. Both PSS and DOT aim to create powerful, unified type systems that support advanced modularity, and provide a formal basis for solving challenges akin to the expression problem, the tag-elimination problem, and others. DOT achieves this, among other features, through path-dependent types, where the type of a member, $p.T$, depends on the term $p$. Because DOT allows objects to contain types as members, it provides a form of dependent typing. PSS takes a more radical approach by collapsing types and terms into a single syntactic category, where the traditional typing relation ($:$) is completely replaced by a universal subtyping relation ($\le$). This design is what enables PSS’s key features described in Sections 3 and 4 of [18].

As described in Section 4, it is left as future work to define a type system that is built upon MPSS and to prove its type safety. Another interesting area to explore is the link between our system and Hutchins’ system, to determine if both well-formed notions are equivalent.

Once this system is defined, it is also left as future work to obtain an algorithm that typechecks terms in MPSS. Hutchins describes an algorithm for his system in [18], but one should adapt his algorithm to this new system, and study upon which conditions it terminates. One possible approach is to use the operational relevance of terms, for which there exist some arguments that lead them to terminate. We leave as future work to explore other practical algorithms which terminate on operationally relevant terms.

Another venue of future work is to study whether PSS and MPSS are Turing-complete. To the best of our knowledge, whether PSS is Turing-complete has not been formally proven yet. The argument in favor of Turing-completeness rests on the existence of a (well-formed) looping combinator in PSS, which would consist of a family of terms $L_n$ such that $L_{n}f$ $\beta$-reduces to $f(L_{n+1}f)$ for any $f$. Such a looping combinator exists for System $\lambda \ast$ [16], which can be encoded into Hutchins’ PSS thanks to the encoding of System $\lambda \ast$ in Hutchins’ PSS, provided on page 47 of [18]. In order to establish Turing-completeness of PSS, one should now adapt the argument made by [14] in Section 2 or the argument made in [15]. There is, however, no simple known expression of a looping combinator in System $\lambda \ast$. The looping combinator from [16] can only be derived mechanically, and working with it directly is proven to be hard as its length is more than 40 pages (see the discussion on the logical consistency and impredicativity of System ${\lambda }_{\mathrm{⊲}}$ on pages 48–51 of [18]). It may therefore be difficult to conclude about Turing-completeness of either PSS or MPSS, which is left as future work.

This paper presents a variant of the PSS originally introduced by Hutchins in [18], which we name MPSS, and proves that our reformulation enjoys a key commutation property which was missing in Hutchins’ system. We also sketch how a type system can be derived from MPSS, which could lead to a type-safe system. To the best of our knowledge PSS and MPSS are the first theories that unify harmoniously terms and types by using a single kind where everything is a subtype.

Meta-theories of languages with advanced features on types are notoriously difficult to work with. We believe our work could help in laying the foundations for a new approach that mixes terms and types in innovative ways.