Open turion opened 2 years ago
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
.
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.
Either
naturally generalises as a monad transformer,ExceptT
, and we've recently established that this is a bona fideSelective
transformer, meaning that there is a natural instanceSelective f => Selective (ExceptT e f)
. I wonder whether there is also such an instance forThe obvious question is whether this has the same
Selective
instance likeExceptT
would have. I believe the instances ofEither e
andValidation e
are isomorphic. But for a selective transformer, we probably also demand thatlift :: f a -> ValidationT e f a
defined byValidation . fmap Success
should be aSelective
morphism, and that law should be checked.If this all works out, then maybe it makes sense to simply rename
Control.Selective.Trans.Except
toControl.Selective.Trans.Validation
.