Is it possible?: Behavior t [Behavior t a] -> Behavior t [a]

Question

Is there a way to have a Behavior t [a] where the values of [a] at time t are the values contained in a Behavior t [Behavior t a] at time t? I.e, a function with the type of:

Behavior t [Behavior t a] -> Behavior t [a]

If this is not possible, is that because of a logical impossibility or a limitation in reactive-banana?

Onceover

Type signature is valid, can you explain what exactly is your problem? If I get it right, you want to do some sort of filtering? – Flatways

I don't know reactive-banana, but there's still definitely a question of whether that type is inhabited. – Hayfork

Thank you for mentioning "type is inhabited", it lead me to the Curry-Howard isomorphism theorem wiki page on Haskell Wiki. – Flatways

Semantically Behavior a is Time -> a such that Behavior [Behavior a] is Time -> [Time -> a] while Behavior [a] is Time -> [a]. Are you looking for something like fix :: Behavior [Behavior a] -> Behavior [a]; fix as t = map ($ t) (as t)? – Hayfork

@Flatways Highly suggest playing around with Software Foundations or Certified Programming with Dependent Types if that stuff interests you. – Hayfork

I don't think there is one. If there were (and it obeyed fairly simple laws), Behavior t would be a Monad. A Monad's join would have type Behavior t (Behavior t a) -> Behavior t a, which is almost the same thing. The closest thing I can find in the reactive-banana docs is switchB, which I imagine switches to the behavior from the most recent event. Moment t is a Monad, but I don't know what it means, and there doesn't seem to be any way to get from a Moment t something back to a Behavior t. Perhaps if you are making your own framework it could be built from changes and switchB. – Firstborn

It's not a logical impossibility, for example, I use a monadic interface to provide a similar feature in this answer: #19502768. Much of the complexity was in allowing exactly that sort of thing to happen. – Firstborn

You also might be interested in this paper, homepages.cwi.nl/~ploeg/papers/monfrp.pdf, which discusses some of the advantages and disadvantages of Arrows and Monads, both of which are applicative, as abstractions for functional reactive programming. As far as I can tell, reactive-banana fits in a third category of being Applicative, but not being a Monad or an Arrow. – Firstborn

Answer 1

The type is trivially inhabited for any Applicative:

{-# LANGUAGE RankNTypes #-}
import Control.Applicative
import Control.Monad
import Data.Functor.Identity
import qualified Data.Traversable as T

f' :: (Applicative f) => f [f a] -> f [a]
f' = const $ pure []

which is clearly not what you intended. So let's ask for inhabitation of

(Traversable t) => Behavior u (t (Behavior u a)) -> Behavior u (t a)

or more generally for which applicatives we can construct

(T.Traversable t) => f (t (f a)) -> f (t a)

This is inhabited for any f that is also a monad:

f :: (Monad m, T.Traversable t) => m (t (m a)) -> m (t a)
f = join . liftM T.sequence

An obvious question arises: If an applicative has such an f, does it have to be a monad? The answer is yes. We just apply f to the Identity traversable (one-element collection - the Traversable instance of Identity) and construct join as

g :: (Applicative m) => (forall t . (T.Traversable t) => m (t (m a)) -> m (t a))
                     -> (m (m a) -> m a)
g f = fmap runIdentity . f . fmap Identity

So our function is inhabited precisely for those applicatives that are also monads.

To conclude: The function you're seeking would exist if and only if Behavior were a Monad. And because it is not, most likely there is no such function. (I believe that if there were a way how to make it a monad, it'd be included in the library.)

Fraudulent

I was nearly compelled by this idea as well, but then I saw that by the model demonstrated in my comment it should be a possible, non-trivial function for any Functor. That obviously still implies Monad, so I guess I'm curious why the model is a monad yet the implementation isn't. – Hayfork

@J.Abrahamson I guess the reason is that the model Time -> a allows us to access any the value at an arbitrary time. But in a FRP implementation this isn't possible, we can generally access "now", or something. I'm not sure, but this could be the reason. – Fraudulent

@PetrPudlák: in the Reader type it's possible to define the monadic join using the Applicative instance: join ra = runReader <$> ra <*> ask. I think we can see the issue in this light: Behavior lacks a counterpart to runReader. – Tavis

@LuisCasillas That's a very interesting point! I don't think at all that there should be runBehavior :: Behavior a -> t -> a, but ought there not be a behaviorNow :: Behavior (Behavior a) -> Behavior a implemented theoretically as behaviorNow f t = f t t? – Hayfork

@J.Abrahamson: I don't know reactive-banana, but Conal's "Push-pull functional programming" does have time :: Behavior Time whose model is the Time -> Time identity. – Tavis

To generalize my earlier point a bit: another way of looking at this is with representable functors: any Functor isomorphic to (->) r (for some r) is a Monad. In the case of FRP, there is an isomorphism between Behavior and (->) Time in the metalanguage that we use to state the model, but in the object language we cannot implement such a thing. – Tavis

Without using dynamic switching (a bit of a pain), the only option seems to be use a Behavior t [a] in the first place and update each item in the boring, non-frp way. – Onceover

Answer 2

As Petr has already indicated, such a function

flatten :: Behavior t [Behavior t a] -> Behavior t [a]

exists if and only if the type Behavior t were a monad.

Here a direct way to see this:

join :: Behavior t (Behavior t a) -> Behavior t a
join = map head . flatten . map (:[])

flatten = join . map sequence

However, for various reasons, Behavior t is not a monad in reactive-banana. This is explained here.

Pedicab