所有固定大小的容器是否都具有强大的单曲面函子，和/或反之亦然？

Question

Applicative类型类表示松散单项函子，该函子将笛卡尔单项结构保留在类型化函数的类别上。

换句话说，给定证明(,)形成单曲面结构的规范同构：

-- 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, ())

类型类及其法律可以等效地写成这样：

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

一个人可能想知道，对于同一个结构，为oplax单曲面的函子可能看起来像：

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

如果我们考虑定义和法律所涉及的类型，就会发现令人失望的事实； OpApplicative没有比Functor更具体的约束：

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

但是，尽管每个Applicative函子（实际上是任何Functor）都是OpApplicative，但是Applicative松弛度和OpApplicative松弛度之间不一定存在良好的关系。因此我们可以使用笛卡尔单曲面结构寻找strong monoidal函子：

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

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

上面的第一定律是微不足道的，因为类型() -> ()的唯一居民是()上的恒等函数。

但是，剩下的三个定律，以及子类本身，是[[not琐碎的。具体来说，并非每个Applicative都是此类的合法实例。

这里有一些Applicative函子，可以为它们声明StrongApplicative的合法实例：

Identity
• VoidF
• (->) r
• Monoid m => (,) m（请参阅答案）
Vec (n :: Nat)
• Stream（无限）

这是我们无法为其提供的某些Applicative：

[]

Either e

Maybe

NonEmptyList

这里的模式表明，从某种意义上讲，StrongApplicative类是FixedSize类，其中“固定大小”

*表示a中居民的多样性^** f a的居民是固定的。

这可以说是两个推测：

每个Applicative代表其类型参数元素的“固定大小”容器都是StrongApplicative的实例

不存在StrongApplicative的实例，其中a的出现次数可以变化

谁能想到反驳这些猜想的反例，或一些令人信服的论证来证明它们是真还是假？

---

*我意识到我没有正确定义形容词“固定大小”。不幸的是，这项任务有点循环。我不知道“固定大小”容器的任何正式描述，并且正在尝试提出一个。到目前为止，StrongApplicative是我最好的尝试。

为了评估这是否是一个好的定义，我需要进行一些比较。给定某种形式的/非正式的定义，对于一个函子，对于其类型参数的居民而言，具有给定的大小或多重性是什么意思，问题是StrongApplicative实例的存在是否能准确地区分固定大小和变化大小的函子。

[由于不了解现有的正式定义，我在使用“固定大小”一词时要求直觉。但是，如果有人已经知道函子大小的现有形式主义并且可以将StrongApplicative与函子进行比较，那就更好了。

**“多重性”在广义上是指函子的共域类型的居民中出现了多少个函子的参数类型的任意元素。这是

无

关于仿函数应用于的特定类型，因此与参数类型的任何特定居民无关。对此不够精确，在注释中引起了一些混乱，因此，这里有一些示例，我认为各种函子的大小/多重性是：

VoidF：固定，0
• [Identity：固定的1
• Maybe：变量，最小0，最大1
• [[]：变量，最小0，最大无限
• [NonEmptyList：变量，最小1，最大无限]
• [Stream：固定的，无限的
• [Monoid m => (,) m：固定的1
• data Pair a = Pair a a：固定，2
• Either x：变量，最小0，最大1
• [data Strange a = L a | R a：固定的1

Answer 1

我们可以至少回答以下问题之一：

每个表示其类型参数元素的“固定大小”容器的Applicative都是StrongApplicative的一个实例

实际上，原始问题中的合法StrongApplicative的示例之一是错误的。适用于写作者的Monoid => (,) m不是StrongApplicative，因为例如husk $ unhusk $ ("foo", ()) == ("", ()) /= ("foo", ())。

类似地，固定大小的容器的示例：

data Strange a = L a | R a

固定多重性1，不是很强的适用性，因为如果我们定义husk = Left，则定义husk $ unhusk $ Right () /= Right ()，反之亦然。用一种等效的方式可以看出，这只是作者对您选择Bool上的monoid的适用。
因此存在不是StrongApplicative的“固定大小”应用程序。是否所有StrongApplicative的大小都固定，尚待观察。