Doesn't support transformer state that depends on the transformed monad

[ehird]

Hi,

I have a monad that looks like

newtype FooT s m a = FooT { unFooT :: StateT (Bar m s) m a }

The problem here is that Bar m s is part of the monadic state, and depends on m, so an attempt to define the associated StT falls down:

data StT (FooT s) a = StFoo (Bar m s) a

(m is unbound.)

Do you have any suggestions for solving this issue? I think it's a limitation in monad-control, but I'm not quite sure.

The definition of Bar in my code is as follows:

newtype Bar m s = Bar { unBar :: m (s, Bar m s) }

(obviously it's not called Bar though :))

[basvandijk]

Yes, this is a known limitation of monad-control.

Note that it's also a limitation of previous versions of monad-control and also of the original monad-peel since there the restore computation also doesn't depend on m:

t m a -> m (t o a)

to quote monad-peel for the reason for this:

"...this type ensures that the result of running the action in m has no remaining side effects in m."

However, I'm not sure anymore why this is important. I will ask Anders Kaseorg (author of monad-peel) about this.

[ehird]

OK, thanks.

I agree with that quote that ensuring the specific choice of monad m cannot be exploited is a good idea, but I think this is ensured by the polymorphism of liftWith. So adding an m parameter to StT and Run seems like it would work to me.

[basvandijk]

Do you mean something like this:

class MonadTrans t ⇒ MonadTransControl t where
  data StT t ∷ (* → *) → * → *
  liftWith ∷ (Monad m, Monad o) ⇒ (Run t o → m α) → t m α
  restoreT ∷ (Monad m, Monad o) ⇒ m (StT t o α) → t m α

type Run t (o ∷ * → *) = ∀ n β. (Monad n) ⇒ t n β → n (StT t o β)

However the polymorphicness of this is problematic for your FooT type:

newtype FooT s m a = FooT { unFooT :: StateT (Bar m s) m a }

newtype Bar m s = Bar s

instance MonadTrans (FooT s) where
    lift = FooT ∘ lift

instance MonadTransControl (FooT s) where
    newtype StT (FooT s) o α = StFoo {unStFoo ∷ (α, Bar o s)}
    liftWith f = FooT $ StateT $ \bar →
                   liftM (\x → (x, bar))
                         (f $ \t → liftM StFoo $ runStateT (unFooT t) bar)
    restoreT = FooT ∘ StateT ∘ const ∘ liftM unStFoo

Here the type checker will complain that in can't deduce (n ~ o) and (m ~ o).

Or do you have something else in mind?

[ehird]

Here is what I imagined:

type Run t m = ∀ β. t m β → m (StT t m β)

class MonadTrans t ⇒ MonadTransControl t where
  data StT t ∷ (* → *) * → *
  liftWith ∷ Monad m ⇒ (Run t m → m α) → t m α
  restoreT ∷ Monad m ⇒ m (StT t m α) → t m α

I have no idea if this would work or not, but it seems correct to me.

(edit: Turned off syntax highlighting since it was flagging up all the Unicode as invalid.)

(edit 2: Corrected Unicode mix-up.)

[basvandijk]

monad-control does build successfully with this change.

And it supports making your FooT an instance of MonadTransControl:

instance MonadTransControl (FooT s) where
    newtype StT (FooT s) m α = StFoo {unStFoo ∷ StT (StateT (Bar m s)) m α}
    liftWith f = FooT $ liftWith $ \run → f (liftM StFoo ∘ run ∘ unFooT)
    restoreT = FooT ∘ restoreT ∘ liftM unStFoo

However users can make more errors with it like:

instance MonadTransControl (StateT s) where
    newtype StT (StateT s) m α = StState {unStState ∷ StateT s m α}
    liftWith f = lift $ f $ return ∘ StState
    restoreT m = StateT $ \s -> m >>= \st → runStateT (unStState st) s

This looks a bit like the problematic code that Anders posted in his email to us:

peel = lift (return return)

I'm not sure how bad it is to allow this.

A solution could be to add more laws that ban this definition. I don't think the current set of laws is sufficient:

 liftWith . const . return = return
 liftWith (const (m >>= f)) = liftWith (const m) >>= liftWith . const . f
 liftWith (\run -> run t) >>= restoreT . return = t

If you know a law that I missed please post it.

Cheers,

Bas

[ehird]

Hmm. The problem is that we want a value of type StT t m a to contain the post-execution state and result of the action, but adding m as a parameter lets us use the computation itself.

I think this could be fixed with a really silly, lawless addition to the typeclass:

value :: ST t m α → α

Then the only monadic computations you can define ST to be are ones that are isomorphic to the "correct" definitions (consider that Writer w α is exactly the current definition of StT (WriterT w) α).

But this feels like a hack.

Edit: Actually, if adding value doesn't break any instances, then we can simply have:

type Run t m = ∀ β. t m β → m (β, StT t m)

class MonadTrans t ⇒ MonadTransControl t where
  data StT t ∷ (* → *) → *
  liftWith ∷ Monad m ⇒ (Run t m → m α) → t m α
  restoreT ∷ Monad m ⇒ m (α, StT t m) → t m α

I actually like this a lot: the monadic state of t m α is the resulting α, plus the transformer-specific state.

It might be worth making (α, StT t m) a data-type, since it's used twice there.

Edit 2: Hmm, this doesn't work; the MaybeT/ErrorT/ListT instances break it. On this basis, I question the correctness of the cpp-generated [] instance...

Edit 3: By the way, the documentation for Run is wrong after that change :)

[ehird]

An idea that occurs to me as far as adding laws goes is to add one to make sure that restoring a single StT value is idempotent: that is, since it captures the post-execution state of the transformer, restoring it twice should be the same as restoring it once.

Then the pathological StateT definition would be banned, because e.g. restoring modify f twice would result in the state being applied to f twice, not once.

Further along those lines, it might be a good idea to express that the restoration must be agnostic as to whatever the current state is: restoring modify f with the broken StateT definition depends on the transformer state at the time of restoration, which is incorrect. But I have a feeling that the idempotency property ensures this, i.e. if restoration depends on current state, then you can construct an initial state value for which restoration of a given state isn't idempotent.

restoreT (return st) >> restoreT (return st) >> m = m is a consequence of idempotency, but feels too weak to be an expression of the property itself.

[basvandijk]

restoreT (return st) >> restoreT (return st) >> m = m

I assume you mean:

restoreT (return st) >> restoreT (return st) >> m = restoreT (return st) >> m

I like it! Maybe we can make it a bit stronger by using a bind instead of >> m as in:

restoreT (return st) >> restoreT (return st) >>= f = restoreT (return st) >>= f

[ehird]

Yes, that works, though it can be simplified and generalised to:

restoreT (return st) >> restoreT (return st') = restoreT (return st')

However, I think I have a better solution. I have devised a new MonadTransControl definition that:

1. supports all current instances correctly;
2. supports FooT perfectly; and
3. simplifies the types (it doesn't even require RankNTypes!)

Edit 2: Oh, I forgot to mention the main benefit to this new design: 4. it doesn't allow you to exploit polymorphism a la the broken StateT instance.

I've put it on hpaste; basically, StT t a is the result of a transformed computation of type t m a (for some m), and SuT t m is the state of a transformed computation of type t m a (for some a). (These should probably be renamed; "Su" is meant to evoke "suspended", i.e. suspended state, but "St" makes no sense as a name with this new scheme).

suspendT lets us capture the state of a transformed computation at any point, runT lets us execute a transformed computation in a given state, producing the result and the final state, and restoreT lets us reify result + state into a transformed computation.

I tried to match the existing style in monad-control for the RWST instance to make things clearer, but as seen in e.g. the StateT instance, while this definition is slightly more verbose for simple transformers, it's simpler for more complex ones.

This is the easy part; the hard parts are

1. finding laws;
2. porting MonadBaseControl, etc.;
3. benchmarking it; and
4. finding something time-consuming to do so that API-compatibility isn't broken twice in one month :-)

Two obvious laws to start with are

restoreT st su >> restoreT st' su' = restoreT st' su'
suspendT >> suspendT = suspendT

Thanks for reading this babble; I'd love to know what you think of this scheme and, especially, if you have any ideas on how to simplify it. :-)

Edit: And another, scarier law: suspendT >>= \su -> runT su m >>= uncurry restoreT = m.

[ehird]

Just pinging this issue in case my comment fell through the cracks — no problem if you don't have any comments yet :)

[basvandijk]

Sorry Elliott, I didn't have time yet to carefuly look at your implementation. I will try do to it this weekend.

[ehird]

Great, just checking; I've heard of GitHub failing to mail about issue comments before...

[arybczak]

What is the status of this issue?

[basvandijk]

Basically I forgot about it.

What would help the issue is:

• see if we can base it on the current monad-control (based on associated type synonyms).
• prove with some benchmarks that it doesn't slow things down by too much.
• investigate how much API breakage this will cause.

Due to being very busy at my new startup I don't have time to do any of these things.

[treeowl]

I know this is really old, but another example to consider is ListT (from list-t). It has an instance of MonadBaseControl but doesn't seem eligible for an instance of MonadTransControl. It looks like

newtype ListT m a = ListT m (Maybe (a, ListT m a))

So the result of running one layer may include more layers, which depend on m.

[treeowl]

@ehird, your hpaste is gone. Is your code available anywhere else?