The Sig programming language is a total functional, clocked synchronous data-flow language. Its core has been designed to admit concise coalgebraic semantics. Universal coalgebra is an expressive theoretical framework for behavioral semantics, but traditionally phrased in abstract categorical language, and generally considered inaccessible. In the present paper, we rephrase the coalgebraic concepts relevant for the Sig language semantics in basic mathematical notation. We demonstrate how the language features characteristic of its paradigms, namely sequential and parallel composition for applicative style, delay for data flow, and apply for higher-order functional programming, are shaped naturally by the semantic structure. Thus the present paper serves two purposes, as a gentle, self-contained and applied introduction to coalgebraic semantics, and as an explication of the Sig core language denotational and operational design.
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 [
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 [
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 SA(X) = A × X. It can be extended to a functor, acting on maps as:
SA(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 f0 : X → A and f+ : X → X with:
f (x) = f0(x), f+(x) Algorithm 2.5. The SA-coalgebras are formal representations of enumeration procedures: The carrier X is the state space, and the operation components f0 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 x0, and collecting the outputs an = f0(xn) from successive states xn+1 = f+(xn), 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 = N2 fib0(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
ϕn bif 0(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.
1More precisely a Set-endofunctor, but no other kind is considered here. 2Functors are also required to preserve identity maps and compositions, but that is irrelevant for the present discussion.
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 [
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.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 SA-coalgebras the homomorphism property for h from (X, f ) to (Y, g) simplifies to: g0 h(x) = f0(x) g+ h(x) = h f+(x)
The SA-coalgebra homomorphisms map computations by one enumeration procedure to equivalent computations by another procedure. The coalgebra (Aω, outA) 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 SA-coalgebra.
Proposition 2.12. Let (X, f ) be an SA-coalgebra. Then there is a map: [(f )] : X → Aω [(f )](x)n = f0 f+n(x) Proposition 2.13. The homomorphism property (2.11) specializes for [(f )] to: headA [(f )](x) = f0(x) tailA [(f )](x) = [(f )] f+(x) It is easy to see that [(f )] is indeed a homomorphism.
Proof.
headA [(f )](x) = [(f )](x)0 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):
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 SA-coalgebras (X, f ) and (Aω, outA), 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 = f0 f+n(x) .
h(x)0 = headA h(x) h(x)n+1 = tailA h(x) n
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 SA-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 [
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 [
Definition 3.1. Fix some nonempty sets A and B, and consider the functor:
TAB(X) = (A → B × X)
TAB(f )(k)(a) = b, f (x)
where k(a) = (b, x)
Algorithmically, the TAB-coalgebras represent the category of Mealy-type stream transducers. Their operations f : X → A → B × X, by Currying equivalent to f : X × A → B × X,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 f0 : X → A → B and f+ : X → A → X, with f (x)(a) = f0(x)(a), f+(x)(a) .
Proposition 3.2. For TAB-coalgebras the homomorphism property for h from (X, f ) and (Y, g) simplifies to: g0 h(x) (a) = f0(x)(a) g+ h(x) (a) = h f+(x)(a) Algorithm 3.3. Execution yields the transformed output stream as a synchronous function of the input stream: exec(f0, f+)(x0): var x := x0 forever var a := receive yield f0(x)(a) x := f+(x)(a) Example 3.4. The following two similar coalgebra operations compute the (cumulative) sum and the (backward) difference transform of a stream of numbers, respectively.
A = R
B = R
X = R sum0(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 TAB-coalgebra operation f , we would have to give a component of type f0 : (Aω → Bω) → A → B, which is not meaningful generically, without additional knowledge of A and B. On second thought, the TAB-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 TAB-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 = α<0n =⇒ k(α)<n = k(α0)<n}
The space of causal stream functions can be endowed with a TAB-coalgebra operation, by a not entirely trivial
construction [
Proposition 3.6. For all k : A ω B we have in particular, at the first step:
headA(α) = headA(α0) =⇒ headB k(α) = headB k(α0) Proposition 3.7. The previous property ensures that there is a generic map satisfying headAB : (A ω B) → A → B headAB(k) headA(α) = headB k(α) with no reference to particular elements of A or B.
Definition 3.8. Now consider a related map defined by the equation:
tailAB(k)(a0)(α) = tailB k(a0 ; α) Proposition 3.9. This map can be specified in analogy to (3.7): tailAB : (A ω B) → A → (A ω B)
tailAB(k) headA(α) tailA(α) = tailB k(α) 3We denote both the currying and uncurrying operations by overlining. Proposition 3.10. The pair of equations (3.7), (3.9) can be combined equivalently:
k(a0 ; α) = headAB(k)(a0) ; tailAB(k)(a0)(α)
The causal function space A ω B admits a TAB-coalgebra operation t, namely t0 = headAB and t+ = tailAB. This is again a final TAB-coalgebra: from any other TAB-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 TAB-coalgebra. Then there is a map: [(f )] : X → (A ω B)
[(f )](x)(α)n = f0 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, [
Proposition 3.12. The homomorphism property (3.2) specializes for the final case to: headAB [(f )](x) (a0) = f0(x)(a0)
tailAB [(f )](x) (a0)(α) = [(f )] f+(x)(a0) (α)
The proof of validity and uniqueness of [(f )] is completely analogous to the SA-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)(a0 ; α) = f0(x)(a0) ; [(f )] f+(x)(a0) (α) 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:
n [(sum)](c)(α)n = c + X αi i=0 [(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 [
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.
The uncurried, quaternary form of TAB-coalgebra operations, r : X × A → B × X, henceforth abbreviated to
X
r : A −→ 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 [
class quad: private var x := x0() step(a): var b (b, x) := r(x, a) return b abstract x0() abstract r(x, a) X Definition 4.2. The denotational semantics [[r ` x]] of a quadrilateral form r : A −→ B with initial state x is given by (homomorphisms to) the final TAB-coalgebra.
[[r ` x]] = [(r)](x) Proposition 4.3. The unique homomorphism for these semantics from (3.12) is specified by: headAB [[r ` x]] (a0) = r0(x, a0) tailAB [[r ` x]] (a0) = [[r ` r+(x, a0)]]
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 k ⊗ l : A × C l : C ω D ω
B × D k : A ω B l : B
ω C l ◦ k : A ω C (k ⊗ l)(α, γ)n = k(α)n, l(γ)n (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)(a0, c0) = headAB(k)(a0), headCD(l)(c0)
tail(A×C)(B×D)(k ⊗ l)(a0, c0) = tailAB(k)(a0) ⊗ tailCD(l)(c0)
4Indeed, the current Sig compiler targets the Java VM [
C) × (B ω
f0(k, l)(a0, c0) = headAB(k)(a0), headCD(l)(c0) f+(k, l)(a0, c0) = tailAB(k)(a0), tailCD(l)(c0) 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.
X Y Proposition 4.6. For any quadrilaterals q : A −→ B and r : C −→ D, there is a quadrilateral q k r such that:
X×Y q k r : A × C −−−→ B × D [[q k r ` x, y]] = [[q ` x]] ⊗ [[r ` y]]
Instead of educated guesses as presented ad-hoc in [
G: [[s ` x, y]] = [[q ` x]] ⊗ [[p ` y]] and work out the homomorphism property according to (4.3):
† z }| s0 (x, y), (a0, c0)
‡ z }| { (4.2) [[s ` s+ (x, y), (a0, c0) ]] = [(s)] s+(x, y)(a0, c0) {(4.3) (4.2) = head(A×C)(B×D) [[s ` x, y]] (a0, c0) = head(A×C)(B×D) [[q ` x]] ⊗ [[r ` y]] (a0, c0) G = head(A×C)(B×D) [(q)](x) ⊗ [(r)](y) (a0, c0)
headAB [(q)](x) (a0), headCD [(r)](y) (c0) (4.3) = q0(x, a0), r0(y, c0) | {z †
} (3.12) = tail(A×C)(B×D) [(s)](x, y) (a0, c0) G = tail(A×C)(B×D) [(q)](x) ⊗ [(r)](y) (a0, c0) (4.5) = tailAB [(q)](x) (a0) ⊗ tailCD [(r)](y) (c0) (3.12) = [(q)] q+(x)(a0) ⊗ [(r)] r+(y)(c0) = [(q)] q+(x, a0) ⊗ [(r)] r+(y, c0) G = [(s)] q+(x, a0), r+(y, c0) (4.2) = [[s ` q+(x, a0), r+(y, c0) ]] | {z ‡ } By matching the marked terms we find the most evident solution: (q k r)0 (x, y), (a, c) = q0(x, a), r0(y, c)
(q k r)+ (x, y), (a, c) = q+(x, a), r+(y, c)
X Y Proposition 4.7. For any quadrilaterals q : A −→ B and r : B −→ C, there is a quadrilateral q · r such that:
X×Y q · r : A −−−→ C
[[(q · r) ` (x, y)]] = [[r ` y]] ◦ [[q ` x]]
Proof Sketch. By reasoning analogously to the preceding case, we find the solution: (q · r)0 (x, y), a = r0 y, q0(x, a)
(q · r)+ (x, y), a = q+(x, a), r+ y, q0(x, a) Definition 4.8. A third meaningful axis of quadrilateral composition can be defined, symmetrically to the
X X X preceding. For any quadrilaterals q : A −→ B and r : C −→ D, there is q # r : A × C −→ B × D, defined as: (q # r)0 x, (a, c) = q0(x, a), r0 q+(x, a), c (q # r)+ x, (a, c) = r+ q+(x, a), c
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 [
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. 5
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 [
Proposition 5.2. The prepending operation as a class of final TAA-coalgebra elements obeys the recurrence: headAA(a0;)(a1) = a0 tailAA(a0;)(a1) = (a1;) Armed with this auxiliary fact, we can formulate the problem.
A Proposition 5.3. There is a quadrilateral form δ : A −→ A such that [[δ ` a0]] = (a0;).
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;).
† δz0(a0, a1{) = δ0(a0)(a1) }|
‡ [(δ)] δz+(a0, a1)) = [(δ)] δ+(a0)(a1)
}| { (3.12) = headAA [(δ)](a0) (a1) =G headAA(a0;)(a1) (5.2) = a0 |{z} † (3.12) = tailAA [(δ)](a0) (a1) =G tailAA(a0;)(a1) By matching the marked terms we find the now evident, but generally mildly surprising, solution (see Figure 4): δ(a0, a1) = (a0, a1) 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 X1 × · · · × Xn is synthesized from the types of the n occurrences of delay operators in a network r, the corresponding initial value ξ = (x1, . . . , xn) 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 (s0, s1, s2, s3):
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. 6
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 [
⇐a
On the other hand, there is the view on a single stream function as a stream of element functions, given by the
headAB and tailAB operations on A ω B. This view had already been explored, albeit in ad-hoc terms, and its
practical relevance argued in [
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 ZAB with an interpretation map, appAB, to represent some set of causal stream functions for each domain–range pair A, B:
appAB : ZAB → (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−A−→B B such that [(@)] = appAB.
Proof. Follow the same derivation strategy as before.
‡ appAB @+(z, a0){ =G [(@)] @+(z, a0) z }| =G headAB appAB(z) (a0) | {z } † (3.12) = tailAB [(@)](z) (a0) =G tailAB appAB(z) (a0) | {z } ‡ By matching the marked terms, we find the specification up to interpretation:
appAB @+(z, a0) = tailAB appAB(z) (a0)
This account is, well, abstract. In particular, no help is given for making ZAB closed in the sense of the right hand equation; for each element z ∈ ZAB, we must also include, for each a0, some sucessor element @+(z, a0) ∈ ZAB 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 WABX with an X interpretation map app0ABX to represent some set RABX ⊆ (A −→ B) of quadrilaterals for each domain–range pair A, B and state space X:
X app0ABX : WABX → (A −→ B) =G headAB appAB(X, w, x) (a0) (6=.2) headAB [[app0ABX (w) ` x]] (a0) (4=.2) headAB [(app0ABX (w))](x) (a0) (3.12) = app0ABX (w)0(x)(a0) = app0ABX (w)0(x, a0) | {z }
† Unlike in the previous attempt, the choice of represented functions, Img(app0ABX ), is completely arbitrary; we shall demonstrate that it need not be closed under any operation. Even finite WABX 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.
ZAB = [ {X} × WABX × X
X appAB(X, w, x) = [[app0ABX (w) ` x]] Proposition 6.3. There is a quadrilateral @ : A −Z−A−→B B, such that [(@)] = appAB.
Proof. Follow the usual derivation strategy.
‡ appAB @+((X,}w|, x), a0)) z { =G tailAB appAB(X, w, x) (a0) (6.2) = tailAB [[app0ABX (w) ` x]] (a0) (4.2) = tailAB [(app0ABX (w))](x) (a0) (3.12)
= [(app0ABX (w))](app0ABX (w)+(x)(a0)) (4.2) = [[app0ABX (w) ` app0ABX (w)+(x)(a0)]] (6=.2) appAB X, w, app0ABX (w)+(x, a0) | {z ‡ } By matching the marked terms, we find the most evident solution: @0 (X, w, x), a0 = app0ABX (w)0(x, a0) @+ (X, w, x), a0 = (X, w, x0) where x0 = app0ABX (w)+(x, a0) 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, x0 is the dynamically changing state variable typed by X. The return value and in-place update effect of app0AB(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.
Example 6.4. Consider the Euler method for numerical integration of autonomous ordinary differential equations: y˙ = f (y) discretized to yn+1 = yn + δt · f (yn) Its implementation with output stream y, indepently of the stream function f given as a class w, is a simple matter of managing a private instance z: class int(dt, w, y0): var y := y0 const z := new w() step(): var u := y y := y + dt * z.step(y) return u 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. 7
Related Work
Coalgebraic approaches have been studied early on in the context of structural operational semantics [
Coalgebraic semantics have been given for programming with objects and classes [
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 [
Coalgebraic streams have been considered as a foundation for synchronous data-flow programming already
in Lucid Synchrone [
A notable high-level approach to coalgebraic streams and natural continuation of [
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. 7.2
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.