Simplify model?

[atzeus]

Hi Heinrich,

I'm confused as to why the model needs the concept of start times.

Isn't it possible define the model more simply as something like this (warning : code complies, but not tested):

{-# Language TupleSections,RecursiveDo,DeriveFunctor,GeneralizedNewtypeDeriving #-} 
import Control.Applicative
import Data.Maybe
import Data.Ratio
import Control.Monad
import Control.Monad.Fix

type Time = Ratio Int

newtype Behavior a = B {runB :: Time -> a } deriving (Functor, Applicative, Monad)

-- monotonically increasing times
newtype Event a = E { getEv :: [(Time, a)] } deriving (Functor)

never :: Event a
never = E []

unionWith :: (a -> a -> a) -> Event a -> Event a -> Event a
unionWith f (E l) (E r) = E $ loop l r where
  loop [] r = r
  loop l [] = l
  loop l@((ta,a) : tl) r@ ((tb,b) : tr) 
   | ta < tb  = (ta, a    ) : loop tl r
   | tb < ta  = (tb, b    ) : loop l  tr
   | otherwise = (ta, f a b) : loop tl tr

filterE :: (a -> Bool) -> Event a -> Event a
filterE p (E es) = E $ [(time,a) | (time,a) <- es, p a]

apply :: Behavior (a -> b) -> Event a -> Event b
apply (B f) (E es) = E  [(time, f time x) | (time,x) <- es]

newtype Moment a = M { runMoment :: Time -> a } deriving (Functor, Applicative, Monad,MonadFix)

-- helper
forgetE :: Time -> Event a -> [(Time, a)]
forgetE t (E es) =  [(time,x) | (time,x) <- es, time >= t] 

stepper :: a -> Event a -> Moment (Behavior a)
stepper i e = M $ \t -> B $ step' i (forgetE t e)
  where step' i [] t = i
        step' i ((ta,a) : te) t
         | t <=  ta  = i
         | otherwise = step' a te t

valueB :: Behavior a -> Moment a
valueB b = M $ runB b

observeE :: Event (Moment a) -> Event a
observeE (E e) = E $ map (\(t,e) -> (t, runMoment e t)) e

switchB :: Behavior a -> Event (Behavior a) -> Moment (Behavior a)
switchB b e = join <$> stepper b e

switchE :: Event (Event a) -> Moment (Event a)
switchE es = M $ \t -> E $ switch [] (forgetDiag t)
  where forgetDiag t = [(time, forgetE time x) | (time,x) <- forgetE t es]
        switch ((ta,a) : ts) r@((tb, _) : _) 
          | ta < tb             = (ta, a) : switch ts r
        switch _ ((tb, b) : t) = switch b t
        switch l []             = l

interpret :: (Event a -> Moment (Event b)) -> [Maybe a] -> [Maybe b]
interpret f = toMaybeE . runEm  . fromMaybeE 
  where runEm i = runMoment (f i) (0 % 1)

fromMaybeE :: [Maybe a] -> Event a
fromMaybeE e = E $ catMaybes $ 
  zipWith (\x t -> fmap (t,) x) e [ i % 1 | i <- [1..]]

toMaybeE :: Event a -> [Maybe a]
toMaybeE (E l) = loop 1 l where
  loop i ((timerat,a) : t) = 
   let time = numerator timerat
   in replicate (time - i) Nothing ++ (Just a : loop (time +1) t)

-- expressed in other primitives:
accumE :: a -> Event (a -> a) -> Moment (Event a)
accumE i e = mdo b <- stepper i steps
                 let combine f = f <$> valueB b 
                 let steps = observeE $ combine <$> e
                 return steps

Is there a reason why this would not work? Or is this a nice simplification?

[HeinrichApfelmus]

In principle, this is a good model for the semantics of FRP, but it has one important problem: It cannot handle recursion if we interpret the types as literal Haskell types. I expect that if you use the code here for the test suite, then the tests that use recursion will go into infinite loops.

The main trouble is that a Haskell list of pairs [(Time, a)] does not support the recursion we need. The reason is that stepper i e cannot decide which value to return at time t until it is clear at which time ta > t the event e = ((ta,a) : te) has its next occurrence. But this time ta may itself depend on the value that stepper needs to decide on! Still, recursion is possible because what we do know for sure is that the event can only happen in the future, ta > t, and we need to convey this information to the compiler in some way.

The model in the library solves this problem by advancing everything in "lock step". It supports recursion. It may look like a discrete model, but under the assumption that all input events happen at a discrete set of times, I can prove that it reproduces continuous-time semantics. (The idea is that only the discrete times at which the inputs happen are relevant.)

Of course, if we interpret the list [(Time,a)] as a "mathematical" construct and not as a literal Haskell type, then we can give an intuitive explanation of recursion. Still, I think that it's not entirely trivial to give a well-defined denotational semantics (à la Scott) that supports recursion.

It may also be possible to adapt the Time type to incorporate information of the kind "I don't know when it will be, but it's definitely not now." I think that's what Conal Elliott tried to do with his unamb combinator, but I don't think that it works well in Haskell code.

[atzeus]

I agree completely on your thoughts on discrete time and continous time and recursion! :)

That being said, it still does not answer why the current model uses "start times". Would the following model work?

{-# Language TupleSections,RecursiveDo,DeriveFunctor,GeneralizedNewtypeDeriving #-} 
import Control.Applicative
import Data.Maybe
import Control.Monad
import Control.Monad.Fix

type Nat = Int -- natural numbers, wrongly represented
type Time = Nat

-- always infinite, isomorphic to Time -> a 
newtype Behavior a = B {runB :: [a] } deriving (Functor)

forgetDiagonal :: [[a]] -> [[a]]
forgetDiagonal l = zipWith drop [0..] l

diagonal :: Behavior (Behavior a) -> Behavior a
diagonal (B l) = B $ map head (forgetDiagonal $ map runB l)

instance Monad Behavior where
  return x = B $ repeat x
  m >>= f  = diagonal $ fmap f m

-- always infinite, isomorphic to Time -> Maybe a
newtype Event a = E { getEv :: [Maybe a] } deriving (Functor)

never :: Event a
never = E $ repeat Nothing

unionWith :: (a -> a -> a) -> Event a -> Event a -> Event a
unionWith f (E l) (E r) = E $ zipWith comb l r where
  comb (Just x) (Just y) = Just (f x y)
  comb Nothing  (Just y) = Just y
  comb (Just x) Nothing  = Just x
  comb Nothing  Nothing  = Nothing

filterMaybe :: Event (Maybe a) -> Event a
filterMaybe (E es) = E $ map join es 

apply :: Behavior (a -> b) -> Event a -> Event b
apply (B fs) (E es) = E  $ zipWith (\f x -> fmap (f $) x) fs es

newtype Moment a = M { runMoment :: Time -> a } deriving (Functor, Applicative, Monad,MonadFix)

-- helper
forgetE :: Time -> Event a -> [Maybe a]
forgetE t (E es) = drop (t-1) es

stepper :: a -> Event a -> Moment (Behavior a)
stepper i e = M $ \t -> B $ replicate (t - 1) i ++ step i (forgetE t e)
  where step i (h : t) = i : step nxt t
          where nxt = case h of
                       Just i -> i
                       Nothing -> i

valueB :: Behavior a -> Moment a
valueB (B b) = M $ \t -> b !! t

observeE :: Event (Moment a) -> Event a
observeE (E e) = E $ zipWith (\e t -> fmap (`runMoment` t) e) e [0..] 

switchB :: Behavior a -> Event (Behavior a) -> Moment (Behavior a)
switchB b e = join <$> stepper b e

switchE :: Event (Event a) -> Moment (Event a)
switchE es = M $ \t -> E $ replicate (t - 1) Nothing ++ switch (getEv never) (forgetE t (forgetDiag es)) where
   forgetDiag :: Event (Event a) -> Event [Maybe a]
   forgetDiag (E es) = E $ zipWith (\e t -> fmap (forgetE t) e) es [0..]
   switch _              (Just s  : t) = head s : switch (tail s) t
   switch (Just x  : ts) (Nothing : t) = Just x : switch ts t
   switch (Nothing : ts) (Nothing : t) = Nothing : switch ts t

interpret :: (Event a -> Moment (Event b)) -> [Maybe a] -> [Maybe b]
interpret f = getEv . (\m -> runMoment m 0)  . f . E

-- expressed in other primitives:
accumE :: a -> Event (a -> a) -> Moment (Event a)
accumE i e = mdo b <- stepper i steps
                 let combine f = f <$> valueB b 
                 let steps = observeE $ combine <$> e
                 return steps

(update : fixed old values of step and switchE) (update 2: fixed nasty strictness property of stepper)

[HeinrichApfelmus]

Ah. It appears to me that this new model should be equivalent to the one in the library (apart from potential off-by-one pitfalls that I didn't check yet but which are not essential). If we denote the Event constructor from reactive-banana with E', then there is a correspondence

E' time es  <=>  forgetE time (E es) 

In a sense, the "starting time" representation is an "optimization"for the forgetE combinator. But since this is a semantic model, we don't really care about optimizations. :smile:

Another way to put it is that in your model, all events and behaviors have "starting time" 0, i.e. we always have forgetE 0 e == e. Note that in the definition of stepper, you have to use replicate to pad the Behavior, so that it starts at 0. The trimE and trimB helpers in reactive-banana have a similar purpose to forgetE and replicate (t-1).

Strictly speaking, from the point of view of semantics, it seems perfectly sensible to also have events that had infinitely many occurrences in the past, i.e. which have no "starting time". In this case, it is again the external events that supply a finite starting time at which the "network" starts reacting to events.

---

I like the idea of "starting" everything at time 0, it makes the model simpler and easier to understand. Would you be ok with me incorporating your model code into the library?

[atzeus]

apart from potential off-by-one pitfalls that I didn't check yet but which are not essential

I also didn't check, so they are probably present :)

Would you be ok with me incorporating your model code into the library?

Of course :)

Another thought: I think the first model I posted, i.e. the model with:

newtype Behavior a = B { getB :: Time -> a } deriving (Functor,Applicative, Monad)
-- monotonically increasing times
newtype Event a = E { getEv :: [(Time, a)] } deriving (Functor)

does actually work.

The problem with recursion is, as you said, that essentially:

-- monotonically increasing times
newtype Event a = E { getEv :: [(Time, a)] } deriving (Functor)

That "monotonically increasing times" is just a comment, while it is essential for the execution model: with this comment it becomes clear that stepper can only "step" once per time point.

However, the function step, as I implemented it, does use the information that the times are monotonically increasing:

stepper :: a -> Event a -> Moment (Behavior a)
stepper i e = M $ \t -> B $ step i ( forgetE t e)
  where step i [] t = i
        step i ((ta,a) : te) t 
          | t <= ta = i    -- no checking of tail when t == ta
          | otherwise = step a te t

I think this works out :) Let's do a test:

test = runB (runMoment body 20) 40
 where
  events = E [(i % 1, 1) | i <- [1..]]
  body = mdo sum <- stepper 0 updates
             let combine r = (+ r) <$> valueB sum
             let updates = observeE $ combine <$> events
             return sum 

Does not loop, returns 20.

Do you think this works? It would be nice, because although I agree that a "discrete" semantics is fine as long as we do not depend on the discretization, this model is much closer to how it is described in the docs and how we informally think about it :)

[atzeus]

Hmmm... This does not work for all cases, things go wrong as soon as filterE is involved, this example loops:

recursive3 :: Event Int -> Moment (Event Int)
recursive3 edec = mdo
    bcounter <- accumB 4 $ (subtract 1) <$ ecandecrease
    let ecandecrease = whenE ((>0) <$> bcounter) edec
    return $ apply (const <$> bcounter) ecandecrease

I'm not sure why though...

[atzeus]

Right, this does not work. The point is that we also need to convince the runtime that no events <= t, where t is some time, are present through filterE...

[HeinrichApfelmus]

Yeah, the representation Event a = [(Time,a)] just doesn't work with recursion, sadly.

Thanks again for your suggestion, I have now cleaned up the model in commit afbce94. (There was indeed an off-by-one mistake. If t=1, then replicate (t - 1) i doesn't add any elements, but if we want to keep the "delayed" semantics for stepper, then it should add one element. Of course, if we don't want the delayed semantics, then the code is fine. :smile:)

[HeinrichApfelmus]

I'll close this for now, but please don't hesitate to open it again if you like.