Categorical Semantics for Functional Reactive Programming
with Temporal Recursion and Corecursion
Wolfgang Jeltsch
TTÜ Küberneetika Instituut
Tallinn, Estonia
wolfgang@cs.ioc.ee

Functional reactive programming (FRP) makes it possible to express temporal aspects of computations
in a declarative way. Recently we developed two kinds of categorical models of FRP: abstract process
categories (APCs) and concrete process categories (CPCs). Furthermore we showed that APCs
generalize CPCs. In this paper, we extend APCs with additional structure. This structure models
recursion and corecursion operators that are related to time. We show that the resulting categorical
models generalize those CPCs that impose an additional constraint on time scales. This constraint
boils down to ruling out ω-supertasks, which are closely related to Zeno’s paradox of Achilles and the
tortoise.

1

Introduction

Functional reactive programming (FRP) makes it possible to express temporal aspects of computations in
a declarative way. Traditional FRP is based on behaviors and events, which denote time-varying values
and values attached to times, respectively. There is a Curry–Howard correspondence between traditional
FRP and an intuitionistic temporal logic with “always” and “eventually” modalities [6, 5]. Thereby the
type constructor for behaviors corresponds to “always,” and the type constructor for events corresponds to
“eventually.”
Extending the temporal logic with “until” operators leads to an extended variant of FRP. Thereby
proofs of “until” propositions correspond to a new class of FRP constructs, which we call processes.
Processes in the FRP sense combine continuous and discrete aspects and generalize behaviors and events
[7, Section 2]. We give an introduction to FRP with processes in Section 2.
We have developed two kinds of models of FRP with processes, which can also be used to model
temporal logic with “until:”
Abstract process categories (APCs) [8] are defined purely axiomatically. They are an extension of
temporal categories [6], which in turn build on categorical models of intuitionistic S4 [9, 2].
Concrete process categories (CPCs) [7] are not defined in a purely axiomatic manner, but use concrete
constructions to express time-dependence of type inhabitance and causality of FRP operations.
Abstract process categories generalize concrete process categories. We describe APCs in Section 3 and
CPCs in Section 5.
The aim of this paper is to extend APCs and CPCs in order to model recursion and corecursion on
processes. We make the following contributions:
• In Section 4, we develop APCs with recursion and corecursion (R-APCs). R-APCs extend APCs
with recursive comonad and completely iterative monad structures that model recursion and corecursion on processes. The extensions to APCs arise naturally as extensions of ideal comonad and
ideal monad structures that APCs already contain.
N.R. Krishnaswami and P.B. Levy (Eds.):
Mathematically Structured Functional Programming 2014 (MSFP 2014).
EPTCS 153, 2014, pp. 127–142, doi:10.4204/EPTCS.153.9

© Wolfgang Jeltsch
This work is licensed under the
Creative Commons Attribution License.

128

Categorical Semantics for FRP with Temporal Recursion and Corecursion
• In Section 6, we develop CPCs with recursion and corecursion (R-CPCs). R-CPCs differ from
CPCs in that they impose an additional constraint on time scales. This constraint boils down to
ruling out ω-supertasks [11]. We show that R-APCs generalize R-CPCs.
We discuss related work in Section 7 and give conclusions and an outlook on further work in Section 8.

2

Functional Reactive Programming with Processes

The FRP dialect we consider here is based on a linear notion of time. However the time scale does not
need to be discrete; so the time domain can be any totally ordered set. Type inhabitance is time-dependent,
which means that every FRP type corresponds to a time-indexed family of sets of inhabitants.
Besides the ordinary type constructors 1, 0, ×, +, and →, our FRP dialect has two binary type
constructors B000 and B100 , which we call the strong and the weak basic process type constructor. Both have
higher precedence than the other binary type constructors.
A value that inhabits a type τ1 B000 τ2 at a time t corresponds to a tuple with the following elements:
• a time t 0 > t
• a function h that maps each time t 00 with t < t 00 < t 0 to a value that inhabits τ1 at t 00
• a value y that inhabits τ2 at t 0
The function h denotes a time-varying value that exists between times t and t 0 . We call this time-varying
value the continuous part of the process. The pair (t 0 , y) denotes an event that occurs at time t 0 and carries
the value y. We call this event the terminal event of the process.
A value that inhabits a type τ1 B100 τ2 at a time t is either a process that inhabits τ1 B000 τ2 at t or a
time-varying value of type τ1 that starts immediately after t and persists forever. We regard constructs of
the latter kind as special processes that never terminate and thus have an infinite continuous part and no
terminal event.
An inhabitant of a type τ1 B000 τ2 or τ1 B100 τ2 has a continuous part that assigns values only to future
times. We define type constructors B00 and B10 for processes that start at the present time:
τ1 B00 τ2 = τ1 × τ1 B000 τ2

τ1 B10 τ2 = τ1 × τ1 B100 τ2

(1)

A pair (x, p) represents a process that starts with x as the initial value of its continuous part, and continues
like the process p.
An inhabitant of a type τ1 B00 τ2 or τ1 B10 τ2 can only terminate in the future. We define type constructors
B0 and B1 for processes that may terminate at the present time:
τ1 B0 τ2 = τ2 + τ1 B00 τ2

τ1 B1 τ2 = τ2 + τ1 B10 τ2

(2)

A value ι1 (y) represents a process whose terminal event occurs immediately and carries the value y, while
a value ι2 (p) represents the process p, which does not terminate immediately.
From the process type constructors, we derive the type constructors 0 , , ^ 0 , and ^ as follows:
0 τ = τ B100 0

τ = τ B10 0

(3)

^ τ=1

^τ = 1 B0 τ

(4)

0

B00

τ

Inhabitants of types 0 τ and τ are non-terminating time-varying values and are called behaviors.
Inhabitants of types ^ 0 τ and ^τ are events.

129

Wolfgang Jeltsch

The FRP dialect described above corresponds to an intuitionistic temporal logic via a Curry–Howard
isomorphism. Thereby time-dependent type inhabitance is related to time-dependent trueness of temporal
propositions. The type constructors B0 and B1 correspond to the strong and weak “until” operators U
and W from linear-time temporal logic (LTL), and the type constructors  and ^ correspond to the
“always” and “eventually” modalities.

3

Abstract Process Categories

Abstract process categories (APCs) are axiomatically defined categorical models of FRP with processes,
which we developed recently [8]. They are an extension of temporal categories, which are models of FRP
with behaviors and events, but without processes [6]. In this section, we give an introduction to APCs.

3.1

The Basics

An APC is a category C with some additional structure. FRP types are modeled by objects of C. If objects
A and B model FRP types τ1 and τ2 , the morphisms from A to B model operations that turn every value
that inhabits τ1 at some time into a value that inhabits τ2 at the same time.
Since FRP has the usual type constructors for finite products, finite sums, and function spaces, we
require C to be a cartesian closed category (CCC) with finite coproducts.

3.2

Temporal Functors

Let 2 denote the interval category, that is, the category with exactly two objects 0 and 1 and a single
non-identity morphism w : 0 → 1. Let furthermore Q be the category 2 × C × C. We require the existence
00 B for
of a functor B00 : Q → C, which we call the basic temporal functor. We use the notation A BW
00
00
00
B (W, A, B). We model the process type constructors B0 and B1 by the partial functor applications B000
and B100 , which are themselves functors from C × C to C.
Every inhabitant of a type τ1 B000 τ2 corresponds to an inhabitant of τ1 B100 τ2 . So there should
be an operation that performs a type conversion from B000 to B100 . We use the natural transformation
00
00
B00
w : B0 → B1 to model this operation.
From the functor B00 , we derive functors B0 , B : Q → C that model the type constructors B00 , B10 , B0 ,
and B1 as well as functors 0 , , ^ 0 , ^ : C → C that model the type constructors for behaviors and events:
0
00
A BW
B = A × A BW
B

 A=
0

^ B=
0

A B100 0
1 B00 B

0
A BW B = B + A BW
B

A =

A B10

(5)

0

(6)

^B = 1 B0 B

(7)

We call the functors introduced in (5) through (7) derived temporal functors.
APCs do not necessarily use the category 2 to model how weak a process type constructor is. Any
category W with finite products is allowed instead. In particular, we can use any category that corresponds
to a partially ordered set with finite meets. This makes it possible to model more advanced termination
properties. An example of such a property is termination with an upper bound on the termination time.
We discuss this example in Subsection 5.2.

130

3.3

Categorical Semantics for FRP with Temporal Recursion and Corecursion

Process Expansion and Joining

An APC contains a natural transformation θ 00 with


00
00
0
00
θW,
A, B : A BW B → A BW B BW B .
This natural transformation models an FRP operation that turns a process p into a process p0 such that the
following holds:
• The process p0 terminates if and only if p terminates.
• The terminal event of p0 , if any, is the terminal event of p.
• The value of the continuous part of p0 at a time t is the suffix of p that starts at t.
We call this FRP operation process expansion. We derive variants of θ 00 that work with B0 and B instead
of B00 :


0
0
0
0
θW,
:
A
B
B
→
A
B
B
BW
B
W
W
A, B
D
E
0
00
0
θW,
(8)
A, B = id ABW B , θ W, A, B ◦ π2


0
θW, A, B : A BW B → A BW
B BW B
0
θW, A, B = id B + θW,
A, B

(9)

Besides the natural transformation θ 00 , an APC also contains a natural transformation ϑ00 with
00
00
00
ϑW,
A, B : A BW ( A BW B) → A BW B .

This natural transformation models an FRP operation that turns a process p into a process p0 such that the
following holds:
• If p terminates, and its terminal event carries a process p∗ , then p0 is the result of concatenating the
continuous part of p and the process p∗ .
• If p does not terminate, then p0 does not terminate, and the continuous part of p0 is the continuous
part of p.
We call this FRP operation process joining. We derive variants of ϑ00 that work with B0 and B instead
of B00 :
0
0
0
ϑW,
A, B : A BW ( A BW B) → A BW B
0
00
ϑW,
A, B = id A × ϑW, A, B

(10)

ϑW, A, B : A BW ( A BW B) → A BW B
f
g
0
ϑW, A, B = id ABW B , ι2 ◦ ϑW,
A, B

(11)

The natural transformations θ 00 and ϑ00 have tofulfill certain coherence
conditions. Regarding θ 00 , we

00
00
require that for all W ∈ Ob(W ) and B ∈ Ob(C), − BW B, θW, −, B is an ideal comonad.
Definition 1 (Ideal comonad). Let C be a category with binary products, let U 0 be an endofunctor on C,
and let δ 0 : U 0 → U 0 (Id × U 0 ) be a natural transformation. We define U, ε, and δ as follows:
U : C→C

ε : U → Id

δ : U → UU

U = Id × U

ε = π1

δ = hidU , δ 0 ◦ π2 i

0

The pair (U 0 , δ 0 ) is an ideal comonad on C if and only if the diagram in Figure 1 commutes.

(12)

131

Wolfgang Jeltsch

U0

U 0ε

U 0δ

U 0U

U 0UU

δ0

idU 0

δ 0U

U0

δ0

U 0U

Figure 1: Coherence of an ideal comonad
00
ABW
ι1

00 B
A BW

00
ABW
ϑ W , A, B

00 ( A B
A BW
W B)

00 ( A B
A BW
W ( A BW B))
00
ϑW
, A, AB

00
ϑW
, A, B

id AB00

WB

WB

00 B
A BW

00 ( A B
A BW
W B)

00
ϑW
, A, B

Figure 2: Coherence of process joining
Regarding ϑ00 , we require that the diagram in Figure 2 commutes. This coherence condition implies
0 −, ϑ 0
op
that every pair A BW
W, A, − is an ideal monad, that is, an ideal comonad on C . Note that we
obtain a diagram for the coherence condition of such an ideal monad by taking the diagram in Figure 2
and replacing B00 and ϑ00 with B0 and ϑ0 .
Finally we require that the diagram in Figure 3 commutes. This ensures that θ 00 and ϑ00 interact
properly.

3.4

Process Merging and the Canonical Nonterminating Process

There are additional constraints on APCs, which ensure that an APC also models two other operations:
process merging and the construction of the sole value of 1 B100 0, which is called the canonical nonterminating process. We do not discuss these additional constraints here, because they are not fundamentally
related to our extension of APCs. We just mention them in the definition of APCs in the next subsection.

00
A BW

( A BW B)

00
θW
, A, AB

WB




0 (A B
00
A BW
W B) BW ( A BW B)

00
ϑW
, A, B

00 B
A BW

0
00
ϑW
, A, B BW θ W , A, B

00
θW
, A, B




0 B B00 B
A BW
W


00
ϑW
0 B, B
, ABW





0 B B00
0 B B
A BW
A BW
W B
W

Figure 3: Coherence between process expansion and joining

132

3.5

Categorical Semantics for FRP with Temporal Recursion and Corecursion

Summary

Let us now state the complete definition of abstract process categories.
Definition 2 (Abstract process category). Let W be a category with finite products, and let C be a CCC
with finite coproducts. Furthermore let B00 be a functor from W × C × C to C, let B0 and B be defined as
in (5), and let θ 00 and ϑ00 be natural transformations with the following typings:


00
00
0
00
θW,
A, B : A BW B → A BW B BW B
00
00
00
ϑW,
A, B : A BW ( A BW B) → A BW B

The tuple (W, C, B00 , θ 00 , ϑ00 ) is an abstract process category (APC) if and only if the following propositions hold:


00 B, θ 00
• For all W ∈ Ob(W ) and B ∈ Ob(C), − BW
W, −, B is an ideal comonad.
• For all W ∈ Ob(W ) and A, B ∈ Ob(C), the diagrams in Figures 2 and 3 commute where θ, ϑ0 ,
and ϑ are defined as in (9), (10), and (11).
D
E
• The natural transformation χ100 , χ200 with


00
0
0
χ 00
i : ( A1 × A2 ) BW1 ×W2 B1 × B2 + B1 × A2 BW2 B2 + A1 BW1 B1 × B2
00
→ Ai BW
Bi
i
00
00
χ 00
i = ϑWi , A i , B i ◦ πi Bπ i [ι1 ◦ πi , ιi ◦ πi , ι3−i ◦ πi ]

(13)

is an isomorphism.
• The morphism !1B100 0 is an isomorphism.
The third and fourth of the above propositions refer to process merging and the canonical nonterminating process mentioned in Subsection 3.4.

4

APCs with Recursion and Corecursion

In Subsection 3.3, we saw that every APC comprises ideal comonads and ideal monads based on temporal
functors. There exists a special kind of ideal comonads, called recursive comonads, which captures a
form of comonadic recursion. Likewise there exists a special kind of ideal monads, called completely
iterative monads, which captures a form of monadic corecursion. In this section, we introduce APCs
with recursion and corecursion (R-APCs), which comprise recursive comonads and completely iterative
monads that model recursion and corecursion on processes.

4.1

Corecursion on Processes



0 −, ϑ 0
If (W, C, B00 , θ 00 , ϑ00 ) is an APC, then every pair A BW
W, A, − is an ideal monad. We extend the
structure of APCs by requiring that every such pair is a completely iterative monad. Completely iterative
monads are defined, for example, by Milius [12, Definition 5.5]. We use a definition that is different from
the one by Milius, but nevertheless equivalent to it. We compare both definitions in Appendix A, where
we also list the advantages that our definition has in our opinion.

133

Wolfgang Jeltsch
f∞

C

T0B
µ 0B

f

T 0 (B + C)

T 0 (id B + f ∞ )

T 0 (B + T 0 B)

Figure 4: Condition for a morphism f ∞ of a completely iterative monad
Definition 3 (Completely iterative monad). Let C be a category with binary coproducts. A pair (T 0 , µ0 )
is a completely iterative monad on C if and only if it is an ideal monad on C, and for every morphism
f : C → T 0 (B + C), there exists a unique morphism f ∞ : C → T 0 B for which the diagram in Figure 4
commutes.


0 −, ϑ 0
By requiring that every pair A BW
W, A, − is a completely iterative monad, we ensure that for
0 (B + C), there is a corresponding morphism f ∞ : C → A B0 B. Let u
every morphism f : C → A BW
W
and u ∞ be the FRP operations that f and f ∞ model, and let z be a value from the domain of u and u ∞ .
The diagram in Figure 4 tells us how the process u ∞ (z) is defined:
• If u(z) terminates, and its terminal event carries a value ι1 (y), then u ∞ (z) terminates at the same
time as u(z), the continuous part of u ∞ (z) is the continuous part of u(z), and the terminal event of
u ∞ (z) carries the value y.
• If u(z) terminates, and its terminal event carries a value ι2 (z 0 ), then u ∞ (z) is the result of concatenating the continuous part of u(z) and the process u ∞ (z 0 ).
• If u(z) does not terminate, then u ∞ (z) does not terminate, and the continuous part of u ∞ (z) is the
continuous part of u(z).
Note that in the second case, u ∞ (z) is defined in terms of u ∞ (z 0 ), but only the suffix of u ∞ (z) that starts
at the termination time of u(z) actually depends on u ∞ (z 0 ). The operator − ∞ models corecursion on
processes.
We derive a variant of − ∞ that works with B instead of B0 . We use the notation − ∞ also for this
variant. This overloading of notation is possible, because we can always deduce from the types which
0 C into a morphism f ∞
variant of − ∞ is meant. The B-variant turns every morphism f : C → B + A BW
that is defined as follows:
f ∞ : C → A BW B


∞
0
f ∞ = id B + id A Bid
f
◦f
W

(14)

Note that the − ∞ on the right-hand side refers to the original B0 -variant. There is also a variant of − ∞ that
00 (B + A × C) into a morphism f ∞ that is defined
works with B00 . It turns every morphism f : C → A BW
as follows:
00
f ∞ : C → A BW
B


00
00
∞
f ∞ = ϑW,
◦
id
B
(id
+
(id
×
f
)
)
◦f
A
B
A
A, B
idW

Again the − ∞ on the right-hand side refers to the original B0 -variant.

(15)

134

Categorical Semantics for FRP with Temporal Recursion and Corecursion
f∗

U0 A

C

δ 0A

f

U 0 ( A × C)

U 0 (id A × f ∗ )

U 0 ( A × U 0 A)

Figure 5: Condition for a morphism f ∗ of a recursive comonad

4.2

Recursion on Processes



00 B, θ 00
We saw in Subsection 3.3 that every pair − BW
W, −, B is an ideal comonad. We extend the structure
of APCs by requiring that every such pair is a recursive comonad. The notion of recursive comonad
is dual to the notion of completely iterative monad. So a recursive comonad on C is just a completely
iterative monad on C op . We give an explicit definition nevertheless.
Definition 4 (Recursive comonad). Let C be a category with binary products. A pair (U 0 , δ 0 ) is a recursive
comonad on C if and only if it is an ideal comonad on C, and for every morphism f : U 0 ( A × C) → C,
there exists a unique morphism f ∗ : U 0 A → C for which the diagram in Figure 5 commutes.


00 B, θ 00
By requiring that every pair − BW
W, −, B is a recursive comonad, we ensure that for every
00 B → C, there is a corresponding morphism f ∗ : A B00 B → C. Let u and u ∗
morphism f : ( A × C) BW
W
∗
be the FRP operations that f and f ∗ model,
 and
 let p be a process from the domain of u . The diagram in
Figure 5 tells us that the value u ∗ (p) is u p† where p† is defined by the following statements:
• The process p† terminates if and only if p terminates.
• The terminal event of p† , if any, is the terminal event of p.
• The value of the continuous part of p† at a time t is (x,u ∗ (p0 )) where x is the value of the continuous
part of p at t, and p0 is the suffix of p that follows t.
Note that u ∗ (p) is defined in terms of u ∗ (p0 ), but p0 is a proper suffix of p. The operator − ∗ models
recursion on processes.
We derive a variant of − ∗ that works with B0 instead of B00 . We use the notation − ∗ also for this
00 B → C into a morphism f ∗ that is defined as
variant. The B0 -variant turns every morphism f : A × C BW
follows:
0
f ∗ : A BW
B→C


∗
00
f ∗ = f ◦ id A × f Bid
id
B
W

(16)

Note that this construction is dual to the construction of the B-variant of − ∞ .

4.3

Summary

We formulate the definition of R-APCs based on the above explanations.
Definition 5 (APC with recursion and corecursion). An APC with recursion and corecursion (R-APC) is
an APC (W, C, B00 , θ 00 , ϑ00 ) for which the following holds:


00 B, θ 00
• For all W ∈ Ob(W ) and B ∈ Ob(C), − BW
W, −, B is a recursive comonad.


0 −, ϑ 0
• For all W ∈ Ob(W ) and A ∈ Ob(C), A BW
W, A, − is a completely iterative monad.

135

Wolfgang Jeltsch

5

Concrete Process Categories

Concrete process categories (CPCs) are models of FRP with processes that use concrete categorical
constructions to express time-dependence of type inhabitance and causality of FRP operations. They are
described in detail in an earlier publication of ours [7, Section 3]. Here we only give a short introduction
to CPCs.

5.1

Core Structure

Let (T, ≤) be a totally ordered set, and let B be a CCC with finite coproducts. We use (T, ≤) to model
the time scale, and B to model ordinary types and functions. Based on (T, ≤), we construct a category I,
which we call the temporal index category of (T, ≤).
Definition 6 (Temporal index category). The temporal index category of a totally ordered set (T, ≤) is the
category I for which the following holds:

homI

Ob(I) = { (t,t o ) ∈ T × T | t ≤ t o }


 t,t o ,t o0
if t = t 0 and t o ≤ t o0
 
(t 0 ,t o0 ), (t,t o ) = 
∅
otherwise


(17)
(18)

We model FRP types and FRP operations by the functor category B I . Let A be an object of B I that
models an FRP type τ. For every object (t,t o ) of I, the object A(t,t o ) of B deals with the FRP values
that inhabit τ at t; it describes the type whose inhabitants give the information we have about these FRP


values at t o . We call t o the observation time. For every morphism t,t o ,t o0 of I, the morphism A t,t o ,t o0
models the function that turns information we have at t o0 into information we have at t o by forgetting all
information acquired after t o
The definition of CPCs requires the category B to have some additional properties, which are necessary
for modeling function types and process types in FRP.
Definition 7 (Concrete process category). Let (T, ≤) be a totally ordered set, let I be its temporal index
category, and let B be a CCC with finite coproducts that
coproducts of families
R has all products and
00
00
A
t,
t
0
(
)
indexed by intervals (t,t ) ⊆ T and all ends of the form t 00 ∈[t, t 0 ] B(t,t )
where A, B ∈ B I . Then
the tuple (T, ≤, B) is a concrete process category (CPC). The actual category that (T, ≤, B) denotes is the
functor category B I .

5.2

The Basic Temporal Functor

The basic temporal functor of a CPC [8, Subsection 4.3] models the weak basic process type constructor
as well as process type constructors that put upper bounds on termination times.
We define the totally ordered set (T∞ , ≤∞ ) such that T∞ = T ∪ {∞} and
t 1 ≤∞ t 2 ⇔ t 1 ≤ t 2 ∨ t 2 = ∞ .
Let W be the category of (T∞ , ≤∞ ). We use W to model constraints regarding termination. Thereby any
object t b ∈ T stands for termination at or before the time t b , and the object ∞ stands for the absence of
any termination guarantees. We define the basic temporal functor as follows.

136

Categorical Semantics for FRP with Temporal Recursion and Corecursion

Definition 8 (Basic temporal functor of a CPC). Let (T, ≤, B) be a CPC, and let W be defined as above.
The basic temporal functor of (T, ≤, B) is the functor B00 : W × B I × B I → B I with


A B00
tb


0




B (t,t o ) = 
Stb



0
S + Q 0
t ∈(t, t o ] A(t ,t o )
 to


where for every t ∗ ∈ T, St ∗ is defined as follows:

a
Y
 
St ∗ =

t 0 ∈(t, t ∗ ]

t 00 ∈(t, t 0 )

if t b < t
if t ≤ t b ≤ t o
if t o < ∞ t b



(19)



A(t 00 ,t o )  × B(t 0 ,t o ) 



(20)

The above definition is actually incomplete. A complete definition would also define the following:


 
00 B i where W ∈ Ob(W ), A, B ∈ Ob B I , and i ∈ Mor(I)
• morphisms A BW


 
00 g
• morphisms f Bid
where
W
∈
Ob(W
),
f
,
g
∈
Mor
B I , and I ∈ Ob(I)
W
I
 

I , and I ∈ Ob(I)
• morphisms id A B00
w id B I where w ∈ Mor(W ), A, B ∈ Ob B
However
defining
these things is a mostly mechanical task. In particular, the definition of morphisms


00 g
can
be
derived from (19) and (20) by replacing 0 with id0 and object expressions of the form
f Bid
W
I
C(t,t o ) with morphism expressions of the form h (t, to ) .

5.3

Relationship to Abstract Process Categories

APCs generalize CPCs. This is expressed by the following theorem.
Theorem 1. Let (T, ≤, B) be a CPC, let I be the temporal index category of (T, ≤), let B00 be the basic
temporal functor of (T, ≤, B), and let W be the category of the totally ordered set (T∞ , ≤∞ ) that is
defined
as described in Subsection 5.2. Then there exist natural transformations θ 00 and ϑ00 such that

W, B I , B00 , θ 00 , ϑ00 is an APC.
Please see our earlier work [8, proof of Theorem 10] for a proof of this theorem.

6

CPCs with Recursion and Corecursion

According to Theorem 1, every CPC gives rise to an APC. However there is no guarantee that this APC is
also an R-APC. In this section, we develop CPCs with recursion and corecursion (R-CPCs). R-CPCs are
a special kind of CPCs whose corresponding APCs are R-APCs.

6.1

Enabling Corecursion on Processes



Let (T, ≤, B) be a CPC. Let furthermore W, B I , B00 , θ 00 , ϑ00 be the APC it induces according to
Theorem 1. This APC models corecursion on processes if and only if for every morphism f : C →
A B0tb (B + C), there exists a unique morphism f ∞ for which the following holds:
f ∞ : C → A B0tb B


0
∞
f ∞ = ϑ0tb, A, B ◦ id A Bid
(id
+
f
)
◦f
B
t
b

(21)

137

Wolfgang Jeltsch

From the definition of B0 in (5) and the definition of the basic temporal functor in Subsection 5.2, it
follows that (21) is true if and only if for all t,t o ∈ T with t ≤ t o , we have


∞
0
f (t,
◦ (id A × h) ◦ f (t, to )
(22)
t o ) = ϑ t b, A, B
(t, t o )

where h is defined as follows:

id0
if t b < t







`

∞
if t ≤ t b ≤ t o
t 0 ∈(t, t b ] id × id + f (t 0, t o )
h=









 `

∞
+ id if t o < ∞ t b
 t 0 ∈(t, to ] id × id + f (t 0, to )

(23)

∞
∞
0
Equations (22) and (23) define f (t,
t o ) in terms of morphisms f (t 0, t o ) with t > t. So if the order ≥ on the
∞
set { t ∈ T | t ≤ t o } is well-founded, (22) and (23) define f (t, to ) by well-founded recursion with recursion
parameter t. As a consequence, there exists a unique f ∞ that fulfills (21).
Based on the above considerations, we require for an R-CPC that for all t ∈ T, the order ≥ on
{ t 0 ∈ T | t 0 ≤ t } is well-founded, which means that we cannot have an infinite ascending sequence of
times that all lie before a certain time. This makes ω-supertasks [11] impossible, which, for example,
implies that the sequence of actions described in Zeno’s paradox of Achilles and the tortoise cannot occur.
Note however that we still allow time scales that are quite different from the discrete time scale (, ≤).

For example, z + 1/n z ∈  ∧ n ∈  \ {0} with the usual ordering of rational numbers is still a
perfectly acceptable time scale.

6.2

Enabling Recursion on Processes



The APC W, B I , B00 , θ 00 , ϑ00 induced by a CPC (T, ≤, B) models recursion on processes if and only if
∗
for every morphism f : ( A × C) B00
t b B → C, there exists a unique morphism f for which the following
holds:
f ∗ : A B00
tb B → C


00
00
f ∗ = f ◦ (id A × f ∗ ) Bid
id
B ◦ θ t b, A, B
t
b

Equation (24) is true if and only if for all t,t o ∈ T with t ≤ t o , we have


∗
00
f (t,
t o ) = f (t, t o ) ◦ h ◦ θ t b, A, B
(t, t o )

(24)

(25)

where h is defined as follows:

id0




`

h =  t 0 ∈(t, tb ] s t 0



Q

∗
` 0
0 +
0 ∈(t, t ] id × f 0
s
t
t
∈(t,
t
]
t
o
o
(t , t o )



Y 

s t 0 = 
id × f (t∗ 00, to )  × id



if t b < t
if t ≤ t b ≤ t o
if t o < ∞ t b

(26)

(27)

t 00 ∈(t, t 0 )

∗
Equations (25) through (27) define f (t,
t o ) by well-founded recursion, assuming that the order ≥ on the set
{ t ∈ T | t ≤ t o } is well-founded. As a consequence, there exists a unique f ∗ that fulfills (24).

138

6.3

Categorical Semantics for FRP with Temporal Recursion and Corecursion

Summary

We formulate the definition of R-CPCs based on the above explanations.
Definition 9 (CPC with recursion and corecursion). A CPC (T, ≤, B) is a CPC with recursion and
corecursion (R-CPC) if and only if for all t ∈ T, the order ≥ on { t 0 ∈ T | t 0 ≤ t } is well-founded.
We have developed R-CPCs such that they give rise to R-APCs. We state the relationship between
R-CPCs and R-APCs in the following theorem.
Theorem 2. The APC that is induced by an R-CPC according to Theorem 1 is an R-APC.

7

Related Work

We can build R-APCs by taking the categorical semantics of the intuitionistic modal logic IK [1] and
successively adding more structure. This leads us first to intuitionistic S4 categories [6, Section 4], which
are closely related to the categorical semantics of intuitionistic S4 variants by Kobayashi [9] and Bierman
and de Paiva [2]. Subsequent additions to intuitionistic S4 categories lead us to temporal categories [6,
Sections 5 and 6], from there to APCs [8], and finally to R-APCs.
Krishnaswami and Benton [10] model FRP categorically based on 1-bounded ultrametric spaces.
Their semantics ensures that morphisms only model causal functions, which is also a key property of
CPCs. However they model only behaviors, not events or even processes. Furthermore they require
the time scale to be discrete. Although this is a restriction, it makes it possible to model recursion on
behaviors.
Cave et al. [4] present an FRP calculus that features inductive and coinductive types and a type
constructor that corresponds to the “next” modality of LTL. The authors show that process types are
definable within their calculus. We strongly conjecture that their calculus also allows for the definition of
recursion and corecursion operators on processes. The downside of their solution is that it is fundamentally
tied to discrete time.
Jeffrey [5, Section 2] defines categories RSet and DRSet. The morphisms of RSet model causal
functions on time-varying values, and the morphisms of DRSet model causal functions that produce
output values based only on a finite history. Jeffrey also introduces a fixed point operator ifix, which is
similar to our − ∗ operator for recursion, but uses time-varying values that lie in the past, while − ∗ uses
processes, whose continuous parts lie in the future. Consequently Jeffrey requires that ≤, and not ≥, is
well-founded on certain intervals.
Birkedal et al. [3] model guarded recursion by the topos of trees. The topos of trees is the category
op
S = SetN , where N is the category of the ordered set (, ≤). If A ∈ Ob(S) models a type τ, an
object An with n ∈  models the type whose inhabitants give the information we have about inhabitants
of τ after n recursion steps, and a morphism Av with v : m → n models the function that forgets the
information acquired during recursion steps n + 1 through m. There is a close connection between this
development and CPCs. Consider the CPC (, ≤, Set). Let I be the temporal index category of this
CPC, and let E be the full subcategory of SetI that is induced
 by those objects that model types with
I
time-independent inhabitance, that is, by those A ∈ Ob Set with ∀k, l, n ∈  . A(k, k + n) = A(l, l + n)
and a similar condition for morphisms. Then the categories S and E are isomorphic. Birkedal et al.
define a fixed point operator based on a “later” type constructor that corresponds to the “next” modality of
temporal logic. Studying the relationship between this fixed point operator and our structure for recursion
and corecursion on processes remains a task for the future.

139

Wolfgang Jeltsch
f†

C

TB
id B +µ 0B

f

B + T 0 (B + C)

id B +T 0 [ι 1, f † ]

B + T 0T B

Figure 6: Condition for a morphism f † of a Milius-style completely iterative monad

8

Conclusions and Further Work

We have developed R-APCs and R-CPCs, which are categorical models of FRP with recursion and
corecursion on processes. R-APCs are defined purely axiomatically, while R-CPCs use concrete structure
to express time-dependence of type inhabitance and causality of FRP operations. We have furthermore
shown that R-APCs generalize R-CPCs.
In the future, we want to develop categorical models of FRP with support for mutable state. Another
goal of ours is to implement FRP in mainstream functional programming languages such that the interface
directly reflects the abstract categorical semantics.

A

Changes in the Completely Iterative Monad Definition

Milius [12, Definition 5.5] defines completely iterative monads differently from us. A simplified version
of his definition is as follows.
Definition 10 (Milius-style completely iterative monad). Let C be a category with binary coproducts. A
pair (T 0 , µ0 ) is a Milius-style completely iterative monad on C if and only if it is an ideal monad on C,
and for every morphism f : C → B + T 0 (B + C), there exists a unique morphism f † : C → T B with
T = Id + T 0 for which the diagram in Figure 6 commutes.
We do not use this definition in this paper, because in our opinion, it has disadvantages:
• The morphism f : C → B + T 0 (B + C) gives us two points per iteration where iterating can come
to an end. These two points correspond to the two sums in the codomain of f . However only one
such point is necessary.
• The codomain of f † uses the derived functor T instead of the actual ideal monad functor T 0 ,
weakening the type of f † .
However our own definition is equivalent to the one by Milius. This fact is expressed by the following
two theorems.
Theorem 3. If (T 0 , µ0 ) is a completely iterative monad on a category C according to Definition 3, then it
is a Milius-style completely iterative monad on C.
Proof. Let (T 0 , µ0 ) be a completely iterative monad according to Definition 3, and let g be an arbitrary
morphism with g : C → B + T 0 (B + C). We have to show that there exists a unique morphism g † for
which the following holds:
g† : C → B + T 0 B


f
g
g † = id B + µ0B ◦ T 0 ι1 , g †
◦g

(28)

140

Categorical Semantics for FRP with Temporal Recursion and Corecursion

We define f as follows:
f : T 0 (B + C) → T 0 (B + T 0 (B + C))
f = T 0 [ι1 , g]

(29)

Since (T 0 , µ0 ) is a completely iterative monad according to Definition 3, there exists a unique f ∞ for
which the following holds:
f ∞ : T 0 (B + C) → T 0 B
f ∞ = µ0B ◦ T 0 (id B + f ∞ ) ◦ f

(30)

According to (29), we have
µ0B ◦ T 0 (id B + f ∞ ) ◦ f = µ0B ◦ T 0 (id B + f ∞ ) ◦ T 0 [ι1 , g]
= µ0B ◦ T 0 [ι1 , (id B + f ∞ ) ◦ g] ,

(31)

so (30) is equivalent to the following equation:
f ∞ = µ0B ◦ T 0 [ι1 , (id B + f ∞ ) ◦ g]

(32)

We define the functions q and r on morphisms as follows:
q : Hom(T 0 (B + C),T 0 B) → Hom(C, B + T 0 B)
q(a) = (id B + a) ◦ g

(33)

r : Hom(C, B + T 0 B) → Hom(T 0 (B + C),T 0 B)
r (b) = µ0B ◦ T 0 [ι1 , b]

(34)

We know that there exists a unique f ∞ with
f ∞ = r (q( f ∞ )) ,

(35)

and we have to prove that there exists a unique g † with
  
g† = q r g†
.

(36)

From (35), it follows that
q( f ∞ ) = q(r (q( f ∞ ))) ,
so g † = q( f ∞ ) fulfills (36). On the other hand, if we have a g † that fulfills (36), we know that
 
   
r g† = r q r g†
.

(37)

(38)

 
Because there is only one f ∞ that fulfills (35), it follows that f ∞ = r g † . From this, we get
  
g † = q r g † = q( f ∞ ) .
So g † = q( f ∞ ) is the unique solution of (36).

(39)


141

Wolfgang Jeltsch

Theorem 4. If (T 0 , µ0 ) is a Milius-style completely iterative monad on a category C, then it is a completely
iterative monad on C according to Definition 3.
Proof. Let (T 0 , µ0 ) be a Milius-style completely iterative monad, and let f be an arbitrary morphism with
f : C → T 0 (B + C). We have to show that there exists a unique morphism f ∞ for which the following
holds:
f ∞ : C → T0B
f ∞ = µ0B ◦ T 0 [ι1 , ι2 ◦ f ∞ ] ◦ f

(40)

We define g as follows:
g : C → B + T 0 (B + C)
g = ι2 ◦ f

(41)

Since (T 0 , µ0 ) is a Milius-style completely iterative monad, there exists a unique g † for which the following
holds:
g† : C → B + T 0 B
g


f
◦g
g † = id B + µ0B ◦ T 0 ι1 , g †

(42)

According to (41), we have


f
g


f
g
id B + µ0B ◦ T 0 ι1 , g †
◦ g = id B + µ0B ◦ T 0 ι1 , g †
◦ ι2 ◦ f
f
g
= ι2 ◦ µ0B ◦ T 0 ι1 , g † ◦ f ,

(43)

so (42) is equivalent to the following equation:
f
g
g † = ι2 ◦ µ0B ◦ T 0 ι1 , g † ◦ f

(44)

We define the functions q and r on morphisms as follows:
q : Hom(C, B + T 0 B) → Hom(C,T 0 B)
q(a) = µ0B ◦ T 0 [ι1 , a] ◦ f

(45)

r : Hom(C,T 0 B) → Hom(C, B + T 0 B)
r (b) = ι2 ◦ b

(46)

We know that there exists a unique g † with
  
g† = r q g†
,

(47)

and we have to prove that there exists a unique f ∞ with
f ∞ = q(r ( f ∞ )) .
Using reasoning analogous to the one at the end of the previous proof, we can deduce that f ∞
the unique solution of (48).

(48)

= q g † is



142

Categorical Semantics for FRP with Temporal Recursion and Corecursion

Acknowledgments
I thank Tarmo Uustalu for all the helpful discussions about the topics of this paper, and in particular, for
introducing me to completely iterative monads and recursive comonads.
This work was supported by the target-financed research theme No. 0140007s12 of the Estonian
Ministry of Education and Research and by the ERDF through the Estonian Center of Excellence in
Computer Science (EXCS) and the national ICTP project Coinduction for Semantics, Analysis, and
Verification of Communicating and Concurrent Reactive Software. I thank all tax payers in the European
Union for funding the ERDF.

References
[1] Gianluigi Bellin, Valeria de Paiva & Eike Ritter (2001): Extended Curry–Howard Correspondence for a Basic
Constructive Modal Logic. In: Proceedings of the 2nd Workshop on Methods for Modalities (M4M-2).
[2] Gavin Bierman & Valeria de Paiva (2000): On an Intuitionistic Modal Logic. Studia Logica 65(3), pp. 383–416,
doi:10.1023/A:1005291931660.
[3] Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer & Kristian Støvring (2012): First Steps in
Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. Logical Methods in Computer
Science 8(4), pp. 1–45, doi:10.2168/LMCS-8(4:1)2012.
[4] Andrew Cave, Francisco Ferreira, Prakash Panangaden & Brigitte Pientka (2014): Fair Reactive Programming.
In: Proceedings of the 41st ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages
(POPL ’14), ACM, New York, pp. 361–372, doi:10.1145/2535838.2535881.
[5] Alan Jeffrey (2012): LTL Types FRP: Linear-Time Temporal Logic Propositions as Types, Proofs as Functional
Reactive Programs. In: Proceedings of the Sixth Workshop on Programming Languages Meets Program
Verification (PLPV ’12), ACM, New York, pp. 49–60, doi:10.1145/2103776.2103783.
[6] Wolfgang Jeltsch (2012): Towards a Common Categorical Semantics for Linear-Time Temporal Logic and
Functional Reactive Programming. Electronic Notes in Theoretical Computer Science 286, pp. 229–242,
doi:10.1016/j.entcs.2012.08.015.
[7] Wolfgang Jeltsch (2013): Temporal Logic with “Until”, Functional Reactive Programming with Processes,
and Concrete Process Categories. In: Proceedings of the 7th Workshop on Programming Languages Meets
Program Verification (PLPV ’13), ACM, New York, pp. 69–78, doi:10.1145/2428116.2428128.
[8] Wolfgang Jeltsch (2014): An Abstract Categorical Semantics for Functional Reactive Programming with
Processes. In: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages Meets
Program Verification (PLPV ’14), ACM, New York, pp. 47–58, doi:10.1145/2541568.2541573.
[9] Satoshi Kobayashi (1997): Monad as Modality.
doi:10.1016/S0304-3975(96)00169-7.

Theoretical Computer Science 175(1), pp. 29–74,

[10] Neelakantan R. Krishnaswami & Nick Benton (2011): Ultrametric Semantics of Reactive Programs. In:
Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS ’11), IEEE, New
York, pp. 257–266, doi:10.1109/LICS.2011.38.
[11] Jon Pérez Laraudogoitia (2013): Supertasks. In Edward N. Zalta, editor: The Stanford Encyclopedia of
Philosophy, spring 2013 edition, Stanford University, Stanford, California. Available at http://plato.
stanford.edu/archives/spr2013/entries/spacetime-supertasks/.
[12] Stefan Milius (2005): Completely Iterative Algebras and Completely Iterative Monads. Information and
Computation 196(1), pp. 1–41, doi:10.1016/j.ic.2004.05.003.

