Are all fixed size containers strong monoidal functors, and/or vice versa?
applicative, category-theory, functor, haskell
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.
Problem
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 `Applicative`s 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