Depending on Session-Typed Processes

Abstract

This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed $\lambda$-calculus. The proposed framework, by allowing session processes to depend on functions and vice-versa, enables us to specify and statically verify protocols where the choice of the next communication action can depend on specific values of received data. Moreover, the type theoretic nature of the framework endows us with the ability to internally describe and prove predicates on process behaviours. Our main results are type soundness of the framework, and a faithful embedding of the functional layer of the calculus within the session-typed layer, showcasing the expressiveness of dependent session types.

1 Introduction

Session types [14, 24] are a typing discipline for communication protocols, whose simplicity provides an extensible framework that allows for integration with a variety of functional type features. One useful instance arising from the proof theoretic exploration of logical quantification is value dependent session types [25]. In this work, one can express properties of exchanged data in protocol specifications separately from communication, but cannot describe protocols where communication actions depend on the actual exchanged data (e.g. [16, Sect. 2]). Moreover, it does not allow functions or values to depend on protocols (i.e. sessions) or communication, thus preventing reasoning about dependent process behaviours, exploring the proofs-as-programs paradigm of dependent type theory, e.g. [8, 17].

Our work addresses the limitations of existing formulations of session types by proposing a type theory that integrates dependent functions and session types using a contextual monad. This monad internalises a session-typed calculus within a dependently-typed $\lambda$-calculus. By allowing session types to depend on $\lambda$-terms and $\lambda$-terms to depend on typed processes (using the monad), we are able to achieve heightened degrees of expressiveness. Exploiting the former direction, we enable writing actual data-dependent communication protocols. Exploiting the latter, we can define and prove properties of linearly-typed objects (i.e. processes) within our intuitionistic theory.

To informally demonstrate how our type theory goes beyond the state of the art in order to represent data-dependent protocols, consider the following session type (we write $\tau \wedge A$ for $\exists x{:}\tau .A$ where x does not occur in A and similarly $\tau \supset A$ for $\forall x{:}\tau .A$ when x is not free in A), $T \triangleq {\textsf {Bool}}\supset \oplus \{\mathtt {t}: {\textsf {Nat}} \wedge \mathbf {1}, \mathtt {f}: {\textsf {Bool}} \wedge \mathbf {1}\}$, representable in existing session typing systems. The type T denotes a protocol which first, inputs a boolean and then either emits the label $\mathtt {t}$, which will be followed by an output of a natural number; or emits the label $\mathtt {f}$ and a boolean. The intended protocol described by T is to take the $\mathtt {t}$ branch if the received value is $\mathtt {t}$ and the $\mathtt {f}$ branch otherwise, which we can implement as Q with channel z typed by T as follows:

$$ \begin{array}{lcl} Q\triangleq & {} z(x).\mathsf {case}\;x\;\mathsf {of}\;(\mathsf {true} \Rightarrow z.\mathtt {t}; z\langle 23 \rangle .\varvec{0}, \ \mathsf {false} \Rightarrow z.\mathtt {f};z\langle \mathsf {true} \rangle .\varvec{0}) \end{array} $$

where z(x).P denotes an input process, $z.\mathtt {t}$ is a process which selects label $\mathtt {t}$ and $z\langle 23 \rangle .P$ is an output on z. However, since the specification is imprecise, process $z(x).\mathsf {case}\;x\;\mathsf {of}\;(\mathsf {false} \Rightarrow z.\mathtt {t}; z\langle 23 \rangle .\varvec{0}, \ \mathsf {true} \Rightarrow z.\mathtt {f};z\langle \mathsf {true} \rangle .\varvec{0})$ is also a type-correct implementation of T that does not adhere to the intended protocol. Using our dependent type system, we can narrow the specification to guarantee that the desired protocol is precisely enforced. Consider the following definition of a session-type level conditional where we assume inductive definition and dependent pattern matching mechanisms ($\mathsf {stype}$ denotes the kind of session types):

$$ \begin{array}{l} \mathtt {if} ~{::}~ \textsf {Bool}\rightarrow \mathsf {stype}\rightarrow \mathsf {stype}\rightarrow \mathsf {stype}\\ \mathtt {if}\ \mathsf {true}\, A\, B \ = \ A \quad \quad \mathtt {if}\ \mathsf {false}\, A\, B \ = \ B \end{array} $$

The type-level function above case analyses the boolean and produces its first session type argument if the value is $\mathsf {true}$ and the second otherwise. We may now specify a session type that faithfully implements the protocol:

$$ T' \triangleq \forall x{:}\textsf {Bool}.\mathtt {if}\,x\,(\textsf {Nat} \wedge \mathbf {1})\, (\textsf {Bool}\wedge \mathbf {1}) $$

A process R implementing such a type on channel z is given below:

$$ \begin{array}{lcl} R \triangleq z(x).\mathsf {case}\;x\;\mathsf {of}\;(\mathsf {true} \Rightarrow z\langle 23 \rangle .\varvec{0}, \ \mathsf {false} \Rightarrow z\langle \mathsf {true} \rangle .\varvec{0}) \end{array} $$

Note that if we flip the two branches of the case analysis in R, the session is no longer typable with $T'$, ensuring that the protocol is implemented faithfully.

The example above illustrates a simple yet useful data-dependent protocol. When we further extend our dependent types with a process monad [29], where $\{c \leftarrow P \leftarrow \overline{u_j};\overline{d_i}\}$ is a functional term denoting a process that may be spawned by other processes by instantiating the names in $\overline{u_j}$ and $\overline{d_i}$, we can provide more powerful reasoning on processes, enabling refined specifications through the use of type indices (i.e. type families) and an ability to internally specify and verify predicates on process behaviours. We also show that all functional types and terms can be faithfully embedded in the process layer using the dependently-typed sessions and process monads.

Contributions. Section 2 introduces our dependent type theory, augmenting the example above by showing how we can reason about process behaviour using type families and dependently-typed functions (Sect. 2.3). We then establish the soundness of the theory (Sect. 2.4). Section 3 develops a faithful embedding of the dependent function space in the process layer (Theorem 3.4). Section 4 concludes with related work. Proofs, omitted definitions and additional examples can be found in [32].

2 A Dependent Type Theory of Processes

This section introduces our dependent type theory combining session-typed processes and functions. The theory is a generalisation of the line of work relating linear logic and session types [4, 25, 29], considering type-level functions and dependent kinds in an intensional type theory with full mutual dependencies between functions and processes. This generalisation enables us to express more sophisticated session types (such as those of Sect. 1) and also to define and prove properties of processes expressed as type families with proofs as their inhabitants. We focus on the new rules and judgements, pointing the interested reader to [5, 25, 26] for additional details on the base theory.

2.1 Syntax

The calculus is stratified into two mutually dependent layers of processes and terms, which we often refer to as the process and functional layers, respectively. The syntax of the theory is given in Fig. 1 (we use x, y for variables ranging over terms and t for variables ranging over types).

Fig. 1.

Syntax of kinds, types, terms and processes

Types and Kinds. The process layer is able to refer to terms of the functional layer via appropriate (dependently-typed) communication actions and through a spawn construct, allowing for processes encapsulated as functional values to be executed. Dually, the functional layer can refer to the process layer via a contextual monad [29] that internalises (open) typed processes as opaque functional values. This mutual dependency is also explicit in the type structure on several axes: process channel usages are typed by a language of session types, which specifies the communication protocols implemented on the used channels, extended with two dependent communication operations $\forall x{:}\tau .A$ and $\exists x{:}\tau .A$, where $\tau$ is a functional type and A is a session type in which x may occur. Moreover, we also extend the language of session types with type-level $\lambda$-abstraction over terms $\lambda x{:}\tau .A$ and session types $\lambda t\,{::}\,K.A$ (with the corresponding elimination forms $A\,M$ and $A\,B$). As we show in Sect. 1, the combination of these features allows for a new degree of expressiveness, enabling us to construct session types whose structure depends on previously communicated values.

The remaining session constructs are standard, following [5]: ${!}A$ denotes a shared session of type A that may be used an arbitrary (finite) number of times; $A \multimap B$ represents a session offering to input a session of type A to then offer the session behaviour B; $A \otimes B$ is the dual operator, denoting a session that outputs A and proceeds as B; $\oplus \{\overline{l_i : A_i}\}$ and represent internal and external labelled choice, respectively; $\mathbf {1}$ denotes the terminated session.

The functional layer is a $\lambda$-calculus with dependent functions $\varPi x{:}\tau .\sigma$, type-level $\lambda$-abstractions over terms and types (and respective type-level applications) and a contextual monadic type $\{\overline{u_j{:}B_j} ; \overline{d_i{:}A_i} \vdash c{:}A\}$, denoting a (quoted) process offering session c:A by using the linear sessions $\overline{d_i{:}A_i}$ and shared sessions $\overline{u_j{:}B_j}$ [29]. We often write $\{A\}$ for $\{\cdot ;\cdot \vdash c{:}A\}$. The kinding system for our theory contains two base kinds $\mathsf {type}$ and $\mathsf {stype}$ of functional and session types, respectively. Type-level $\lambda$-abstractions require dependent kinds $\varPi x{:}\tau .K$ and $\varPi t\,{::}\,K.K'$, respectively. We note that the functional connectives form a standard dependent type theory [11, 21].

Terms and Processes. Terms include the standard $\lambda$-abstractions $\lambda x{:}\tau .M$, applications $M\,N$ and variables x. In order to internalise processes within the functional layer we make use of a monadic process wrapper, written $\{c \leftarrow P \leftarrow \overline{u_j}; \overline{d_i}\}$. In such a construct, the channels c, $\overline{u_j}$ and $\overline{d_i}$ are bound in P, where c is the session channel being offered and $\overline{u_j}$ and $\overline{d_i}$ are the session channels (linear and shared, respectively) being used. We write $\{c \leftarrow P \leftarrow \epsilon \}$ when P does not use any ambient channels, which we abbreviate to $\{P\}$.

The syntax of processes follows that of [5] extended with the monadic elimination form $c \leftarrow M \leftarrow \overline{u_j} ; \overline{d_i} ; Q$. Such a process construct denotes a term M that is to be evaluated to a monadic value of the form $\{c \leftarrow P \leftarrow \overline{u_j} ; \overline{d_i}\}$ which will then be executed in parallel with Q, sharing with it a session channel c and using the provided channels $\overline{u_j}$ and $\overline{d_i}$. We write $c\leftarrow M \leftarrow \epsilon ; Q$ when no channels are provided for the execution of M and often abbreviate this to $c\leftarrow M ; Q$. The process $\overline{c}\langle d \rangle .P$ denotes the output of the fresh channel d along channel c with continuation P, which binds d; $({\varvec{\nu }}c)P$ denotes channel hiding, restricting the scope of c to P; c(x).P denotes an input along c, bound to x in P; $c\langle M \rangle .P$ denotes the output of term M along c with continuation P; ${!}c(x).P$ denotes a replicated input which spawns copies of P; the construct $c.\mathsf {case}\{\overline{l_i \Rightarrow P_i}\}$ codifies a process that waits to receive some label $l_j$ along c, with continuation $P_j$; dually, c.l; P denotes a process that emits a label l along c and continues as P; $[c\leftrightarrow d]$ denotes a forwarder between c and d, which is operationally implemented as renaming; $P\mid Q$ denotes parallel composition and $\varvec{0}$ the null process.

2.2 A Dependent Typing System

We now introduce our typing system, defined by a series of mutually inductive judgements, given in Fig. 2. We use $\varPsi$ to stand for a typing context for dependent $\lambda$-terms (i.e. assumptions of the form $x{:}\tau$ or $t\,{::}\,K$, not subject to exchange), $\varGamma$ for a typing context for shared sessions of the form u:A (implicitly subject to weakening and contraction) and $\varDelta$ for a linear context of sessions x:A. The context well-formedness judgments $\varPsi \vdash$ and $\varPsi ; \varDelta \vdash$ require that types and kinds (resp. session types) in $\varPsi$ (resp. $\varDelta$) are well-formed. The judgments $\varPsi \vdash K$, $\varPsi \vdash \tau \,{::}\,K$ and $\varPsi \vdash A\,{::}\,K$ codify well-formedness of kinds, functional and session types (with kind K), respectively. Their rules are standard.

Fig. 2.

Typing judgements

Typing. An excerpt of the typing rules for terms and processes is given in Figs. 3 and 4, respectively, noting that typing enforces types to be of base kind $\mathsf {type}$ (respectively $\mathsf {stype}$). The rules for dependent functions are standard, including the type conversion rule which internalises definitional equality of types. We highlight the introduction rule for the monadic construct, which requires the appropriate session types to be well-formed and the process P to offer c:A when provided with the appropriate session contexts.

In the typing rules for processes (Fig. 4), presented as a set of right and left rules (the former identifying how to offer a session of a given type and the latter how to use such a session), we highlight the rules for dependently-typed communication and monadic elimination (for type-checking purposes we annotate constructs with the respective dependent type – this is akin to functional type theories). To offer a session $c{:}\exists x{:}\tau .A$ we send a term M of type $\tau$ and then offer a session $c{:}A\{M/x\}$; dually, to use such a session we perform an input along c, bound to x in Q, warranting a use of c as a session of (open) type A. The rules for the universal are dual. Offering a session $c{:}\forall x{:}\tau .A$ entails receiving on c a term of type $\tau$ and offering c:A. Using a session of such a type requires sending along c a term M of type $\tau$, warranting the use of c as a session of type $A\{M/x\}$.

The rule for the monadic elimination form requires that the term M be of the appropriate monadic type and that the provided channels $\overline{u_j}$ and $\overline{y_i}$ adhere to the typing specified in M’s type. Under these conditions, the process Q may then use the session c as session A. The type conversion rules reflect session type definitional equality in typing.

Fig. 3.

Typing for terms (Excerpt – See [32])

Fig. 4.

Typing for processes (Excerpt – See [32])

Definitional Equality. The crux of any dependent type theory lies in its definitional equality. Type equality relies on equality of terms which, by including the monadic construct, necessarily relies on a notion of process equality.

Our presentation of an intensional definitional equality of terms follows that of [12], where we consider an intrinsically typed relation, including $\beta$ and $\eta$ conversion (similarly for type equality which includes $\beta$ and $\eta$ principles for the type-level $\lambda$-abstractions). An excerpt of the rules for term equality is given in Fig. 5. The remaining rules are congruence rules and closure under symmetry, reflexivity and transitivity. Rule $(\mathsf {TMEq}\beta )$ captures the $\beta$-reduction, identifying a $\lambda$-abstraction applied to an argument with the substitution of the argument in the function body (typed with the appropriately substituted type). We highlight rule $(\mathsf {TMEq}\{\}\eta )$, which codifies a general $\eta$-like principle for arbitrary terms of monadic type: We form a monadic term that applies the monadic elimination form to M, forwarding the result along the appropriate channel, which becomes a term equivalent to M.

Definitional equality of processes is summarised in Fig. 6. We rely on process reduction defined below. Definitional equality of processes consists of the usual congruence rules, (typed) reductions and the commutting conversions of linear logic and $\eta$-like principles, which allows for forwarding actions to be equated with the primitive syntactic forwarding construct. Commutting conversions amount to sound observational equivalences between processes [22], given that session composition requires name restriction (embodied by the $(\mathsf {cut})$ rule): In rule $(\mathsf {PEqCC}\forall )$, either process can only be interacted with via channel c and so postponing actions of P to after the input on c (when reading the equality from left to right) cannot impact the process’ observable behaviours. While P can in general interact with sessions in $\varDelta$ (or with Q), these interactions are unobservable due to hiding in the $(\mathsf {cut})$ rule.

Fig. 5.

Definitional equality of terms (Excerpt – See [32])

Fig. 6.

Definitional equality of processes (Excerpt – See [32])

Operational Semantics. The operational semantics for the $\lambda$-calculus is standard, noting that no reduction can take place inside monadic terms. The operational (reduction) semantics for processes is presented below where we omit closure under structural congruence and the standard congruence rules [4, 25, 29]. The last rule defines spawning a process in a monadic term.

$$ \begin{array}{ll} c\langle M \rangle .P \mid c(x).Q \xrightarrow {} P \mid Q\{M/x\} &{} \overline{c}\langle x\rangle .P \mid c(x).Q \xrightarrow {} ({\varvec{\nu }}x)(P \mid Q)\\ {!}c(x).P \mid \overline{c}\langle x \rangle .Q \xrightarrow {} {!}c(x).P \mid ({\varvec{\nu }}x)(P \mid Q)\quad &{} c.\mathsf {case}\{\overline{l_i \Rightarrow P_i}\} \mid c.l_j;Q \xrightarrow {} P_j \mid Q\,\,\,\,(l_j \in \overline{l_i})\\ ({\varvec{\nu }}c)(P \mid [c\leftrightarrow d]) \xrightarrow {} P\{d/c\} &{} c\leftarrow \{c\leftarrow P \leftarrow \overline{u_j};\overline{d_i}\} \leftarrow \overline{u_j};\overline{d_i} ; Q \xrightarrow {} ({\varvec{\nu }}c)(P \mid Q) \end{array} $$

2.3 Example – Reasoning About Processes Using Dependent Types

The use of type indices (i.e. type families) in dependently typed frameworks adds information to types to produce more refined specifications. Our framework enables us to do this at the level of session types.

Consider a session type that “counts down” on a natural number (we assume inductive definitions and dependent pattern matching in the style of [21]):

$$ \begin{array}{lcl} \mathsf {countDown} &{} {::} &{} \varPi x{:}\mathsf {Nat}.\mathsf {stype}\\ \mathsf {countDown}\,(\mathsf {succ}(n)) &{} = &{} \exists y{:}\mathsf {Nat}.\mathsf {countDown}(n)\\ \mathsf {countDown}\,\,\,\mathsf {z} &{} = &{} \mathbf {1}\end{array} $$

The type family $\mathsf {countDown}(n)$ denotes a session type that emits exactly n numbers and then terminates. We can now write a (dependently-typed) function that produces processes with the appropriate type, given a starting value:

$$ \begin{array}{lcl} \mathsf {counter} &{} : &{} \varPi x{:}\mathsf {Nat}.\{\mathsf {countDown}(x)\}\\ \mathsf {counter}\,\,\,(\mathsf {succ}(n)) &{} = &{} \{c \leftarrow c\langle \mathsf {succ}(n) \rangle . \, d \leftarrow \mathsf {counter}(n) ; [d\leftrightarrow c]\}\\ \mathsf {counter}\,\,\,\mathsf {z} &{} = &{} \{c\leftarrow \varvec{0}\} \end{array} $$

Note how the type of $\mathsf {counter}$, through the type family $\mathsf {countDown}$, allows us to specify exactly the number of times a value is sent. This is in sharp contrast with existing recursive (or inductive/coinductive [18, 30]) session types, where one may only specify the general iterative nature of the behaviour (e.g. “send a number and then recurse or terminate”).

The example above relies on session type indexing in order to provide additional static guarantees about processes (and the functions that generate them). An alternative way is to consider “simply-typed” programs and then prove that they satisfy the desired properties, using the language itself. Consider a simply-typed version of the counter above described as an inductive session type:

$$ \begin{array}{lcl} \mathsf {simpleCounterT} &{} {::} &{} \mathsf {stype}\\ \mathsf {simpleCounterT} &{} = &{} \oplus \{\mathsf {dec} : \mathsf {Nat}\wedge \mathsf {simpleCounterT} , \mathsf {done} : \mathbf {1}\} \end{array} $$

There are many processes that correctly implement such a type, given that the type merely dictates that the session outputs a natural number and recurses (modulo the $\mathsf {dec}$ and $\mathsf {done}$ messages to signal which branch of the internal choice is taken). A function that produces processes implementing such a session, mirroring those generated by the $\mathsf {counter}$ function above, is:

$$ \begin{array}{lcl} \mathsf {simpleCounter} &{} : &{} \mathsf {Nat}\rightarrow \{\mathsf {simpleCounterT}\}\\ \mathsf {simpleCounter}\,\,\,(\mathsf {succ}(n)) &{} = &{} \{c\leftarrow c.\mathsf {dec}; ({\varvec{\nu }}d)(d\langle \mathsf {succ}(n) \rangle .\varvec{0}\mid d(x). c\langle x\rangle .\\ &{}&{} \,\,\, d\leftarrow \mathsf {simpleCounter}(n); [d\leftrightarrow c]) \} \\ \mathsf {simpleCounter} \quad \mathsf {z} &{} = &{} \{c\leftarrow c.\mathsf {done};\varvec{0}\} \\ \end{array} $$

The process generated by $\mathsf {simpleCounter}$, after emiting the $\mathsf {dec}$ label, spawns a process in parallel that sends the appropriate number, which is received by the parallel thread and then sent along the session c. Despite its simplicity, this example embodies a general pattern where a computation is spawned in parallel (itself potentially spawning many other threads) and the main thread then waits for the result before proceeding.

While such a process is typable in most session typing frameworks, our theory enables us to prove that the counter implementation above indeed counts down from a given number by defining an appropriate (inductive) type family, indexed by monadic values (i.e. processes):

$$ \begin{array}{lcl} \mathsf {corrCount} &{} {::} &{} \varPi x{:}\mathsf {Nat}.\varPi y{:}\{\mathsf {simpleCounterT}\}.\mathsf {type}\\ \mathsf {corr}_z &{} : &{} \mathsf {corrCount}\,\mathsf {z}\,\{c\leftarrow c.\mathsf {done};\varvec{0}\}\\ \mathsf {corr}_n &{} : &{} \varPi n {:}\mathsf {Nat}.\varPi P{:}\{\mathsf {simpleCounterT}\}. \mathsf {corrCount}\,n\,P \rightarrow \\ &{} &{} \mathsf {corrCount}\,(\mathsf {succ}(n))\,\{c\leftarrow c.\mathsf {dec}; c\langle \mathsf {succ}(n) \rangle .d\leftarrow P ; [d\leftrightarrow c]\} \end{array} $$

The type family $\mathsf {corrCount}$, indexed by a natural number and a monadic value implementing the session type $\mathsf {simpleCounter}$, is defined via two constructors: $\mathsf {corr}_z$, which specifies that a correct 0 counter emits the $\mathsf {done}$ label and terminates; and $\mathsf {corr}_n$, which given a monadic value P that is a correct n-counter, defines that a correct $(n+1)$-counter emits $n+1$ and then proceeds as P (modulo the label emission bookkeeping).

The proof of correctness of the $\mathsf {simpleCounter}$ function above is no more than a function of type $\varPi n{:}\mathsf {Nat}.\mathsf {corrCount}\,n$ $(\mathsf {simpleCounter}(n))$, defined below:

$$ \begin{array}{lcl} \mathsf {prf} &{} : &{} \varPi n{:}\mathsf {Nat}.\mathsf {corrCount}\,n \,(\mathsf {simpleCounter}(n))\\ \mathsf {prf}\quad \mathsf {z} &{} = &{} \mathsf {corr}_z\\ \mathsf {prf}\quad (\mathsf {succ}(n)) &{} = &{} \mathsf {corr}_n\,n\,(\mathsf {simpleCounter}(n))\,(\mathsf {prf}\,n) \end{array} $$

Note that in this scenario, the processes that index the $\mathsf {corrCount}$ type family are not syntactically equal to those generated by $\mathsf {simpleCounter}$, but rather definitionally equal.

Typically, the processes that index such correctness specifications tend to be distilled versions of the actual implementations, which often perform some additional internal computation or communication steps. Since our notion of definitional equality of processes includes reduction (and also commuting conversions which account for type-preserving shuffling of internal communication actions [26]), the type conversion mechanism allows us to use the techniques described above to generally reason about specification conformance.

2.4 Type Soundness of the Framework

The main goal of this section is to present type soundness of our framework through a subject reduction result. We also show that our theory guarantees progress for terms and processes. The development requires a series of auxiliary results (detailed in [32]) pertaining to the functional and process layers which are ultimately needed to produce the inversion properties necessary to establish subject reduction. We note that strong normalisation results for linear-logic based session processes are known in the literature [3, 26, 30], even in the presence of impredicative polymorphism, restricted corecursion and higher-order data. Such results are directly applicable to our work using appropriate semantics preserving type erasures.

In the remainder we often write $\varPsi \vdash \mathcal {J}$ to stand for a well-formedness, typing or definitional equality judgment of the appropriate form. Similarly for $\varPsi ; \varGamma ; \varDelta \vdash \mathcal {J}$. We begin with the substitution property, which naturally holds for both layers, noting that the dependently typed nature of the framework requires substitution in both contexts, terms and in types.

Lemma 2.1

(Substitution). Let $\varPsi \vdash M :\tau$:

• 1. If $\varPsi , x{:}\tau , \varPsi ' \vdash \mathcal {J}$ then $\varPsi , \varPsi '\{M/x\} \vdash \mathcal {J}\{M/x\}$;

• 2. If $\varPsi , x{:}\tau , \varPsi ' ; \varGamma ; \varDelta \vdash \mathcal {J}$ then $\varPsi , \varPsi '\{M/x\} ; \varGamma \{M/x\} ; \varDelta \{M/x\}\vdash \mathcal {J}\{M/x\}$

Combining substitution with a form of functionality for typing (i.e. that substitution of equal terms in a well-typed term produces equal terms) and for equality (i.e. that substitution of equal terms in a definitional equality proof produces equal terms), we can establish validity for typing and equality, which is a form of internal soundness of the type theory stating that judgments are consistent across the different levels of the theory.

Lemma 2.2

(Validity for Typing). (1) If $\varPsi \vdash \tau \,{::}\,K$ or $\varPsi \vdash A\,{::}\,K$ then $\varPsi \vdash K$; (2) If $\varPsi \vdash M : \tau$ then $\varPsi \vdash \tau \,{::}\,\mathsf {type}$; and (3) If $\varPsi ; \varGamma ; \varDelta \vdash P\,{::}\,z{:}A$ then $\varPsi \vdash A\,{::}\,\mathsf {stype}$.

Lemma 2.3

(Validity for Equality)

• 1. If $\varPsi \vdash M = N : \tau$ then $\varPsi \vdash M : \tau$, $\varPsi \vdash N : \tau$ and $\varPsi \vdash \tau \,{::}\, \mathsf {type}$

• 2. If $\varPsi \vdash \tau = \sigma \,{::}\,K$ then $\varPsi \vdash \tau \,{::} \,K$, $\varPsi \vdash \sigma \,{::}\,K$ and $\varPsi \vdash K$

• 3. If $\varPsi \vdash A = B\,{::}\,K$ then $\varPsi \vdash A\,{::}\,K$, $\varPsi \vdash B\,{::}\,K$ and $\varPsi \vdash K$

• 4. If $\varPsi \vdash K = K'$ then $\varPsi \vdash K$ and $\varPsi \vdash K'$

• 5. If $\varPsi ; \varGamma ; \varDelta \vdash P = Q\,{::}\,z{:}A$ then $\varPsi ; \varGamma ; \varDelta \vdash P\,{::}\,z{:}A$, $\varPsi ; \varGamma ; \varDelta \vdash Q\,{::}\,z{:}A$ and $\varPsi \vdash A\,{::}\, \mathsf {stype}$.

With these results we establish the appropriate inversion and injectivity properties which then enable us to show unicity of types (and kinds).

Theorem 2.4

(Unicity of Types and Kinds)

• 1. If $\varPsi \vdash M : \tau$ and $\varPsi \vdash M : \tau '$ then $\varPsi \vdash \tau = \tau ' \,{::}\,\mathsf {type}$

• 2. If $\varPsi \vdash \tau \,{::}\,K$ and $\varPsi \vdash \tau \,{::}\, K'$ then $\varPsi \vdash K = K'$

• 3. If $\varPsi ; \varGamma ; \varDelta \vdash P\,{::}\, z{:}A$ and $\varPsi ; \varGamma ; \varDelta \vdash P\,{::}\, z{:}A'$ then $\varPsi \vdash A = A'\,{::}\, \mathsf {stype}$

• 4. If $\varPsi \vdash A\,{::}\, K$ and $\varPsi \vdash A\,{::}\, K'$ then $\varPsi \vdash K = K'$.

All the results above, combined with the process-level properties established in [5, 26, 27] enable us to show the following:

Theorem 2.5

(Subject Reduction – Terms). If $\varPsi \vdash M : \tau$ and $M\xrightarrow {} M'$ then $\varPsi \vdash M' : \tau$.

Theorem 2.6

(Subject Reduction – Processes). If $\varPsi ; \varGamma ; \varDelta \vdash P\,{::}\, z{:}A$ and $P \xrightarrow {} P'$ then $\exists Q$ such that $P' \equiv Q$ and $\varPsi ; \varGamma ; \varDelta \vdash Q\,{::}\, z{:}A$.

Theorem 2.7

(Progress – Terms). If $\varPsi \vdash M : \tau$ then either M is a value or $M \xrightarrow {} M'$.

As common in logical-based session type theories, typing enforces a strong notion of global progress which states that closed processes that are waiting to perform communication actions cannot get stuck (this relies on a notion of live process, defined as $\mathsf {live}(P)$ iff $P \equiv ({\varvec{\nu }}\tilde{n})(\pi .Q \mid R)$ for some process R, sequence of names $\tilde{n}$ and a non-replicated guarded process $\pi .Q$). We note that the restricted typing for P is without loss of generality, due to the $(\mathsf {cut})$ rule.

Theorem 2.8

(Progress – Processes). If $\varPsi ;\cdot ;\cdot \vdash P\,{::}\,c{:}\mathbf {1}$ and $\mathsf {live}(P)$ then $\exists Q$ such that $P \xrightarrow {} Q$.

3 Embedding the Functional Layer in the Process Layer

Having introduced our type theory and showcased some of its informal expressiveness in terms of the ability to specify and statically verify true data dependent protocols, as well as the ability to prove properties of processes, we now develop a formal expressiveness result for our theory, showing that the process level type constructs are able to encode the dependently-typed functional layer, faithfully preserving type dependencies.

Specifically, we show that (1) the type-level constructs in the functional layer can be represented by those in the process layer combined with the contextual monad type, and (2) all term level constructs can be represented by session-typed processes that exchange monadic values. Thus, we show that both $\lambda$-abstraction and application can be eliminated while still preserving non-trivial type dependencies. Crucially, we note that the monadic construct cannot be fully eliminated due to the cross-layer nature of session type dependencies: In the process layer, simply-kinded dependent types (i.e. types with kind $\mathsf {stype}$) are of the form $\forall x{:}\tau .A$ where $\tau$ is of kind $\mathsf {type}$ and A of kind $\mathsf {stype}$ (where x may occur). Operationally, such a session denotes an input of some term M of type $\tau$ with a continuation of type $A\{M/x\}$. Thus, to faithfully encode type dependencies we cannot represent such a type with a non-dependently typed input (e.g. a type of the form $A \multimap B$).

3.1 The Embedding

A first attempt. Given the observation above, a seemingly reasonable option would be to attempt an encoding that maintains monadic objects solely at the level of type indices and then exploits Girard’s encoding [9] of function types $\tau \rightarrow \sigma$ as ${{!}}{\!\!\llbracket }\tau {\rrbracket \!\!}\rightarrow {\!\!\llbracket }\sigma {\rrbracket \!\!}$, which is adequate for session-typed processes [28]. Thus a candidate encoding for the type $\varPi x{:}\tau .\sigma$ would be $\forall x{:}\{{\!\!\llbracket }\tau {\rrbracket \!\!}\}. {{!}} {\!\!\llbracket }\tau {\rrbracket \!\!}\multimap {\!\!\llbracket }\sigma {\rrbracket \!\!}$, where ${\!\!\llbracket }{-}{\rrbracket \!\!}$ denotes our encoding on types. If we then consider the encoding at the level of terms, typing dictates the following (we write ${\!\!\llbracket }M {\rrbracket \!\!}_z$ for the process encoding of $M : \tau$, where z is the session channel along which one may observe the “result” of the encoding, typed with ${\!\!\llbracket }\tau {\rrbracket \!\!}$):

$$\begin{aligned} \begin{array}{lcl} {\!\!\llbracket }\lambda x{:}\tau . M {\rrbracket \!\!}_z &{} \triangleq &{} z(x).z(x').{\!\!\llbracket }M{\rrbracket \!\!}_z \\ {\!\!\llbracket }M\, N{\rrbracket \!\!}_z &{} \triangleq &{} ({\varvec{\nu }}x)({\!\!\llbracket }M {\rrbracket \!\!}_x \mid x\langle \{{\!\!\llbracket }N{\rrbracket \!\!}_y\}\rangle .\overline{x}\langle x'\rangle .({!}x'(y).{\!\!\llbracket }N{\rrbracket \!\!}_y \mid [x\leftrightarrow z])\\ \end{array} \end{aligned}$$

However, this candidate encoding breaks down once we consider definitional equality. Specifically, compositionality (i.e. the relationship between ${\!\!\llbracket }M\{N/x\}{\rrbracket \!\!}_z$ and the encoding of N substituted in that of M) requires us to relate ${\!\!\llbracket }M\{N/x\}{\rrbracket \!\!}_z$ with $({\varvec{\nu }}x)({\!\!\llbracket }M {\rrbracket \!\!}_z\{\{{\!\!\llbracket }N{\rrbracket \!\!}_y\}/x\} \mid {!}x'(y).{\!\!\llbracket }N{\rrbracket \!\!}_y)$, which relies on reasoning up-to observational equivalence of processes, a much stronger relation than our notion of definitional equality. Therefore it is fundamentally impossible for such an encoding to preserve our definitional equality, and thus it cannot preserve typing in the general case.

A faithful embedding. We now develop our embedding of the functional layer into the process layer which is compatible with definitional equality. Our target calculus is reminiscent of a higher-order (in the sense of higher-order processes [23]) session calculus [19]. Our encoding ${\!\!\llbracket }{-}{\rrbracket \!\!}$ is inductively defined on kinds, types, session types, terms and processes. As usual in process encodings of the $\lambda$-calculus, the encoding of a term M is indexed by a result channel z, written ${\!\!\llbracket }M {\rrbracket \!\!}_z$, where the behaviour of M may be observed.

Fig. 7.

An embedding of dependent functions into processes

The embedding is presented in Fig. 7, noting that the encoding extends straightforwardly to typing contexts, where functional contexts $\varPsi , x{:}\tau$ are mapped to $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\},x{:}\{{\!\!\llbracket }\tau {\rrbracket \!\!}\}$. The mapping of base kinds is straightforward. Dependent kinds $\varPi x{:}\tau .K$ rely on the monad for well-formedness and are encoded as (session) kinds of the form $\varPi x{:}\{{\!\!\llbracket }\tau {\rrbracket \!\!}\}.{\!\!\llbracket }K {\rrbracket \!\!}$. The higher-kinded types in the functional layer are translated to the corresponding type-level constructs of the process layer where all objects that must be $\mathsf {type}$-kinded rely on the monad to satisfy this constraint. For instance, $\lambda x{:}\tau .\sigma$ is mapped to the session-type abstraction $\lambda x{:}\{{\!\!\llbracket }\tau {\rrbracket \!\!}\}.{\!\!\llbracket }\sigma {\rrbracket \!\!}$ and the type-level application $\tau \,M$ is translated to ${\!\!\llbracket }\tau {\rrbracket \!\!}\,\{{\!\!\llbracket }M{\rrbracket \!\!}_c\}$. Given the observation above on embedding the dependent function type $\varPi x{:}\tau .\sigma$, we translate it directly to $\forall x{:}\{{\!\!\llbracket }\tau {\rrbracket \!\!}\}.{\!\!\llbracket }\sigma {\rrbracket \!\!}$, that is, functions from $\tau$ to $\sigma$ are mapped to sessions that input processes implementing ${\!\!\llbracket }\tau {\rrbracket \!\!}$ and then behave as ${\!\!\llbracket }\sigma {\rrbracket \!\!}$ accordingly. The encoding for monadic types simply realises the contextual nature of the monad by performing a sequence of inputs of the appropriate types (with the shared sessions being of ${!}$ type).

The mutually dependent nature of the framework requires us to extend the mapping to the process layer. Session types are mapped homomorphically (e.g. ${\!\!\llbracket }A \multimap B {\rrbracket \!\!}\triangleq {\!\!\llbracket }A {\rrbracket \!\!}\multimap {\!\!\llbracket }B {\rrbracket \!\!}$) with the exception of dependent inputs and outputs which rely on the monad, similarly for type-level functions and application.

The encoding of $\lambda$-terms is guided by the embedding for types: the abstraction $\lambda x{:}\tau .M$ is mapped to an input of a term of type $\{{\!\!\llbracket }\tau {\rrbracket \!\!}\}$ with continuation ${\!\!\llbracket }M{\rrbracket \!\!}_z$; application $M\,N$ is mapped to the composition of the encoding of M on a fresh name x with the corresponding output of $\{{\!\!\llbracket }N {\rrbracket \!\!}_y\}$, which is then forwarded to the result channel z; monadic expressions are translated to the appropriate sequence of inputs, as dictated by the translation of the monadic type; and, the translation of variables makes use of the monadic elimination form (since the encoding enforces variables to always be of monadic type) combined with forwarding to the appropriate result channel.

The mapping for processes is mostly homomorphic, using the monad constructor as needed. The only significant exception is the encoding for monadic elimination which must provide the encoded monadic term ${\!\!\llbracket }M{\rrbracket \!\!}_c$ with the necessary channels. Since the session calculus does not support communication of free names this is achieved by a sequence of outputs of fresh names combined with forwarding of the appropriate channel. To account for replicated sessions we must first trigger the replication via an output which is then forwarded accordingly.

We can illustrate our encoding via a simple example of an encoded function (we omit type annotations for conciseness):

$$\begin{aligned} \begin{array}{l} {\!\!\llbracket }(\lambda x.x)\,(\lambda x.\lambda y.y){\rrbracket \!\!}_z = ({\varvec{\nu }}c)({\!\!\llbracket }\lambda x.x {\rrbracket \!\!}_c \mid c\langle \{ {\!\!\llbracket }\lambda x.\lambda y.y {\rrbracket \!\!}_w \} \rangle .[c\leftrightarrow z]) \\ =\,({\varvec{\nu }}c)(c(x).y\leftarrow x;[y\leftrightarrow c] \mid c\langle \{w(x).w(y).d\leftarrow y;[d\leftrightarrow w]\}\rangle .[c\leftrightarrow z])\\ \xrightarrow {}^+ z(x).z(y).d\leftarrow y;[d\leftrightarrow z] \ = \ {\!\!\llbracket }\lambda x.\lambda y.y{\rrbracket \!\!}_z \end{array} \end{aligned}$$

3.2 Properties of the Embedding

We now state the key properties satisfied by our embedding, ultimately resulting in type preservation and operational correspondence. For conciseness, in the statements below we list only the cases for terms and processes, omitting those for types and kinds (see [32]). The key property that is needed is a notion of compositionality, which unlike in the sketch above no longer falls outside of definitional equality.

Lemma 3.1

(Compositionality)

• 1. $\varPsi ; \varGamma ; \varDelta \vdash {\!\!\llbracket }M \{N/x\}{\rrbracket \!\!}_z = {\!\!\llbracket }M{\rrbracket \!\!}_z\{\{{\!\!\llbracket }N {\rrbracket \!\!}_y\}/x\}\,{::}\, z{:}{\!\!\llbracket }A\{N/x\}{\rrbracket \!\!}$

• 2. $\varPsi ; \varGamma ; \varDelta \vdash {\!\!\llbracket }P\{M/x\}{\rrbracket \!\!}\,{::}\,z{:}{\!\!\llbracket }A \{M/x\}{\rrbracket \!\!}$ iff $\varPsi ; \varGamma ; \varDelta \vdash {\!\!\llbracket }P {\rrbracket \!\!}\{\{{\!\!\llbracket }M {\rrbracket \!\!}_c\}/x\}\,{::} \,z{:}{\!\!\llbracket }A {\rrbracket \!\!}$$\{\{{\!\!\llbracket }M {\rrbracket \!\!}_c\}/x\}$.

Given the dependently typed nature of the framework, establishing the key properties of the encoding must be done simultaneously (relying on some auxiliary results – see [32]).

Theorem 3.2

(Preservation of Equality)

• 1. If $\varPsi \vdash M = N : \tau$ then $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ; \cdot ; \cdot \vdash {\!\!\llbracket }M {\rrbracket \!\!}_z = {\!\!\llbracket }N {\rrbracket \!\!}_z\,{::}\,z{:}{\!\!\llbracket }\tau {\rrbracket \!\!}$

• 2. If $\varPsi ; \varGamma ; \varDelta \vdash P = Q\,{::}\,z{:}A$ then $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ; {\!\!\llbracket }\varGamma {\rrbracket \!\!}; {\!\!\llbracket }\varDelta {\rrbracket \!\!}\vdash {\!\!\llbracket }P {\rrbracket \!\!}= {\!\!\llbracket }Q{\rrbracket \!\!}\,{::}\, z{:}{\!\!\llbracket }A {\rrbracket \!\!}$.

Theorem 3.3

(Preservation of Typing)

• 1. If $\varPsi \vdash M : \tau$ then $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ; \cdot ; \cdot \vdash {\!\!\llbracket }M {\rrbracket \!\!}_z\,{::}\,z{:}{\!\!\llbracket }\tau {\rrbracket \!\!}$

• 2. If $\varPsi ; \varGamma ; \varDelta \vdash P\,{::}\,z{:}A$ then $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ; {\!\!\llbracket }\varGamma {\rrbracket \!\!}; {\!\!\llbracket }\varDelta {\rrbracket \!\!}\vdash {\!\!\llbracket }P{\rrbracket \!\!}\,{::}\,z{:}{\!\!\llbracket }A {\rrbracket \!\!}$.

Theorem 3.4

(Operational Correspondence). If $\varPsi ; \varGamma ; \varDelta \vdash P\,{::}\, z{:}A$ and $\varPsi \vdash M : \tau$ then:

• 1. (a) If $P \xrightarrow {} P'$ then ${\!\!\llbracket }P {\rrbracket \!\!}\xrightarrow {}^+ Q$ with $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ; {\!\!\llbracket }\varGamma {\rrbracket \!\!}; {\!\!\llbracket }\varDelta {\rrbracket \!\!}\vdash Q = {\!\!\llbracket }P'{\rrbracket \!\!}\,{::}\,z{:}{\!\!\llbracket }A{\rrbracket \!\!}$ and

  (b) if ${\!\!\llbracket }P{\rrbracket \!\!}\xrightarrow {} P'$ then $P \xrightarrow {}^+ Q$ with $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ; {\!\!\llbracket }\varGamma {\rrbracket \!\!}; {\!\!\llbracket }\varDelta {\rrbracket \!\!}\vdash P' = {\!\!\llbracket }Q{\rrbracket \!\!}\,{::}\,z{:}{\!\!\llbracket }A{\rrbracket \!\!}$

• 2. (a) If $M \xrightarrow {} M'$ then ${\!\!\llbracket }M {\rrbracket \!\!}_z \xrightarrow {}^+ N$ with $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ; \cdot ; \cdot \vdash N = {\!\!\llbracket }M '{\rrbracket \!\!}_z\,{::}\,z{:}{\!\!\llbracket }\tau {\rrbracket \!\!}$ and

  (b) if ${\!\!\llbracket }M {\rrbracket \!\!}_z \xrightarrow {} P$ then $M \xrightarrow {} N$ with $\{{\!\!\llbracket }\varPsi {\rrbracket \!\!}\} ;\cdot ;\cdot \vdash {\!\!\llbracket }N {{\rrbracket \!\!}_{z}} = P\,{::}\,z{:}{\!\!\llbracket }\tau {\rrbracket \!\!}$.

In Theorem 3.4, (a) is commonly referred to as operational completeness, with (b) establishing soundness. As exemplified above, our encoding satisfies a very precise operational correspondence with the original $\lambda$-terms.

4 Related and Future Work

Enriching Session Types via Type Structure. Exploiting the linear logical foundations of session types, [25] considers a form of value dependencies where session types can state properties of exchanged data values, while the work [29] introduces the contextual monad in a simply-typed setting. Our development not only subsumes these two works, but goes beyond simple value dependencies by extending to a richer type structure and integrating dependencies with the contextual monad. Recently, [1] considers a non-conservative extension of linear logic-based session types with sharing, allowing true non-determinism. Their work includes dependent quantifications with shared channels, but their type syntax does not include free type variables, so the actual type dependencies do not arise (see [1, 37:8]). Thus none of the examples in this paper can be represented in [1]. The work [16] studies gradual session types. To the best of our knowledge, the main example in [1, Sect. 2] is statically representable in our framework as in the example of Sect. 1, where protocol actions depend on values that are communicated (or passed as function arguments).

In the context of multiparty session types, the theory of multiparty indexed session types is studied in [7], and implemented in a protocol description language [20]. The main aim of these works is to use indexed types to represent an arbitrary number of session participants. The work [31] extends [25] to multiparty sessions in order to treat value dependency across multiple participants. Extending our framework to multiparty [15] or non-logic based session types [14] is an interesting future topic.

Combining Linear and Dependent Types. Many works have studied the various challenges of integrating linearity in dependent functional type theories. We focus on the most closely related works. The work [6] introduced the Linear Logical Framework (LLF), integrating linearity with the LF [11] type theory, which was later extended to the Concurrent Logical Framework (CLF) [33], accounting for further linear connectives. Their theory is representable in our framework through the contextual monad (encompassing full intuitionistic linear logic), depending on linearly-typed processes that can express dependently typed functions (Sect. 3).

The work of [17] integrates linearity with type dependencies by extending LNL [2]. Their work is aimed at reasoning about imperative programs using a form of Hoare triples, requiring features that we do not study in this work such has proof irrelevance and computationally irrelevant quantification. Formally, their type theory is extensional which introduces significant technical differences from our intensional type theory, such as a realisability model in the style of NuPRL [10] to establish consistency.

Recently, [8] proposed an extension of LLF with first-class contexts (which may contain both linear and unrestricted hypotheses). While the contextual aspects of their theory are reminiscent of our contextual monad, their framework differs significantly from ours, since it is designed to enable higher-order abstract syntax (commonplace in the LF family of type theories), focusing on a type system for canonical LF objects with a meta-language that includes contexts and context manipulation. They do not consider additives since their integration with first-class contexts can break canonicity.

While none of the above works considers processes as primitive, their techniques should be useful for, e.g. developing algorithmic type-checking and integrating inductive and coinductive session types based on [18, 26, 30].

Dependent Types and Higher-Order $\pi$-calculus. The work [35] studies a form of dependent types where the type of processes takes the form of a mapping $\varDelta$ from channels x to channel types T representing an interface of process P. The dependency is specified as $\varPi (x{:}T)\varDelta$, representing a channel abstraction of the environment. This notion is extended to an existential channel dependency type $\varSigma (x{:}T)\varDelta$ to address fresh name creation [13, 34]. Combining our process monad with dependent types can be regarded as an “interface” which describes explicit channel usages for processes. The main differences are (1) our dependent types are more general, treating full dependent families including terms and processes in types, while [13, 34, 35] study only channel dependency to environments (i.e. neither terms nor processes appear in types, only channels); and (2) our calculus emits only fresh names, not needing to handle the complex scoping mechanism treated in [13, 34]. In this sense, the process monad provides an elegant framework to handle higher-order computations and assign non-trivial types to processes.