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

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.


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)

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