What is this special functor structure called?

Question

Suppose that F is an applicative functor with the additional laws (with Haskell syntax):

1. pure (const ()) <*> m === pure ()
2. pure (\a b -> (a, b)) <*> m <*> n === pure (\a b -> (b, a)) <*> n <*> m
3. pure (\a b -> (a, b)) <*> m <*> m === pure (\a -> (a, a)) <*> m

What is the structure called if we omit (3.)?

Where can I find more info on these laws/structures?

Comments on comments

Functors which satisfy (2.) are often called commutative.

The question is now, whether (1.) implies (2.) and how these structures can be described. I am especially interested in structures which satisfies (1-2.) but not (3.)

Examples:

• The reader monad satisfies (1-3.)
• The writer monad on a commutative monoid satisfies only (2.)
• The monad F given below satisfies (1-2.) but not (3.)

Definition of F:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
import Control.Monad.State

newtype X i = X Integer deriving (Eq)

newtype F i a = F (State Integer a) deriving (Monad)

new :: F i (X i)
new = F $ modify (+1) >> gets X

evalF :: (forall i . F i a) -> a
evalF (F m) = evalState m 0

We export only the types X, F, new, evalF, and the instances.

Check that the following holds:

• liftM (const ()) m === return ()
• liftM2 (\a b -> (a, b)) m n === liftM2 (\a b -> (b, a)) n m

On the other hand, liftM2 (,) new new cannot be replaced by liftM (\a -> (a,a)) new:

test = evalF (liftM (uncurry (==)) $ liftM2 (,) new new)
    /= evalF (liftM (uncurry (==)) $ liftM (\a -> (a,a)) new)

Comments on C. A. McCann's answer

I have a sketch of proof that (1.) implies (2.)

pure (,) <*> m <*> n

=

pure (const id) <*> pure () <*> (pure (,) <*> m <*> n)

=

pure (const id) <*> (pure (const ()) <*> n) <*> (pure (,) <*> m <*> n)

=

pure (.) <*> pure (const id) <*> pure (const ()) <*> n <*> (pure (,) <*> m <*> n)

=

pure const <*> n <*> (pure (,) <*> m <*> n)

= ... =

pure (\_ a b -> (a, b)) <*> n <*> m <*> n

= see below =

pure (\b a _ -> (a, b)) <*> n <*> m <*> n

= ... =

pure (\b a -> (a, b)) <*> n <*> m

=

pure (flip (,)) <*> n <*> m

Observation

For the missing part first consider

pure (\_ _ b -> b) <*> n <*> m <*> n

= ... =

pure (\_ b -> b) <*> n <*> n

= ... =

pure (\b -> b) <*> n

= ... =

pure (\b _ -> b) <*> n <*> n

= ... =

pure (\b _ _ -> b) <*> n <*> m <*> n

Lemma

We use the following lemma:

pure f1 <*> m  ===   pure g1 <*> m
pure f2 <*> m  ===   pure g2 <*> m

implies

pure (\x -> (f1 x, f2 x)) m  ===  pure (\x -> (g1 x, g2 x)) m

I could prove this lemma only indirectly.

The missing part

With this lemma and the first observation we can prove

pure (\_ a b -> (a, b)) <*> n <*> m <*> n

=

pure (\b a _ -> (a, b)) <*> n <*> m <*> n

which was the missing part.

Questions

Is this proved already somewhere (maybe in a generalized form)?

Remarks

(1.) implies (2.) but otherwise (1-3.) are independent.

To prove this, we need two more examples:

• The monad G given below satisfies (3.) but not (1-2.)
• The monad G' given below satisfies (2-3.) but not (1.)

Definition of G:

newtype G a = G (State Bool a) deriving (Monad)

putTrue :: G ()
putTrue = G $ put True

getBool :: G Bool
getBool = G get

evalG :: G a -> a
evalG (G m) = evalState m False

We export only the type G, putTrue, getBool, evalG, and the Monad instance.

The definition of G' is similar to the definition of G with the following differences:

We define and export execG:

execG :: G' a -> Bool
execG (G m) = execState m False

We do not export getBool.

Answer 1

Your first law is a very strong requirement; it implies that the functor can have no distinguished "shape" independent of the parametric portion. This rules out any functor that contains extra values (State, Writer, &c.) as well as any functor using sum types (Either, [], &c.). So this limits us to things like fixed-size containers.

Your second law requires commutativity, which means that order of nesting (that is, functor composition) doesn't matter. This might actually be implied by the first law, since we already know that the functor can't contain any information other than the parametric values, and you explicitly require preservation of that here.

Your third law requires that the functor be idempotent as well, which means that nesting something within itself using fmap is equivalent to itself. This probably implies that if the functor is a monad as well, join involves some sort of "taking the diagonal". Basically, this means that liftA2 (,) should behave like zip, not a cartesian product.

The second and third together imply that however many "primitives" the functor might have, any composition is equivalent to combining at most one of each primitive, in any order. And the first implies that if you throw out the parametric information, any combination of primitives is the same as using none at all.

In summary, I think what you have is the class of functors isomorphic to Reader. That is, functors where f a describes values of type a indexed by some other type, such as a subset of the natural numbers (for fixed-size containers) or an arbitrary type (as with Reader).

I'm not sure how to convincingly prove most of the above, unfortunately.