Abstract
We explore type systems and programming abstractions for the safe usage of resources. In particular, we investigate how to use types to modularly specify and check when programs are allowed to use their resources, e.g., when programming a robot arm on a production line, it is crucial that painted parts are given enough time to dry before assembly. We capture such temporal resources using a time-graded variant of Fitch-style modal type systems, develop a corresponding modally typed, effectful core calculus, and equip it with a graded-monadic denotational semantics illustrated by a concrete presheaf model. Our calculus also includes graded algebraic effects and effect handlers. They are given a novel temporally aware treatment in which operations’ specifications include their execution times and their continuations know that an operation’s worth of additional time has passed before they start executing, making it possible to safely access further temporal resources in them.
You have full access to this open access chapter, Download conference paper PDF
Similar content being viewed by others
Keywords
![figure a](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figa_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figb_HTML.png)
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.
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.
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.
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figp_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figw_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figy_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figaa_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figac_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figad_HTML.png)
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.
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.
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
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.
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figap_HTML.png)
and the “time travelling” operation \(\varGamma \mathbin {-}\tau \) as (where \(\tau _+ \equiv 1 + \tau ''\) for some \(\tau ''\))
![figure aq](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figaq_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figar_HTML.png)
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].
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]:
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbh_HTML.png)
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
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbj_HTML.png)
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
We also require \((\eta ^{\dashv },\varepsilon ^{\dashv })\) to interact well with the strong monoidal structures:
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
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.,
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbr_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbs_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbt_HTML.png)
An analogous use of \(\langle \tau \rangle \dashv [ \tau ]\) also appears in the cases for operations, e.g., in
![figure bu](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbu_HTML.png)
Next, the Unbox case of the interpretation is defined as
![figure bv](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbv_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbw_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figbx_HTML.png)
where we write \([\![H]\!]\) for the point-wise interpretation of operation clauses
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figcb_HTML.png)
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](http://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-031-30829-1_1/MediaObjects/543386_1_En_1_Figcc_HTML.png)
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.
Notes
- 1.
Eta-contraction is not type-preserving: https://github.com/agda/agda/issues/2732
- 2.
For brevity, we use the term modal type system to interchangeably refer to both modal type systems and natural deduction systems of (intuitionistic) modal logics.
- 3.
Depending on which exact modal logic one is trying to capture, the form of contexts used in the introduction/elimination rules can differ, see [19] for a detailed overview.
- 4.
We present \(\lambda _{[\tau ]}\) formally using algebraic operations with explicit continuations, while in code snippets we use so-called generic effects [59] without explicit continuations.
- 5.
For concreteness, we work with \((\mathbb {N}, 0, +, \mathbin {\scriptstyle \dot{\smash {\textstyle -}}}, \leqslant )\) for time grades, but we do not foresee problems generalising these to come from other analogous algebraic structures.
- 6.
- 7.
To be more specific, we use a modal notion of \([ - ]\)-strength that we define below.
- 8.
As \(\lambda _{[\tau ]}\) does not include sub-effecting (see §6.2), a discretely graded monad T suffices.
References
Ahman, D., Bauer, A.: Runners in Action. In: Proc. of 29th European Symp. on Programming, ESOP 2020. Lect. Notes Comput. Sci., vol. 12075, pp. 29–55. Springer (2020)
Ahman, D., Fournet, C., Hritcu, C., Maillard, K., Rastogi, A., Swamy, N.: Recalling a witness: foundations and applications of monotonic state. Proc. ACM Program. Lang. 2(POPL), 65:1–65:30 (2018)
Ahman, D., Pretnar, M., Radešček, J.: Higher-Order Asynchronous Effects (2021), extended abstract presented at the 9th ACM-SIGPLAN Wksh. on Higher-Order Programming with Effects, HOPE 2021
Atkey, R.: Syntax and Semantics of Quantitative Type Theory. In: Proc. of 33rd Annual ACM/IEEE Symp. on Logic in Computer Science, LICS 2018. pp. 56–65. ACM (2018)
Bahr, P., Grathwohl, H.B., Møgelberg, R.E.: The clocks are ticking: No more delays! In: Proc. of 32nd Annual ACM/IEEE Symp. on Logic in Computer Science, LICS 2017. pp. 1–12. IEEE Computer Society (2017)
Bahr, P., Graulund, C., Møgelberg, R.E.: Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks. Proc. ACM Program. Lang. 3(ICFP), 109:1–109:27 (2019)
Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press (2013)
Bauer, A.: What is algebraic about algebraic effects and handlers? CoRR abs/1807.05923 (2018)
Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebr. Meth. Program. 84(1), 108–123 (2015)
Beck, J.M.: Triples, algebras and cohomology. Reprints in Theory and Applications of Categories (2), 1–59 (2003), Note: Originally published as: Ph.D. thesis, Columbia University, 1967
Benton, N., Bierman, G.M., de Paiva, V., Hyland, M.: Linear lambda-calculus and categorial models revisited. In: Selected Papers from Computer Science Logic, CSL ’92. Lect. Notes Comput. Sci., vol. 702, pp. 61–84. Springer (1992)
Bierman, G.M., de Paiva, V.: On an Intuitionistic Modal Logic. Studia Logica 65(3), 383–416 (2000)
Birkedal, L., Clouston, R., Mannaa, B., Møgelberg, R.E., Pitts, A.M., Spitters, B.: Modal dependent type theory and dependent right adjoints. Math. Struct. Comput. Sci. 30(2), 118–138 (2020)
Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded Dependent Type Theory with Coinductive Types. In: Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016. Lect. Notes Comput. Sci., vol. 9634, pp. 20–35. Springer (2016)
Borghuis, V.: Coming to terms with modal logic: on the interpretation of modalities in typed lambda-calculus. Ph.D. thesis, Mathematics and Computer Science, Technische Universiteit Eindhoven (1994)
Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A Core Quantitative Coeffect Calculus. In: Proc. of 23rd European Symp. on Programming, ESOP 2014. Lect. Notes Comput. Sci., vol. 8410, pp. 351–370. Springer (2014)
Carboni, A., Johnstone, P.: Connected limits, familial representability and artin glueing. Math. Struct. Comput. Sci. 5(4), 441–459 (1995)
Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair reactive programming. In: Proc. of 41st Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2014. pp. 361–372. ACM (2014)
Clouston, R.: Fitch-Style Modal Lambda Calculi. In: Proc. of 21st Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2018. Lect. Notes Comput. Sci., vol. 10803, pp. 258–275. Springer (2018)
Convent, L., Lindley, S., McBride, C., McLaughlin, C.: Doo bee doo bee doo. J. Funct. Program. 30, Â e9 (2020)
Dolan, S., Eliopoulos, S., Hillerström, D., Madhavapeddy, A., Sivaramakrishnan, K.C., White, L.: Concurrent System Programming with Effect Handlers. In: Trends in Functional Programming. pp. 98–117. Springer (2018)
Fujii, S., Katsumata, S., Melliès, P.: Towards a Formal Theory of Graded Monads. In: Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016. Lect. Notes Comput. Sci., vol. 9634, pp. 513–530. Springer (2016)
Gaboardi, M., Katsumata, S., Orchard, D.A., Breuvart, F., Uustalu, T.: Combining effects and coeffects via grading. In: Proc. of 21st ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2016. pp. 476–489. ACM (2016)
Ghica, D.R., Smith, A.I.: Bounded Linear Types in a Resource Semiring. In: Proc. of 23rd European Symp. on Programming, ESOP 2014. Lect. Notes Comput. Sci., vol. 8410, pp. 331–350. Springer (2014)
Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)
Gratzer, D.: Normalization for multimodal type theory. In: Proc. of 37th Annual ACM/IEEE Symp. on Logic in Comp. Sci., LICS 2022. pp. 2:1–2:13. ACM (2022)
Gratzer, D., Cavallo, E., Kavvos, G.A., Guatto, A., Birkedal, L.: Modalities and parametric adjoints. ACM Trans. Comput. Logic 23(3) (2022)
Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. Log. Methods Comput. Sci. 17(3) (2021)
Haller, P., Prokopec, A., Miller, H., Klang, V., Kuhn, R., Jovanovic, V.: Scala documentation: Futures and promises (October 2022), available online at https://docs.scala-lang.org/overviews/core/futures.html
Honda, K., Vasconcelos, V., Kubo, M.: Language Primitives and Type Discipline for Structured Communication-Based Programming. In: Proc. of 7th European Symp. on Programming, ESOP 1998. Lect. Notes Comput. Sci., vol. 1381, pp. 122–138. Springer (1998)
Hyland, M., Plotkin, G., Power, J.: Combining effects: Sum and tensor. Theor. Comput. Sci. 357(1–3), 70–99 (2006)
Jeltsch, W.: Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. In: Proc. of the 28th Conf. on the Mathematical Foundations of Programming Semantics, MFPS 2012. ENTCS, vol. 286, pp. 229–242. Elsevier (2012)
Jeltsch, W.: Abstract categorical semantics for resourceful functional reactive programming. J. Log. Algebraic Methods Program. 85(6), 1177–1200 (2016)
Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, Â e20 (2018)
Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Proc. of 41st Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 2014. pp. 633–646. ACM (2014)
Katsumata, S., McDermott, D., Uustalu, T., Wu, N.: Flexible presentations of graded monads. Proc. ACM Program. Lang. 6(ICFP), 902–930 (2022)
Kavvos, G.A.: The Many Worlds of Modal \(\lambda \)-calculi: I. Curry-Howard for Necessity, Possibility and Time. CoRR abs/1605.08106 (2016)
Kelly, G.: Basic Concepts of Enriched Category Theory. No. 64 in Lecture Notes in Mathematics, Cambridge University Press (1982)
Kock, A.: Strong functors and monoidal monads. Archiv der Mathematik 23(1), 113–120 (1972)
Koopman, P., Fokker, J., Smetsers, S., van Eekelen, M., Plasmeijer, R.: Functional Programming in Clean. University of Nijmegen (1998), draft
Kripke, S.A.: Semantical Analysis of Modal Logic I. Normal Propositional Calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 9(5-6), 67–96 (1963)
Krishnaswami, N.R.: Higher-order functional reactive programming without spacetime leaks. In: Proc. of 18th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2013. pp. 221–232. ACM (2013)
Leijen, D.: Algebraic Effect Handlers with Resources and Deep Finalization. Tech. Rep. MSR-TR-2018-10, Microsoft Research (April 2018)
Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182–210 (2003)
Mac Lane, S.: Categories for the Working Mathematician. No. 5 in Graduate Texts in Mathematics, Springer-Verlag (1971)
Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext, Springer (1992)
Mannaa, B., Møgelberg, R.E.: The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In: Proc. of 3rd Int. Conf. on Formal Structures for Computation and Deduction, FSCD 2018. LIPIcs, vol. 108, pp. 23:1–23:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
Martini, S., Masini, A.: A Computational Interpretation of Modal Proofs, pp. 213–241. Springer Netherlands (1996)
McBride, C.: I Got Plenty o’ Nuttin’. In: A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Lect. Notes Comput. Sci., vol. 9600, pp. 207–233. Springer (2016)
McDermott, D., Uustalu, T.: Flexibly Graded Monads and Graded Algebras. In: Proc. of 14th Int. Conf. on Mathematics of Program Construction, MPC 2022. Lect. Notes Comput. Sci., vol. 13544, pp. 102–128. Springer (2022)
Melliès, P.A.: Parametric Monads and Enriched Adjunctions (2012), manuscript. https://www.irif.fr/~mellies/tensorial-logic/8-parametric-monads-and-enriched-adjunctions.pdf
Moggi, E.: Computational Lambda-Calculus and Monads. In: Proc. of 4th Ann. Symp. on Logic in Computer Science, LICS 1989. pp. 14–23. IEEE (1989)
Moon, B., Eades III, H., Orchard, D.: Graded Modal Dependent Type Theory. In: Proc. of 30th European Symp. on Programming, ESOP 2021. Lect. Notes Comput. Sci., vol. 12648, pp. 462–490. Springer (2021)
Murphy VII, T.: Modal Types for Mobile Code. Ph.D. thesis, School of Computer Science, Carnegie Mellon University (2008)
Nakano, H.: A Modality for Recursion. In: Proc. of 15th Annual IEEE Symp. on Logic in Computer Science, LICS 2000. pp. 255–266. IEEE Computer Society (2000)
Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5-6), 865–911 (2008)
Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: Unified Static Analysis of Context-Dependence. In: Proc. of 40th International Colloquium on Automata, Languages, and Programming, ICALP 2013. Lect. Notes Comput. Sci., vol. 7966, pp. 385–397. Springer (2013)
Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: Proc. of 19th ACM SIGPLAN Int. Conf. on Functional Programming,ICFP 2014. pp. 123–135. ACM (2014)
Plotkin, G., Power, J.: Algebraic Operations and Generic Effects. Appl. Categor. Struct. (1), 69–94 (2003)
Plotkin, G.D., Power, J.: Notions of Computation Determine Monads. In: Proc. of 5th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2002. Lect. Notes Comput. Sci., vol. 2303, pp. 342–356. Springer (2002)
Plotkin, G.D., Pretnar, M.: Handling Algebraic Effects. Log. Methods Comput. Sci. 9(4:23) (2013)
Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almquist and Wiksell (1965)
Radešček, J.: Asinhroni algebrajski učinki. Master’s thesis, Faculty of Mathematics and Physics, University of Ljubljana (2021)
Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proc. of 17th IEEE Symp. on Logic in Computer Science, LICS 2002. pp. 55–74. IEEE Computer Society (2002)
Schwinghammer, J.: A Concurrent Lambda-Calculus with Promises and Futures. Master’s thesis, Programming Systems Lab, Universität des Saarlandes (2002)
Simpson, A.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh (1994)
Smirnov, A.L.: Graded monads and rings of polynomials. J. Math. Sci. 151(3), 3032–3051 (2008)
The Agda Team: The Agda Wiki. Available at https://wiki.portal.chalmers.se/agda/pmwiki.php (2022)
Valliappan, N., Ruch, F., Cortiñas, C.T.: Normalization for Fitch-style modal calculi. Proc. ACM Program. Lang. 6(ICFP), 772–798 (2022)
Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2-3), 384–418 (2014)
Weber, M.: Familial 2-functors and parametric right adjoints. Theory Appl. Categories 18(22), 665–732 (2007)
Wickline, P., Lee, P., Pfenning, F., Davies, R.: Modal Types as Staging Specifications for Run-Time Code Generation. ACM Comput. Surv. 30(3es), Â 8 (1998)
Acknowledgements
We thank Andrej Bauer, Juhan-Peep Ernits, Niccolò Veltri, and Niels Voorneveld for useful discussions. We also thank one of the reviewers for drawing our attention to the recent work on presenting Fitch-style modal types in terms of parametric right adjoints, and its relationship to the work presented in this paper. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0024.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2023 The Author(s)
About this paper
Cite this paper
Ahman, D. (2023). When Programs Have to Watch Paint Dry. In: Kupferman, O., Sobocinski, P. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2023. Lecture Notes in Computer Science, vol 13992. Springer, Cham. https://doi.org/10.1007/978-3-031-30829-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-031-30829-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-30828-4
Online ISBN: 978-3-031-30829-1
eBook Packages: Computer ScienceComputer Science (R0)