Search code examples
haskellfunctorapplicativecategory-theory

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

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