A Realizability Interpretation for Intersection and Union Types

Abstract

Proof-functional logical connectives allow reasoning about the structure of logical proofs, in this way giving to the latter the status of first-class objects. This is in contrast to classical truth-functional connectives where the meaning of a compound formula is dependent only on the truth value of its subformulas.

In this paper we present a typed lambda calculus, enriched with strong products, strong sums, and a related proof-functional logic. This calculus, directly derived from a typed calculus previously defined by two of the current authors, has been proved isomorphic to the well-known Barbanera-Dezani-Ciancaglini-de’Liguoro type assignment system. We present a logic $\mathcal{L}^{\cap \cup }$ featuring two proof-functional connectives, namely strong conjunction and strong disjunction. We prove the typed calculus to be isomorphic to the logic $\mathcal{L}^{\cap \cup }$ and we give a realizability semantics using Mints’ realizers [Min89] and a completeness theorem. A prototype implementation is also described.

Work supported by the COST Action CA15123 EUTYPES “The European research network on types for programming and verification”.

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

This paper is a contribution to the study of intersection and union type systems and their role in logical investigations.

There are two well-known points of view on type systems: (i) types as specifications and terms as programs, and (ii) types as propositions and terms as evidence. Let us call the former the “computational” perspective, and the latter the “logical” one.

In the logical view a type judgment $t:\sigma$ is taken to mean that t is a construction providing evidence of the proposition $\sigma$, reducing to a canonical element of $\sigma$. Typed $\lambda$-calculi defined in this way are at the core of proof assistants and logical frameworks. On the other hand, in the computational view a judgment $t:\sigma$ is taken to mean that t denotes an element of the datatype $\sigma$, which may in fact be defined in a way external to the system for making type-judgments.

Within the computational tradition itself there are two approaches: explicitly-typed calculi (“Church-style”) and type assignment systems (“Curry-style”). These represent more than a difference in presentation: in type assignment systems types provide a means for making assertions about the semantics of raw terms, while in explicitly typed calculi types are a method of insuring that only well-behaved terms are considered at all.

The logical view resides naturally in a system of Church-style explicit typing. Existing logical frameworks and proof assistants take such explicitly-typed calculi for their foundation.

Intersection types originated within the computational perspective as a tool for analyzing the functional behavior of $\lambda$-terms: intersection type systems give characterizations of each of the sets of strongly normalizing, weakly normalizing, and head-normalizing terms [Pot80, CDC80, BCDC83]. From a program-ming languages perspective, intersection types support (finitary) overloading. Subtyping arises naturally in the study of intersection types.

Later, union types were introduced, as a foundational study [BDCd95] and also from programming languages motivation [MPS86, CF93, Dun12]. Union types are somewhat similar to sum types, but as Pierce [Pie02] notes: “The main formal difference between disjoint and non-disjoint union types is that the latter lack any kind of case construct: if we know only that a value v has type $T_1 \cup T_2$ then the only operations we can safely perform on v are ones that make sense for both $T_1$ and $T_2$”.

Naturally, the question arose whether intersection, union, and subtyping can be given a logical explanation. Pottinger [Pot80] already identified this question: “Since the meaning of $\cap$ is reasonably clear (to claim that $A \cap B$ is to claim that one has a reason for asserting A which is also a reason for asserting B ), it would obviously be of interest to figure out how to add $\cap$ to intuitionist logic and then consider the analysis of intuitionist mathematical reasoning in the light of the resulting system”. A natural logical analogue of computational interpretation of union types is “if we want to reason from an assumption v that $T_1 \cup T_2$ holds, then we may reason separately assuming v is evidence of $T_1$ and that v is evidence of $T_2$ as long as we use that evidence in the same way.”

There has subsequently been a lot of work on this question of understanding “proof-functional” connectives [MR72, LE85, Min89, AB91, BM94, DCGV97] where the logical analogue of intersection has come to be called “strong conjunction”, with “strong disjunction” corresponding to union of course, and, in [DCGV97] with subtyping associated with “relevant implication", long of interest to philosophers. It became clear that a focus on realizability was most fruitful, typically taking untyped terms (from $\lambda$-calculus or combinatory logic) as realizers.

Independent of this thread of research, the question arose whether intersection and union type systems could be presented naturally in Church-style, i.e. explicitly typed. There are technical obstacles to an explicitly-typed treatment that would inherit the core properties of the type-assignment approach: subject reduction, subject expansion, strong normalization, unicity of typing, decidability of type reconstruction and type checking. Several proposals [PT94, Rey96, CLV01] [Ron02, WDMT02, WH02, Dun12] were explored, none of which met all the criteria above. The system presented here derives from the system of $\varLambda _\mathsf{{t}}^{\cap }$ [LR07] subsequently generalized in the system $\varLambda _\mathsf{t}^{\cap \cup }$ [DL10] to include union types. These systems do satisfy the core properties listed above. They do not include subtyping, and left open the question of a logical interpretation of the $\lambda$-calculus presented.

All of the work on understanding the logical aspects of intersection, union, and subtyping took place in the Curry-style framework. This was natural given the fact that type assignment was the most natural framework for intersection and union types, because the typing rules are not syntax directed. But the fact that most uses of $\lambda$-calculi in logical systems use explicitly-typed terms poses a compelling question, the main topic of the current paper:

Can a logical investigation of intersection and union types, with/without subtyping, take place in the context of an explicitly-typed $\lambda$ -calculus?

The motivation is that success here should point the way towards applications of intersection and union types in proof assistants and logical frameworks. The hope is that they can provide as much insight into logical systems as they have in the computational arena.

1.1 Contributions

Our results can be thought of as exploring the relationships between the following four formal systems:

• the original system $\varLambda ^{{\cap \cup }}_\mathsf{u}$ for type assignment with intersection and union types from [BDCd95],

• the typed calculus $\varLambda _\mathsf{t}^{\cap \cup }$ for type assignment with intersection and union types defined in [DL10],

• the proof-functional logic $\mathcal{L}^{\cap \cup }$, defined in this paper, and

• a natural deduction system $\mathsf {NJ}(\beta )$ for derivations in first-order intuitionistic logic with untyped $\lambda$-terms.

Judgements in these systems take the following four forms below. On the right-hand sides of the turnstiles, M is an untyped $\lambda$-term, $\varDelta$ is a simply-typed $\lambda$-term with strong products and strong sums, and $\sigma$ is a simple type formed using $\rightarrow , \cap , \text { and } \cup$. The $r_{\sigma }[M]$ are typing predicates to be realized.

The relationship between $\varLambda _\mathsf{t}^{\cap \cup }$ and $\varLambda ^{{\cap \cup }}_\mathsf{u}$ was explored in [DL10], and is recalled in Sect. 2. The first contribution of this paper is the definition of a new notion, the essence $\mathord {\wr }\,\varDelta \,\mathord {\wr }$ of a typed term $\varDelta$, used to connect $\varLambda _\mathsf{t}^{\cap \cup }$ and $\mathcal{L}^{\cap \cup }$. Specifically, we prove, as Theorem 6,

$$\begin{aligned} \varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma \text { if and only if } \varGamma \vdash \varDelta : \sigma \text { and } \mathord {\wr }\,\!\varDelta \,\mathord {\wr } \sqsubseteq M. \end{aligned}$$

(1)

Here $\varGamma$ is obtained from $\varGamma ^{^{\!@}}\!\!$ by erasing all the “$x\text{@ }$”, and $\sqsubseteq$ is a suitable syntactic preorder on untyped $\lambda$-terms. This justifies thinking of $\mathcal{L}^{\cap \cup }$ as a proof-functional logic. We think of the $\varLambda _\mathsf{t}^{\cap \cup }$ as a bridge between the intersection and union type assignment system and the logic $\mathcal{L}^{\cap \cup }$.

Our second contribution is to show how $\varLambda _\mathsf{t}^{\cap \cup }$ supports a realizability analysis of $\mathcal{L}^{\cap \cup }$. In particular, Sect. 3 shows that

$$\begin{aligned} \varGamma ^{^{\!@}}\!\!\vdash M @ \varDelta : \sigma \text { and only if } \varDelta \text { realizes } G_\varGamma \vdash r_\sigma [M]. \end{aligned}$$

(2)

Together with the equivalence in (1) this represents a complete analysis of the relationship between Curry-style and Church-style typing and the associated logic for intersection and union.

Section 4 presents further theoretical and pragmatic developments. Subsect. 4.1 extends the typed system and the logic by adding a natural notion of subtyping. This is represented in the type assignment system as a non-syntax-directed substitution rule, in the typed calculus as an explicit coercion, and in the logic calculus as another well-known proof-functional connective called relevant implication. In Subsect. 4.2 we briefly describe our prototype implementation of the type checking and proof inhabitation for the system with intersection/strong conjunction and union/strong disjunction and coercions as relevant implication.

1.2 Related Work

There are far too many studies of type systems featuring intersection, union, and subtyping to identify individually here. We have tried to outline the main currents of research in the introduction; here we will mention some work that is directly related to the contributions of this paper.

The formal investigation of soundness and completeness for a notion of realizability was initiated by Lopez-Escobar [LE85] and subsequently refined by Mints [Min89]. It is Mints’ approach that we build on here.

The connection between intersection types and relevant implication was noticed by Alessi and Barbanera in [AB91]. Barbanera and Martini [BM94] studied three proof-functional operators, namely the strong conjunction, the relevant implication (see Meyer-Routley’s [MR72] system $B^+$), and the strong equivalence connective for double implication, relating those connectives with suitable type assignments system, a realizability semantics and a completeness theorem.

Dezani-Ciancaglini, Ghilezan, and Venneri [DCGV97], investigated a Curry-Howard interpretation of intersection and union types (for Combinatory Logic). Using the well understood relation between combinatory logic and $\lambda$-calculus, they encode type-free $\lambda$-terms in suitable combinatoric logic formulas and then type them using intersection and union types. As they put it, their goal is “...to set out a logical system... such that the intersection and union type constructors are interpreted as propositional connectives and then their derivability is completely represented by derivability in a logical Hilbert-style, axiomatization.” This is a complementary approach to the realizability-based one here.

Barbanera, Dezani-Ciancaglini, and de’Liguoro [BDCd95] presented an untyped $\lambda$-calculus with related type assignment system featuring intersection and union types. The previous work [DL10] presented a typed calculus that explored the relationship between the proof-functional intersections and unions and the truth-functional (strong) products and (strong) sums; the intersection and union aspect of the system was isomorphic, after erasure, to the Barbanera-Dezani-Ciancaglini-de’Liguoro [BDCd95] type assignment system. The type system we consider is built out of an infinitely enumerable set of type variables $\phi _0, \phi _1, \ldots$ and the constant type $\omega$, by means of the arrow (“$\rightarrow$”), union (“$\cup$”), and intersection (“$\cap$”) constructors. Therefore, types have the following syntax:

$$\begin{aligned} \begin{array}{rcl} \sigma&{:}{:=}&\phi \mid \omega \mid \sigma \rightarrow \sigma \mid \sigma \cup \sigma \mid \sigma \cap \sigma . \end{array} \end{aligned}$$

Fig. 1.

The Intersection and Union Type Assignment System $\varLambda ^{{\cap \cup }}_\mathsf{u}$ [BDCd95].

Fig. 2.

The Typed Calculus $\varLambda _\mathsf{t}^{\cap \cup }$ [DL10].

2 Type Assignment $\varLambda ^{{\cap \cup }}_\mathsf{u}$ and the Typed Calculus $\varLambda _\mathsf{t}^{\cap \cup }$

The type assignment system $\varLambda ^{{\cap \cup }}_\mathsf{u}$ is the set of inference rules for assigning intersection and union types to terms of the pure $\lambda$-calculus. The presentation here, in Fig. 1, is taken from [BDCd95]: the terms are standard raw $\lambda$-terms, and the types are generated from a set of base types by the constructors $\rightarrow , \cap ,$ and $\cup$.

Theorem 1

(Main properties of $\varLambda ^{{\cap \cup }}_\mathsf{u}$ [BDCd95]).  

Characterization.:

The terms typable without use of the $\omega$ rule are precisely the strongly normalizing terms.    $\square$

Parallel reduction.:

If $B \vdash M : \sigma$ and $M \rightarrow _{gk} N$ then $B \vdash N : \sigma$. Here $\rightarrow _{gk}$ is the “Gross-Knuth” reduction, where all residuals of redexes in M are contracted (Def. 13.2.7 in [Bar84]).   $\square$

 

In [DL10] a typed $\lambda$-calculus $\varLambda _\mathsf{t}^{\cap \cup }$ was defined, whose goal was to capture a decidable and Church-style version of the Curry-style $\varLambda ^{{\cap \cup }}_\mathsf{u}$. The pseudo-terms of the $\varLambda _\mathsf{t}^{\cap \cup }$ calculus have the form $M\text{@ }\varDelta$, where M and $\varDelta$ have the following syntax:

Note that the metasymbols $\overline{\lambda }$ and $\cdot$ are per se nothing but parts of the strong sum construction. The typed judgments are of the shape $\varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma$, where in a nutshell M is a type-free $\lambda$-term, $\varDelta$ is a typed $\lambda$-term enriched with strong product, strong sum, projections, and injections to faithfully “memorize” every step of a type assignment derivation, and $\varGamma ^{^{\!@}}\!\!$ contains declarations of the shape $x_\iota \text{@ }\iota {:}\sigma$, where $x_\iota$ and $\iota$ are free-variables of M and $\varDelta$, respectively. The inference rules are presented in Fig. 2. The main feature of the system was to keep M to be “synchronized” with $\varDelta$. As an example, we can derive the judgement $\vdash \lambda x_\iota .x_\iota @ \langle {\lambda \iota {:}\sigma _1.\iota }\, ,\,{\lambda \iota {:}\sigma _2.\iota } \rangle : (\sigma _1 \rightarrow \sigma _1) \cap (\sigma _2\rightarrow \sigma _2)$. As another example, the term $[ {\overline{\lambda } \iota _1{:}\sigma _1.\varDelta _1}\, ,\,{\overline{\lambda } \iota _2{:}\sigma _2.\varDelta _1} ]\cdot \varDelta _3$ corresponds to the familiar case statement. The type $\omega$ plays the role of a terminal object, that is to say it is an object with a single element. The connection with type-assignment is this: every term can be assigned type $\omega$ so all proofs of that judgment have no content: all these proofs are considered identical ([Rey98], p. 372). As is typical we name the unique element of the terminal object as $*$.

The relation between untyped and typed reductions is subtle because of the presence of the “Gross-Knuth” parallel reduction in the untyped calculus and a fairly complex notion of synchronization of M and $\varDelta$, via synchronized $\beta$- and $\varDelta$-reductions in the typed calculus. In a nutshell, for a given term $M\text{@ }\varDelta$, the computational part (M) and the logical part ($\varDelta$) grow up together while they are built through application of rules ($V\!ar$), ($\rightarrow I$), and ($\rightarrow E$), but they get disconnected when we apply the $(\cap I)$, $(\cup I)$ or $(\cap E)$ rules, which change the $\varDelta$ but not the M. This disconnection is “logged” in the $\varDelta$ via occurrences of $\langle {-}\, ,\,{-} \rangle$, $[ {-}\, ,\,{-} ]$, $\mathsf{pr_i}$, and $\mathsf{in_i}$. In order to correctly identify the reductions that need to be performed in parallel in order to preserve the correct syntax of the term, an ad hoc notion of “overlapping” that helps to define a redex taking into account the surrounding context was defined in [DL10]. Therefore, we define $\Rightarrow$ as the union of two reductions: $\Rightarrow _{\beta }$ dealing with $\beta$-reduction occurring in both M and $\varDelta$, and $\Rightarrow _{\varDelta }$ dealing with reductions arising from reduction only in $\varDelta$. We refer to the complete reduction definition in [DL10]. Here are some main properties of the system $\varLambda _\mathsf{t}^{\cap \cup }$. Since the system is explicitly typed, properties such as type checking and type reconstruction are immediate.

Theorem 2

(Main properties of $\varLambda _\mathsf{t}^{\cap \cup }$ [DL10]).  

Subject reduction.:

If $\varGamma ^{^{\!@}}\!\!\vdash M\text{@ }\varDelta : \sigma$ and $M\text{@ }\varDelta \Rightarrow M'\text{@ }\varDelta '$, then $\varGamma ^{^{\!@}}\!\!\vdash M'\text{@ }\varDelta ':\sigma$.   $\square$

Church-Rosser.:

The reduction relation $\Rightarrow$ is confluent.    $\square$

Strong normalization.:

If $M \text{@ }\varDelta$ is typable without using rule $(\omega )$ then M is strongly normalizing.    $\square$

Type reconstruction algorithm.:

There is an algorithm ${\mathsf {Type}}$ satisfying  

Soundness.:

If ${\mathsf {Type}}(\varGamma ^{^{\!@}}\!\!,M\text{@ }\varDelta ) = \sigma$, then $\varGamma ^{^{\!@}}\!\!\vdash M\text{@ }\varDelta : \sigma$.   $\square$

Completeness.:

If $\varGamma ^{^{\!@}}\!\!\vdash M\text{@ }\varDelta :\sigma$, then ${\mathsf {Type}}(\varGamma ^{^{\!@}}\!\!,M\text{@ }\varDelta ) = \sigma$.   $\square$

 

Type checking algorithm.:

There is an algorithm ${\mathsf {Typecheck}}$ satisfying $\varGamma ^{^{\!@}}\!\!\vdash M\text{@ }\varDelta :\sigma$ if and only if ${\mathsf {Typecheck}}(\varGamma ^{^{\!@}}\!\!, M\text{@ }\varDelta ,\sigma )=\mathsf{true}$.

Judgment decidability.:

It is decidable whether $\varGamma ^{^{\!@}}\!\!\vdash M\text{@ }\varDelta :\sigma$ is derivable.    $\square$

Isomorphism of typed-untyped derivations.:

Let ${\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{u}}$ and ${\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{t}}$ be the sets of all (un)typed derivations. There are functions ${\mathcal F}: {\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{t}}\Rightarrow {\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{u}}$ and ${\mathcal G}: {\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{u}}\Rightarrow {\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{t}}$ showing the systems $\varLambda _\mathsf{t}^{\cap \cup }$ and $\varLambda ^{{\cap \cup }}_\mathsf{u}$ to be isomorphic in the following sense: ${\mathcal F}\circ {\mathcal G}$ is the identity in ${\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{u}}$ and ${\mathcal G}\circ {\mathcal F}$ is the identity in ${\mathcal D}{} { {\!er}}{\varLambda ^{\!{\cap \cup }}_\mathsf{t}}$ modulo uniform naming of variable-marks, i.e., ${\mathcal G}({\mathcal F}(\varGamma ^{^{\!@}}\!\!\vdash M\text{@ }\varDelta :\sigma ))={\mathsf {ren}}(\varGamma ^{^{\!@}}\!\!) \vdash {\mathsf {ren}}(M\text{@ }\varDelta ):\sigma$, where ${\mathsf {ren}}$ is a simple function renaming the free occurrences of variable-marks.    $\square$

 

The algorithms ${\mathsf {Type}}$ and ${\mathsf {Typecheck}}$ in Fig. 3 are exactly the ones from [DL10].

Fig. 3.

The Type Reconstruction and Type Checking Algorithms for $\varLambda _\mathsf{t}^{\cap \cup }$.

2.1 The Proof Essence Partial Function

We start with a simple question: assuming $M\text{@ }\varDelta$ is derivable, can we extract the computational part M from a proof-term $\varDelta$? Luckily the answer is positive. To do that, let us extend the pure $\lambda$-calculus syntax by a constant $\varOmega$, typable by $\omega$ only, and consider the following pre-order join (partial) operation:

Definition 3

Let $\sqsubseteq$ be the least pre-congruence over untyped $\lambda$-terms extended with the constant $\varOmega$ such that:

• 1. $\varOmega \sqsubseteq M$ for any M

• 2. if $M =_\alpha M'$ and $M' \sqsubseteq N$ then $M \sqsubseteq N$

• 3. if $M =_\eta M'$ and $M' \sqsubseteq N$ then $M \sqsubseteq N$

By identifying $\eta$-convertible terms, the relation $\sqsubseteq$ is a partial order; next we show that the set of extended $\lambda$-terms is closed under join of compatible terms: M and N are compatible, written $M \uparrow N$, if $M \sqsubseteq P \sqsupseteq N$, for some P. Although the next lemma is intuitively clear its proof rather technical. We include the proof because existence of join of compatible terms is necessary for the subsequent definition of “essence” to make sense; it also provides a decision method for compatibility and a method to compute the join.

Fig. 4.

Syntactical join

Lemma 4

For any pair M, N of extended $\lambda$-terms it is decidable whether they are compatible. Moreover, if $M \uparrow N$ then there exists a term $M \sqcup N$ which is the join of M and N w.r.t. $\sqsubseteq$ that is unique up to $\eta$-equality.

Proof

First observe that if $M \sqsubseteq P =_\eta Q$ then $P \sqsubseteq Q$, as $\sqsubseteq$ includes $=_\eta$ and $M \sqsubseteq Q$, by transitivity of $\sqsubseteq$.

Let $\le$ be the last pre-congruence such that $\varOmega \le M$, for any M. Then the relation $\sqsubseteq$ coincides with the transitive closure of $(=_\eta \, \le ) \cup (\le \, =_\eta )$, where $M (=_\eta \, \le ) N$ if $M =_\eta P \le N$ for some P, and similarly $M (\le \, =_\eta ) N$. Now suppose that

$$\begin{aligned} M =_\eta M' \le P \ge N =_\eta N' \end{aligned}$$

Since $\eta$-reduction is Church-Rosser and strongly normalizing, there exist the unique $\eta$-normal forms $M''$ of $M,M'$, and $P''$ of P and $N''$ of $N, N'$, respectively. By definition and the above remark we have $M'' \sqsubseteq P'' \sqsupseteq N''$; we claim that $M'' \le P'' \ge N''$.

If $M' \le P$, then for some context with n holes $C[\cdot ]_1 \cdots [\cdot ]_n$ we have $M' \equiv C[\varOmega ]_1 \cdots [\varOmega ]_n$ and $P \equiv C[P_1]_1 \cdots [P_n]_n$ for some $P_i$’s. Assuming for simplicity $n = 1$ and that $M' \rightarrow _\eta M''$ in one step by contracting the $\eta$-redex $\lambda x.R\,x$, we either have that the hole filled by $\varOmega$ does not occur in R or that R contains it. In the first case $\lambda x.R\,x$ is (the only) $\eta$-redex of P and we trivially obtain $P \rightarrow _\eta P'' \ge M''$ by contracting the same redex. In the second case $\varOmega$ is a subterm of R which is such that $R \le R'$ and $P \equiv C[\lambda x.R'\,x]$ for some $R'$: then we have $M'' \equiv C[R] \le C[R'] \equiv P''$ with $P\rightarrow _\eta P''$. The case of $n > 1$ or $M' \rightarrow ^+_\eta M''$ in several steps is a straightforward generalization thereof. By a similar reasoning we conclude that $P'' \ge N''$ as well. Also the proof that if

$$\begin{aligned} M \le Q =_\eta Q' \ge N \end{aligned}$$

then $M'' \le Q'' \ge N''$, where $M''$, $Q''$ and $N''$ are the respective $\eta$-normal forms of M, Q and $Q'$, N is analogous.

From this it follows that if $M \sqsubseteq P \sqsupseteq N$, then $M'' \le P'' \ge N''$ for their respective $\eta$-normal forms; as the inverse implication holds by definition, we can decide whether $M \uparrow N$ by reducing both M and N to their $\eta$-normal forms $M''$ and $N''$, and then deciding whether they are compatible w.r.t. the simpler relation $\le$. In such a case we have that $M \sqcup N = M'' \vee N''$, where $\vee$ is defined in Fig. 4, namely the lub w.r.t. $\le$.    $\square$

Let us define the essence of a $\varDelta$, written $\mathord {\wr }\,\varDelta \,\mathord {\wr }$, as a partial mapping as follows:

Definition 5

(Proof essence). The type-free essence M of a typed proof $\varDelta$ is:

The “essence” map is partial because join is such; it is however always defined when applied to a typed proof-term $\varDelta$ in the typed calculus $\varLambda _\mathsf{t}^{\cap \cup }$ of [DL10] (see Theorem 6 below) and it produces a type-free $\lambda$-term M. Note that M and $\varDelta$ are both typable with $\sigma$ using the type assignment and the type system, respectively. Summarizing, the signature of the essence is as follows:

Fig. 5.

The proof-functional logic $\mathcal{L}^{\cap \cup }$.

2.2 The Proof-Functional Logic

Indeed, for a given typable $\varDelta$, the left-hand side of the $\text{@ }$, namely M, can be omitted since it represents just the essence of $\varDelta$, i.e. $\mathord {\wr }\,\varDelta \,\mathord {\wr } \sqsubseteq M$. Thus we can introduce the proof-functional logic, called $\mathcal{L}^{\cap \cup }$ and presented in Fig. 5. The following theorem holds:

Theorem 6

(Equivalence). Let $\varGamma$ be obtained by $\varGamma ^{^{\!@}}\!\!$, simply by erasing all the “$x\text{@ }$”. Then $\varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma$ if and only if $\varGamma \vdash \varDelta : \sigma$ and $\mathord {\wr }\,\varDelta \,\mathord {\wr } \sqsubseteq M$.    $\square$

Proof

The left-to-right is by induction over the the derivation of $\varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma$. First observe that if the derivation consists of axiom $(\omega )$ then $\varDelta \equiv *$ and $\sigma = \omega$ and $\mathord {\wr }\,*\,\mathord {\wr } = \varOmega \sqsubseteq M$. If the derivation ends by

then by induction we have that both $\mathord {\wr }\,\varDelta _1\,\mathord {\wr }$ and $\mathord {\wr }\,\varDelta _2\,\mathord {\wr }$ are defined and that $\mathord {\wr }\,\varDelta _1\,\mathord {\wr } \sqsubseteq M \sqsupseteq \mathord {\wr }\,\varDelta _2\,\mathord {\wr }$, therefore $\mathord {\wr }\,\langle {\varDelta _1}\, ,\,{\varDelta _2} \rangle \,\mathord {\wr } = \mathord {\wr }\,\varDelta _1\,\mathord {\wr } \sqcup \mathord {\wr }\,\varDelta _2\,\mathord {\wr }$ is defined and $\mathord {\wr }\,\varDelta _1\,\mathord {\wr } \sqcup \mathord {\wr }\,\varDelta _2\,\mathord {\wr } \sqsubseteq M$ as desired.

If the derivation ends by $(\cup E)$ we reason in the same way as in case $(\cap I)$, while all other cases are immediate by induction and the fact that $\sqsubseteq$ is a pre-congruence.

The converse direction is is a straightforward induction over the derivation of $\varGamma \vdash \varDelta : \sigma$.    $\square$

Since $\mathcal{L}^{\cap \cup }$ is a proof-functional logic it is natural to consider the pair “$\varDelta :\sigma$” as a logical formula. Pictorially speaking, we could say that the type assignment system of [BDCd95] and the logic $\mathcal{L}^{\cap \cup }$ are “bridged” by the typed system $\varLambda _\mathsf{t}^{\cap \cup }$, and the above. We prove this fact by means of the concept of essence. This is, to the best of our knowledge, the first attempt to interpret union as a proof-functional connective.

3 Realizability Interpretation of Union Types

In contrast to the system of intersection types, the type assignment system $\varLambda ^{{\cap \cup }}_\mathsf{u}$ has no simple set-theoretic interpretation (see [BDCd95]). On the other hand system $\varLambda _\mathsf{t}^{\cap \cup }$ is grounded on the proof-functional logic $\mathcal{L}^{\cap \cup }$, though this is hardly standard. In this section we provide both a natural semantics for union types and a foundation for the logic $\mathcal{L}^{\cap \cup }$. We do this by interpreting the union type assignment system into the intuitionistic first order theory $\mathsf {NJ}(\beta )$, Mint’s provable realizability of intersection types extended with union. Then we prove that the $\varDelta$’s terms of system $\varLambda _\mathsf{t}^{\cap \cup }$ are just proof-terms in $\mathsf {NJ}(\beta )$.

From Theorem 6 we know that if $\varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma$, then there is a tight relation among $\varDelta$ and M, which is captured by the essence mapping. Comparing system $\varLambda ^{\cap \cup }_\mathsf{\!{\, t}}$ to the original $\varLambda ^{{\cap \cup }}_\mathsf{u}$ it is easily seen that $\varDelta$ is a proof-term of the statement $M:\sigma$ in system $\varLambda ^{{\cap \cup }}_\mathsf{u}$. But $\varDelta$ is a simply typed term: in fact if we drop the restriction concerning the “essence” in rules $(\cap I)$ and $(\cup E)$ in system $\mathcal{L}^{\cap \cup }$ replacing $\sigma \cap \tau$ by $\sigma \times \tau$ and $\sigma \cup \tau$ by $\sigma +\tau$ then we get a simply typed $\lambda$-calculus with product and sums, namely the intuitionistic propositional logic with implication, conjunction, and disjunction in disguise.

We will provide a foundation for the proof-functional logic $\mathcal{L}^{\cap \cup }$ by interpreting the $\mathcal{L}^{\cap \cup }$ into an extension of Mints’ provable realizability. However when proving a formula $r_{\sigma }[M]$ we have two kinds of realizers: the former is the untyped $\lambda$-term M, that we propose to call just a “method” borrowing terminology from Barbanera-Martini, the latter kind are $\varDelta$’s that turn out to be realizers in the ordinary sense of intuitionistic logic.

Therefore, we prove a completeness proof that this is the case, namely that $\varGamma \vdash \varDelta :\sigma$ is derivable in $\mathcal{L}^{\cap \cup }$ if and only if $\varDelta$ realizes $G_\varGamma \vdash r_{\sigma }[M]$ for some M related to $\varDelta$ by the essence mapping.

For this aim we use and extend Mints’ approach of Provable Realizability [Min89, AB91, BM94]. We interpret the statement $\vdash M \text{@ }\varDelta : \sigma$ as “$\varDelta$ is a construction of $M:\sigma$”; on the other hand $M:\sigma$ is the meaning of the formula $r_{\sigma }[M]$, provided that we extend the notion to cope with union types; the latter formula reads as “M is a method to assess $\sigma$” in terms of [LE85, BM94]; now the meaning of $\varDelta$ is that of a constructive proof of $r_{\sigma }[M]$, and hence it is a “realizer” of this formula. In short we have “two kinds" of realizers on two levels: the M, which is a Mints’ realizer of $\sigma$, and the $\varDelta$ which is an ordinary realizer, in the sense of standard Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic, of the statement $r_{\sigma }[M]$.

To avoid confusion, in the following we shall reserve the word “realizer” for the $\varDelta$-terms, and we will use the word “method” referring to the untyped $\lambda$-term M.

Definition 7

Let $\mathbf{P}_{\phi }(x)$ be a unary predicate for each atomic type $\phi$. Then we define the predicates $r_{\sigma }[M]$ for types $\sigma$ and terms M by induction over $\sigma$, as the first order logical formulae:

In the above $\supset$, $\wedge$ and $\vee$ are the logical connectives for implication, conjunction and disjunction respectively, that must be kept distinct from $\cap$ and $\cup$. In the first order language whose terms are type-free $\lambda$-terms, we have formulas of the shape $r_{\sigma }[M]$, whose intended meaning is that M is a method for $\sigma$ in the intersection-union type discipline. Note that in $r_{\sigma }[x]$ the term-variable x is the only free-variable; in particular in $r_{\sigma _1\rightarrow \sigma _2}[M] \equiv \forall y. r_{\sigma _1}[y] \supset r_{\sigma _2}[M \, y]$ we assume that $y\not \in {\mathsf {Fv}}(M)$.

By $\mathsf {NJ}$ we mean the natural-deduction presentation of the intuitionistic first-order predicate calculus. Derivations in $\mathsf {NJ}$ are trees of judgments $G\vdash A$, where G is the set of undischarged assumptions, rather than trees of formulas as in Gentzen’s original formulation.

Definition 8

(The system $\mathsf {NJ}(\beta )$ ). The system $\mathsf {NJ}(\beta )$ is the natural deduction system for first order intuitionistic logic with untyped $\lambda$-terms and predicates $\mathbf{P}_{\phi }(x)$, the latter being axiomatized via the Post rules:

If A is a formula of $\mathsf {NJ}(\beta )$ and is a set of formulæ (a context), then we write $G \vdash _{\mathsf {NJ}(\beta )}A$ to mean that A is derivable in G. To the context of the logic $\mathcal{L}^{\cap \cup }$ we associate the $\mathsf {NJ}(\beta )$ context . Note that and $x_\iota \not \in {\mathsf {Fv}}(G_\varGamma )$, since $\iota \not \in Dom(\varGamma )$, by context definition.

The following lemmas are useful to eliminate some of the intricacies of using derivations in the full system $\mathsf {NJ}(\beta )$, involving the universal quantifier in the definition of $r_{\sigma \rightarrow \tau }[M]$.

Lemma 9

The following rule is admissible in $\mathsf {NJ}(\beta )$:

Proof

By induction over the proof of $G_\varGamma \vdash _{\mathsf {NJ}(\beta )}A\{M/x\}$.    $\square$

Lemma 10

The following rules are admissible in $\mathsf {NJ}(\beta )$:

Proof

In each case, use induction over the proof of the indicated premisses.    $\square$

In spite of the similarity of the rules in Lemma 9 with those of system $\mathcal{L}^{\cap \cup }$ there are no restrictions on the shape of the derivations of the $r_{\sigma }[M]$. This is due to the fact the last lemma is about derivations of the predicate $r_{\sigma }[M]$ and not just of the proof-functional “formula” $\sigma$. Nonetheless we have:

Lemma 11

If $\varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma$ in system $\varLambda ^{\cap \cup }_\mathsf{\!{\, t}}$ then $G_\varGamma \vdash _{\mathsf {NJ}(\beta )}r_{\sigma }[M]$.

Proof

By induction over the derivation of $\varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma$ using Lemmas 9, and 10   $\square$

Theorem 12

(Soundness). If $\varGamma \vdash \varDelta :\sigma$ is derivable in $\mathcal{L}^{\cap \cup }$ then there exists M such that $G_\varGamma \vdash _{\mathsf {NJ}(\beta )}r_{\sigma }[M]$.

Proof

By Theorem 6 if $\varGamma \vdash \varDelta :\sigma$ is derivable then $\varGamma ^{^{\!@}}\!\!\vdash M \text{@ }\varDelta : \sigma$ for some $M \sqsupseteq \mathord {\wr }\,\varDelta \,\mathord {\wr }$. The thesis follows by Lemma 11.    $\square$

We say that the derivation of $G_\varGamma \vdash r_{\sigma }[M]$ is standard if it uses only the rules of the Post system, rule $(Eq\beta \eta )$ and the rules from Lemmas 9 and 10; then we write $G_\varGamma \vdash _S r_{\sigma }[M]$.

Recall that $\mathsf {NJ}(\beta )$ is a particular case of systems called I(S) in [Pra71], which enjoys the property of being strongly normalizable. The normal form of a derivation, called “fully normal derivation” by Prawitz, is split into a topmost “analytical part” consisting of elimination rules, an intermediate “minimum part” consisting of rules of the Post system, and a final “synthetical part” (ending with the very conclusion of the derivation) only consisting of introduction rules. This implies the subformula property.

Lemma 13

If $G_\varGamma \vdash _{\mathsf {NJ}(\beta )}r_{\sigma }[M]$ then $G_\varGamma \vdash _S r_{\sigma }[M]$.

Proof

By induction over the fully-normal derivation of $G_\varGamma \vdash r_{\sigma }[M]$, and then by cases of $\sigma$. If $\sigma$ is $\phi$ or $\omega$ then both the analytic and the synthetic parts are empty, and the thesis is immediate. Otherwise:  

Case $\sigma \equiv \sigma _1 \cap \sigma _2$.:

Since $r_{\sigma _1 \cap \sigma _2}[M] \equiv r_{\sigma _1}[M] \wedge r_{\sigma _2}[M]$, the fully-normal derivation of $G_\varGamma \vdash r_{\sigma _1}[M] \wedge r_{\sigma _2}[M]$ must end with $(\wedge I)$, whose premises are $G_\varGamma \vdash r_{\sigma _i}[M]$, $i\in \{1,2\}$ and the thesis follows by induction.

Case $\sigma = \sigma _1 \rightarrow \sigma _2$.:

We have $r_{\sigma _1\rightarrow \sigma _2}[M] \equiv \forall y. r_{\sigma _1}[y] \supset r_{\sigma _2}[M \, y]$, so that the synthetic part ends by:

where $y\not \in {\mathsf {Fv}}(G_\varGamma ) \cup {\mathsf {Fv}}(M)$ because of the side condition of rule $(\forall I)$ and the definition of $r_{\sigma _1\rightarrow \sigma _2}[M]$. By induction $G_\varGamma , r_{\sigma _1}[y] \vdash _S r_{\sigma _2}[M \, y]$, from which we obtain the standard derivation:

Case $\sigma = \sigma _1\cup \sigma _2$.:

Then $r_{\sigma _1\cup \sigma _2}[M] \equiv r_{\sigma _1}[M] \vee r_{\sigma _2}[M]$ and the fully-normal derivation of $G_\varGamma \vdash r_{\sigma _1}[M] \vee r_{\sigma _2}[M]$ ends by $(\vee I)$, therefore by induction $G_\varGamma \vdash _S r_{\sigma _i}[M]$ with $i\in \{ 1,2 \}$ and the thesis follows.    $\square$

 

Definition 14

( $\varDelta$ -realizability). We say that a closed $\varDelta$ realizes the formula $r_{\sigma }[M]$, written $\varDelta \Vdash r_{\sigma }[M]$, if $\mathord {\wr }\,\varDelta \,\mathord {\wr }\sqsubseteq {M}$ and:

We then define $\varDelta \Vdash G_\varGamma \vdash r_{\sigma }[M]$ where $\varDelta$ is a possibly open term such that ${\mathsf {Fv}}(\varDelta ) = \{ \iota _1,\ldots ,\iota _k \} \subseteq {\mathsf {Fv}}(\varGamma )$, if and only if for all closed $\varDelta _1,\ldots ,\varDelta _k$ and terms $N_1,\ldots ,N_k$ such that $\varDelta _i \Vdash r_{\varGamma (\iota _i)}[N_i]$ for all $i = 1,\ldots ,k$ it is the case that (writing $x_i \equiv x_{\iota _i}$):

$$\begin{aligned} \varDelta \{\varDelta _1 / \iota _1\}\cdots \{\varDelta _k / \iota _k\} \Vdash r_{\sigma }[M\{N_1 / x_1\}\cdots \{N_k / x_k\}]. \end{aligned}$$

Lemma 15

If $G_\varGamma \vdash _{\mathsf {NJ}(\beta )}r_{\sigma }[M]$ then there exists $\varDelta$ such that $\varDelta \Vdash G_\varGamma \vdash r_{\sigma }[M]$.

Proof

By Lemma 13 we can argue by induction over the standard derivation of $G_\varGamma \vdash r_{\sigma }[M]$. If it ends by a Post rule, then the thesis is trivial. Suppose that it ends by the inference

Then by induction there are $\varDelta _1,\varDelta _2$ such that $\mathord {\wr }\,\varDelta _i\,\mathord {\wr } \sqsubseteq M$ and $\varDelta _i \Vdash G_\varGamma \vdash r_{\sigma _i}[M]$. Taking $\varDelta \equiv \langle {\varDelta _1}\, ,\,{\varDelta _2} \rangle$ we have that $\mathord {\wr }\,\varDelta _1\,\mathord {\wr } \sqsubseteq M \sqsupseteq \mathord {\wr }\,\varDelta _2\,\mathord {\wr }$ and $\mathord {\wr }\,\varDelta \,\mathord {\wr } = \mathord {\wr }\,\varDelta _1\,\mathord {\wr } \sqcup \mathord {\wr }\,\varDelta _2\,\mathord {\wr } \sqsubseteq M$ hence $\varDelta \Vdash G_\varGamma \vdash r_{\sigma _1\cap \sigma _2}[M]$. All other cases are similar.    $\square$

Lemma 16

If $\varDelta \Vdash G_\varGamma \vdash r_{\sigma }[M]$ then there exists N and $\varDelta '$ such that $M =_{\beta \eta } N$ and $\varGamma ^{^{\!@}}\!\!\vdash N \text{@ }\varDelta ' : \sigma$.

Proof

By induction over $\sigma$.    $\square$

Theorem 17

(Completeness). If $G_\varGamma \vdash _{\mathsf {NJ}(\beta )}r_{\sigma }[M]$ then there exists $N=_{\beta \eta }M$ and $\varDelta$ such that $\varGamma ^{^{\!@}}\!\!\vdash N \text{@ }\varDelta : \sigma$ and therefore $\varGamma \vdash \varDelta :\sigma$.

Proof

By the hypothesis and Lemma 15 we know that there is a $\varDelta '$ such that $\varDelta ' \Vdash G_\varGamma \vdash r_{\sigma }[M]$. By Lemma 16 this implies that $\varGamma ^{^{\!@}}\!\!\vdash N \text{@ }\varDelta : \sigma$ for some $\varDelta$ and $N=_{\beta \eta }M$, and we conclude by Theorem 6.    $\square$

4 Further Logical Developments and Implementation

There is active ongoing work on both the theoretical and practical directions of this project.

4.1 Implicit Subtyping as Explicit Coercions

The logic $\mathcal{L}^{\cap \cup }$ does not encompass the subtyping relation treated in [BDCd95], which extends the subtyping relation among intersection types introduced in [BCDC83]. Given such a relation $\le$, the subsumption rule takes the form:

This rule has a character similar to the intersection and union introduction rules because the subject M of the conclusion is the same as in the premise. This calls for a consistent treatment on the side of the $\varDelta$’s that are typed terms. In [DL10] it was hinted that the subtyping as coercion should be the proper approach, in the sense that whenever $\sigma \le \tau$ there should exist a coercion $\lambda$-term $\textit{coe}_{\sigma \le \tau }: \sigma \rightarrow \tau$ such that the following rule is sound:

According to the logic $\mathcal{L}^{\cap \cup }$ this rule is sound if $\mathord {\wr }\,\textit{coe}_{\sigma \le \tau }(\varDelta )\,\mathord {\wr } \sqsubseteq M$, while according to the realizability interpretation this is the case if realizers of $r_{\sigma }[M]$ are sent to realizers of $r_{\tau }[M]$. We argue that this is the case by showing that, at least for the type theory $\varXi$ from [BDCd95], we could establish the following:

Conjecture 18

If $\sigma \le \tau \in \varXi$ then there exists a combinator $\textit{coe}_{\sigma \le \tau }$ such that $\vdash \textit{coe}_{\sigma \le \tau }:\sigma \rightarrow \tau$ is a theorem of $\mathcal{L}^{\cap \cup }$ and $\mathord {\wr }\,\textit{coe}_{\sigma \le \tau }\,\mathord {\wr } \sqsubseteq \lambda x.x$.

We end this subsection by observing that Conjecture 18 is in accordance with the logical interpretation of intersection types proposed in [BM94]. In fact from the logical point of view, subtyping of intersection (and union) types corresponds to inject concepts and rules proper to the Minimal Relevant Logical system $B^+$ introduced by Meyer-Routley in’72. As nicely explained in the Barbanera-Martini paper, the relevant implication, denoted by $\supset _r$ from the logic side and $\rightarrow _r$ from the type side, captures the behavior of the coercion function $coe_{\sigma \le \tau }$ as follows:

“To assert $\sigma \rightarrow _r \tau$ (read also $\sigma \le \tau$ ) is to assert that any proof-inhabitant of $\sigma$ is also a proof-inhabitant of $\tau$”.

Our system then meets the latter requirement because any coercion is “essentially” the identity.

4.2 Logical Frameworks

The results presented here are part of a larger project to build a small logical framework, à la the Edinburgh Logical Framework [HHP93], featuring proof-functional logical connectives like strong conjunction (intersection) and strong sum (union), and allowing reasoning about the structure of logical proofs, in this way giving to the latter the status of first-class objects. We could also mention the high expressivity of ad hoc (intersection) polymorphism, since it allows to typecheck the untyped $\lambda$-term abstraction $\lambda x.x \, x$ (self-application), essence of a suitable $\varDelta$ term, with the intersection type $(\sigma \cap (\sigma \rightarrow \sigma )) \rightarrow \sigma$. Other insights could come in studying case constructs typechecked with union types.

Another positive outcome of this research line would be the introduction of proof-functional types into existing interactive theorem provers such as Coq [Coq16] or Isabelle [Isa16], and dependently typed programming languages such as Agda [Agd16], Epigram [Epi16], or Idris [Idr16].

Finally, other advances in research line could come in studying other proof-functional logical connectives, like relevant implication (where the implication is established by an identity map) and strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), the two being proof-functional interpretations of subtyping and provable type isomorphism, respectively.

4.3 Prototype Implementation

Our current implementation experiments with a small kernel for a logical framework featuring union and intersection types satisfying the De Brujin Principle saying “Keep the framework as weak as possible (A plea for weaker frameworks").

The prototype is written in the functional language ML. Its Read-Eval-Print-Loop (REPL) can read a file containing some signatures, and process it using a lexer, then a parser. Then it can do the following actions:

• type-check the proof

• normalize the proof using strong reduction

• add some definitions in the global context

• perform a (human interactive) type inhabitation algorithm

We are putting our current efforts into make the REPL to consider proofs ($\varDelta$ terms) as a genuine first-class objects.

We implemented the $\varLambda _\mathsf{t}^{\cap \cup }$ calculus and the proof-functional logic $\mathcal{L}^{\cap \cup }$ as presented here. We have added a wildcard type called “?” to deal with union introduction, and we added an unification algorithm to apply eliminations rule for implication and union types. The actual type system also features a first implementation of dependent-types à la LF: explicit coercions and strong equivalence are on the top of our implementation’ todo list. The aim of the prototype is to check the expressiveness of the proof-functional nature of the logical engine in the sense that when the user must prove e.g. a strong conjunction formula $\sigma _1 \cap \sigma _2$ obtaining (mostly interactively) a witness $\varDelta _1$ for $\sigma _1$, the prototype can “squeeze” the essence M of $\varDelta _1$ to accelerate, and in some case automatize, the construction of a witness $\varDelta _2$ proof for the formula $\sigma _2$ having the same essence M of $\varDelta _1$. Existing proof assistants could get some benefit if extended with a proof-functional logic. We are also started an encoding of the proof-functional operators of intersection and union in Coq. The actual state of the prototype can be retrieved at https://github.com/cstolze/Bull.