Should Validation be a Selective transformer?

[turion]

Either naturally generalises as a monad transformer, ExceptT, and we've recently established that this is a bona fide Selective transformer, meaning that there is a natural instance Selective f => Selective (ExceptT e f). I wonder whether there is also such an instance for

newtype ValidationT e f a = ValidationT { runValidationT :: f (Validation e a) }

The obvious question is whether this has the same Selective instance like ExceptT would have. I believe the instances of Either e and Validation e are isomorphic. But for a selective transformer, we probably also demand that lift :: f a -> ValidationT e f a defined by Validation . fmap Success should be a Selective morphism, and that law should be checked.

If this all works out, then maybe it makes sense to simply rename Control.Selective.Trans.Except to Control.Selective.Trans.Validation.

[snowleopard]

I think you are right that we can define ValidationT but the instance will probably be different: EitherT usually short-circuits the computation on the first failure, whereas Validation aggregates errors using the supplied Semigroup e.

[turion]

Ah, so the Applicative instances are different! Good point. Interesting, so ValidationT e m and ExceptT e m will be isomorphic as functors and as selectives, but not as applicatives. And yet the Selective instance will probably satisfy the compatibility laws with the Applicative instance (I'm just assuming this based on your Coq proof for Validation e). Yet another way how selectives can be subtly different.