[<<][meta_siso][>>][..]Sun Aug 23 10:33:50 EDT 2015

(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 arrow: 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 systems? 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. Strange. 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->).

[Reply][About]

[<<][meta_siso][>>][..]