Introduction

Streams are a ubiquitous fundamental data structure, even more so in the realms of reactive and data floworiented computation. Semantic foundations in terms of universal coalgebra and coinduction [14] have been proposed almost twenty years ago [3,15], but remain woefully obscure to the general programming community.

Here we set out to exploit the recent development of the Sig language as a use case for coalgebraic semantics. Unlike for previous technical papers, the priority here is not on the exposition of novel theoretical foundations or practical implementations, but on the clarification and justification of already established solutions. As such it is intended for a broader audience with a general background in programming languages. Consequently, the present paper is partly a self-contained educational summary of pre-existing isolated parts of technical work, and partly a report on novel work to connect the dots. In particular, there has been a considerable rhetorical gap between the theoretical framework [17] and the implementation strategy employed by the actual compiler [18]. While the design appears fairly obvious and grounded in standard compiler constructor wisdom, a rigorous reconstruction by calculation from first principles would obviously be more satisfactory. Notable novel contributions are:

• pseudorandom number generators as illuminating examples of coinductive stream computations (2.8), (5.6);

• a method to derive operational facts from abstract coalgebraic specifications (3.12) that qualifies as a basic form of coinductive program synthesis;

• its application to a number of basic concepts of functional stream programming, resulting in rigorous justification of the plausible implementation strategy by calculation (4.6), (4.7), (5.3), (6.3).

Copyright c by the paper's authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.

We introduce concepts of universal coalgebra as we go. Statements that have been specialized for the present discussion are marked with asterisks. For a more comprehensive exposition, see [14]. The material is organized into progressive sections which discuss streams, stream transformers, composition of stream transformers, delay, and higher order function application, respectively. Section 2 also summarizes the basic working tools of the colgebraic framework. These are completely standard as in [14], but contrarily to present custom, we spell them out in non-categorical language, and add novel and domain-specific examples. By analogy, the content of sections 3 and 4 is rephrased from [14] and our own theoretical work [17].

Since the present discussion is focused on calculation of operational semantics and space is limited, the frontend features and usage of the Sig language will be mentioned only in passing. We point to our recent work [18,19] for detailed discussions.

Zeroth Order: Streams

Definition* 2.1 (Functor). A functor 1 F is a pair of homonymous constructions: One that assigns to each set X a set F (X), and another that assigns to each map f : X → Y a map F (f ) : F (X) → F (Y ).2 Definition 2.2 (Stream Functor). Fix some nonempty set A and consider the Cartesian pairing operator S A (X) = A × X. It can be extended to a functor, acting on maps as:

S A (f )(a, x) = a, f (x)

For any functor F , we can define the concepts of mathematical structures called F -coalgebras and their homomorphisms, or structure-preserving maps.

Definition* 2.3 (Coalgebra

). An F -coalgebra is a structure (X, f ), where the set X is called the carrier, and the map f : X → F (X) is called the operation.

Definition 2.4 (Stream Coalgebra Operation). Concretely, the SA -coalgebras are structures (X, f : X → A×X).

Usually it is more convenient to decompose the pair-valued map f equivalently as f 0 : X → A and f + : X → X with:

f (x) = f 0 (x), f + (x)

Algorithm 2.5. The S A -coalgebras are formal representations of enumeration procedures: The carrier X is the state space, and the operation components f 0 and f + specify, for each state, the output element from A and transition to the next state, respectively. Such a procedure is naturally executed by starting from an initial state x 0 , and collecting the outputs a n = f 0 (x n ) from successive states x n+1 = f + (x n ), as an infinite stream. In pseudocode:

exec(f0, f+)(x0): var x := x0 forever yield f0(x)

x := f+(x) Example 2.6. The default textbook example of a stream enumeration procedure is the iterative Fibonacci algorithm:

A = N X = N 2 fib 0 (a, b) = b fib + (a, b) = (a + b, a)

Its state is the pair of the next and current Fibonacci number, respectively.

Example 2.7. A procedure that is related in a non-obvious mathematical way, to be explained later in (2.19), is the following coalgebra,

A = R X = N bif 0 (n) = ϕ n √ 5 where ϕ = 1 + √ 5 2 bif + (n) = n + 1

which has simply a sequence index as its state, and thus qualifies as a closed-form generator; the projection bif 0 specifies each element of the sequence directly.

Generating streams coalgebraically goes beyond the power of classical recursive sequence definitions; the state may contain relevant information that is not available from the observable output. Typical examples that exhibit this feature are pseudorandom number generators.

Example 2.8. The family of Marsaglia's four-word xorshift random number generators [8] is specified in coalgebraic form as

A = 2 X = (2 ) 4 xsr 0 (x, y, z, w) = r xsr + (x, y, z, w) = (y, z, w, r) where r = (x ⇐ a ⇒ b) ⊕ (w ⇒ c)

where is integer word length, a, b, c are small integer constants from a table of recommendations, ⊕ is bitwise exclusive or, and the characteristic operations are combinations of exclusive or and bit shifts:

(n ⇒ k) = n ⊕ (n k) (n ⇐ k) = n ⊕ (n k)

So far, we have argued only operationally what the given examples mean. But one can do much better in the coalgebraic framework. The intuitive execution model from (2.5) can be given a formal foundation. Definition 2.9 (Coalgebra of Streams). The set of infinite streams A ω admits an S A -coalgebra operation:

s : A ω → A × A ω s 0 (α) = α 0 s + (α) n = α n+1

where s 0 and s + are commonly known as head and tail, respectively, and s −1 as cons. In order to let A vary, we write explicitly:

out A : A ω → A × A ω head A : A ω → A cons A : A × A ω → A ω tail A : A ω → A ω

We also abbreviate cons A (a 0 , α) to a 0 ; α, which saves many parentheses. Note that indices start always at zero. Definition* 2.10 (Homomorphism). Let (X, f ) and (Y, g) be F -coalgebras. A map h : X → Y is a homomorphism from (X, f ) to (Y, g) if and only if:

g(h(x)) = F (h)(f (x))

Proposition 2.11. For S A -coalgebras the homomorphism property for h from (X, f ) to (Y, g) simplifies to:

g 0 h(x) = f 0 (x) g + h(x) = h f + (x)

The S A -coalgebra homomorphisms map computations by one enumeration procedure to equivalent computations by another procedure. The coalgebra (A ω , out A ) is special, firstly in the sense that it abstracts from any actual computation by reading elements from a stream that is assumed to be given beforehands, and secondly due to the fact that it admits a particular map from any other S A -coalgebra. Proposition 2.12. Let (X, f ) be an S A -coalgebra. Then there is a map:

[ (f )] : X → A ω [ (f )](x) n = f 0 f n + (x)

Proposition 2.13. The homomorphism property (2.11) specializes for [ (f )] to:

head A [ (f )](x) = f 0 (x) tail A [ (f )](x) = [ (f )] f + (x) It is easy to see that [ (f )] is indeed a homomorphism. Proof. head A [ (f )](x) = [ (f )](x) 0 tail A [ (f )](x) n = [ (f )](x) n+1 (2.12) = f 0 f 0 + (x) (2.12) = f 0 f n+1 + (x) = f 0 (x) = f 0 f n + f + (x) (2.12) = [ (f )] f + (x) n

Proposition 2.14. The two equations of (2.13) can be combined -the recursive equivalent of the closed form (2.12), and declarative equivalent of imperative algorithm (2.5):

[ (f )](x) = f 0 (x) ; [ (f )] f + (x)

The homomorphism [ (f )] : X → A ω gives the intended denotational semantics of the pseudocode (2.5), mapping each initial state to the stream of ensuing outputs. It is natural in the sense that it is the unique homomorphism of its type. Proposition 2.15. Any homomorphism h : X → A ω between S A -coalgebras (X, f ) and (A ω , out A ), that is each map of that type satisfying (2.11), is in fact equivalent to (2.12).

Proof. By induction in n, with induction hypothesis IH:

h(x) n = f 0 f n + (x) . h(x) 0 = head A h(x) h(x) n+1 = tail A h(x) n (2.11) = f 0 (x) (2.11) = h(f + (x)) n = f 0 f 0 + (x) IH = f 0 f n + f + (x) = f 0 f n+1 + (x)

This uniqueness is an instance of an important general pattern. Definition* 2.16. An F -coalgebra (Y, g) is called final if and only if there is a unique homomorphism from any other F -coalgebra (X, f ). Proposition* 2.17. Final F -coalgebras are essentially unique; any pair of them is connected by a unique bijective homomorphism.

In that terminology, streams are "the" final S A -coalgebra, and the final semantics of enumeration algorithms. It has several nice properties, of which we can state only the first in terms of the framework established so far.

Remark 2.18. The uniqueness proof given above concisely embodies the relationship of the coalgebraic approach to streams to traditional index-subscript-based notations: The proof is the only invocation of the induction principle necessary, and only at the meta level. It establishes a coinductive definition principle: any small-step behavior map f : X → A × X gives rise to a unique big-step behavior map [ (f )] : X → A ω . Note that in coinduction, foundation via terminating base cases is neither required nor particularly useful.

Example 2.19. Now we can state the intended use and precise meaning of the above examples.

• The standard Fibonacci sequence is obtained from (2.6) as [ (fib)](1, 0).

• A near-Fibonacci sequence is obtained from (2.7) as [ (bif )](0). It has the funny property that rounding [ (bif )](0) n yields [ (f ib)](1, 0) n , which can be derived from Binet's formula.

• A stream of reasonably random-looking integer words (that pass standard statistical tests [8]) is obtained from (2.8) by applying [ (xsr)] to four seed values.

In this section, we have introduced the concepts of stream spaces as final coalgebras, and of coinductively defined streams (as a generalization of classical recursively defined sequences) as the corresponding unique homomorphisms. This idea is well established, see for instance [7]. So far, the benefits of the theoretical framework are rather modest. Straightforward intuitions are confirmed, but little further insight is produced. Things shall get more illuminating now, when input is added.

First Order: Stream Transforms

Definition 3.1. Fix some nonempty sets A and B, and consider the functor:

T AB (X) = (A → B × X) T AB (f )(k)(a) = b, f (x) where k(a) = (b, x)

Algorithmically, the T AB -coalgebras represent the category of Mealy-type stream transducers. Their operations f : 3 specify the output element from B and transition to next state, given the current state and input element from A. Again, it is sometimes convenient to consider instead the component maps

X → A → B × X, by Currying equivalent to f : X × A → B × X,f 0 : X → A → B and f + : X → A → X, with f (x)(a) = f 0 (x)(a), f + (x)(a) .

Proposition 3.2. For T AB -coalgebras the homomorphism property for h from (X, f ) and (Y, g) simplifies to:

g 0 h(x) (a) = f 0 (x)(a) g + h(x) (a) = h f + (x)(A = R B = R X = R sum 0 (x, a) = a + x dif 0 (x, a) = a − x sum + (x, a) = a + x dif + (x, a) = a

However, there is a catch; the general function space A ω → B ω is too large to be the adequate semantic domain! Namely, it turns out that for a suitable T AB -coalgebra operation f , we would have to give a component of type f 0 : (A ω → B ω ) → A → B, which is not meaningful generically, without additional knowledge of A and B. On second thought, the T AB -coalgebras specify sequential elementwise computation on streams, and the internal state X can be used to transport information forwards in time, but not backwards. As a result, all stream transforms implemented by T AB -coalgebras have the property of causality: output up to each step is determined by input only up to the same step. Definition 3.5 (Causality). Let α <n denote the sequence of the first n elements of the infinite stream α. Then we can define the space of causal stream functions:

A ω B = {k : A ω → B ω | ∀ n. α <n = α <n =⇒ k(α) <n = k(α ) <n }

The space of causal stream functions can be endowed with a T AB -coalgebra operation, by a not entirely trivial construction [17]. Proposition 3.6. For all k : A ω B we have in particular, at the first step:

head A (α) = head A (α ) =⇒ head B k(α) = head B k(α )

Proposition 3.7. The previous property ensures that there is a generic map satisfying

head AB : (A ω B) → A → B head AB (k) head A (α) = head B k(α)

with no reference to particular elements of A or B.

Definition 3.8. Now consider a related map defined by the equation:

tail AB (k)(a 0 )(α) = tail B k(a 0 ; α)

Proposition 3.9. This map can be specified in analogy to (3.7):

tail AB : (A ω B) → A → (A ω B) tail AB (k) head A (α) tail A (α) = tail B k(α)

Proposition 3.10. The pair of equations (3.7), (3.9) can be combined equivalently:

k(a 0 ; α) = head AB (k)(a 0 ) ; tail AB (k)(a 0 )(α)

The causal function space A ω B admits a T AB -coalgebra operation t, namely t 0 = head AB and t + = tail AB . This is again a final T AB -coalgebra: from any other T AB -coalgebra (X, f ) there is a unique homomorphism [ (f )], which however can not be written down in closed form quite as neatly as in (2.12).

Definition 3.11. Let (X, f ) be a T AB -coalgebra. Then there is a map:

[ (f )] : X → (A ω B) [ (f )](x)(α) n = f 0 f + . . . f + (x)(α 0 ) . . . (α n−1 ) (α n )

This makes the causality property explicit: the n-th element of [ (f )](x)(α) makes only use of up to the n-th element of the given, infinite input stream α. Causal stream computations are particularly well-behaved in online, reactive or real-time context: Assume that the elements of input are being made available at successive points in time. Once the first n elements have been obtained, the n-th output element can be computed, with a latency that depends only on the computation itself and can be determined by standard worst-case execution time analyses, but not on the environment. Thus productiveness (elementwise termination, [15]) of computations becomes a local property. Proposition 3.12. The homomorphism property (3.2) specializes for the final case to:

head AB [ (f )](x) (a 0 ) = f 0 (x)(a 0 ) tail AB [ (f )](x) (a 0 )(α) = [ (f )] f + (x)(a 0 ) (α)

The proof of validity and uniqueness of [ (f )] is completely analogous to the S A -case; refer to (2.13) and (2.15), respectively. Proposition 3.13. Specialization of (3.10) with k = [ (f )](x) and (3.12) gives the recursive equivalent of the closed form (3.11):

[ (f )](x)(a 0 ; α) = f 0 (x)(a 0 ) ; [ (f )] f + (x)(a 0 ) (α)

Algorithm 3.14. The following literal translation into Haskell syntax is a valid and useful, purely functional program:

trans :: (x -> a -> (b, x)) -> x -> [a] -> [b]

trans f x (a0 : as) = f0 x a0 : trans f (fp x a0) as where f0 x a = fst (f x a) fp x a = snd (f x a)

Example 3.15. The stream transforms of (3.4) have the desired semantics:

[ (sum)](c)(α) n = c + n i=0 α i [ (dif )](d)(α) 0 = α 0 − d [ (dif )](d)(α) n+1 = α n+1 − α n that is [ (dif )](d)(α) n = α n − (d ; α) n Remark 3.16. The forward difference transform, ∇(α) n = α n − α n+1 , is not causal.

In this section, we have introduced coinductively defined, causal stream transformers as a coalgebraic perspective on Mealy automata, in strong analogy to plain coinductive streams. The coalgebraic approach suggests a head-tail structure for transformers, which has incidentally also been exploited for continuation-based functional reactive programming [10].

The closed-form notation which has worked well for coinductive streams breaks down in the transformer case. This is quite typical for coalgebraic structures, which are often ill-suited to classical syntax-oriented formal representation, and therefore usually phrased in the more abstract language of category theory. Figure 1: T AB -coalgebra (X, r) in quadrilateral form, from [17].

Compositional Stream Networks

The uncurried, quaternary form of T AB -coalgebra operations, r : X × A → B × X, henceforth abbreviated to r : A X − → B, plays a central role in the semantics of the Sig language. Any data-flow network definition in Sig is brought to this canonical operational form via a series of program transformations described in [17]. The same form also suggests a visual, quadrilateral presentation, as illustrated in Figure 1. The dichotomy of public I/O and private state suggests an object-oriented approach to execution. 4 Alluding to the visual form, and for lack of a more fitting name, we shall call the elements of a function space A X − → B quadrilaterals. Algorithm 4.1. Execution is reified as objects that consume one input element and produce one output element on each synchronous call of a public method. Control is transferred back after each element; the stream is held together by side-effect updates on the private state. The missing pieces r 0 , r + , x 0 are modeled as abstract methods.

head AB [[r x]] (a 0 ) = r 0 (x, a 0 ) tail AB [[r x]] (a 0 ) = [[r r + (x, a 0 )]]

Semantically, stream functions can be composed meaningfully along several axes, namely parallel and (data)sequential.

Definition 4.4. Parallel and sequential composition of stream functions are defined in the obvious way:

k : A ω B l : C ω D k ⊗ l : A × C ω B × D (k ⊗ l)(α, γ) n = k(α) n , l(γ) n k : A ω B l : B ω C l • k : A ω C (l • k)(α) n = l k(α) n Proposition 4.5.

The definition of parallel composition has the equivalent recursive form:

head (A×C)(B×D) (k ⊗ l)(a 0 , c 0 ) = head AB (k)(a 0 ), head CD (l)(c 0 ) tail (A×C)(B×D) (k ⊗ l)(a 0 , c 0 ) = tail AB (k)(a 0 ) ⊗ tail CD (l)(c 0 ) Proof. Implement k ⊗ l = [ (f )](k, l) coalgebraically as (A ω C) × (B ω D), f with: f 0 (k, l)(a 0 , c 0 ) = head AB (k)(a 0 ), head CD (l)(c 0 ) f + (k, l)(a 0 , c 0 ) = tail AB (k)(a 0 ), tail CD (l)(c 0 )

The proof of correctness of this solution and transformation to the above form are left as an exercise to the reader.

These abstract semantic concepts of composition can be pulled back to the concrete quadrilateral form.

Proposition 4.6. For any quadrilaterals q : A X − → B and r : C Y − → D, there is a quadrilateral q r such that:

q r : A × C X×Y −−−→ B × D [[q r x, y]] = [[q x]] ⊗ [[r y]]

Instead of educated guesses as presented ad-hoc in [17], we can now give a formal derivation.

Proof. Take the composite s = q r as unknown and to be solved for. Assume the goal

G: [[s x, y]] = [[q x]] ⊗ [[p y]]

and work out the homomorphism property according to (4.3): † s 0 (x, y), (a 0 , c 0 )

(4.3) = head (A×C)(B×D) [[s x, y]] (a 0 , c 0 ) (4.2) = head (A×C)(B×D) [[q x]] ⊗ [[r y]] (a 0 , c 0 ) G = head (A×C)(B×D) [ (q)](x) ⊗ [ (r)](y) (a 0 , c 0 ) (4.5) = head AB [ (q)](x) (a 0 ), head CD [ (r)](y) (c 0 ) (4.3) = q 0 (x, a 0 ), r 0 (y, c 0 ) † [[s ‡ s + (x, y), (a 0 , c 0 ) ]] (4.2) = [ (s)] s + (x, y)(a 0 , c 0 ) (3.12) = tail (A×C)(B×D) [ (s)](x, y) (a 0 , c 0 ) G = tail (A×C)(B×D) [ (q)](x) ⊗ [ (r)](y) (a 0 , c 0 ) (4.5) = tail AB [ (q)](x) (a 0 ) ⊗ tail CD [ (r)](y) (c 0 ) (3.12) = [ (q)] q + (x)(a 0 ) ⊗ [ (r)] r + (y)(c 0 ) = [ (q)] q + (x, a 0 ) ⊗ [ (r)] r + (y, c 0 ) G = [ (s)] q + (x, a 0 ), r + (y, c 0 ) (4.2) = [[s q + (x, a 0 ), r + (y, c 0 ) ‡ ]]

By matching the marked terms we find the most evident solution:

(q r) 0 (x, y), (a, c) = q 0 (x, a), r 0 (y, c) (q r) + (x, y), (a, c) = q + (x, a), r + (y, c) Proposition 4.7. For any quadrilaterals q : A X − → B and r : B Y − → C, there is a quadrilateral q • r such that: Proof Sketch. By reasoning analogously to the preceding case, we find the solution:

q • r : A X×Y −−−→ C [[(q • r) (x, y)]] = [[r y]] • [[q x]]

(q • r) 0 (x, y), a = r 0 y, q 0 (x, a) (q • r) + (x, y), a = q + (x, a), r + y, q 0 (x, a) Definition 4.8. A third meaningful axis of quadrilateral composition can be defined, symmetrically to the preceding. For any quadrilaterals q : A X − → B and r : C X − → D, there is q r : A × C X − → B × D, defined as:

(q r) 0 x, (a, c) = q 0 (x, a), r 0 q + (x, a), c (q r) + x, (a, c) = r + q + (x, a), c

All three compositions are depicted in Figure 2.

Remark 4.9. A "diagonal" composition of the form depicted in Figure 3, probably expected by any reader familiar with the state monad in functional programming [24], is conspicuously absent, as it breaks the synchronous paradigm where "horizontal" data flow is instantaneous. By constrast, such an operation makes perfect sense in sequential programming, where data dependency (b) is generally understood to entail state dependency (x ).

A little formal detail can make a big difference: for the state monad form, quadrilaterals are simply curried the other way, to r : A → (S → B × S), but the resulting change of perspective is enormous. As a side effect, comparison of coinductive and functional reactive programming styles is very difficult, due to the orthogonal attitudes.

Remark 4.10. Cyclic data flow cannot be constructed by the given composition operators. For the Sig approach to cycles, see the next section.

In this section, we have introduced the quadrilateral form of elementwise stream computation, which corresponds straightforwardly to either the state monad or the coinductive stream transformer approach on the theoretical side, and to an object-oriented implementation strategy on the practical side. We have calculated parallel and sequential composition operators on quadrilaterals, and confirmed the visual and formal intuitive solutions. The method used to obtain these calculations is of general notability: We have reworked the coalgebraic semantic equations according to (4.3), using the specification of the desired operation in the process, and read off the most evident solution by syntactic pattern matching. Despite the simple approach, we shall find this method of coinductive program synthesis just as useful for other primitive operations of stream programming language implementations.

State and Delay

The quadrilateral form, and the explicit management of state, exists only in the intermediate representation of Sig programs. The front-end language takes a more high-level approach, adapted to pervasive patterns of causal stream programming. On the one hand, element-wise computations where output β n depends on input α n only are extremely common. They are implemented for free, by simply ignoring the state axis.

On the other hand, dependency on past inputs often has relative and bounded form, with β n depending on α n−i for a few small delay lengths i only. To this end, Sig features a single-step delay operator. In [17] we have argued for its implementation in quadrilateral form by appeal to operational intuition. Actually we can do better in the coalgebraic framework, and derive the same result from a rigorous semantic specification.

Definition 5.1. The semantic delay operator takes an initial value and a stream to be delayed by one step.

delay A : A → A ω A delay A (a 0 )(α) 0 = a 0 delay A (a 0 )(α) n+1 = α n

In other words, delay A is simply cons A with explicit causality; the initial value is prepended, and delay A (α) n+1 depends on α n exactly. We abbreviate cons A (a 0 ) to (a 0 ;).

Proposition 5.2. The prepending operation as a class of final T AA -coalgebra elements obeys the recurrence:

head AA (a 0 ;)(a 1 ) = a 0 tail AA (a 0 ;)(a 1 ) = (a 1 ;)

Armed with this auxiliary fact, we can formulate the problem.

Proposition 5.3. There is a quadrilateral form δ :A A − → A such that [[δ a 0 ]] = (a 0 ;).

The reader is encouraged to pause for an educated guess before reading on.

Proof. Follow the derivation strategy of (4.6) with the goal G:

[ (δ)](a) = (a;). † δ 0 (a 0 , a 1 ) = δ 0 (a 0 )(a 1 ) [ (δ)] ‡ δ + (a 0 , a 1 )) = [ (δ)] δ + (a 0 )(a 1 ) (3.12) = head AA [ (δ)](a 0 ) (a 1 ) (3.12) = tail AA [ (δ)](a 0 ) (a 1 ) G = head AA (a 0 ;)(a 1 ) G = tail AA (a 0 ;)(a 1 ) (5.2) = a 0 † (5.2) = (a 1 ;) G = [ (δ)] (a 1 ) ‡

By matching the marked terms we find the now evident, but generally mildly surprising, solution (see Figure 4):

δ(a 0 , a 1 ) = (a 0 , a 1 )

This formal argument rigorously reconstructs the previous intuitive construction of δ:

Simultaneously route pre-state to output and input to post-state, respectively, such that the current input becomes pre-state and hence output in the next step, and so forth.

Algorithm 5.4. With specialization to δ, the object-oriented implementation becomes:

class delay extends quad: step(a): var a' := x x := a return a' A visualization of delay is depicted in Figure 4. Delay operators can be combined freely with stateless computations in a data flow network. The quadrilateral form is obtained by synthesizing a pair of pre-and post-state variable for each occurrence of delay, and wiring them in the way depicted on the right hand side. Since each δ node is replaced by a pair of independent identities, the network may be simplified afterwards by propagation.

Remark 5.5. Apparent data flow through the δ node is broken in the process. Hence delayed feedback loops no longer appear as cycles. The Sig language forbids instantaneous cyclic data flow; only networks that become acyclic by delay elimination are valid.

Since the state space X 1 × • • • × X n is synthesized from the types of the n occurrences of delay operators in a network r, the corresponding initial value ξ = (x 1 , . . . , x n ) need to be inferred as well. Then the semantics of the network is the single causal stream function [[r ξ]]. The Sig front-end language provides a binary delay operator of the form a;e which translates to δ(e) with implied initial value a.

Example 5.6. The random number generators from (2.8) in delay-based state-implicit form are depicted in Figure 5, left hand side. The shift register structure is more clearly elucidated than in the coalgebraic form, or in the original imperative code, for that matter. The following pseudocode in simplified Sig describes this network, including seed values (s 0 , s 1 , s 2 , s 3 ):

[ -> r where r := (x ^<< a ^>> b) ^(w ^>> c) x := s0 ; s1 ; s2 ; w w := s3 ; r ]

The result of state synthesis from delay operators is depicted in Figure 5, right hand side. Note the absence of cycles. The object-oriented implementation gives the moral equivalent of the original presentation in the C language, in pseudocode: class xsr(s0, s1, s2, s3): var x := s0; y := s1; z := s2; w := s3 step(): r := (x ^<< a ^>> b) ^(w ^>> c) (x, y, z, w) := (y, z, w, r) return r

In this section, we have introduced the single-step delay operator, the crucial ingredient in stream programming beyond memoryless elementwise computation and basic operation of the pervasive "shift register" algorithmic pattern. We have calculated the mildly confusing implementation of delay as the identical quadrilateral, and illustrated the transition from delay to explicit state in the front-to-core reduction of the Sig language.

Higher Order: Stream Function Application

Higher-order functions are notoriously a more complex subject in a stream context than in ordinary functional programming. However, they are of crucial importance for the high-level expressivity of a practical stream programming language.

On the one hand, if streams are the first-class citizens, then there are streams of stream functions, and functions on these, to deal with. An abstract semantics has been given in terms of comonads [22,23]. All theoretical elegance notwithstanding, that theoretical framework is even less well-known to the general programming community than coalgebras. Apparently it is also less directly tied to practical matters; we are not aware of any relevant implementation it could have inspired. On the other hand, there is the view on a single stream function as a stream of element functions, given by the head AB and tail AB operations on A ω B. This view had already been explored, albeit in ad-hoc terms, and its practical relevance argued in [3]. We have given a systematic theoretical reconstruction in [17] and independently a practical implementation strategy in [18].

In the following section, in order to connect the two more precisely, we follow up on the method already applied in the two preceding section, and calculate a representation for first-class stream functions and its interpretation from a coalgebraic specification.

As a first approximation, assume a generic abstract datatype Z AB with an interpretation map, app AB , to represent some set of causal stream functions for each domain-range pair A, B:

app AB : Z AB → (A ω B)

The type of the interpretation map, with the final coalgebra range, suggests a definition by homomorphism.

Proposition 6.1.

There is a quadrilateral @ : A

Z AB − −− → B such that [ (@)] = app AB .

Proof. Follow the same derivation strategy as before. † @ 0 (z, a 0 ) = @ 0 (z)(a 0 ) ‡ app AB @ + (z, a 0 ) G = [ (@)] @ + (z, a 0 )

(3.12) = head AB [ (@)](z) (a 0 ) = [ (@)] @ + (z)(a 0 ) G = head AB app AB (z) (a 0 ) † (3.12) = tail AB [ (@)](z) (a 0 ) G = tail AB app AB (z) (a 0 ) ‡

By matching the marked terms, we find the specification up to interpretation:

@ 0 (z, a 0 ) = head AB app AB (z) (a 0 ) app AB @ + (z, a 0 ) = tail AB app AB (z) (a 0 )

This account is, well, abstract. In particular, no help is given for making Z AB closed in the sense of the right hand equation; for each element z ∈ Z AB , we must also include, for each a 0 , some sucessor element @ + (z, a 0 ) ∈ Z AB whose interpretation is the stream function tail of the interpretation of z.

The problem can be simplified substantially, if the representation is given at the same implementation level as its usage context, namely in terms of quadrilaterals. Assume a generic abstract datatype W ABX with an interpretation map app ABX to represent some set R ABX ⊆ (A X − → B) of quadrilaterals for each domain-range pair A, B and state space X:

app ABX : W ABX → (A X − → B)

Unlike in the previous attempt, the choice of represented functions, Img(app ABX ), is completely arbitrary; we shall demonstrate that it need not be closed under any operation. Even finite W ABX will do.

Any stream function may be implemented by various quadrilaterals: only the input-output relation is specified, but neither the state space parameter X, nor the initial state x ∈ X. Packing these information items into a dependent record type yields our improved datatype of stream functions: Definition 6.2.

Z AB = X {X} × W ABX × X app AB (X, w, x) = [[app ABX (w) x]]

Proposition 6.3. There is a quadrilateral @ : A

Z AB − −− → B, such that [ (@)] = app AB .

Proof. Follow the usual derivation strategy. † @ 0 ((X, w, x), a 0 )

app AB ‡ @ + ((X, w, x), a 0 )) = @ 0 (X, w, x)(a 0 ) G = tail AB app AB (X, w, x) (a 0 ) G = head AB app AB (X, w, x) (a 0 ) (6.2) = tail AB [[app ABX (w) x]] (a 0 ) (6.2) = head AB [[app ABX (w) x]] (a 0 ) (4.2) = tail AB [ (app ABX (w))](x) (a 0 ) (4.2) = head AB [ (app ABX (w))](x) (a 0 ) (3.12) = [ (app ABX (w))](app ABX (w) + (x)(a 0 )) (3.12) = app ABX (w) 0 (x)(a 0 ) (4.2) = [[app ABX (w) app ABX (w) + (x)(a 0 )]] = app ABX (w) 0 (x, a 0 ) †(6.2)

= app AB X, w, app ABX (w) + (x, a 0 ) ‡ By matching the marked terms, we find the most evident solution: @ 0 (X, w, x), a 0 = app ABX (w) 0 (x, a 0 ) @ + (X, w, x), a 0 = (X, w, x ) where x = app ABX (w) + (x, a 0 )

The calculated solution keeps the first two fields of the dependent record, namely the state space X and the quadrilateral reference w constant, and updates only the transient state component x. Hence we have kept our promise that the choice of represented stream functions is completely arbitrary, and not subject to any closure constraints.

This solution also goes extremely well with the object-oriented approach to implementation, where X and w are realized statically as a field declaration and method binding, respectively, whereas as x, x is the dynamically changing state variable typed by X. The return value and in-place update effect of app AB (w) can be understood as the invocation of the step update on a private instance of the class implementing w. Thus the application of stream functions is realized as the aggregation of objects. Note how variables w and z have been chosen to allude to the above formal datatypes, how the new operation instantiates w to z, with unknown initial private state, and how the method invocation z.step performs the computations of @ 0 and @ + as interface data flow and side effect, respectively. The pictured code pattern, distilled from the preceding formal reasoning, is in line with what could be expected from a competent imperative programmer. On the one hand, this observation serves to illustrate that the calculation of higher-order function semantics is not so much of theoretical, but rather of practical interest, and relevant for efficient code generation. On the other hand, it embodies the aspiration of the Sig design to reconcile formal semantics with domain-specific low-level programming lore.

In this section, we have introduced the dynamic application operator for coinductive stream functions, as the key ingredient for higher-order programming. We have given a formal representation in terms of dependent records, the mathematical metaphor for objects with hidden state and virtual step methods, and calculated the intuitive solution, namely application-as-aggregation, by coinductive synthesis.

Conclusion

Related Work

Coalgebraic approaches have been studied early on in the context of structural operational semantics [20], for their potential to reduce the conceptual distance between denotational and operational semantics considerably. Whereas algebraic approaches produce abstract metaphors of computational concepts, their coalgebraic duals lead to more concrete descriptions of hands-on computational business, but at the same level of formal rigor.

Coalgebraic semantics have been given for programming with objects and classes [6], and with abstract data types [5]. Whereas these deal with the general expressivity of the respective concepts, we are only interested in OO in a narrow, back-end sense; namely for the implementation of quadrilaterals, the common denominator of our operational semantics of stream programming, in terms of private state variables and public I/O interfaces.

Coinductive datatypes and their associated recursive functions play an important role in functional programming under the Curry-Howard correspondence: in dependently typed languages such as Agda [16], constructive theorem provers such as Coq [2], (both of which have worrying issues with coinduction [9]), categorical languages such as Charity [4], and "elementary" approaches to total functional programming [15,21].

Coalgebraic streams have been considered as a foundation for synchronous data-flow programming already in Lucid Synchrone [3]. They remain a viable, if not very popular, alternative to streams-as-functions-of-time approaches, analogously to closed-form versus recursive mathematical definitions of sequences.

A notable high-level approach to coalgebraic streams and natural continuation of [14] is stream calculus [12], which extends the classical mathematical framework of infinitesimal calculus to streams, and presents computations as systems of differential equations. However, that approach is both more general than warranted for our present purpose, considering more than just causal stream functions [11], and more mathematical, with a particular emphasis on linear relationships [1,13].

By contrast, we feel that the operational aspect, namely the adequate representation of low-level loop-based programming patterns that pervade real-world stream processing, has not been fully appreciated. We consider the design and implementation of Sig a well-arguable case in point.

Outlook

For the sake of accessibility, we have not pushed the coalgebraic framework to the limits of its expressivity. In particular, we have omitted accounts for semantic relations, embodied in the formal concepts of behavioral equivalence and bisimulation. These would be relevant to the calculation of semantics-preserving program transformations, such as featuring in code optimization passes of the Sig compiler, as well as in the study of alternative solutions to the ones we have calculated as the "most evident".

Nevertheless, we consider the method for the calculation of practically illuminating operational specifications, as applied repeatedly in each of the preceding sections, a valuable tool in the coalgebraic semantics box, as well as promising step towards more general coinductive program synthesis.