What is this special functor structure called?
applicative, category-theory, haskell
Solution
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.
Problem
Suppose that F is an applicative functor with the additional laws (with Haskell syntax): - `pure (const ()) <*> m` === `pure ()` - `pure (\a b -> (a, b)) <*> m <*> n` === `pure (\a b -> (b, a)) <*> n <*> m` - `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`.