Are all fixed size containers strong monoidal functors, and/or vice versa?

Question

The Applicative typeclass represents lax monoidal functors that preserve the cartesian monoidal structure on the category of typed functions.

In other words, given the canonical isomorphisms witnessing that (,) forms a monoidal structure:

-- Implementations left to the motivated reader
assoc_fwd :: ((a, b), c) -> (a, (b, c))
assoc_bwd :: (a, (b, c)) -> ((a, b), c)

lunit_fwd :: ((), a) -> a
lunit_bwd :: a -> ((), a)

runit_fwd :: (a, ()) -> a
runit_bwd :: a -> (a, ())

The typeclass and its laws can equivalently be written like this:

class Functor f => Applicative f
  where
  zip :: (f a, f b) -> f (a, b)
  husk :: () -> f ()

-- Laws:

-- assoc_fwd >>> bimap id zip >>> zip
-- =
-- bimap zip id >>> zip >>> fmap assoc_fwd

-- lunit_fwd
-- =
-- bimap husk id >>> zip >>> fmap lunit_fwd

-- runit_fwd
-- =
-- bimap id husk >>> zip >>> fmap runit_fwd

One might wonder what a functor that is oplax monoidal with respect to the same structure might look like:

class Functor f => OpApplicative f
  where
  unzip :: f (a, b) -> (f a, f b)
  unhusk :: f () -> ()

-- Laws:

-- assoc_bwd <<< bimap id unzip <<< unzip
-- =
-- bimap unzip id <<< unzip <<< fmap assoc_bwd

-- lunit_bwd
-- =
-- bimap unhusk id <<< unzip <<< fmap lunit_bwd

-- runit_bwd
-- =
-- bimap id unhusk <<< unzip <<< fmap runit_bwd

If we think about the types involved in the definitions and laws, the disappointing truth is revealed; OpApplicative is no more specific a constraint than Functor:

instance Functor f => OpApplicative f
  where
  unzip fab = (fst <$> fab, snd <$> fab)
  unhusk = const ()

However, while every Applicative functor (really, any Functor) is trivially OpApplicative, there is not necessarily a nice relationship between the Applicative laxities and OpApplicative oplaxities. So we can look for strong monoidal functors wrt the cartesian monoidal structure:

class (Applicative f, OpApplicative f) => StrongApplicative f

-- Laws:
-- unhusk . husk = id
-- husk . unhusk = id
-- zip . unzip = id
-- unzip . zip = id

The first law above is trivial, since the only inhabitant of the type () -> () is the identity function on ().

However, the remaining three laws, and hence the subclass itself, is not trivial. Specifically, not every Applicative is a lawful instance of this class.

Here are some Applicative functors for which we can declare lawful instances of StrongApplicative:

• Identity
• VoidF
• (->) r
• Monoid m => (,) m (see answers)
• Vec (n :: Nat)
• Stream (infinite)

And here are some Applicatives for which we cannot:

• []
• Either e
• Maybe
• NonEmptyList

The pattern here suggests that the StrongApplicative class is in a sense the FixedSize class, where "fixed size" ^* means that the multiplicity ^** of inhabitants of a in an inhabitant of f a is fixed.

This can be stated as two conjectures:

• Every Applicative representing a "fixed size" container of elements of its type argument is an instance of StrongApplicative
• No instance of StrongApplicative exists in which the number of occurrences of a can vary

Can anyone think of counterexamples that disprove these conjectures, or some convincing reasoning that demonstrates why they are true or false?

---

* I realize that I haven't properly defined the adjective "fixed size". Unfortunately the task is a little bit circular. I don't know of any formal description of a "fixed size" container, and am trying to come up with one. StrongApplicative is my best attempt so far.

In order to evaluate whether this is a good definition however, I need something to compare it to. Given some formal/informal definition of what it means for a functor to have a given size or multiplicity with respect to inhabitants of its type argument, the question is whether the existence of a StrongApplicative instance precisely distinguishes functors of fixed and varying size.

Not being aware of an existing formal definition, I'm making an appeal to intuition in my usage of the term "fixed size". However if someone already knows of an existing formalism for the size of a functor and can compare StrongApplicative to it, so much the better.

** By "multiplicity" I'm referring in a loose sense to "how many" arbitrary elements of the functor's parameter type occur in an inhabitant of the functor's codomain type. This is without regard to the specific type the functor is applied to, and hence without regard to any specific inhabitants of the parameter type.

Not being precise about this has caused some confusion in the comments, so here's some examples of what I would consider the size/multiplicity of various functors to be:

• VoidF: fixed, 0
• Identity: fixed, 1
• Maybe: variable, minimum 0, maximum 1
• []: variable, minimum 0, maximum infinite
• NonEmptyList: variable, minimum 1, maximum infinite
• Stream: fixed, infinite
• Monoid m => (,) m: fixed, 1
• data Pair a = Pair a a: fixed, 2
• Either x: variable, minimum 0, maximum 1
• data Strange a = L a | R a: fixed, 1

Answer 1

Let's take representable functors as our definition of "fixed size container":

class Representable f where
    type Rep f
    tabulate :: (Rep f -> a) -> f a
    index :: f a -> Rep f -> a

The real Representable has a few laws and superclasses, but for the purposes of this answer, we actually need just two properties:

tabulate . index = id
index . tabulate = id

(Okay, we also need a law-abiding instance StrongApplicative ((->) r). Easy peasy, you already agree it exists.)

If we take that definition, then I can confirm that conjecture 1:

Every Applicative representing a "fixed size" container of elements of its type argument is an [law-abiding] instance of StrongApplicative

is true. Here's how:

instance Representable f => Applicative f where
    zip (fa, fb) = tabulate (zip (index fa, index fb))
    husk = tabulate . husk

instance Representable f => OpApplicative f where
    unzip fab = let (fa, fb) = unzip (index fab) in (tabulate fa, tabulate fb)
    unhusk = unhusk . index

instance Representable f => StrongApplicative f

There's a lot of laws to prove, but I'll focus just on the Big Four that StrongApplicative add -- you probably already believe the lead-in ones for Applicative and OpApplicative, but if you don't, their proofs look just like the ones below (which in turn look quite a lot like each other). For clarity, I will use zipf, huskf, etc. for the function instance, and zipr, huskr, etc. for the representable instance, so you can keep track of which is which. (And so that it's easy to verify that we don't take the thing we're trying to prove as an assumption! It's okay to use unhuskf . huskf = id when proving unhuskr . huskr = id, but it would be wrong to assume unhuskr . huskr = id in that same proof.)

The proof of each law proceeds in basically the same way: unroll definitions, drop the isomorphism that Representable gives you, then use the analogous law for functions.

unhuskr . huskr
= { def. of unhuskr and huskr }
(unhuskf . index) . (tabulate . huskf)
= { index . tabulate = id }
unhuskf . huskf
= { unhuskf . huskf = id }
id

huskr . unhuskr
= { def. of huskr and unhuskr }
(tabulate . huskf) . (unhuskf . index)
= { huskf . unhuskf = id }
tabulate . index
= { tabulate . index = id }
id

zipr (unzipr fab)
= { def. of unzipr }
zipr (let (fa, fb) = unzipf (index fab) in (tabulate fa, tabulate fb))
= { def. of zipr }
let (fa, fb) = unzipf (index fab) in tabulate (zipf (index (tabulate fa), index (tabulate fb)))
= { index . tabulate = id }
let (fa, fb) = unzipf (index fab) in tabulate (zipf (fa, fb))
= { def. of (fa, fb) }
tabulate (zipf (unzipf (index fab)))
= { zipf . unzipf = id }
tabulate (index fab)
= { tabulate . index = id }
fab

unzipr (zipr (fa, fb))
= { def. of zipr }
unzipr (tabulate (zipf (index fa, index fb)))
= { def. of unzipr }
let (fa', fb') = unzipf (index (tabulate (zipf (index fa, index fb))))
in (tabulate fa', tabulate fb')
= { index . tabulate = id }
let (fa', fb') = unzipf (zipf (index fa, index fb))
in (tabulate fa', tabulate fb')
= { unzipf . zipf = id }
let (fa', fb') = (index fa, index fb)
in (tabulate fa', tabulate fb')
= { def. of fa' and fb' }
(tabulate (index fa), tabulate (index fb))
= { tabulate . index = id }
(fa, fb)

Answer 2

We can answer at least one of these questions in the negative:

Every Applicative representing a "fixed size" container of elements of its type argument is an instance of StrongApplicative

In fact one of the examples of a lawful StrongApplicative in the original question is wrong. The writer applicative Monoid => (,) m is not StrongApplicative, because for example husk $ unhusk $ ("foo", ()) == ("", ()) /= ("foo", ()).

Similarly, the example of a fixed size container:

data Strange a = L a | R a

of fixed multiplicity 1, is not a strong applicative, because if we define husk = Left then husk $ unhusk $ Right () /= Right (), and vice versa. An equivalent way to view this is that this is just the writer applicative for your choice of monoid on Bool.

So there exist "fixed size" applicatives that are not StrongApplicative. Whether all StrongApplicatives are of fixed size remains to be seen.

Answer 3

• Every Applicative representing a "fixed size" container of elements of its type argument is an instance of StrongApplicative
• No instance of StrongApplicative exists in which the number of occurrences of a can vary

Can anyone think of counterexamples that disprove these conjectures, or some convincing reasoning that demonstrates why they are true or false?

I’m not sure about that first conjecture, and based on discussions with @AsadSaeeduddin it’s likely to be difficult to prove, but the second conjecture is true. To see why, consider the StrongApplicative law husk . unhusk == id; that is, for all x :: f (), husk (unhusk x) == x. But in Haskell, unhusk == const (), so that law is equivalent to saying for all x :: f (), husk () == x. But this in turn implies that there can only exist one distinct value of type f (): if there were two values x, y :: f (), then x == husk () and husk () == y, so x == y. But if there is only one possible f () value, then f must be of fixed shape. (e.g. for data Pair a = Pair a a, there is only one value of type Pair (), this being Pair () (), but there are multiple values of type Maybe () or [()].) Thus husk . unhusk == id implies that f must be of fixed shape.