While thinking about how to generalize monads, I came up with the following property of a functor F:
inject :: (a -> F b) -> F(a -> b)
-- which should be a natural transformation in both a and b.
In absence of a better name, I call the functor F bindable if there exists a natural transformation inject
shown above.
The main question is, whether this property is already known and has a name, and how is it related to other well-known properties of functors (such as, being applicative, monadic, pointed, traversable, etc.)
The motivation for the name "bindable" comes from the following consideration: Suppose M is a monad and F is a "bindable" functor. Then one has the following natural morphism:
fbind :: M a -> (a -> F(M b)) -> F(M b)
This is similar to the monadic "bind",
bind :: M a -> (a -> M b) -> M b
except the result is decorated with the functor F.
The idea behind fbind
was that a generalized monadic operation can produce not just a single result M b but a "functor-ful" F of such results. I want to express the situation when a monadic operation yields several "strands of computation" rather than just one; each "strand of computation" being again a monadic computation.
Note that every functor F has the morphism
eject :: F(a -> b) -> a -> F b
which is converse to "inject". But not every functor F has "inject".
Examples of functors that have "inject": F t = (t,t,t)
or F t = c -> (t,t)
where c is a constant type. Functors F t = c
(constant functor) or F t = (c,t)
are not "bindable" (i.e. do not have "inject"). The continuation functor F t = (t -> r) -> r
also does not seem to have inject
.
The existence of "inject" can be formulated in a different way. Consider the "reader" functor R t = c -> t
where c is a constant type. (This functor is applicative and monadic, but that's beside the point.) The "inject" property then means R (F t) -> F (R t)
, in other words, that R commutes with F. Note that this is not the same as the requirement that F be traversable; that would have been F (R t) -> R (F t)
, which is always satisfied for any functor F with respect to R.
So far, I was able to show that "inject" implies "fbind" for any monad M.
In addition, I showed that every functor F that has "inject" will also have these additional properties:
- it is pointed
point :: t -> F t
if F is "bindable" and applicative then F is also a monad
if F and G are "bindable" then so is the pair functor F * G (but not F + G)
if F is "bindable" and A is any profunctor then the (pro)functor
G t = A t -> F t
is bindablethe identity functor is bindable.
Open questions:
is the property of being "bindable" equivalent to some other well-known properties, or is it a new property of a functor that is not usually considered?
are there any other properties of the functor "F" that follow from the existence of "inject"?
do we need any laws for "inject", would that be useful? For instance, we could require that R (F t) be isomorphic to F (R t) in one or both directions.
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.
A functor
f
is called rigid if it has theinject
method as shown. Note that every functor has theeject
method.The law of "nondegeneracy" must hold:
A rigid functor is always pointed:
If a rigid functor is applicative then it is automatically monadic:
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
andList
. These are functors that have more than one constructor: as a rule, such functors are not rigid.The problem with implementing
inject
forMaybe
is thatinject
must transform a function of typea -> Maybe b
intoMaybe(a -> b)
whileMaybe
has two constructors. A function of typea -> Maybe b
could return different constructors for different values ofa
. However, we are supposed to construct a value of typeMaybe(a -> b)
. If for somea
the given function producesNothing
, we don't have ab
so we can't produce a total functiona->b
. Thus we cannot returnJust(a->b)
; we are forced to returnNothing
as long as the given function producesNothing
even for one value ofa
. But we cannot check that a given function of typea -> Maybe b
producesJust(...)
for all values ofa
. Therefore we are forced to returnNothing
in all cases. This will not satisfy the law of nondegeneracy.So, we can implement
inject
iff 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
where
id :: f a -> f a
. This shows that we can have an f-algebraf a -> a
for any typea
, as long as it is wrapped insidef
. It is not true that any monad has an algebra; for example, the various "future" monads as well as theIO
monad describe computations of typef a
that do not allow us to extract values of typea
- we shouldn't be able to have a method of typef a -> a
even if wrapped inside anf
-container. This shows that the "future" monads and theIO
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 inp (f t) -> f (p t)
for any functorp
. Rigidity is the same as being able to interchange the order only with respect to the "reader" functorr 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 typec
. However, not all rigid functors are representable. An example is the functorg
defined byThe functor
g
are not equivalent toc -> t
with a fixed typec
.Further examples of rigid functors that are not representable (i.e. not "distributive") are functors of the form
a t -> f t
wherea
is any contrafunctor andf
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.
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 havefbind
as shown in the question, we needf
to be rigid. Then we can implementfbind
asWe 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 monadm
.The second use case grows out of the following consideration. Suppose we have a program
p :: a
that internally uses a functionf :: b -> c
. Now, we notice that the functionf
is very slow, and we would like to refactor the program by replacingf
with a monadic "future" or "task", or generally with a Kleisli arrowf' :: b -> m c
for some monadm
. We, of course, expect that the programp
will become monadic as well:p' :: m a
. Our task is to refactorp
intop'
.The refactoring proceeds in two steps: First, we refactor the program
p
so that the functionf
is explicitly an argument ofp
. Assume that this has been done, so that now we havep = q f
whereSecond, we replace
f
byf'
. We now assume thatq
andf'
are given. We would like to construct the new programq'
of the typeso that
p' = q' f'
. The question is whether we can define a general combinator that will refactorq
intoq'
,It turns out that
refactor
can be constructed only ifm
is a rigid functor. In trying to implementrefactor
, we find essentially the same problem as when we tried to implementinject
forMaybe
: we are given a functionf' :: b -> m c
that could return different monadic effectsm c
for differentb
, but we are required to constructm a
, which must represent the same monadic effect for allb
. This cannot work, for instance, ifm
is a monad with more than one constructor.If
m
is rigid (and we do not need to require thatm
be a monad), we can implementrefactor
: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 theIO
monad are not rigid. This again shows that rigidity is, in a sense, a stronger property than monadicity.