Keywords

figure a

1 Introduction

The correct usage of resources is at the heart of many programs, especially if they control safety-critical machinery. Such resources can take many different forms: ensuring that file handles are not arbitrarily duplicated or discarded (as captured by linear and uniqueness types) [11, 25, 40], or guaranteeing that communication happens according to protocols (as specified by session types) [30, 70], or controlling how data is laid out in memory (as in Hoare and separation logics) [2, 34, 56, 64], or assuring that resources are correctly finalised [1, 43].

In contrast to the above approaches that predominantly focus on how resources are used, we study how to modularly specify and verify when programs can use their resources—we call such resources temporal. For instance, consider the following code snippet controlling a robot arm on a (car) production line:

figure b

Here, the correct execution of the program (and thus operation of the robot arm it is controlling) relies on the car parts given enough time to dry between painting and assembly. Therefore, in its current form, the above code is correct only if a compiler (or a scheduler) inserts enough of a time delay at compile time (resp. dynamically blocks program’s execution for enough time) between the calls to \(\textsf{paint}\) and \(\textsf{assemble}\). However, in either case, one still faces the question of how to reason about the correctness of the compiled code (resp. dynamic checks).

In this paper, we focus on developing a type system based means for reasoning about the temporal correctness of the code that the above-mentioned compiler might produce, or that a programmer might write directly when full control of the code is important. In particular, we had three desiderata we set out to fulfil:

  1. 1.

    We did not want the delay between \(\textsf{paint}\) and \(\textsf{assemble}\) to be limited to just blocking execution, with the robot sitting idly while watching paint dry. Instead, we wanted a flexible formalism that would allow the robot to spend that time doing other useful work, while ensuring that enough time passes.

  2. 2.

    We wanted the passage of time of program execution to be modelled within the type system, rather than being left to some unspecified meta-level run-time.

  3. 3.

    We wanted the resulting language to give programmers the freedom to redefine the behaviour of operations such as \(\textsf{paint}\) and \(\textsf{assemble}\), say, via effect handling [61], while respecting the operations’ temporal specifications.

Paper Structure We achieve these goals by designing a mathematically natural core programming language for safe and correct programming with temporal resources: on the one hand, based on a time-graded, temporal variant of Fitch-style modal type systems [19, 27], and on the other hand, on graded monads [35, 51, 67].

We review modal types and discuss how we use them to capture temporal resources in §2. In §3, we present \(\lambda _{[\tau ]}\)—our modally typed, effectful, equationally presented core calculus for safe programming with temporal resources. We justify the design of \(\lambda _{[\tau ]}\) by giving it a mathematically natural sound denotational semantics in §4, based on graded monads and adjunctions between strong monoidal functors, including a concrete presheaf example. In §5, we briefly discuss a specialisation of \(\lambda _{[\tau ]}\) with equations for time delays. We review related work and remark on future work in §6, and conclude in §7. This paper is also accompanied by an online appendix (https://arxiv.org/abs/2210.07738) that presents further details of renamings and denotational semantics that we omit in §3 and §4.

For supplementary rigour, we have formalised the main results of §3 and §4 also in Agda [68], available at https://github.com/danelahman/temporal-resources/releases/tag/fossacs2023. Regrettably, it currently lacks (i) proofs of some auxiliary lemmas noted in Prop. 4 due to a bug in Agda where with-abstractions produce ill-typed terms,Footnote 1 and (ii) two laws of the presheaf model because unfolding of definitions produces unmanageably large terms for Agda.

2 Modal Types for Temporal Resources

We begin with an overview of (Fitch-style) modal type systems and how a time-graded variant of them naturally captures temporal aspects of resources.

2.1 (Fitch-Style) Modal Types

A modal type system extends the types of an underlying type system with new modal type formers,Footnote 2 e.g., , which states that the type is to be considered and reasoned about in a different mode compared to X, which can take many forms. For instance, in Kripke’s possible worlds semantics, means that values of type X are available in all future worlds [41]; in run-time code generation, the type captures generators of X-typed code [72]; and in asynchronous and distributed programming, the type specifies mobile X-typed values [3, 54, 63].

Many different approaches to presenting modal type systems have been developed, with one of the main culprits being the difficulty of getting the introduction rule for correct. Namely, bearing in mind Kripke’s possible worlds semantics, the introduction rule for must allow one to use only those hypotheses that also hold in all future worlds, while at the same time ensuring that the system still enjoys expected structural properties. Solutions to this problem have involved proving in a context containing only -types [62] (with a failure of structural properties in the naive approaches), or building a form of explicit substitutions into the introduction rule for to give the rule premise access to only -types [12], or incorporating the Kripke semantics in the type system by explicitly indexing types with worlds [66]—see [37] for an in-depth survey.

In this paper, we build on Fitch-style modal type systems [15, 19, 27, 48], where the typing rules for are given with respect to another modality, , that acts on contexts, resulting in a particularly pleasant type-theoretic presentation.

As an illustrative example, in a Fitch-style modal type system corresponding to the modal logic S4 (whose Kripke models require the order on worlds to be reflexive and transitive, thus also corresponding to natural properties of time), the typing rules for variables and the type have the following form:Footnote 3

figure p

Intuitively, the context modality creates a barrier in the premise of Shut so that only -typed variables can be used from \(\varGamma \) in t, achieving the above-mentioned correctness goal for the introduction rule of . Alternatively, in the context of Kripke’s possible worlds semantics, one can also read the occurrences of the modality as advancing the underlying world—in Shut, t in the premise is typed in some future world compared to where is typed at. This intuition will be useful to how we use a similar modality to capture the passage of time in \(\lambda _{[\tau ]}\). The context weakening \(\varGamma ,\varGamma '\) in Open ensures the admissibility of structural rules, and in the possible worlds reading, it intuitively expresses that if is available in some world, then X will be available in all possible future worlds.

2.2 Modal Types for Temporal Resources

Next, we give a high-level overview of how we use a time-graded variant of Fitch-style modal type systems to capture temporal properties of resources in \(\lambda _{[\tau ]}\). For this, we use the production line code snippet from §1 as a working example.

A Naive Approach Before turning to modal types, a naive solution to achieve the desired time delay would be for \(\textsf{paint}\) to return the required drying time and for the program to delay execution for that time duration, e.g., as expressed in

figure w

It is not difficult to see that we could generalise this solution to allow performing other useful activities while waiting for \(\tau _{\text {dry}}\) time to pass. So are we done and can we conclude the paper here? Well, no, because this solution puts all the burden for writing correct code on the shoulders of the programmer, with successful typechecking giving no additional guarantees that \(\tau _{\text {dry}}\) indeed will have passed.

A Temporal Resource Type Instead, inspired by Fitch-style modal type systems and Kripke’s possible worlds semantics of the -modality, we propose a temporal resource type, written \([ \tau ]\, X\), to specify that a value of type X will become available for use in at most \(\tau \) time units, or to put it differently, the boxed value of type X can be explicitly unboxed only when at least \(\tau \) time units have passed. Concretely, \([ \tau ]\, X\) is presented by the following two typing rules:

figure y

Above, \(\tau \)s are natural numbers that count discrete time moments, and \(Y \mathbin {!}\tau '\) is a type of computations returning Y-typed values and executing in \(\tau '\) time units.

Analogously to the context modality of Fitch-style modal type systems, we introduce a similar modality on contexts, written \(\langle \tau \rangle \), to express that when typechecking a term of the form \(\varGamma , \langle \tau \rangle \vdash V : X\), we can safely assume that at least \(\tau \) time will have passed before V is accessed or executed, as in the premise of the Box rule. Accordingly, in Unbox, we require that at least \(\tau \) time units have passed since the resource V of type \([ \tau ]\, X\) was created or brought into scope, by typing V in the “earlier” context \(\varGamma \mathbin {-}\tau \) (we define this operation in §3.3).

Encapsulating temporal resources as a type gives us flexible first-class access to them, and allows to pack them in data structures and pass them to functions.

Modelling Passage of Time As we see in the Unbox rule, we can unbox a temporal resource only when enough time has passed since its creation. This begs the question: How can the passage of time be modelled within the type system? For this, we propose a new notion of temporally aware graded algebraic effects, where each operation \(\textsf{op}\) is specified not only by its parameter and result types, but also by its prescribed execution time, and with \(\textsf{op}\)’s continuation knowing that \(\textsf{op}\)’s worth of additional time has passed before it begins executing. We refer the reader to [8, 31, 35, 60] for background on ordinary (graded) algebraic effects.

For instance, the \(\textsf{paint}\) operation, taking \(\tau _{\text {paint}}\) time, is typed in \(\lambda _{[\tau ]}\) asFootnote 4

figure aa

Here, \(\langle \tau _{\text {paint}} \rangle \) expresses that from the perspective of any es in M, an additional \(\tau _{\text {paint}}\) time will have passed compared to the beginning of the execution of \(\textsf{paint}\;V\; (x \,.\, M)\), which is typed in the “earlier” context \(\varGamma \). Also, observe that \(\textsf{paint}\)’s result x is available after \(\tau _{\text {paint}}\) time has passed (i.e., after \(\textsf{paint}\) finishes), and its type has the car part types wrapped as temporal resources, ensuring that any further operations (e.g., \(\textsf{assemble}\)) can access them only after at least \(\tau _{\text {dry}}\) time has passed after \(\textsf{paint}\) finishes. The \(\textsf{delay}\; \tau \) operation is typed analogously.

Finally, similarly to algebraic operations, we also use the context modality \(\langle \tau \rangle \) to model the passage of time in sequential composition, as specified in

figure ac

The type \(X \mathbin {!}\tau \) (for specifying the execution time of computations) is standard from graded monads style effect systems [35]. The novelty of our work is to use this effect information to inform continuations that they can safely assume that the given amount of additional time has passed before they start executing.

Putting It All Together We conclude this overview by revisiting the production line code snippet and note that in the \(\lambda _{[\tau ]}\)-calculus we can write it as

figure ad

Observe that apart from the operations, the code looks identical to the naive, unsafe solution discussed earlier. However, crucially, now any code that wants to use the outputs of \(\textsf{paint}\) will typecheck only if these resources are accessed after at least \(\tau _{\text {dry}}\) time units have passed after \(\textsf{paint}\) finishes. In the code snippet, this is achieved by blocking execution with \(\textsf{delay}\; \tau _{\text {dry}}\) for \(\tau _{\text {dry}}\) time units, but this could have been equally well achieved by executing other useful operations \(\textsf{op}_1 ;\; \ldots ;\; \textsf{op}_n\), as long as they collectively take at least \(\tau _{\text {dry}}\) time.

Fig. 1.
figure 1

Types of \(\lambda _{[\tau ]}\).

Full size image

3 A Calculus for Programming with Temporal Resources

We now recast the ideas explained above as a formal, modally typed, effectful core calculus, called \(\lambda _{[\tau ]}\). We base it on the fine-grain call-by-value \(\lambda \)-calculus [44].

3.1 Types

The types of \(\lambda _{[\tau ]}\) are given in Fig. 1. Ground types include base types \(\textsf{b}\), and are closed under finite products and the modal temporal resource type \([ \tau ]\, A\). The latter denotes that an A-typed value will become available in at most \(\tau \) time units, where \(\tau \in \mathbb {N}\) counts discrete time moments.Footnote 5 The ground types can also come with constants \(\textsf{f}\) with associated constant signatures \(\textsf{f} : (A_1,\ldots ,A_n) \rightarrow B\).

To model operations such as \(\textsf{paint}\) and \(\textsf{assemble}\) discussed in §2.2, we assume a set of operations symbols \(\mathcal {O}\), with each \(\textsf{op}\in \mathcal {O}\) assigned an operation signature \(\textsf{op}: A_\textsf{op} \leadsto B_\textsf{op} \mathbin {!} \tau _\textsf{op}\), which specifies that \(\textsf{op}\) accepts inputs of type \(A_\textsf{op}\), returns values of type \(B_\textsf{op}\), and its execution takes \(\tau _\textsf{op}\) time units. Observe that by typing operations with ground types, as opposed to simply with base types, we can specify operations such as \(\textsf{paint} : \textsf{Part} \leadsto ([ \tau _{\text {dry}} ]\, \textsf{Part}) \mathbin {!} \tau _{\text {paint}}\), returning values that can be accessed only after a certain amount of time, here, after \(\tau _{\text {dry}}\).

Value types extend ground types with function type \(X \rightarrow Y \mathbin {!}\tau \) that specifies functions taking X-typed arguments to computations that return Y-typed values and take \(\tau \) time to execute, as expressed by the computation type \(Y \mathbin {!}\tau \).

3.2 Terms

The syntax of terms is given in Fig. 2, separated into values and computations.

Values include variables, constants, finite tuples, functions, and the boxing up of temporal resources, , which allows us to consider an arbitrary value V as a temporal resource as long as it is safe to access V after \(\tau \) time units.

Computations include returning values, sequential composition, function application, pattern-matchingFootnote 6, algebraic operation calls, effect handling, and the unboxing of temporal resources, where given a temporal resource V of type \([ \tau ]\, X\), the computation is used to access the underlying value of type X if at least \(\tau \) time units have passed since the creation of the resource V.

Fig. 2.
figure 2

Values, computations, and effect handlers of \(\lambda _{[\tau ]}\).

Full size image

In addition to user-specifiable operation calls (via operation signatures and effect handling), we include a separate operation that blocks the execution of its continuation for the given amount of time. For simplicity, we require effect handlers to have operation clauses \(M_\textsf{op}\) for all \(\textsf{op}\in \mathcal {O}\), but we do not allow s to be handled in light of the equations we want of them in §5, where all consecutive s are collapsed and all zero- s are removed.

3.3 Type System

We now equip \(\lambda _{[\tau ]}\) with a modal type-and-effect system. On the one hand, for modelling temporal resources, we build on Fitch-style modal type systems [19]. On the other hand, for modelling effectful computations and their specifications, we build on type-and-effect systems for calculi based on graded monads [35].

The typing judgements are written as \(\varGamma \vdash V : X\) and \(\varGamma \vdash M : X \mathbin {!}\tau \), where \(\tau \) specifies M’s execution time and \(\varGamma \) is a temporal typing context, given by

$$ \varGamma \mathrel {\;{:}{:}{=}\ }\cdot \mathrel {\;\big |\ \ }\varGamma , x \mathinner {:}X \mathrel {\;\big |\ \ }\varGamma , \langle \tau \rangle $$

Here, \(\langle \tau \rangle \) is a temporal context modality, akin to in Fitch-style systems. We use it to express that when typechecking a term of the form \(\varGamma , \langle \tau \rangle \vdash V : X\), we can safely assume that at least \(\tau \) time will have passed before the resource V is accessed or executed. The rules defining these judgements are given in Fig. 3.

Fig. 3.
figure 3

Typing rules of \(\lambda _{[\tau ]}\).

Full size image

In contrast to Fitch-style modal type systems discussed in §2.1, Var does not restrict the \(\varGamma '\) right of x to not include any context modalities. This is so because in the possible worlds reading of \(\lambda _{[\tau ]}\) (see §4) we treat all types as being monotone for time—this is not usually the case for formulae in modal logics such as S4, but in \(\lambda _{[\tau ]}\) this models that once any value is available it will remain so.

As in systems based on graded monads, Return specifies that returning a value takes zero time, and Let that the execution time of sequentially composed computations is the sum of the individual ones. Novel to \(\lambda _{[\tau ]}\), Let, Op, Delay, and Handle state that the continuations can safely assume that relevant amount of additional time has passed before they start executing, as discussed in §2.2.

When typing the operation clauses \(M_\textsf{op}\) in Handle, we universally quantify (at the meta-level) over the execution time \(\tau ''\) of the continuation k of \(M_\textsf{op}\). We do so as the operation clauses \(M_\textsf{op}\) must be able to execute at any point when effect handling recursively traverses M. Further, observe that k is wrapped inside a resource type. This ensures that k is invoked only after \(\tau _\textsf{op}\) amount of time has been spent in \(M_\textsf{op}\), thus guaranteeing that the temporal discipline is respected. Note that this enforces a linear discipline for our effect handlers: for \(\tau _\textsf{op}> 0\), k must be executed exactly once for \(M_\textsf{op}\)’s execution time to match \(\tau _\textsf{op}+ \tau ''\).

Finally, Box specifies that in order to box up a value V of type X as a temporal resource of type \([ \tau ]\, X\), we must be able to type V when assuming that \(\tau \) additional time units will have passed before V is accessed. At the same time, Unbox specifies that we can unbox a temporal resource V of type \([ \tau ]\, X\) only if at least \(\tau \) time units have passed since its creation: the time captured by \(\varGamma \) must be at least \(\tau \), and we must be able to type V in a \(\tau \) time units “earlier” context \(\varGamma \mathbin {-}\tau \). The time captured by a context, \(\textsf{time}\; \varGamma \), is calculated recursively as

figure ap

and the “time travelling” operation \(\varGamma \mathbin {-}\tau \) as (where \(\tau _+ \equiv 1 + \tau ''\) for some \(\tau ''\))

figure aq

taking \(\varGamma \) to an “earlier” state by removing \(\tau \) worth of modalities and variables.

3.4 Admissibility of Renamings and Substitutions

We now show that expected structural and substitution rules [7] are admissible.

Theorem 1

The typing relations \(\varGamma \vdash V : X\) and \(\varGamma \vdash M : X \mathbin {!}\tau \) are closed under standard structural rules of weakening, exchange of consecutive variables, and contraction (omitted here). Furthermore, both typing relations are also closed under rules making \(\langle - \rangle \) into a strong monoidal functor (with a co-strength) [45]:

figure ar

where \(\varGamma \vdash J\) ranges over both typing relations, where the first two rules hold in both directions, and the last rule expresses that if we can type J using a variable “now”, we can also type J if that variable was brought into scope “earlier”.

Proof

First, we define a renaming relation \(\rho : \varGamma \leadsto \varGamma '\), and then prove by induction that if \(\varGamma \vdash J\) and \(\rho : \varGamma \leadsto \varGamma '\) then \(\varGamma ' \vdash J[\rho ]\), where \(J[\rho ]\) is J renamed with \(\rho \). The \(\leadsto \) relation is defined as the reflexive-transitive-congruent closure of rules corresponding to the desired structural rules, e.g., \(\textsf{var}^r_{x \mathinner {:}X \in \varGamma } : \varGamma , y \mathinner {:}X \leadsto \varGamma \) and \(\mu ^r : \varGamma , \langle \tau _1 + \tau _2 \rangle \leadsto \varGamma , \langle \tau _1 \rangle , \langle \tau _2 \rangle \). The full list is given in the online appendix.

For the Var and Unbox cases of the proof, we show that if \(\rho : \varGamma \leadsto \varGamma '\) and \(x \in _\tau \varGamma \), then \(\rho \, x \in _{\tau '} \varGamma '\) for some \(\tau '\) with \(\tau \leqslant \tau '\), where \(x \in _\tau \varGamma \) means that \(x \in \varGamma \) and there is \(\tau \) worth of modalities right of x in \(\varGamma \), and \(\rho \, x\) is the variable that \(\rho \) maps x to. For Unbox, we further prove that if \(\rho : \varGamma \leadsto \varGamma '\), then for any \(\tau \) we can build \(\rho \mathbin {-}\tau : \varGamma \mathbin {-}\tau \leadsto \varGamma ' \mathbin {-}\tau \), using the result about \(\in _{\tau }\) to ensure that \(\rho \) does not map any \(x \in \varGamma \mathbin {-}\tau \) outside of \(\varGamma ' \mathbin {-}\tau \). We also establish that if \(\varGamma \leadsto \varGamma '\), then \(\textsf{time}\; \varGamma \leqslant \textsf{time}\; \varGamma '\), allowing us to deduce \(\tau \leqslant \textsf{time}\; \varGamma '\) from \(\tau \leqslant \textsf{time}\; \varGamma \).

The admissibility of the rules corresponding to \(\mu ^r\) (and its inverse) relies on us having defined context splitting in Unbox using \(\varGamma \mathbin {-}\tau \), as opposed to more rigidly as \(\varGamma ,\varGamma '\), as in [19], as then it would be problematic if the split happens between \(\langle \tau _1 \rangle ,\langle \tau _2 \rangle \). Inverses of the last two rules in Thm. 1 are not valid—they would allow unboxing temporal resources without enough time having passed.

Theorem 2

The typing relations \(\varGamma \vdash V : X\) and \(\varGamma \vdash M : X \mathbin {!}\tau \) are closed under substitution, i.e., if \(\varGamma , x \mathinner {:}X, \varGamma ' \vdash J\) and \(\varGamma \vdash W : X\), then \(\varGamma , \varGamma ' \vdash J[W/x]\), where J[W/x] is standard recursively defined capture-avoiding substitution [7].

Proof

The proof proceeds by induction on the derivation of \(\varGamma , x \mathinner {:}X, \varGamma ' \vdash J\). The most involved case is Unbox, where we construct the derivation of by first analysing whether \(\tau \leqslant \textsf{time}\; \varGamma '\), which tells us whether x is in the context \((\varGamma , x \mathinner {:}X, \varGamma ') \mathbin {-}\tau \) of V, based on which we learn whether W continues to be substituted for x in V or whether \(V[W/x] = V\).

3.5 Equational Theory

We conclude the definition of \(\lambda _{[\tau ]}\) by equipping it with an equational theory to reason about program equivalence, defined using judgements \(\varGamma \vdash V \equiv W : X\) and \(\varGamma \vdash M \equiv N : X \mathbin {!}\tau \), where we presuppose that the terms are well-typed for the given contexts and types. The rules defining these relations are given in Fig. 4. We omit standard equivalence, congruence, and substitutivity rules [7].

Fig. 4.
figure 4

Equational theory of \(\lambda _{[\tau ]}\).

Full size image

The equational theory consists of standard \(\beta /\eta \)-equations for the unit, product, and function types. We also include monadic equations for and  [52]. For \(\textsf{op}\) and , we include algebraicity equations, allowing us to pull them out of  [8]. For , we include equations expressing that effect handling recursively traverses a term, replacing each \(\textsf{op}\)-occurrence with the operation clause \(M_\textsf{op}\), leaving s untouched, and finally executes the continuation N when reaching return values [61]. Finally, we include \(\beta \)/\(\eta \)-equations for and , expressing that behaves as a pattern-matching elimination form for .

4 Denotational Semantics

We justify the design of \(\lambda _{[\tau ]}\) by giving it a mathematically natural semantics based on adjunctions between strong monoidal functors [45] (modelling modalities) and a strongFootnote 7 graded monad [35] (modelling computations). We assume general knowledge of category theory, only spelling out details specific to \(\lambda _{[\tau ]}\). To optimise for space, we discuss the abstract model structure simultaneously with a concrete example using presheaves [46], but note that the interpretation is defined, and its soundness proved, with respect to the abstract structure.

When referring to the abstract model structure, we denote the underlying category with \(\mathbb {C}\). Meanwhile, the concrete presheaf example is given in \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), consisting of functors from \((\mathbb {N},\leqslant )\) to the category \(\textsf{Set}\) of sets and functions.

The model in \(\textsf{Set}^{(\mathbb {N},\leqslant )}\) is similar to Kripke’s possible worlds semantics, except that in \(\textsf{Set}^{(\mathbb {N},\leqslant )}\) all objects are monotone for \(\leqslant \), i.e., for any \(A \in \textsf{Set}^{(\mathbb {N},\leqslant )}\) we have functions \(A(t_1 \leqslant t_2) : A(t_1) \rightarrow A(t_2)\) respecting reflexivity and transitivity, whereas Kripke models are commonly given by discretely indexed presheaves and only modalities change worlds. For \(\lambda _{[\tau ]}\), working in \(\textsf{Set}^{(\mathbb {N},\leqslant )}\) gives us that when a resource becomes available, it will remain so without need for reboxing, leading to a more natural system for temporal resources and a simpler Var rule.

4.1 Interpretation of Types

Value Types and Contexts To interpret value types, we require the category \(\mathbb {C}\) to have finite products \((\mathbb {1}, A \times B)\) and exponentials \(A \Rightarrow B\), so as to model the unit, product, and function types. In \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), the former are given point-wise using the finite products in \(\textsf{Set}\), and the latter are given as , where \(\textsf{hom}\, t : (\mathbb {N},\leqslant ) \rightarrow \textsf{Set}\) is the covariant hom-functor for \((\mathbb {N},\leqslant )\), given by  [46]. When unfolding it further, the above means that \((A \Rightarrow B)(t)\) is the set of functions \((f_{t'} : A(t') \rightarrow B(t'))_{t' \in \{t' \in \mathbb {N} \vert t \leqslant t'\}}\) that are natural in \(t'\), capturing the intuition that in \(\lambda _{[\tau ]}\) functions can be applied in any future context. For base types, we require an object \([\![\textsf{b}]\!]\) of \(\mathbb {C}\) for each \(\textsf{b}\).

To interpret the temporal resource type, we require a strong monoidal functor \([ - ] : (\mathbb {N},\leqslant ) \rightarrow [ \mathbb {C}, \mathbb {C}]\), where \([ \mathbb {C}, \mathbb {C}]\) is the category of endofunctors on \(\mathbb {C}\). This means that we have functors \([ \tau ]: \mathbb {C}\rightarrow \mathbb {C}\), for all \(\tau \in \mathbb {N}\), together with morphisms \([ \tau _1 \leqslant \tau _2 ]_A : [ \tau _1 ] A \rightarrow [ \tau _2 ] A\), natural in A and respecting \(\leqslant \). Strong monoidality of \([ - ]\) means that we have natural isomorphisms \({\varepsilon _A : [ 0 ] A \overset{\cong }{\rightarrow }\ A}\) and \(\delta _{A,\tau _1,\tau _2} : [ \tau _1 + \tau _2 ] A \overset{\cong }{\rightarrow }\ [ \tau _1 ] ([ \tau _2 ] A)\), satisfying time-graded variants of comonad laws [10]:

$$ \varepsilon \circ \delta _{A,0,\tau } \equiv \textsf{id}\qquad [ \tau ](\varepsilon ) \circ \delta _{A,\tau ,0} \equiv \textsf{id}\qquad \delta _{[ \tau _3 ] A,\tau _1,\tau _2} \circ \delta _{A,\tau _1 + \tau _2,\tau _3} \equiv [ \tau _1 ] (\delta ) \circ \delta $$

We also require \((\delta _{A,\tau _1,\tau _2},\delta ^{-1}_{A,\tau _1,\tau _2}) \) to be monotone in \(\tau _1, \tau _2\), i.e., if \(\tau _1 \leqslant \tau '_1\) and \(\tau _2 \leqslant \tau '_2\), then \([ \tau '_1 ] ([ \tau _2 \leqslant \tau '_2 ]) \circ [ \tau _1 \leqslant \tau '_1 ] \circ \delta \equiv \delta \circ [ \tau _1 + \tau _2 \leqslant \tau '_1 + \tau '_2 ]_A\). We omit the indices of the components of natural transformations when convenient.

In \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), we define , with \([ \tau ]A\)-values given by future A-values, and with \((\varepsilon _A,\varepsilon _A^{-1},\delta _A,\delta _A^{-1})\) given by identities on A-values, combined with the laws of \((0,+)\), e.g., as .

Using the above, we interpret a value type X as an object \([\![X]\!]\) of \(\mathbb {C}\), as

figure bh

where \(T\) is a graded monad for modelling computations—we return to it below. The interpretation of ground types \([\![A]\!]^g\) is defined similarly, so we omit it here.

Next, we define the interpretation of contexts, for which we require another strong monoidal functor, \(\langle - \rangle : (\mathbb {N},\leqslant )^{\text {op}} \rightarrow [ \mathbb {C}, \mathbb {C}]\). Note that \(\langle - \rangle \) is contravariant—this enables us to model the structural rules that allow terms typed in an earlier context to be used in future ones (see Thm. 1). We denote the strong monoidal structure of \(\langle - \rangle \) with \(\eta _A : A \overset{\cong }{\rightarrow }\ \langle 0 \rangle A\) and \(\mu _{A, \tau _1, \tau _2} : \langle \tau _1 \rangle (\langle \tau _2 \rangle A) \overset{\cong }{\rightarrow }\ \langle \tau _1 + \tau _2 \rangle A\), required to satisfy time-graded variants of monad laws [45], given by

$$ \mu _{\!A,0,\tau } \circ \eta \equiv \textsf{id}\qquad \mu _{\!A,\tau ,0} \circ \langle \tau \rangle (\eta ) \equiv \textsf{id}\qquad \mu _{A,\tau _1 + \tau _2, \tau _3} \circ \mu _{\langle \tau _3 \rangle A,\tau _1,\tau _2} \equiv \mu \circ \langle \tau _1 \rangle (\mu ) $$

and \((\mu _{A, \tau _1, \tau _2},\mu ^{-1}_{A, \tau _1, \tau _2})\) have to be monotone in \(\tau _1,\tau _2\), similarly to \((\delta ,\delta ^{-1}) \) above.

In \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), we define , as past A-values, with the side-condition \(\tau \leqslant t\) crucial for the existence of the adjunctions \(\langle \tau \rangle \dashv [ \tau ]\) we require below. We define \((\eta _A,\eta _A^{-1},\mu _A,\mu _A^{-1})\) similarly to earlier, as identities on A-values, combined with the laws of \((0,+,\mathbin {\scriptstyle \dot{\smash {\textstyle -}}})\), so as to satisfy the side-conditions.

With this, we can interpret contexts \(\varGamma \) as functors \([\![\varGamma ]\!] : \mathbb {C}\rightarrow \mathbb {C}\), given by:

figure bj

We interpret contexts as functors to easily manipulate denotations of composite contexts, e.g., we then have \(\iota _{\varGamma ;\varGamma ';A} : [\![\varGamma ,\varGamma ']\!]A \overset{\cong }{\rightarrow }\ [\![\varGamma ']\!]([\![\varGamma ]\!]A)\), natural in A.

Finally, to formulate the semantics of computation types and terms, we require there to be a family of adjunctions \(\langle \tau \rangle \dashv [ \tau ]\), i.e., natural transformations \(\eta ^{\dashv }_{A,\tau } : A \rightarrow [ \tau ] (\langle \tau \rangle A)\) (the unit) and \(\varepsilon ^{\dashv }_{A,\tau } : \langle \tau \rangle ([ \tau ] A) \rightarrow A\) (the counit), for all \(\tau \in \mathbb {N}\), satisfying time-graded variants of standard adjunction laws [45], given by

$$ \varepsilon ^{\dashv }_{\langle \tau \rangle A,\tau } \circ \langle \tau \rangle (\eta ^{\dashv }_{A,\tau }) \equiv \textsf{id}\qquad [ \tau ](\varepsilon ^{\dashv }_{A,\tau }) \circ \eta ^{\dashv }_{[ \tau ]A,\tau } \equiv \textsf{id}$$

We also require \((\eta ^{\dashv },\varepsilon ^{\dashv })\) to interact well with the strong monoidal structures:

$$ \begin{array}{c} [ \tau ] (\langle 0 \leqslant \tau \rangle ) \circ \eta ^{\dashv }_{A,\tau } \circ \eta ^{-1} \circ \varepsilon \equiv [ 0 \leqslant \tau ] \qquad [ \tau _1 ] ([ \tau _2 ] (\mu )) \circ [ \tau _1 ](\eta ^{\dashv }_{\langle \tau _1 \rangle A,\tau _2}) \circ \eta ^{\dashv }_{A,\tau _1} \equiv \delta \circ \eta ^{\dashv }\\ \langle 0 \rangle ([ 0 \leqslant \tau ]) \circ \eta \circ \varepsilon ^{-1} \circ \varepsilon ^{\dashv }_{A,\tau } \equiv \langle 0 \leqslant \tau \rangle \quad \varepsilon ^{\dashv }_{A,\tau _1} \circ \langle \tau _1 \rangle (\varepsilon ^{\dashv }_{[ \tau _1 ] A, \tau _2}) \circ \langle \tau _1 \rangle (\langle \tau _2 \rangle (\delta )) \equiv \varepsilon ^{\dashv }\circ \mu \end{array} $$

Proposition 1

It then follows that \(\eta ^{\dashv }_{A,0} \equiv \varepsilon ^{-1}_{\langle 0 \rangle A} \circ \eta _A\) and \(\varepsilon ^{\dashv }_{A,0} \equiv \varepsilon _A \circ \eta ^{-1}_{[ 0 ]A}\).

In \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), \(\eta ^{\dashv }_{A,\tau }\) and \(\varepsilon ^{\dashv }_{A,\tau }\) are given by identities on A-values, respectively combined with \(\tau \leqslant t + \tau \) and monotonicity for \((t \mathbin {\scriptstyle \dot{\smash {\textstyle -}}}\tau ) + \tau \equiv t\). For the latter, we crucially know \(\tau \leqslant t\) due to the side-condition included in the definition of \(\langle - \rangle \).

We note that modulo the time grades \(\tau \), the above structure is analogous to the models of the Fitch-style presentation of S4 [19], where is modelled by an idempotent comonad,  by an idempotent monad, and boxing/unboxing by . This is also why we present \([ - ]\) and \(\langle - \rangle \) as comonad- and monad-like.

Computation Types For computation types, we require a \([ - ]\)-strong graded monad \((T,\eta ^{T},\mu ^{T},\textsf{str}^{T})\) on \(\mathbb {C}\), with grades in \(\mathbb {N}\).Footnote 8 In detail, this means a functor \(T: \mathbb {N} \rightarrow [ \mathbb {C}, \mathbb {C}]\), together with natural transformations \(\eta ^{T}_A : A \rightarrow T\, 0\, A\) (the unit), \(\mu ^{T}_{A,\tau _1,\tau _2} : T\, \tau _1 (T\, \tau _2\, A) \rightarrow T\, (\tau _1 + \tau _2)\, A\) (the multiplication), and \(\textsf{str}^{T}_{A,B,\tau } : [ \tau ]A \times T\, B\, \tau \rightarrow T\, (A \times B)\, \tau \) (the strength), with the first two satisfying standard graded monad laws (see [35] or \((\eta ,\mu )\) of \(\langle - \rangle \)). Below we only present the laws for \(\textsf{str}^{T}\) because it has a novel temporal aspect to it—its first argument appears under \([ \tau ]\). As such, \(\textsf{str}^{T}\) expresses that if we know an A-value will be available after \(\tau \) time units, we can push it into computations taking \(\tau \)-time to execute.

We say that \(T\) is a \([ - ]\)-strong graded monad following the parlance of Bierman and de Paiva [12]—in their work they model the possibility modality as a -strong monad. While the laws governing \(\textsf{str}^{T}\) are not overly different from standard graded strength laws [35], we have to correctly account for \([ - ]\) in them

$$ \begin{array}{c} \textsf{str}^{T}_{A,B,0} \circ (\varepsilon ^{-1}_A \times \eta ^{T}_A) \equiv \eta ^{T}_{A \times B} \quad \mu ^{T}_{A \times B,\tau _1,\tau _2} \circ T\, (\textsf{str}^{T}) \circ \textsf{str}^{T}\equiv \textsf{str}^{T}\circ (\delta ^{-1} \times \mu ^{T}) \\ T\, (\textsf{snd}) \circ \textsf{str}^{T}_{A,B,\tau } \equiv \textsf{snd} \quad T\, (\alpha ) \circ \textsf{str}^{T}\circ (\textsf{m}\times \textsf{id}) \circ \alpha ^{-1} \equiv \textsf{str}^{T}_{A,B \times C,\tau } \circ (\textsf{id}\times \textsf{str}^{T}) \end{array} $$

where \(\alpha _{A,B,C} : (A \times B) \times C \overset{\cong }{\rightarrow }\ A \times (B \times C)\), and \(\textsf{m}_{A,B,\tau }: [ \tau ] A \times [ \tau ] B \rightarrow [ \tau ] (A \times B)\) witnesses that \([ \tau ]\) is monoidal for \(\times \), which follows from \([ \tau ]\) being a right adjoint [45]. Observe that it is the \([ - ]\)-strength that naturally gives \(T\) a temporal flavour—the rest of it is standard [35]. Below we show that \(\textsf{str}^{T}\) is also mathematically natural, admitting an analogous characterisation to ordinary strength.

Proposition 2

Analogously to ordinary strong and enriched monads [39], \(T\) having \([ - ]\)-strength is equivalent to \([ - ]\)-enrichment of \(T\), given by morphisms \({[ \tau ](A \Rightarrow B) \rightarrow (T\,\tau \,A \Rightarrow T\,\tau \,B)}\) respecting \(\mathbb {C}\)’s self-enrichment [38] and \((\eta ^{T},\mu ^{T})\).

In order to model operations \(\textsf{op}\) and in §4.2, we require \(T\) to be equipped with algebraic operations: we ask there to be families of natural transformations \(\textsf{op}^{T}_{A,\tau } : [\![A_\textsf{op}]\!]^g \times [ \tau _\textsf{op} ]([\![B_\textsf{op}]\!]^g \Rightarrow T\, \tau \, A) \rightarrow T\, (\tau _\textsf{op}+ \tau )\, A\), for all \(\textsf{op}: A_\textsf{op} \leadsto B_\textsf{op} \mathbin {!} \tau _\textsf{op} \in \mathcal {O}\), and \(\textsf{delay}^{T}_{A,\tau '}\, \tau : [ \tau ] (T\, \tau '\, A) \rightarrow T\, (\tau + \tau ')\, A\), for all \(\tau \in \mathbb {N}\), satisfying algebraicity laws [61], which state that both commute with \(\mu ^{T}\) and \(\textsf{str}^{T}\), e.g.,

$$ \textsf{str}^{T}_{A, B, \tau + \tau '} \circ (\textsf{id}\times \textsf{delay}^{T}\, \tau ) \equiv \textsf{delay}^{T}_{A \times B,\tau '}\, \tau \circ [ \tau ](\textsf{str}^{T}) \circ \textsf{m}\circ (\delta _{A,\tau ,\tau '} \times \textsf{id}) $$

In \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), we can define \(T\) as the initial algebra of a corresponding signature functor for operations \(\textsf{op}\) and , analogously to the usual treatment of algebraic effects [8]. Concretely, such \(T\) is determined inductively by three cases

figure br

with \((\eta ^{T},\mu ^{T},\textsf{str}^{T},\textsf{op}^{T},\textsf{delay}^{T})\) defined in the expected way, e.g., \(\textsf{str}^{T}\) is given by recursively traversing a computation of type \(T\, \tau \, B\) and moving the argument of type \([ \tau ] A\) under \(\textsf{ret}\) cases, modifying \(\tau \) when going under the \(\textsf{op}\) and \(\textsf{delay}\) cases.

4.2 Interpretation of Value and Computation Terms

The interpretation of values and computations is defined simultaneously. We only present the temporally interesting cases—full details are in the online appendix.

As \(\lambda _{[\tau ]}\) does not have sub-effecting and includes enough type annotations for typing derivations to be unique, this interpretation is coherent by construction.

Values We assume a morphism \([\![\textsf{f}]\!] : [\![A_1]\!]^g \times \ldots \times [\![A_n]\!]^g \rightarrow [\![B]\!]^g\) for every \(\textsf{f} : (A_1,\ldots ,A_n) \rightarrow B\). We interpret a well-typed value \(\varGamma \vdash V : X\) as a morphism \([\![\varGamma \vdash V : X]\!] : [\![\varGamma ]\!]\mathbb {1}\rightarrow [\![X]\!]\) in \(\mathbb {C}\) by induction on the given typing derivation.

Most of the value cases are standard, and analogous to other calculi based on fine-grain call-by-value [44] and graded monads [35], using the Cartesian-closed structure of \(\mathbb {C}\). The temporally interesting cases are Var and Box, given by

figure bs

where \(\textsf{e}_{A,\varGamma } : [\![\varGamma ]\!]A \rightarrow \langle \textsf{time}\; \varGamma \rangle A\) extracts and collapses all temporal modalities in \(\varGamma \), and the counit-like \(\varepsilon ^{\langle \rangle }_{A,\tau }\) is given by the composite \(\langle \tau \rangle A \overset{\langle 0 \leqslant \tau \rangle _A}{-\!\!\!-\!\!\!-\!\!\!\rightarrow } \langle 0 \rangle A \overset{\eta ^{-1}_A}{-\!\!\!\rightarrow } A\).

Computations We interpret a well-typed computation \(\varGamma \vdash M : X \mathbin {!}\tau \) as a morphism \([\![\varGamma \vdash M : X \mathbin {!}\tau ]\!] : [\![\varGamma ]\!]{\mathbb {1}} \rightarrow T\,\tau \,[\![X]\!]\) in \(\mathbb {C}\) by induction on the typing derivation. The definition is largely unsurprising and follows a pattern similar to [35, 44]—the novelty lies in controlling the occurrences of \(\langle - \rangle \) and \([ - ]\).

In Let, we use \(\langle \tau \rangle \dashv [ \tau ]\) to push the environment “into the future”, and then follow the standard monadic strength-followed-by-multiplication pattern [35, 52]:

figure bt

An analogous use of \(\langle \tau \rangle \dashv [ \tau ]\) also appears in the cases for operations, e.g., in

figure bu

Next, the Unbox case of the interpretation is defined as

figure bv

showing that temporal resources follow the common pattern in which elimination forms are modelled by counits of adjunctions, whereas units model introduction forms (akin to functions). The morphism \(\eta ^{\text {PRA}}_{\varGamma ,A,\tau } : [\![\varGamma ]\!]A \rightarrow \langle \tau \rangle ([\![\varGamma \mathbin {-}\tau ]\!] A)\) extracts and collapses \(\tau \) worth of context modalities in \(\varGamma \), as long as \(\tau \leqslant \textsf{time}\; \varGamma \). It is a semantic counterpart to an observation that the context modality \(\varGamma , \langle \tau \rangle \) is a parametric right adjoint to the \(\varGamma \mathbin {-}\tau \) operation, as in recent dependently typed presentations of Fitch-style modal types [27], see §6.1 for further discussion.

Finally, we discuss the interpretation of effect handling. For this, we additionally require \(\mathbb {C}\) to have set-indexed products \(\varPi _{i \in I} A_i\) and handling morphisms

figure bw

satisfying laws which state that \(\chi _A\) returns a graded \(T\)-algebra [22, 50], e.g., we require \(\textsf{uncurry}(\chi _{A,0,\tau '}) \circ (\textsf{id}\times \eta ^{T}) \equiv \textsf{snd}\), where \(\textsf{uncurry}\) (and \(\textsf{curry}\) earlier) is part of the universal property of \(A \Rightarrow B\). We also require similar laws for \(\chi \)’s interaction with \(\textsf{op}^{T}\) and \(\textsf{delay}^{T}\). In \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), \(\chi \) is defined by recursively traversing a given tree, replacing all occurrences of \(\textsf{op}\, a\, k\) with respective operation clauses.

Writing \(\mathcal {H}\) for the domain of \(\chi _{[\![Y]\!],\tau ,\tau '}\), the Handle case is then defined as

figure bx

where we write \([\![H]\!]\) for the point-wise interpretation of operation clauses

$$ [\![\varGamma ]\!]\mathbb {1}\overset{\langle \langle \textsf{id}\rangle _{\tau '' \in \mathbb {N}} \rangle _{\textsf{op}\in \mathcal {O}}}{-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!\longrightarrow } \varPi _{\textsf{op}\in \mathcal {O}} \varPi _{\tau '' \in \mathbb {N}} \Big ([\![\varGamma ]\!]\mathbb {1}\Big ) \overset{\varPi _{\textsf{op}\in \mathcal {O}} \varPi _{\tau '' \in \mathbb {N}} \big ( \textsf{curry}([\![M_\textsf{op}\, \tau '']\!] \,\circ \, \alpha ^{-1}) \big )}{-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!-\!\!\!\longrightarrow } \mathcal {H} $$

4.3 Renamings, Substitutions, and Soundness

We now show how syntactic renamings and substitutions relate to semantic morphism composition, using which we then prove the interpretation to be sound.

Proposition 3

Given \(\rho : \varGamma \,{\leadsto }\, \varGamma '\) and \(\varGamma \vdash J\), then \([\![J[\rho ]]\!] \equiv [\![J]\!] \circ [\![\rho ]\!]_{\mathbb {1}}\), where the interpretation of renamings \([\![\rho ]\!]_A : [\![\varGamma ']\!]A \rightarrow [\![\varGamma ]\!]A\) is defined by induction on the derivation of \(\rho : \varGamma \leadsto \varGamma '\), with the morphism \([\![\rho ]\!]_A\) also natural in A.

Proposition 4

Given \(\varGamma , x \mathinner {:}X, \varGamma ' \vdash J\) and \(\varGamma \vdash W : X\), we have \([\![J[W/x]]\!] \equiv [\![J]\!] \circ \iota _{\varGamma ,x \mathinner {:}X;\varGamma ';\mathbb {1}}^{-1} \circ [\![\varGamma ']\!]\big (\langle \textsf{id}, [\![W]\!] \rangle \big ) \circ \iota _{\varGamma ;\varGamma ';\mathbb {1}}\), where \((\iota ,\iota ^{-1})\) are discussed in §4.1.

Proof

We prove both results by induction on the derivation of \({\varGamma \vdash J}\). The proofs are unsurprising but require us to prove auxiliary lemmas about recursively defined renamings and semantic morphisms. For example, for Prop. 3, we show \(\eta ^{\text {PRA}}\circ [\![\rho ]\!] \equiv \langle \tau \rangle ([\![\rho \mathbin {-}\tau ]\!]) \circ \eta ^{\text {PRA}}: [\![\varGamma ']\!] A \rightarrow \langle \tau \rangle ([\![\varGamma \mathbin {-}\tau ]\!]A)\), and for Prop. 4, that \(\eta ^{\text {PRA}}\circ \iota \equiv \langle \tau \rangle \big (\iota \big ) \circ \eta ^{\text {PRA}}: [\![\varGamma , \varGamma ']\!] A \rightarrow \langle \tau \rangle \big ([\![\varGamma ' \mathbin {-}\tau ]\!]([\![\varGamma ]\!] A)\big )\), when \(\tau \leqslant \textsf{time}\; \varGamma '\).

Theorem 3

Given \(\varGamma \vdash I \equiv J\) derived using the rules in §3.5, then \([\![I]\!] \equiv [\![J]\!]\).

Proof

The proof proceeds by induction on the derivation of \(\varGamma \vdash I \equiv J\), using Prop. 3 and Prop. 4 to unfold the renamings and substitutions in the equations of §3.5, and using the properties of the abstract structure we required \(\mathbb {C}\) to have.

5 Quotienting Delays

Observe that in \(\lambda _{[\tau ]}\) the computations and cannot be proved equivalent, though in some situations this might be desired.

In order to deem the above two programs (and others alike) equivalent, we extend \(\lambda _{[\tau ]}\)’s equational theory with the following natural equations for s:

figure cb

Theorem 4

If the algebraic operations \(\textsf{delay}^{T}\!\) of \(T\) satisfy analogous two equations, the interpretation of §4 is sound for this extended equational theory.

For the concrete model in \(\textsf{Set}^{(\mathbb {N},\leqslant )}\), we have to quotient \(T\) [36] by these two equations—the resulting graded monad is determined inductively by the cases

figure cc

where \((T\, \tau \, A)(t)\) and \((S\, \tau \, A)(t)\) are defined simultaneously in such a way that only non-zero, non-consecutive \(\textsf{delay}\)s can appear in the tree structure.

6 Related and Future Work

6.1 Related Work

We contribute to two prominent areas: (i) modal types and (ii) graded monads.

As noted in §2.1, modal types provide a mathematically natural means for capturing many aspects of programming. Adding to §2.1, types corresponding to the eventually and always modalities of temporal logics capture functional reactive programming (FRP) [18, 32, 42], including a combination with linearity and time-annotations to model resources [33], where all values are annotated with inhabitation times. Recently, FRP has also been studied in Fitch-style [6]. Starting with Nakano [55], modal types have also been used for guarded recursion, even in the dependently typed setting [5, 14, 47], including in Fitch-style [13].

We also note that \(\lambda _{[\tau ]}\)’s time grades \(\tau \) and the \(\varGamma \mathbin {-}\tau \) operation are closely related to recent dependently typed Fitch-style frameworks. Namely, [28] develops a multimodal type theory (MTT) where types \([ \mu ]X\) are indexed by 1-cells \(\mu \) of a strict 2-category (a mode theory). The time grades \(\tau \) of \(\lambda _{[\tau ]}\) are an example of such mode theories, given by the delooping of \(\mathbb {N}\), i.e., by a single 0-cell, \(\tau \)s as 1-cells, and \(\tau \leqslant \tau '\)s as 2-cells. While ensuring the admissibility of and naturality under substitutions, MTT with its indirect elimination rule for \([ \mu ]X\) is weaker than earlier systems (such as [13]). The direct-style elimination rule is recovered in [27] by observing that in addition to \(\varGamma , \langle \mu \rangle \) being a left adjoint to \([ \mu ]X\), it should further form a parametric right adjoint (PRA) [17, 71] to contexts of the form \(\varGamma / (r : \mu )\), where r is a substitution \(\cdot , \langle \mu \rangle \leadsto \varGamma \). The operation \(\varGamma \mathbin {-}\tau \) in \(\lambda _{[\tau ]}\) is an instance of this: \(\mu \) is a \(\tau \), r corresponds to the condition \(\tau \leqslant \textsf{time}\; \varGamma \) in Unbox, contexts \(\varGamma / (r : \mu )\) are given by \(\varGamma \mathbin {-}\tau \), and the PRA situation is witnessed by renamings \(((\varGamma \mathbin {-}\tau ), \langle \tau \rangle ) \leadsto \varGamma \), when \(\tau \leqslant \textsf{time}\; \varGamma \), and \(\varGamma \leadsto ((\varGamma , \langle \tau \rangle ) \mathbin {-}\tau )\).

Graded monads provide a uniform framework for different effect systems and effect-based analyses [22, 35, 36, 50, 51]. A major contribution of ours is showing that context modalities can inform continuations of preceding computations’ effects. While the theory of graded monads can be instantiated with any ordered monoid, we focus on natural numbers to model time, but do not expect complications generalising \(\lambda _{[\tau ]}\) to other structures with same properties as \((\mathbb {N}, 0, +, \mathbin {\scriptstyle \dot{\smash {\textstyle -}}}, \leqslant )\), and perhaps even to grading T and \(\langle - \rangle \), \([ - ]\) with different structures, akin to [23].

Our use of \([ \tau ]\, X\) to restrict when resources are available is somewhat reminiscent of coeffects [16, 24, 57, 58] and quantitative type systems [4, 49, 53]. In these works, variables are graded by (semi)ring-valued rs, as \(x \mathinner {:}_r X\), counting how many times and in which ways x is used, enabling applications such as liveness and dataflow analyses [57]. Semantically, these systems often interpret \(x \mathinner {:}_r X\) using a graded comonad, as , where one can access X only if \(r \equiv 1\). Of such works, the closest to ours is that of Gaboardi et al. [23], who combine coeffects with effectful programs via distributive laws between the grades of coeffects and effects, allowing coeffectful analyses to be propagated through effectful computations.

We also note that the type \([ \tau ]\, X\) can be intuitively also viewed as a temporally-graded variant of promise types [29, 65], in that it expresses that a value of type X will be available in the future, but with additional time guarantees.

6.2 Future Work

Currently, \(\lambda _{[\tau ]}\) does not support sub-effecting: we cannot deduce from \({\tau \leqslant \tau '}\) and \({\varGamma \vdash M : X \mathbin {!}\tau }\) that \({\varGamma \vdash M : X \mathbin {!}\tau '}\). Of course, we can simulate this by inserting \(\tau ' \!\mathbin {\scriptstyle \dot{\smash {\textstyle -}}}\tau \) worth of explicit s into M, but this is extremely intensional, fixing where s happen. In particular, we cannot type equations such as if was sub-effected to \(\tau > 0\), with the \(\langle \tau \rangle \) in N’s context the culprit. However, when considering sub-effecting as a coercion \(\textsf{coerce}_{\tau \leqslant \tau '}\, M\), we believe we can add it by considering equations stating that it will produce all the possible ways how \(\tau ' \!\mathbin {\scriptstyle \dot{\smash {\textstyle -}}}\tau \) worth of s could be inserted into M. Of course, this will require a more complex non-deterministic semantics.

It would be neat if \(\lambda _{[\tau ]}\) also included recursion in a way that programs could make use of the temporal discipline. This is likely unattainable for general recursion, but we hope that primitive recursion (say, on natural numbers) can be added via type-dependency of time grades \(\tau \) on the values being recursed on.

It would be interesting to combine \(\lambda _{[\tau ]}\) with linear [25] and separation logics [34, 64] to model linear and spatial properties of temporal resources. Another goal would be to add concurrency, e.g., using (multi)handlers [9, 20, 21]. We also plan to look into capturing expiring and available-for-an-interval style resources.

Further, we plan to study \(\lambda _{[\tau ]}\)’s operational semantics, namely, one that takes time seriously and does not model s simply as uninterpreted operations [9], together with developing a prototype, and proving normalisation akin to [26, 69].

We also plan to study the completeness of the denotational semantics of \(\lambda _{[\tau ]}\). For such semantic investigations, it could be beneficial to also study the general theory of the kinds of temporally aware graded algebraic effects used in this paper, by investigating their algebras and equational presentations [36, 50].

7 Conclusion

We have shown how a temporal, time-graded variant of Fitch-style modal type systems, when combined with an effect system based on graded monads, provides a natural framework for safe programming with temporal resources. To this end, we developed a modally typed, effectful, equationally-presented core calculus, and equipped it with a sound denotational semantics based on strong monoidal functors (for modelling modalities) and graded monads (for modelling effects). The calculus also includes temporally aware graded algebraic effects and effect handlers, with the continuations of the former knowing that an operation’s worth of additional time has passed before they start executing, and where the user-defined effect handlers are guaranteed to respect this temporal discipline.