Sun Aug 23 10:33:50 EDT 2015

sys vs <*>

  (Signal f0 f) <*> (Signal a0 a) = Signal (f0, a0) fa where
    fa (sf, sa) = do
      (sf', f') <- f sf
      (sa', a') <- a sa
      return ((sf', sa'), f' a')

sys p0 p (Signal i0 i) = Signal o0 o where
  o0 = (i0, p0)
  o (si, su) = do
    (si', i') <- i si
    (su', o') <- p su i'
    return $ ((si', su'), o')

for Applicative:

  s -> m (s, i -> m o)

for sys:

  s i -> m (s, o)

Not the same..

In any case, these are the key equations, realizing:
- there is an Applicative instance and,
- it is enough to have operators

shared implication:

  s -> m (s, i -> m o)     lift tuple to (i ->), m
  s -> m (i -> m (s, o))

  s i -> m (s, o)          lift (i ->) to m
  s -> m (i -> m (s, o))

Here are some proofs of type equivalences.  p4 is especially surprising to me.

-- Constructive proofs of normal forms
-- Applicative form to normal form.
p1 :: Monad m => (s -> m (s, i -> m o)) -> s -> m (i -> m (s, o))
p1 f s = return (\i -> do
                    (s', f') <- f s
                    o <- f' i
                    return (s', o))

-- Update equation form to normal form
p2 :: Monad m => (s -> i -> m (s, o)) -> s -> m (i -> m (s, o))
p2 f s = return (\i -> f s i)

-- Update equation inside monad.
p3 :: Monad m => (s -> m (i -> m (s, o))) -> m (s -> i -> m (s, o))
p3 f = return (\s i -> do
                  f' <- f s
                  f' i)

-- Lift inputs out again?
p4 :: Monad m => (m (s -> i -> m (s, o))) -> s -> i -> m (s, o)
p4 mf s i = do
  f <- mf
  f s i

It seems it is always possible to "undo" a wrapped or a lifted Kleisli

unlift1 :: Monad m => m (a -> m b) -> a -> m b
unlift1 mf a = do f <- mf; f a

unlift2 :: Monad m => (m a -> m b) -> a -> m b
unlift2 f = f . return

With this in mind, can Signal -> Signal maps be converted back to

p5 :: Monad m => ((s -> m (s, i)) -> s -> m(s, o)) -> s -> i -> m (s o)

That doesn't seem to be straightforward.  Is this strictly more general?
Nope, it should work something like this:

p5 f s i = (f (\() -> return ((), i))) s

But this needs the initial state to have a generic input s (here
replaced with unit ()).

So this works as well, but needs Signal, and will produce an
existential type as well.

So strangely, all these representations are as good as equivalent.

Maybe the misunderstanding comes from Signal not being an infinite
sequence, but a parameterized generator of such.

Essentially, a Signal is a Kleisli arrow, which has many lifted forms
that can be transformed back to a -> m b.

So is this relevant for mapping Signal -> Signal to something else?
Can't get (s->i->m(s,o)) because of the existential type.

Is it possible to do this:

unsys :: (Signal m i -> Signal m o) -> Signal m (i -> m o)

It's possible to construct this:
s -> i -> m (s, o)

But can that be converted to this?
s -> m (s, i -> m o)

It doesn't look like this is possible because s can't be moved outside
of (i->).