We study the operational semantics of an untyped computational lambda calculus whose normal forms represent queries on databases. The calculus extends the computational core with additional operations and rewriting rules whose efect is to turn the monadic type of computations into a multiset monad that captures tables. Moreover, we introduce comonadic constructs and additional rewriting rules to be able to form tables of tables. Proving confluence becomes tricky: we succeed exploiting decreasing diagrams. In the second part, we study a Curry style type assignment system for the calculus. We introduce an idempotent intersection type system establishing type invariance under conversion.
add two more co-monadic constructs to reflect computations into values, following ideas
by [
The calculus we are going to introduce takes inspiration from the (untyped) NRC
calculus [
Because of the important application to databases, from now on we call our extension of the ©-calculus the -calculus.
Intersection Types were introduced by Coppo and Dezani-Ciancaglini in the late 70’s
[
In the same way that simple types guarantee termination, intersection types do the same. However, they also characterize termination, that is, they type all terminating -terms. Intersection types have also a very elegant semantic flavour, since they may be seen as a syntactic presentation of denotational models. Notwithstanding, here we do not delve into the denotational semantics of the calculus, and keep the treatment at the syntactical level. In fact, intersection types have shown to be remarkably flexible, since diferent termination forms can be characterized by tuning details of the type system ( e.g., weak/strong normalization, head/weak/call-by-value evaluation). In the present work, we introduce an idempotent intersection type discipline and prove it enjoys the subject convertibility, i.e., the type is preserved not only by reduction, but also by expansion. This is the key property to reach the soundness and completeness results of the type system with respect to termination.
To get an account of the history and expressivity of intersection types, see for example
the recent survey by Bono and Dezani-Ciancaglini [
Contributions. The first contribution of the work is the design of the -calculus
in Section 2, which goes beyond the mere efort to fit the NRC into a well-assessed
monadic frame. Indeed, this can be considered as an experiment of extending © with
algebraic operators (other cases are [
The second contribution, treated in Section 3, is the proof of a fundamental property
of the calculus: confluence. The proof is labour-intensive because the rewriting rules
associated to algebraicity of the operators turn them into control operators: each operator
can capture its context and then erase or duplicate it, and many critical pairs arise.
Moreover, there is also the issue of the interplay between the equational theory and the
rewriting theory. Technically, we make strong use of van Oostrom’s decreasing diagram
technique [
Section 4 is devoted to the third contribution: an idempotent, monadic, intersection types assignment system, proved to enjoy subject convertibility. The intersection type theory we present is monadic version of strict intersection types in the case the monad into account is the multiset monad equipped with the possibility of reflect and reify types. This contribution can be seen as a first step to characterize convergent terms of the calculus and as a first move in obtaining a resource-aware type system for the calculus into consideration.
Future work and related ones are discussed in Section 5.
relation are reported below: Definition 2.1 (Term syntax).
The syntax of the untyped computational SQL -calculus, shortly , and its reduction
Val : , Com : , ::= | . ::= [ ] | ⋆ | ⟨⟨ ⟩⟩ | ⊎ | ∅ | ! Like in ©, terms are of either sorts Val and Com, representing values and computations, respectively. Variables , abstractions . — where is bound in — and the constructors [ ] and ⋆ , written return and »= in Haskell-like syntax, respectively, form the syntax of ©, which is agnostic on the interpretation of computations. In
, instead, computations are meant to be understood as tables, i.e., multisets of values, and therefore [ ] is interpreted as the singleton whose only element is and ⋆ as the bind operator of the multiset monad. The binary and 0-ary operators ⊎ and ∅ are additionally used to construct tables. The pair of constructs ⟨⟨·⟩⟩ and ! are used to reflect computations into labels, allowing to form tables of (reflected) tables. Note that bound variables so that the capture avoiding substitution ⟨⟨·⟩⟩ can be understood as the unit of a comonad. Terms are identified up to renaming of { / } is always well defined;
( ) denotes the set of free variables in . Finally, like in ©, application among computations can be encoded by (. ⋆
), where is fresh.
≡ ⋆ Wrapping up, the syntax can be condensed in the motto:
SQL ≈ © + operations over tables + monadic reification/reflection with the latter extension being orthogonal to the second one.
We are now in place to introduce the reduction relation, later closed under contexts: Definition 2.2 (Reduction). The reduction relation is the union of the following binary relations over Com: ) ⊎ ) ⊎ ) ∅1) ∅2)
!) ) ( ⋆ . ( ⋆ .
[ ] ⋆ .
The first two rules, taken from ©, are oriented monadic equations. The next two rules capture algebraicity of the ⊎ operator, but only w.r.t. contexts made of ⋆ only (e.g., there is no rule ( ⊎ ) ⊎ ↦→ ( ⊎ ) ⊎ ( ⊎ ) because that would be unsound for
the contextual closure of SQL under computational contexts, where such contexts are mutually defined with value contexts as follows:
V ::= ⟨·Val⟩ | .
C | ⟨⟨C⟩⟩ C ::= ⟨·Com⟩ | [V] | C ⋆ | ⋆
Value Contexts V | C ⊎ | ⊎ C | !V
Computation Contexts Notice that the hole of each kind of context has to be filled in with a proper kind of term.
We equip the calculus with a sound, but not complete, equational theory for multisets,
taken from [
Definition 2.3 (Equational theory ).
) ) ⊎ ∅ ⊎ ∅ = = ∅ ⊎
The exact choice of rewriting and equational rules that we pick seems rather arbitrary
at first: the empty set is not the neutral element of
⊎ and the monadic operations are not
forced to be completely algebraic (e.g., ⊎ does not commute with contexts that include
thunks or force). This choice was made in order to keep the calculus as close as possible
to the reference NRC calculus in [
postponed.
We modularize the proof of confluence by first showing that the equational part can be Getting rid of the equational theory. A classic tool to modularize a proof of confluence is Hindley-Rosen lemma, stating that the union of confluent reductions is itself confluent if they all commute with each other. Let us first define what commutation between a reduction relation and an equational theory means, and then state that result properly. Definition 3.1. Given a reduction relation →− and an equational theory = , we say that →− commutes over = if for all , , such that = →− , there exists such that →− = .
Lemma 3.2 (Hindley-Rosen). Let ℛ 1 and ℛ 2 be relations on the set . If ℛ 1 and ℛ 2 are confluent and commute with each other, then ℛ 1 ∪ ℛ 2 is confluent.
We will exploit that to focus just on the reduction relation while proving confluence. Lemma 3.3. = commutes with →−.
Hence, by Lemma 3.3 one needs just the confluence of
→− modulo .
→− to assert the confluence of
Remark 3.4. One can be also interested in the modulo confluence, which is in general
diferent from the confluence modulo (see ch. 14 of [
Decreasing diagram. Now that is possible to omit the equational theory induced by
Definition 2.3, we need to prove the commutation of all the reduction rules, and in
this intent, we use decreasing diagrams by van Oostrom [
exist a presentation (, {→− } ∈ ) of ℛ and a well-founded strict order > on such that: ← · → ⊆ ←∨*→ · −→= · ∨←{*→} · ←=− · ←∨*→ , where ∨¯ = { ∈ | ∃ ∈ ¯. > }, ∨ abbreviates ∨{ }, and →−* (resp. ←*→ ) and −→= (resp. ←=→ ) are the transitive and reflexive closures of the relation →− (resp. ↔).
Let us give a hint about the above definition. The property of decreasiness is stated for relations, seen as a family of labelled binary relations. Such labels are equipped with a well-founded, strict, order such that every peak can be rejoined in a particular way, regulated by that specific order on labels.
The following theorem, due to van Oostrom, states that decreasiness implies confluence. confluent.
Theorem 3.6 (van Oostrom [
In [
Now the point is to find a proper labelling and a strict order on that labelling that satisfies the property of decreasiness. If one considers diagrams involving as labels of potential labellings. Consider, for instance, the following diagram: rules of ⊎ or ⊎ vs. ∅1 and ∅2, it is easy to perceive how these rules should be ordered ( 1 ⊎ 2) ⋆ . ∅ - ( 1 ⋆ . ∅) ⊎ ( 2 ⋆ . ∅
) ⊎ ∅ ∅ 2 2 2 ∅ (( 1 ⊎ 2) ⋆ .
order over labels we are searching for (read it as: these rules can always be postponed at the end of a reduction sequence). .
. ( ⋆ . Indeed,
)). where ¯1 = (( 1 ⋆ . ) ⊎ ( 2 ⋆ . ), ¯2 = ( 1 ⋆ . )) ⊎ ( 2 ⋆
The case for vs ⊎ , however, shows the need for a non-trivial approach, since depending on which context the rules are applied, we need either > ⊎ or < ⊎ . ⊎ · )) ⋆ . 2 - ( 1 ⊎ 2) ⋆ .
The case for ⊎ vs. ⊎ can seem innocent, for example: ( 1 ⊎ 2) ⋆ . ( 1 ⊎ 2)
- ( 1 ⋆ . ( 1 ⊎ 2)) ⊎ ( 2 ⋆ . ( 1 ⊎ 2)) ⊎
? 1) ⊎ (( 1 ⊎ 2) ⋆ . 2) ⊎ 2 ⊎ (( 1 ⊎ 2) ⋆ . where ¯ ≡ ( 1 ⋆ . ( 1 ⋆ . 1) ⊎ ( 1 ⋆ . 1) ⊎ ( 2 ⋆ . 2) ⊎ ( 2 ⋆ . 1) ⊎ ( 1 ⋆ . 1) ⊎ ( 2 ⋆ . ⊎ 2
? - ¯ = ^ 2) ⊎ ( 2 ⋆ . 2) 2) and ^ ≡ Remark 3.7. Actually, for more complex terms the diagram is not so elegant. Consider for example the term ≡ ( 1 ⊎ 2) ⋆ (( 1 ⊎ 2) ⊎ 3). If one is seeking a modular proof of confluence, it is possible to consider the rewriting system made by just the rules ⊎ and ⊎ . Both together are weakly Church-Rosser (provable by easy induction) and terminating (since the number of ⊎ symbols in a term is finite), thus by Newman’s Lemma, the rewrite system is Church-Rosser. By the way, we are searching for the right application of van Oostrom’s decreasing diagram, hence we are to introduce a generalized version of ⊎ and ⊎ , respectively.
follows
Gen ⊎ ) (. . . ( 1 ⊎ 2) ⊎ . . . ⊎ ) ⋆ . ↦→Gen⊎
Gen ⊎ ) ⋆ . (. . . ( 1 ⊎ 2) ⊎ . . . ⊎ ) ↦→Gen⊎
( ⋆ .
( ⋆ .
) ⊎ ( 2 ⋆ .
1) ⊎ ( ⋆ .
) ⊎ . . . ⊎ ( ⋆ .
2) ⊎ . . . ⊎ ( ⋆ .
)
)
Multi-reduction. The confluence proof we are going to sketch avoids the issue with vs.
⊎ reported above by considering multiple reductions. Roughly speaking, this means that
we consider a labelling that comprehends reduction rules that can perform simultaneously
in many ’parts’ of the term, called formally positions. For a fair formalization of these
basic notions of rewriting theory, please see, e.g., [
A parallel rewrite step is a sequence of reductions at a set of parallel positions, ensuring that the result does not depend upon a particular sequentialization of . Given a reduction step we define its parallel version as Par .
We are now ready to state our main result: Theorem 3.9 (Confluence) .
is confluent.
Proof sketch. 1. All reduction rules strongly commute with !: proved by tedious inspection of all cases. 2. Under the following order for parallel rewriting steps, all remaining rules are decreasing as well: also proved by tedious inspection of all cases.
Par > Par >
ParGen⊎ > ParGen⊎ > ∅1 > ∅2
E.g., ∅ ∅1← ∅ ⋆ . ⊎ →−⊎ →−2∅1 ∅ ⊎ ∅.
3. Confluence is obtained combining the previous points with Lemma 3.3 and
Theorem 3.6, following [
Intersection types are an extension of Curry’s simple type assignment system to untyped
-terms, obtained by adding new types ∧ ′ to be assigned to terms that have both type
and ′. Intersection type assignment systems form a whole family in the literature; see
[
In building an intersection type discipline for , we actually do not extend the
system in [
Definition 4.1 (Intersection Types Syntax). Let range over a countable set of type variables (the atoms); then we define three sorts of types by mutual induction as follows:
ValType : ComType : BlindType : ::=
∧∅ →− ::= | → | ⋀︀ ≥0 | ⟨⟨ ⟩⟩ (value types) ::= [ ] | ∅^ | ⊎ (computation types) (blind types)
the symbol for an empty union. As for the terms, we equip computational types in Definition 4.1 with an equational theory stating the commutativity of union and the idempotency of the emptyset type ∅^ w.r.t. the union of types. We then introduce for all the computational types a boolean predicate emptyin( ), that is true if and only if ∅^ ∈ . In such a way, we can speak of canonical form of computational types for SQL: it is easy to see that for every ∈ ComType there exists a canonical form (up to commutativity of union) ⨄︀ ≥0[ ] ⊎ ∅^ if emptyin( ), or ⨄︀ > 0[ ], otherwise. These forms will be used in type assignment systems to clarify and handle generic computational types when needed.
system for .
We are now in place to introduce the type assignment Definition 4.2 (Type assignment). A basis is a finite set of typings Γ = { 1 : 1, . . . : } with pairwise distinct variables , whose domain is the set (Γ) = { 1, . . . , }. A basis determines a function from variables to types such that Γ( ) = if : ∈ Γ, Γ( ) is the empty intersection ∧∅, otherwise.
A judgment is an expression of either shapes: Γ ⊢ : or Γ ⊢ : . It is derivable if it is the conclusion of a derivation according to the rules in Figure 1.
The blind types to which we are taking inspiration are the ones presented by Kesner et al. in [23, 25] to grant strong normalization even in the presence of terms whose occurrences will all be erased during computation. The intersection types discipline assigns to terms being erased ∧∅ and therefore the terms would not be typed, not capturing their divergence. Instead, we type them with a blind type, which states that the term will not receive at runtime any input to be used and it can return any output. : ∈ Γ Γ ⊢ :
(Ax) Γ ⊢ : Γ ⊢ ⟨⟨ ⟩⟩ : ⟨⟨ ⟩⟩
Γ ⊢ : Γ ⊢ .
: Γ( ) →− (Γ ⊢ : ) =1,..., Γ ⊢ : ︁⋀
The union operator for types is introduced just for computations as regulated in rule (⊎ I). The introduction of bind is split in two, depending on the cases in which the type associated with the computation is just an empty union type or not. In fact, in the case of (⋆∅ I) we explicitly ask for the value to have an empty intersection to deal with the case the computation has just the empty union type. The rule (⋆ I), instead, takes care of the case in which the computation has non empty union type ( is strictly greater than 0) and possibly the empty union type (this is the meaning of ⨄︀ case, the empty union type, if it is in the premise, is propagated to the resulting type. ≤1 ∅^ ); in such a
We are now in place to state the main results of the presented type system.
→− , then Γ ⊢ : . →− , then Γ ⊢ : .
The above theorems state two results: the first is the subject reduction, a desirable property for all type systems. The second property, the subject expansion, on the other hand, is typical of intersection types and the key to proving characterisation results. This property, indeed, states that the type of a term is preserved even going backwards in its reduction.
In the present work, we have introduced a computational -calculus SQL as an extension of
the computational core © [
We leave for future works the full characterization of convergent terms, via soundness and completeness of the type system, plus a deep investigation on the semantical level via a filter model construction as in [26].
Related works. As mentioned in the Introduction, SQL stems from NRC calculus in [
In designing our type system, we were deeply influenced by the desire to reach a
quantitative type system for SQL, and in doing so we took inspiration from [
We find that our calculus and type system have substantial connections with dependent
type systems, even if not yet explored in detail. This is the case with the intuition
borrowed from [
Long-term perspectives. Considering the structure of the present work, we set two long-term goals. The first is related to the confluence proof based on decreasing diagrams in Section 3, since the labelling extracts an order over reduction rules to design a well-behaved normalizing strategy.
Concerning the type system, our idempotent intersection type one is just a mid-term objective, since we are interested in defining an appropriate intersection type system based on tight multi-types [28] to capture quantitatively the set of terminating queries according to strategy extracted from the confluence proof. Such non-idempotent type systems have been proven to be useful in detecting the length of normalizing reductions and the size of the normal forms, which in our case is the size of the computed SQL queries, via the type system itself. As a result, extending such non-idempotent intersection type disciplines for should capture even more quantitative, computational information about the queries themselves.
We would like to thank th reviewers for taking the necessary time and efort to review the manuscript. We sincerely appreciate all your valuable comments and suggestions, which helped us in improving the quality of the manuscript. [23] D. Kesner, P. Vial, Consuming and persistent types for classical logic, in: H. Hermanns, L. Zhang, N. Kobayashi, D. Miller (Eds.), LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, ACM, 2020, pp. 619–632. URL: https://doi.org/10.1145/3373718.3394774. doi:10.1145/3373718.3394774. [24] D. Kesner, A. Viso, Encoding tight typing in a unified framework, in: F. Manea, A. Simpson (Eds.), 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, pp. 27:1–27:20. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.27. doi:10.4230/LIPIcs.CSL.2022. 27. [25] D. Kesner, P. Vial, Non-idempotent types for classical calculi in natural deduction style, Log. Methods Comput. Sci. 16 (2020). URL: https://doi.org/10.23638/ LMCS-16(1:3)2020. doi:10.23638/LMCS-16(1:3)2020. [26] U. de’Liguoro, R. Treglia, From semantics to types: The case of the imperative -calculus, Theor. Comput. Sci. 973 (2023) 114082. URL: https://doi.org/10.1016/j. tcs.2023.114082. doi:10.1016/j.tcs.2023.114082. [27] U. D. Lago, M. Gaboardi, Linear dependent types and relative completeness, Log.
Methods Comput. Sci. 8 (2011). URL: https://doi.org/10.2168/LMCS-8(4:11)2012. doi:10.2168/LMCS-8(4:11)2012. [28] B. Accattoli, S. Graham-Lengrand, D. Kesner, Tight typings and split bounds, fully developed, J. Funct. Program. 30 (2020) e14. URL: https://doi.org/10.1017/ S095679682000012X. doi:10.1017/S095679682000012X.