Instances of transformers not needing the Monad constraint?

[turion]

Is there for example an instance:

instance Selective f => Selective (ReaderT r f a)

[snowleopard]

@turion Interesting question! Here is an instrance for ReaderT:

instance Selective f => Selective (ReaderT env f) where
    select (ReaderT x) (ReaderT f) = ReaderT $ \env -> select (x env) (f env)

I guess this should trivially satisfy the laws since accessing the environment env is not an observable effect.

I wonder if we can prove that the behaviour we get must coincide with that of the existing instance with the Monad constraint. If yes, then we should export the above instance, since it's more general.

[turion]

Assuming that select = selectM for f, we have:

ReaderT $ \env -> select (x env) (f env)
= ReaderT $ \env -> selectM (x env) (f env)
= ReaderT $ \env -> x env >>= \e -> case e of
    Left  a -> ($a) <$> f env
    Right b -> pure b
= ReaderT $ \env -> do
    e <- x env
    case e of
      Left  a -> ($a) <$> f env
      Right b -> pure b

On the other hand, consider >>= for ReaderT (https://hackage.haskell.org/package/transformers-0.5.2.0/docs/src/Control.Monad.Trans.Reader.html#line-148), which is:

ReaderT m >>= k = ReaderT $ \env -> do
  e <- m env
  runReaderT (k e) env

Then selectM for ReaderT r f expands as follows:

selectM (ReaderT x) (ReaderT f)
-- definition of selectM
= (ReaderT x) >>= \e -> case e of
    Left  a -> ($a) <$> (ReaderT f)
    Right b -> pure b
-- definition of >>=
= ReaderT $ \env -> do
    e <- x env
    runReaderT (case e of
      Left  a -> ($a) <$> (ReaderT f)
      Right b -> pure b
    ) env
-- evaluate runReaderT in both branches
= ReaderT $ \env -> do
    e <- x env
    case e of
      Left  a -> runReaderT (($a) <$> (ReaderT f)) env
      Right b -> runReaderT (pure b) env

Then by looking up the definitions of fmap and pure for ReaderT one arrives at the other implementation.

I'm pretty sure you can prove something like that for other transformers as well.

[turion]

Here is an interesting observation related to this:

The signature for the Applicative instance of ExceptT is (https://hackage.haskell.org/package/transformers-0.5.6.2/docs/Control-Monad-Trans-Except.html#t:ExceptT):

(Functor m, Monad m) => Applicative (ExceptT e m)

One would think that (Applicative m) => Applicative (ExceptT e m) should be sufficient. But it isn't. When ap-ing ExceptT f <*> ExceptT a, one needs to inspect in which branch of m (Either e a) f is! So one needs exactly Selective to make ExceptT an Applicative!

To me this sounds like there should be yet another Either-related transformer newtype EitherT m e a = EitherT { runEitherT :: m (Either e a) } which has the following instance:

instance Selective m => Applicative (EitherT m e) where
...

This is not the same as ComposeEither, because that executes all effects. This new variant here does not execute the effect of a in f <*> a when f throws an error.

Semantically this is the same as the transformers implementation: https://hackage.haskell.org/package/transformers-0.5.6.2/docs/src/Control.Monad.Trans.Except.html#line-186

I stumbled upon this because I wanted to implement instance Selective m => Selective (ExceptT e m). But this is not possible because Applicative (ExceptT e m) needs Monad m, because when transformers was written they didn't know about Selective. But for this new EitherT we can implement such an instance.

[snowleopard]

@turion Your proof sketch looks convincing. I've added more general instances for IdentityT and ReaderT in #38.

Here is an interesting observation related to this [...]

Oh, wow, that's so cool! It's a shame we can't have a meaningful instance Selective m => Selective (ExceptT e m) because the applicative instance currently requires a monad. I don't mind adding a new module Control.Selective.EitherT which declares all the instances as you described. Would you like to do it? Happy to review!

[turion]

Here is an interesting observation related to this [...]

Oh, wow, that's so cool! It's a shame we can't have a meaningful instance Selective m => Selective (ExceptT e m) because the applicative instance currently requires a monad. I don't mind adding a new module Control.Selective.EitherT which declares all the instances as you described. Would you like to do it? Happy to review!

Yes, I'll give it a try.

[turion]

StateT can't work fundamentally, thus RWST neither. It remains to be seen whether ContT works, but I'm pessimistic ;)

[turion]

It remains to be seen whether ContT works, but I'm pessimistic ;)

ContT has no contraints at all, so there is nothing to do there.

The only transformers for which it works then are WriterT, ExceptT and MaybeT.

AccumT doesn't work for the same reason as StateT: If you have something of type s -> m x, you can't make an m (s -> x) from it for a general selective m. (Otherwise Selective was the same as Monad I think.) But you need it to pass the previously computed state to the later continuation. Maybe something can be done with Control.Selective.Multi and an extra constraint on the state type, but then the instances don't form a hierarchy anymore, since the Monad (StateT s m) instance doesn't need that extra constraint on the state type.

[snowleopard]

@turion I agree with your analysis: state-passing seems monadic in nature.

I wonder if switching from s -> f (a, s) to f (s -> (a, s)) gives you anything useful. Probably not?

[turion]

I wonder if switching from s -> f (a, s) to f (s -> (a, s)) gives you anything useful. Probably not?

This is a transformer as far as I know, but it's strictly less expressive than StateT. For example, I believe that you can't even write the following program:

main = flip evalStateT 23 $ do
  n <- get
  lift $ print n

[snowleopard]

We now know that we can implement instances for IdentityT, ReaderT, WriterT, ExceptT and MaybeT. And that we can't for StateT and AccumT.

Can we characterise the functors on both sides somehow?

[turion]

One thing that springs to my mind is that the ones for which it works are all of the form Compose f m or Compose m f, where m is the inner monad of the transformer, and f is Identity,Reader r,Writer r, and so on.StateT s mandAccumT w mare not simple compositions ofm` with another functor.

Given that we have Applicative f, Selective g => Selective (Compose f g) (where g is inner), but not the other way around (https://github.com/snowleopard/selective/issues/12), only some these transformer instances can be of that form. Let's see.

• ReaderT r m = Compose (Reader r) m
• WriterT w m = Compose m (Writer w)
• ExceptT e m = Compose m (Either e)

I'm pretty sure that the ReaderT r m and Compose (Reader r) m instances are equivalent. However, the WriterT w m instance uses Selective m, whereas Compose m (Writer w) doesn't. It's two different stories again for ExceptT, keeping in mind that I wrote a new ExceptT instance (https://github.com/snowleopard/selective/pull/39) with Selective m => Applicative ExceptT e m, whereas the transformers version doesn't have this constraint. Confusing.

I'd suspect that there is a more efficient way of composing two selectives, i.e. Selective f, Selective g => Selective (Compose f g), but I can't figure it out.

Another angle might be that Writer w and Either e can be "inspected" in a way that IO can't, and therefore it's possible to write instances that are not possible for a general Selective. In that case, the task lies in expressing what exactly "can be inspected" means.

[turion]

Is there a sensible ListT instance? Because ListT done right also isn't a composition.

[snowleopard]

I don't think there exists an "interesting" implementation of Selective f, Selective g => Selective (Compose f g). There are some comments in the sources:

https://github.com/snowleopard/selective/blob/598558581f198727cafbec88f270ffffae67bb98/src/Control/Selective.hs#L469-L483

Do they look convincing?

I do agree with you, however, that composition seems key to the question. Perhaps, we need some additional constraints to make the composition work, like Inspectable?

In that case, the task lies in expressing what exactly "can be inspected" means.

One direction that seemed promising, but which I didn't have time to explore, is functors that have some limited form of join. See "Composing Monads" by Mark Jones (particularly prod and dorp): http://web.cecs.pdx.edu/~mpj/pubs/composing.html.

[turion]

Do they look convincing?

Yes, that's why I meant that inspecting might be important.

I do agree with you, however, that composition seems key to the question. Perhaps, we need some additional constraints to make the composition work, like Inspectable?

I don't know that typeclass and can't find anything on it.

I usually think about "being able to inspect a functor" as "container functors", "polynomial functors", or "strictly polynomial functors". (See e.g. https://en.wikipedia.org/wiki/Container_(type_theory)#Indexed_containers, https://bartoszmilewski.com/2014/01/14/functors-are-containers/ for some intuition, https://www.cs.le.ac.uk/people/mabbott/docs/appsem.pdf) Every such functor has "shapes" and "positions. Shapes say which different variants of that functor can occur, and positions say how many elements of the type are present. For example Maybe has two shapes, Just and Nothing. Just has one position (since Just a contains one a) and Nothing has no positions. A lot of functors are containers:

Functor	Shapes	Positions
Maybe a	Just, Nothing	Just: 1, Nothing: 0
[a]	One for every natural number n (corresponding to the list of length n	The number n has n positions (one for every list element
Either e a	Right, Left e for every e	Right: 1, Left e: 0
State s a	One for every function s -> s	Each shape has s positions

Reader, Writer, Accum, Identity, and all "algebraic" functors are all containers. I think even FreeT and ProgramT are. All additional structures like natural transformations, Applicative, Selective, Monad etc. can be expressed in container language very nicely (but one needs dependent types).

Two prominent counterexamples are ContT r m (it's always a counterexample) and IO. For IO the reason is simply that it is an opaque builtin that doesn't have any structure that is visible to the user. That's simply a design decision. But IO is not a special in that regard. Other counterexamples are the somewhat arcane SelectT (not related to Selective) and LogicT.

So we might think that if the outer functor f is Selective (let's take f = Maybe for example) and the inner g is Selective and a container, we could write:

select :: Maybe (g (Either a b)) -> Maybe (g (a -> b)) -> Maybe (g b) 
select Nothing  _        = Nothing 
select (Just x) (Just y) = Just (select x y) 
select (Just x) Nothing  = _ -- Now inspect `x` whether it contains only `Right b`s, and if yes, extract the obvious `g b`

Unfortunately it's not possible to express in Haskell what a container functor is. But it gives me an idea... I'll comment on https://github.com/snowleopard/selective/issues/12.

One direction that seemed promising, but which I didn't have time to explore, is functors that have some limited form of join. See "Composing Monads" by Mark Jones (particularly prod and dorp): http://web.cecs.pdx.edu/~mpj/pubs/composing.html.

prod and dorp are functions with two type parameters, though (both monads). The advantage of monad transformers is that to make t m a monad we only need m to be a monad, and not have any structure that depends on both. That avoids the "quadratic instance problem" faced by mtl.

Applied to selective, I want to say that it wouldn't be very useful to find a typeclass WillComposeWell f g such that we have instance (Selective f, WillComposeWell f g) => Selective (Compose f g). We should look for a unary constraint on g instead.

[snowleopard]

I do agree with you, however, that composition seems key to the question. Perhaps, we need some additional constraints to make the composition work, like Inspectable?

I don't know that typeclass and can't find anything on it.

Ah, sorry, I meant a hypothetical Inspectable. I don't really know how this type class should really look like.

Thanks for your further comments. I'm familiar with container functors a bit, but I've never viewed them as equivalent to "inspectable functors". That may well be a valid viewpoint, but I don't see how to formally justify it.

[turion]

I'm familiar with container functors a bit, but I've never viewed them as equivalent to "inspectable functors". That may well be a valid viewpoint, but I don't see how to formally justify it.

The more I think about it: Probably the only relevant thing about container functors here is roughly that when all positions of a container are finite, then it is Traversable.

[snowleopard]

@turion Thanks for finishing #39!

Shall we add the Maybe transformer too? I suppose it's just a stripped-down version of the Except transformer.

[turion]

Ah right. Do you want that as a newtype ExceptT (), (less implementation, more conversion), or as a newtype over transformers MaybeT? -- Diese Nachricht wurde von meinem Android-Gerät mit K-9 Mail gesendet.

[snowleopard]

I think I'd prefer to avoid the indirection via ExpectT.