Is this property of a functor stronger than a monad?
To improve terminology a little bit, I propose to call these functors "rigid" instead of "bindable". The motivation for saying "rigid" will be explained below.
Definition
A functor f
is called rigid if it has the inject
method as shown. Note that every functor has the eject
method.
class (Functor f) => Rigid f where
inject :: (a -> f b) -> f(a -> b)
eject :: f(a -> b) -> a -> f b
eject fab x = fmap (\ab -> ab x) fab
The law of "nondegeneracy" must hold:
eject . inject = id
Properties
A rigid functor is always pointed:
instance (Rigid f) => Pointed f where
point :: t -> f t
point x = fmap (const x) (inject id)
If a rigid functor is applicative then it is automatically monadic:
instance (Rigid f, Applicative f) => Monad f where
bind :: f a -> (a -> f b) -> f b
bind fa afb = (inject afb) <*> fa
The property of being rigid is not comparable (neither weaker nor stronger) than the property of being monadic: If a functor is rigid, it does not seem to follow that it is automatically monadic (although I don't know specific counterexamples for this case). If a functor is monadic, it does not follow that it is rigid (there are counterexamples).
Basic counterexamples of monadic functors that are not rigid are Maybe
and List
. These are functors that have more than one constructor: such functors cannot be rigid.
The problem with implementing inject
for Maybe
is that inject
must transform a function of type a -> Maybe b
into Maybe(a -> b)
while Maybe
has two constructors. A function of type a -> Maybe b
could return different constructors for different values of a
. However, we are supposed to construct a value of type Maybe(a -> b)
. If for some a
the given function produces Nothing
, we don't have a b
so we can't produce a total function a->b
. Thus we cannot return Just(a->b)
; we are forced to return Nothing
as long as the given function produces Nothing
even for one value of a
. But we cannot check that a given function of type a -> Maybe b
produces Just(...)
for all values of a
. Therefore we are forced to return Nothing
in all cases. This will not satisfy the law of nondegeneracy.
So, we can implement inject
if f t
is a container of "fixed shape" (having only one constructor). Hence the name "rigid".
Another explanation as to why rigidity is more restrictive than monadicity is to consider the naturally defined expression
(inject id) :: f(f a -> a)
where id :: f a -> f a
. This shows that we can have an f-algebra f a -> a
for any type a
, as long as it is wrapped inside f
. It is not true that any monad has an algebra; for example, the various "future" monads as well as the IO
monad describe computations of type f a
that do not allow us to extract values of type a
- we shouldn't be able to have a method of type f a -> a
even if wrapped inside an f
-container. This shows that the "future" monads and the IO
monad are not rigid.
A property that is strictly stronger than rigidity is distributivity from one of E. Kmett's packages. A functor f
is distributive if we can interchange the order as in p (f t) -> f (p t)
for any functor p
. Rigidity is the same as being able to interchange the order only with respect to the "reader" functor r t = a -> t
. So, all distributive functors are rigid.
All distributive functors are necessarily representable, which means they are equivalent to the "reader" functor c -> t
with some fixed type c
. However, not all rigid functors are representable. An example is the functor g
defined by
type g t = (t -> r) -> t
The functor g
are not equivalent to c -> t
with a fixed type c
.
Constructions and examples
Further examples of rigid functors that are not representable (i.e. not "distributive") are functors of the form a t -> f t
where a
is any contrafunctor and f
is a rigid functor. Also, the Cartesian product and the composition of two rigid functors is again rigid. In this way, we can produce many examples of rigid functors within the exponential-polynomial class of functors.
My answer to What is the general case of QuickCheck's promote function? also lists the constructions of rigid functors:
f = Identity
- if
f
andg
are both rigid then the functor producth t = (f t, g t)
is also rigid - if
f
andg
are both rigid then the compositionh t = f (g t)
is also rigid - if
f
is rigid andg
is any contravariant functor then the functorh t = g t -> f t
is rigid
One other property of rigid functors is that the type r ()
is equivalent to ()
, i.e. there is only one distinct value of the type r ()
. This value is point ()
, where point
is defined above for any rigid functor r
. (I have a proof but I will not write it here, because I could not find an easy one-line proof.) A consequence is that a rigid functor must have only one constructor. This immediately shows that Maybe
, Either
, List
etc. cannot be rigid.
Connection with monads
If f
is a monad that has a monad transformer of the "composed-outside" kind, t m a = f (m a)
, then f
is a rigid functor.
The "rigid monads" are possibly a subset of rigid functors because construction 4 only yields a rigid monad if f
is also a rigid monad rather than an arbitrary rigid functor (but the contravariant functor g
can still be arbitrary). However, I do not have any examples of a rigid functor that is not also a monad.
The simplest example of a rigid monad is type r a = (a -> p) -> a
, the "search monad". (Here p
is a fixed type.)
To prove that a monad f
with the "composed-outside" transformer t m a = f (m a)
also has an inject
method, we consider the transformer t m a
with the foreign monad m
chosen as the reader monad, m a = r -> a
. Then the function inject
with the correct type signature is defined as
inject = join @t . return @r . (fmap @m (fmap @f return @m))
with appropriate choices of type parameters.
The non-degeneracy law follows from the monadic naturality of t
: the monadic morphism m -> Identity
(substituting a value of type r
into the reader) is lifted to the monadic morphism t m a -> t Id a
. I omit the details of this proof.
Use cases
Finally, I found two use cases for rigid functors.
The first use case was the original motivation for considering rigid functors: we would like to return several monadic results at once. If m
is a monad and we want to have fbind
as shown in the question, we need f
to be rigid. Then we can implement fbind
as
fbind :: m a -> (a -> f (m b)) -> f (m b)
fbind ma afmb = fmap (bind ma) (inject afmb)
We can use fbind
to have monadic operations that return more than one monadic result (or, more generally, a rigid functor-ful of monadic results), for any monad m
.
The second use case grows out of the following consideration. Suppose we have a program p :: a
that internally uses a function f :: b -> c
. Now, we notice that the function f
is very slow, and we would like to refactor the program by replacing f
with a monadic "future" or "task", or generally with a Kleisli arrow f' :: b -> m c
for some monad m
. We, of course, expect that the program p
will become monadic as well: p' :: m a
. Our task is to refactor p
into p'
.
The refactoring proceeds in two steps: First, we refactor the program p
so that the function f
is explicitly an argument of p
. Assume that this has been done, so that now we have p = q f
where
q :: (b -> c) -> a
Second, we replace f
by f'
. We now assume that q
and f'
are given. We would like to construct the new program q'
of the type
q' :: (b -> m c) -> m a
so that p' = q' f'
. The question is whether we can define a general combinator that will refactor q
into q'
,
refactor :: ((b -> c) -> a) -> (b -> m c) -> m a
It turns out that refactor
can be constructed only if m
is a rigid functor. In trying to implement refactor
, we find essentially the same problem as when we tried to implement inject
for Maybe
: we are given a function f' :: b -> m c
that could return different monadic effects m c
for different b
, but we are required to construct m a
, which must represent the same monadic effect for all b
. This cannot work, for instance, if m
is a monad with more than one constructor.
If m
is rigid (and we do not need to require that m
be a monad), we can implement refactor
:
refactor bca bmc = fmap bca (inject bmc)
If m
is not rigid, we cannot refactor arbitrary programs. So far we have seen that the continuation monad is rigid, but the "future"-like monads and the IO
monad are not rigid. This again shows that rigidity is, in a sense, a stronger property than monadicity.
Here is one possible presentation of rigid functors. I have taken the liberty to bikeshed your names a bit, for reasons I'll soon get to:
flap :: Functor f => f (a -> b) -> a -> f b
flap u a = ($ a) <$> u
class Functor g => Rigid g where
fflip :: (a -> g b) -> g (a -> b)
fflip f = (. f) <$> extractors
extractors :: g (g a -> a)
extractors = fflip id
-- "Left inverse"/non-degeneracy law: flap . fflip = id
instance Rigid ((->) r) where
fflip = flip
Some remarks on my phrasing:
I have changed the names of
inject
andeject
tofflip
andflap
, mainly because, to my eyes,flap
looks more like injecting, due to things like this:sweep :: Functor f => f a -> b -> f (a, b) sweep u b = flap ((,) <$> u) b
I took the
flap
name from protolude. It is a play onflip
, which is fitting because it is one of two symmetrical ways of generalising it. (We can either pull the function outside of an arbitraryFunctor
, as inflap
, or pull aRigid
functor outside of a function, as infflip
.)extractors
andfflip
are interdefinable, making it possible to write, for example, this neat instance for the search/selection monad:newtype Sel r a = Sel { runSel :: (a -> r) -> a } deriving (Functor, Applicative, Monad) via SelectT r Identity instance Rigid (Sel r) where -- Sel r (Sel r a -> a) ~ ((Sel r a -> a) -> r) -> Sel r a -> a extractors = Sel $ \k m -> m `runSel` \a -> k (const a)
A significant fact about extractors
is that it gives rise to the following combinator:
distributeLike :: (Rigid g, Functor f) => f (g a) -> g (f a)
distributeLike m = (<$> m) <$> extractors
distributeLike
is a more general version of distribute
from the Distributive
class. A lawful distribute
, in turn, must abide by the following laws, which are dual to the laws of Traversable
:
-- Identity law
fmap runIdentity . distribute = runIdentity
-- Composition law
fmap getCompose . distribute = distribute . fmap distribute . getCompose
-- Naturality law (always holds, by parametricity)
-- For any natural transformation t
fmap t . distribute = distribute . t
Since fflip
is distributeLike
with reader (that is, the function functor) as the other functor, and that flap
is distribute
for reader, both flap . fflip = id
and fflip . flap = id
are special cases of...
-- m :: f (g a)
distributeLike (distributeLike m) = m
... with appropriate choices of f
and g
. Now, the property above can be shown to be equivalent to the following conditions:
distributeLike
forg
follows the identity law of distributive functors (which, by the way, is equivalent to the rigid law);distributeLike
forf
also follows the identity law of distributive functors;Either of the following equivalent conditions hold:
a.
distributeLike
forf
follows the composition law of distributive functors; orb. All
f a -> a
functions made available byextractors
forf
are natural ina
.
In particular, as flap
is a lawful distribute
, flap . fflip = id
amounts to the identity law for g
(condition #2), and fflip . flap = id
, to f
being distributive (conditions #1 and #3).
(The conditions above can be established by analysing distributeLike . distributeLike = id
in terms of extractors
, following a similar strategy to the one I applied to the composition law in the "The roadblock, and a detour" section of my post "Every Distributive is Representable".)
For the sake of illustration, let's consider the case of Sel r
. As you note, it is rigid but not distributive, its distributeLike
follows the identity law but not the composition one. Accordingly, fflip . flap = id
does not hold.
With respect to finding a place for Rigid
in the type class constellation, I would highlight condition #3b as being particularly interesting. It appears that, given how extractors @f :: forall a. f (f a -> a)
is fully polymorphic in a
, for it to provide non-natural f a -> a
extractors f
must not be strictly positive, corresponding to construction #4 in the "Constructions and examples" section of your answer. The lack of strict positivity makes it possible for extractors
to incorporate non-naturality (through a user-supplied contravariant argument) without having it specified explicitly in its definition. That being so, only functors that aren't strictly positive, such as Sel r
, might be rigid without being distributive.
Miscellaneous remarks
Looking at
fflip
andflap
from a monadic point of view, we might say that rigid monads are equipped with an injective conversion from Kleisli arrows to static arrows. With distributive monads, the conversion is upgraded to an isomorphism, which is a generalisation of howApplicative
andMonad
are equivalent forReader
. One curious aspect of non-distributive rigid monads is thatfflip
being injective but not surjective implies that there are more static arrows than Kleisli arrows, which is a quite unusual state of affairs.extractors
condenses much of whatDistributive
is about. For any distributive functorg
, there is ag (g a -> a)
value in which each position is filled with a matchingg a -> a
natural extractor function. With rigid functors that aren't distributive, this tidy correspondence no longer holds. WithSel r
, for instance, everya -> r
gives rise to an extractor, which generally isn't natural. That ultimately precludes havingdistribute
/fflip
(and also, by the way,tabulate
) as isomorphisms. In fact, the very notion of a shape with well-defined positions arguably breaks down when dealing with functors that aren't strictly positive.Distributive
is dual toTraversable
, and there are several correspondences between facts about the two classes. (In particular, the presentation ofDistributive
asRepresentable
, in terms of an isomorphism to the reader functor, mirrors the shape-and-contents formulation ofTraversable
, which can be expressed in terms of an isomorphism to some list-like functor.) That being so, one might wonder if a notion analogous toRigid
make sense forTraversable
. I believe it does, though it is unclear how useful such a concept could possibly be. One example of a "co-rigid" pseudo-traversable would be a data structure equipped with a traversal that duplicates effects, but then discards the corresponding duplicate elements upon rebuilding the structure under the applicative layer, so that the identity law is followed, but not the composition one.