Sequences, streams, and segments

What kind of thing is a movie? Or a song? Or a trajectory from point A to point B? If you’re a computer programmer/programmee, you might say that such things are sequences of values (frames, audio samples, or spatial locations). I’d suggest that these discrete sequences are representations of something more essential, namely a flow of continuously time-varying values. Continuous models, whether in time or space, are often more compact, precise, adaptive, and composable than their discrete counterparts.

Functional programming offers great support for sequences of variable length. Lazy functional programming adds infinite sequences, often called streams, which allows for more elegant and modular programming.

Functional programming also has functions as first class values, and when the function’s domain is (conceptually) continuous, we get a continuous counterpart to infinite streams.

Streams, sequences, and functions are three corners of a square. Streams are discrete and infinite, sequences are discrete and finite, and functions-on-reals are continuous and infinite. The missing corner is continuous and finite, and that corner is the topic of this post.

infinitefinite
discreteStream Sequence
continuousFunction ???

You can download the code for this post.

Edits:

  • 2008-12-01: Added Segment.hs link.
  • 2008-12-01: Added Monoid instance for function segments.
  • 2008-12-01: Renamed constructor “DF” to “FS” (for “function segment”)
  • 2008-12-05: Tweaked the inequality in mappend on (t :-># a).

Streams

I’ll be using Wouter Swierstra’s Stream library. A stream is an infinite sequence of values:

data Stream a = Cons a (Stream a)

Stream is a functor and an applicative functor.

instance Functor Stream where
    fmap f (Cons x xs) = Cons (f x) (fmap f xs)
 
instance Applicative Stream where
    pure  = repeat
    (<*>) = zipWith ($)
 
repeat :: a -> Stream a
repeat x = Cons x (repeat x)

Comonads

Recently I’ve gotten enamored with comonads, which are dual to monads. In other words, comonads are like monads but wearing their category arrows backwards. I’ll be using the comonad definitions from the category-extras library.

The most helpful intuitive description I’ve found is that comonads describe values in context.

The return method injects a pure value into a monadic value (having no effect).

return  :: Monad m     => a -> m a

The dual to monadic return is extract (sometimes called “counit” or “coreturn“), which extracts a value out of a comonadic value (discarding the value’s context). category-extras library splites this method out from Comonad into the Copointed class:

extract :: Copointed w => w a -> a

Monadic values are typically produced in effectful computations:

a -> m b

Comonadic values are typically consumed in context-sensitive computations:

w a -> b

(Kleisli arrows wrap the producer pattern, while CoKleisli arrows wrap the consumer pattern.)

Monads have a way to extend a monadic producer into one that consumes to an entire monadic value:

(=<<) :: (Monad m) => (a -> m b) -> (m a -> m b)

We more often see this operation in its flipped form (obscuring the conceptual distinction between Haskell arrows and arbitrary category arrows):

(>>=) :: (Monad m) => m a -> (a -> m b) -> m b

Dually, comonads have a way to extend a comonadic consumer into one that produces an entire comonadic value:

extend :: (Comonad w) => (w a -> b) -> (w a -> w b)

which also has a flipped version:

(=>>) :: (Comonad w) => w a -> (w a -> b) -> w b

Another view on monads is as having a way to join two monadic levels into one.

join      :: (Monad   m) => m (m a) -> m a

Dually, comonads have a way to duplicate one level into two:

duplicate :: (Comonad w) => w a -> w (w a)

For a monad, any of join, (=<<), and (>>=) can be used to define the others. For a comonad, any of duplicate, extend, and (=>>) can be used to define the others.

The Stream comonad

What might the stream comonad be?

The Stream library already has functions of the necessary types for extract and duplicate, corresponding to familiar list functions:

head :: Stream a -> a
head (Cons x _ ) = x
 
tails :: Stream a -> Stream (Stream a)
tails xs = Cons xs (tails (tail xs))

where

tail :: Stream a -> Stream a
tail (Cons _ xs) = xs

Indeed, head and tails are just what we’re looking for.

instance Copointed Stream where extract   = head
instance Comonad   Stream where duplicate = tails

There is also a Monad instance for Stream, in which return is repeat (matching pure as expected) and join is diagonalization, producing a stream whose nth element is the nth element of the nth element of a given stream of streams.

Exercise: The indexing function (!!) is a sort of semantic function for Stream. Show that (!!) is a morphism for Functor, Applicative, Monad, and Comonad. In other words, the meaning of the functor is the functor of the meanings, and similarly for the other type classes. The Comonad case has a little wrinkle. See the posts on type class morphisms.

Adding finiteness

Lists and other possibly-finite sequence types add an interesting new aspect over streams, which is concatenation, usually wrapped in a Monoid instance.

class Monoid o where
    mempty  :: o
    mappend :: o -> o -> o

Lists also have take and drop operations, which can undo the effect of concatenation, as well as a notion of length (duration). Let’s generalize these three to be methods of a new type class, Segment, so that we can defined continuous versions.

class Segment seg len where
    length :: seg -> len
    drop   :: len -> seg -> seg
    take   :: len -> seg -> seg

For lists, we can use the prelude functions

instance Segment [a] Int where
    length = Prelude.length
    drop   = Prelude.drop
    take   = Prelude.take

Or the more generic versions:

instance Integral i => Segment [a] i where
    length = genericLength
    drop   = genericDrop
    take   = genericTake

These three functions relate to mappend, to give us the following “Segment laws”:

drop (length as) (as `mappend` bs) == bs
take (length as) (as `mappend` bs) == as
 
t <= length as ==> length (take t as) == t
t <= length as ==> length (drop t as) == length as - t

Adding continuity

Streams and lists are discrete, containing countably many or finitely many elements. They both have continuous counterparts.

When we think of a stream as a function from natural numbers, then John Reynolds’s alternative arises: functions over real numbers, i.e., a continuum of values. If we want uni-directional streams, then stick with non-negative reals.

Many stream and list operations are meaningful and useful not only for discrete sequences but also for their continuous counterparts.

The infinite (stream-like) case is already handled by the class instances for functions found in the GHC base libraries (Control.Functor.Instances and Control.Applicative).

instance Functor ((->) t) where
    fmap = (.)
 
instance Applicative ((->) t) where
    pure = const
    (f <*> g) x = (f x) (g x)
 
instance Monad ((->) t) where
    return = const
    f >>= k = \ t -> k (f t) t

As a consequence,

  join f == f >>= id == \ t -> f t t

Assume a type wrapper, NonNeg, for non-negative values. For discrete streams, r == NonNeg Integer, while for continuous streams, r == NonNeg R, for some type R representing reals.

The co-monadic instances from the category-extras library:

instance Monoid o => Copointed ((->) o) where
    extract f = f mempty
 
instance Monoid o => Comonad ((->) o) where
    duplicate f x = \ y -> f (x `mappend` y)

Finite and continuous

Functions provide a setting for generalized streams. How do we add finiteness? A very simple answer is to combine a length (duration) with a function, to form a “function segment”:

data t :-># a = FS t (t -> a)

The domain of this function is from zero to just short of the given length.

Now let’s define class instances.

Exercise: Show that all of the instances below are semantically consistent with the Stream and ZipList instances.

Monoid

Empty function segments have zero duration. Concatenation adds durations and samples either function, right-shifting the second one.

instance (Ord t, Num t) => Monoid (t :-># a) where
    mempty = FS 0 (error "sampling empty 't :-># a'")
    FS c f `mappend` FS d g =
      FS (c + d) (\ t -> if t <= c then f t else g (t - c))

Segment

The Segment operations are easy to define:

instance Num t => Segment (t :-># a) t where
    length (FS d _) = d
    drop t (FS d f) = FS (d - t) (\ t' -> f (t + t'))
    take t (FS _ f) = FS t f

Notice what’s going on with drop. The length gets shortened by t (the amount dropped), and the function gets shifted (to the “left”) by t.

There’s also a tantalizing resemblance between this drop definition and duplicate for the function comonad. We’ll return in another post to tease out this and

I’ve allowed dropping or taking more than is present, though these cases can be handled with an error or a by taking or dropping fewer elements (as with the list drop and take functions).

Functor, Zip and Applicative

fmap applies a given function to each of the function values, leaving the length unchanged.

instance Functor ((:->#) t) where
    fmap h (FS d f) = FS d (h . f)

zip pairs corresponding segment values and runs out with the shorter segment. (See More beautiful fold zipping for the Zip class.)

instance Ord t => Zip ((:->#) t) where
    FS xd xf `zip` FS yd yf = FS (xd `min` yd) (xf `zip` yf)

pure produces a constant value going forever. (<*>) applies functions to corresponding arguments, running out with the shorter.

instance (Ord t, Bounded t) => Applicative ((:->#) t) where
    pure a = FS maxBound (const a)
    (<*>)  = zipWith ($)

Copointed and Comonad

extract pulls out the initial value (like head).

instance Num t => Copointed ((:->#) t) where
    extract (FS _ f) = f 0

duplicate acts like tails. The generated segments are progressivly dropped versions of the original segment.

instance Num t => Comonad ((:->#) t) where
    duplicate s = FS (length s) (flip drop s)

Monad

I don’t know if there is a monad instance for ((:->#) t). Simple diagonalization doesn’t work for join, since the nth segment might be shorter than n.

What’s ahead?

The instances above remind me strongly of type class instances for several common types. Another post will tease out some patterns and reconstruct (t :-># a) out of standard components, so that most of the code above can disappear.

Another post incorporates (t :-># a) into a new model and implementation of relative-time, comonadic FRP.

13 Comments

  1. Eyal Lotem:

    Hey, another nice post, Conal!

    I was wondering about the Segment class:

    instance Num t => Segment (t :-># a) t where
        length (DF d _) = d
        drop t (DF d f) = DF (d - t) (\ t’ -> f (t + t’))
        take t (DF _ f) = DF t f
    

    Is there a reason that drop/take are not more general than that (in a separate, more general class)? Could they not be implemented for the infinite/discrete case?

  2. Paul Liu:

    The Co-algebraic structure of streams are long known, and Tarmo and Varmo’s paper, the Essence of Dataflow Programming, gave a extensive comonadic treatment.

    But I believe an important point missing from both their paper and your blog post here is that in order to be a comonad, it has to satisfy the laws. I emphasize this because not just every stream representation, but a stream together with a current position into it, is a comonad. Further more, the comonad laws actually enforce a moving position in the stream, which is best explained visually if one try to plot the laws as pictures.

    Although comonad captures a moving stream, it doesn’t enforce causality. So comonad alone wouldn’t be enough for FRP, just like Applicative Functors, or any other well known abstract formalisms. Paul and I recently worked on a Causal Commutative Arrows paper, which tried to address this issue.

  3. Paul Liu:

    (sorry, hitting the post button too early!)

    The primitive for causality is the unit delay (or init as in our paper). But not everyone likes it because it seems to break the continuity. Yampa, and earlier FRP implementations like SOE, used integral for continuous values, and accum for discrete ones rather than emphasizing delay as a primitive. We dodged this question and instead propose a product law:

    init i *** init j = init (i, j)

    where *** is the parallel arrow composition. So it remains abstract without refering to a concrete semantics.

    On the other hand, by not representing first class signals, the arrow framework actually do not care if time starts from 0 or is relative. Time itself is abstracted away, just like in Comonads, or Applicative Functors. So why does the starting point matter?

  4. conal:

    @Eyal: Thanks for the suggestion. I hadn’t thought of splitting up the Segment class. drop could indeed go into another class, since it works for infinite-only types like (t -> a) (for ordered infinite t) as well as for possibly-finite ones like [a] and (t :-># a). take yields a finite result, so I think would be problematic.

  5. conal:

    @Paul: Thanks for the reminder to check the comonad laws, which I haven’t done yet. Do you think ((:->#) t) passes or fails?

  6. Steven Fodstad:

    The dual to the statement “Nothing escapes a monad” is the statement “Nothing can create a comonad”. And just as every monad needs to have a method to violate that rule in order to be useful (State has runState; lists have head and (!!); IO can be executed), every comonad needs to have a way to create a value (most likely more than one way) in order to be useful. These functions will not be modeled by the comonad interface.

    I think choosing a proper set of functions that create comonadic values (other than what’s provided in the definition of a comonad) should be enough to enforce causality. I haven’t done enough work on this to say for certain, though.

  7. Paul Liu:

    @Conal, I think ((:->#) t) would satisfy comonad laws due to the way duplicate is defined, which indeed enforces a moving position by dropping “the past”.

    A question I’m always asking myself is that, do we gain anything from declaring signals (both behaviors and events) an instance of such abstract formalisms like Comonad or Applicative Functor?

    Sure, we get a few primitives to write program with and some nice properties (i.e., the laws) associated with them. But do they help? To what extent?

    I for one do not think Applicative Functor provides any more insights than Functors except some coding convenience perhaps. As for Comonad, I don’t know, the laws are actually more interesting than those of Applicative Functors, but I’m not sure how to make use of them.

  8. conal:

    @Paul: Thanks for the hunch about ((:->#) t) satisfying the comonad laws.

    I like your question about relating our abstractions to standard algebraic notions embodied by type classes. I appreciate the “syntactic” (so to speak) and semantic benefits. By syntactic, I mean inheriting a standard vocabulary so that I don’t have to define so much of it myself. That vocabulary guides me to tools that I might not have thought to try out. By “semantic benefits”, I mean both the class laws, as you mentioned, and the semantic morphisms.

    For instance, much of the syntactic and semantic foundation of FRP (the explicit signal variety) can be captured via class instances and the corresponding type class morphisms. When those morphisms hold, I know I’m in the universal flow, rather than just making stuff up. I’m confident that my formalism will be powerful, predictable, and a pleasure to use. When the morphisms fail, or aren’t even defined, as currently with Reactive events, I know to expect pain and where to start when trying to improve things.

    For signals in particular, Applicative has been great, since it (or Zip) captures the essence of concurrent composition. And the semantic model and applicative morphism tell us exactly what the Applicative instance must mean.

  9. Luke Palmer:

    @Paul: I played with causal arrows a while ago. But there was no unit step or any such thing in the formalism. My definition was that a transformation R of time functions is causal if it satisfies R(f)_t = R(f_t)_t, where _t means roughly “restricted to times after t”. It’s a pretty weak constraint, and can be formalized (after redefining “after”) even in relativistic (as in Einstein) systems :-) . I do think causality is a big deal in FRP, and capturing it properly will be key to its full potential.

  10. Luke Palmer:

    Oh, another note, regarding the comonad laws. While whatever work you might do to prove that your code is correct will entail this, it might be helpful anyway. Your representation for reactive is Reactive A = A * Future (Reactive A), which is the cofree comonad over the Future functor, which always satisfies the comonad laws.

  11. conal:

    Thanks bunches for the tip, Luke!

  12. geophf:

    Hello, Conal,

    I liked your discussion about comonads, and, as I used the concept to describe “realized” constants, I linked your post into my article “Realized Constants are Comonadic“.

    I had started exploring comonadic structures before for you posted your description, and I felt the loss, as they are a really simple concept, but other than Edward Kmett’s (very excellent) site and sigfpe’s blog, there seemed to be little interest in them.

    Thank you for bringing this useful concept to the fore.

    cheers, geophf

  13. Conal Elliott » Blog Archive » Sequences, segments, and signals:

    [...] post Sequences, streams, and segments offered an answer to the the question of what’s missing in the following box: [...]

Leave a comment