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 StrongApplicative
s 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 ofStrongApplicative
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 ofStrongApplicative
- No instance of
StrongApplicative
exists in which the number of occurrences ofa
can varyCan 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.