SplineT fails right identity

[mitchellwrosen]

In trying to prove right identity for SplineT, I got stuck.

m >>= return = m

Here's what I got:

right identity
==============
m >>= return = m

-- Unwrap
SplineT v >>= return

-- Definition of >>=
SplineT (VarT (g (unSplineT (SplineT v))))
  where
    g v x = do
      (e, v') <- runVarT v x
      case e of
        Left  b -> pure (Left b, VarT (g v'))
        Right c -> runVarT (unSplineT (return c)) x))

-- Newtype
SplineT (VarT (g v))
  where
    g v x = do
      (e, v') <- runVarT v x
      case e of
        Left  b -> pure (Left b, VarT (g v'))
        Right c -> runVarT (unSplineT (return c)) x))

-- Definition of g
SplineT (VarT (\x -> do
  (e, v') <- runVarT v x
  case e of
    Left  b -> pure (Left b, VarT (g v'))
    Right c -> runVarT (unSplineT (return c)) x))
  where
    g v x = do
      (e, v') <- runVarT v x
      case e of
        Left  b -> pure (Left b, VarT (g v'))
        Right c -> runVarT (unSplineT (return c)) x))

  -- Case: e == Left b
  SplineT (VarT (\x -> do
    (e, v') <- runVarT v x
    pure (e, VarT (g v'))))

  -- Here, cannot reduce

At the end there, I'm trying to reduce that thing to just SplineT v. If VarT (g v') == v', then the proof would proceed as:

-- VarT (g v') = v'
SplineT (VarT (\x -> do
  (e, v') <- runVarT v x
  pure (e, v')

-- m >>= pure = m
SplineT (VarT (\x -> runVarT v x))

-- Eta reduction
SplineT (VarT (runVarT v))

-- Newtype
SplineT v

However, VarT (g v') is clearly not v' (equivalently, g is clearly not runVarT), per the definition of g. So, SplineT is unfortunately not a monad.

[schell]

I also get confused at the '-- Definition of g' step, and what I have to offer may not be valid but it could point you in the right direction. I propose that we can cancel out the Left case of e by considering that any m that matches Left will recurse until it matches Right. Let's assume it never concludes (and never matches Right). In that case return is never hit and by using a hand-wavey-law-of-infinities it can be removed, leaving us with m = m, which is true. This logic only holds if you believe exampleA = exampleB where:

exampleA :: Monad m => m ()
exampleA = fix $ \f -> f >>= return

exampleB :: Monad m => m ()
exampleB = fix $ \f -> f

It intuitively makes sense to me, since Infinity + 1 == Infinity, but I may not be able to use that argument here. If that's acceptable then we can go on and simplify only the Right path. ¯(ツ)/¯

[schell]

I didn't need fix in my example, it's easier just to ask if \f -> f is equivalent to \f -> f >>= return.

[schell]

I think we may be able to say that \f -> f >>= return = \f -> f because of the right identity monad law itself. So if we can simplify the Left path as a recursive function that never concludes (like simply \f -> f) then we can move on.

[schell]

So when e == Right c

SplineT (VarT (\x -> do
  (Right c, v') <- runVarT v x
  runVarT (unSplineT (return c)) x))

then we expand return c using the definition of pure

SplineT (VarT (\x -> do
  (Right c, v') <- runVarT v x
  runVarT (unSplineT (SplineT $ VarT $ const $ return (Right c, done $ Right c))) x))

we can then cancel the newtype stuff - both SplineT and VarT

SplineT (VarT (\x -> do
  (Right c, v') <- runVarT v x
  const $ return (Right c, done $ Right c) x))
-}

then get rid of const and x - and hide v'

SplineT (VarT (\x -> do
  (Right c, _) <- runVarT v x
  return (Right c, done $ Right c)))

maybe then we try substituting done...

SplineT (VarT (\x -> do
  (Right c, _) <- runVarT v x
  return (Right c, VarT $ \_ -> return (Right c, done b))))

where do we go next?

[schell]

I think the second to last step is it. If we assume that v is a VarT that produces a (Right c, _), then the snd in the returned tuple (done $ Right c) is never evaluated. It just produces (Right c, _). That also happens to be the form we see here. Does that mean equivalence?

SplineT (VarT (\x -> do
  (Right c, _) <- runVarT v x
  return (Right c, _)))

It may be easier to think about it in these terms - our original v must have been

let v = VarT (\_ -> do
          (Right c, _) <- runVarT v x
          return (Right c, done $ Right c))
in SplineT v

But we know that at this point the input value doesn't matter as we've hit bottom and are producing (Right c, _) indefinitely without evaluating the snd in the tuple, so we can get rid of x and use const

SplineT $ VarT $ const $ return (Right c, done $ Right c)

which is the definition of return c!

Maybe it's too late but that seems to make some sense...

[mitchellwrosen]

Consider the following:

foo :: VarT IO () (Either Int Bool)
foo = VarT (\() -> pure (Left 1, bar))

bar :: VarT IO (Either Int Bool)
bar = VarT (\() -> pure (Right True, foo))

spline :: SplineT () Int IO Bool
spline = SplineT foo

By the right identity law, we should have:

spline >>= return = spline

However, what I just derived on paper, which I will happily type up here (although I think you will immediately see the problem), is that

spline >>= return

is equivalent to

SplineT (VarT (\() -> pure (Left 1, pure (Right True))))

i.e. a spline that is left once, then right forever, as opposed to the original SplineT foo, which oscillates.

[mitchellwrosen]

Just throwing this type out there:

newtype SplineT a b m c = SplineT { runSplineT :: a -> m (Either c (b, SplineT a b m c)) }

instance Functor m => Functor (SplineT a b m) where
  fmap f = ...

instance Monad m => Monad (SplineT a b m) where
  return x = SplineT (\_ -> return (Left x))

  s >>= f = SplineT (\a ->
    runSplineT s a >>= \case
      Left c -> runSplineT (f c) a
      Right (b, s') -> return (Right (b, s' >>= f)))

(haven't proven the laws yet, but this one feels right to me). Does that look like a spline to you?

Edit: The laws do hold!

[schell]

Given the definition of >>= spline should produce the output value 1 and then return True. Any further evaluation using the spline machinery should continue to conclude in True. The underlying VarT that is used to create spline will oscillate, but the spline itself concludes.

I'll have to take a look at how to write outputStream and the other untilXXX combinators using the type you suggested. The whole point of SplineT is to sequence event streams into continuous streams - using VarT under the hood was a natural way to accomplish that. The type looks like a spline though :)

[mitchellwrosen]

Ah, I see what you are saying. I had another look at the API and yes, things like scanSpline do not let you observe the difference. However, runSplineT is exported, and with it, you can:

foo :: VarT IO () (Either Int Bool)
foo = VarT (\() -> pure (Left 1, bar))

bar :: VarT IO () (Either Int Bool)
bar = VarT (\() -> pure (Right True, foo))

-- Just print everything that comes out of the inner VarT
debugSpline :: (Show b, Show c) -> SplineT a b IO c -> [a] -> IO ()
debugSpline (SplineT v0) = go v0
 where
  go _ [] = pure ()
  go v (a:as) = do
    (b, v') <- runVarT v a
    print b
    go v' as

spline :: SplineT () Int IO Bool
spline = SplineT foo

> debugSpline spline [(),(),(),()]
Left 1
Right True
Left 1
Right True

> debugSpline (spline >>= return) [(),(),(),()]
Left 1
Right True
Right True
Right True

[schell]

Yeah, you're right - and your type suggestion actually makes things much more simple, so I'm trying it out. If I get the same performance (I'm guessing the less complex code will be better than or equal to) then this will be great, thanks! 👍

[mitchellwrosen]

No problem!

On Sep 12, 2016 12:33 AM, "Schell Carl Scivally" notifications@github.com wrote:

Yeah, you're right - and your type suggestion actually makes things much more simple, so I'm trying it out. If I get the same performance (I'm guessing the less complex code will be >=) then this will be great, thanks! 👍

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/schell/varying/issues/8#issuecomment-246242610, or mute the thread https://github.com/notifications/unsubscribe-auth/ABBlprkaoD0z8v2w-Pp0vJ8SSZzSCu2Qks5qpNX8gaJpZM4J53Em .

[schell]

Performance is just fine on #9 :)

[schell]

@mitchellwrosen - do you still have the spline proofs? I'd like to include them in the next version of the documentation, if so! 👍

[mitchellwrosen]

I actually don't, but I can write them up again! Can you assign an issue to me?

[schell]

Yes! Thanks! I think we're pretty ready for a 1.0 release, but I'd like to put your proofs in the docs first 💯

[mitchellwrosen]

Huh, I just made a funny observation. SplineT a b m c is just the fixpoint of the following functor:

(a ->) . m . Either c . (b ,)

that is,

-- newtype Fix f = Fix (f (Fix f))

infixr :.
type (:.) = Compose -- Data.Functor.Compose

type SplineT a b m c = Fix ((->) a :. m :. Either c :. (,) b)

This isn't really relevant to the monad instance, but still fun to think about :P

[schell]

Huh - I guess I didn't realize you could 'fix' at the type level. Cool!