haskell - Is this property of a functor stronger than a monad?

Question

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 bindable

• the 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.

Answer 1

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:

1. f = Identity
2. if f and g are both rigid then the functor product h t = (f t, g t) is also rigid
3. if f and g are both rigid then the composition h t = f (g t) is also rigid
4. if f is rigid and g is any contravariant functor then the functor h 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.