所有固定大小的容器都是强幺半群函子，和/或反之亦然？

Question

该Applicative类型类代表松懈monoidal函子是保留对输入功能类别的笛卡尔monoidal结构。

换句话说，给定规范同构见证(,)形成幺半群结构：

-- 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透明度之间不一定有很好的关系。所以我们可以在笛卡尔幺半群结构中寻找强幺半群函子：

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

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

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

然而，其余的三个定律，以及子类本身，都不是微不足道的。具体来说，并非每个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，那就更好了。

** 通过“多重性”，我指的是在函子的 codomain 类型的居民中出现函子参数类型的“多少”任意元素。这是没有考虑到函子被施加到特定类型的，因此不考虑参数类型的任何特定居民。

对此的不准确导致了评论中的一些混乱，所以这里有一些我认为各种函子的大小/多重性的例子：

• 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 = Leftthen husk $ unhusk $ Right () /= Right ()，反之亦然。看待这一点的等效方式是，这只是适用于您在 上选择幺半群的作者Bool。

所以存在“固定大小”的应用程序不是StrongApplicative. 是否所有StrongApplicatives 都是固定大小还有待观察。

Answer 2

让我们将可表示的函子作为我们对“固定大小容器”的定义：

class Representable f where
    type Rep f
    tabulate :: (Rep f -> a) -> f a
    index :: f a -> Rep f -> a

RealRepresentable有一些定律和超类，但对于这个答案，我们实际上只需要两个属性：

tabulate . index = id
index . tabulate = id

（好吧，我们也需要一个守法的人instance StrongApplicative ((->) r)。容易，你已经同意它存在。）

如果我们采用这个定义，那么我可以证实猜想 1：

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

是真的。就是这样：

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

有很多的法律证明，但我会只专注于四大该StrongApplicative插件-你可能已经相信引入药粥Applicative和OpApplicative，但如果你不这样做，他们的证据看起来就像下面的那些（这反过来看起来很像彼此）。为了清楚起见，我将使用zipf，huskf等的功能实例，并且zipr，huskr等为表现的情况下，这样你就可以跟踪哪个是哪个。（这样很容易验证我们没有将我们试图证明的东西作为假设！unhuskf . huskf = id在证明时使用是可以的unhuskr . huskr = id，但unhuskr . huskr = id在同一个证明中假设是错误的。）

每个定律的证明都以基本相同的方式进行：展开定义，去掉给出的同构Representable，然后对函数使用类似的定律。

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)

Answer 3

\n

\n
• 每个Applicative表示其类型参数的元素的“固定大小”容器都是一个实例StrongApplicative
\n
• StrongApplicative不存在出现次数a可以变化的实例
\n

\n\n

谁能想出反驳这些猜想的反例，或者一些令人信服的推理来证明它们为何正确或错误？

\n

\n\n

我\xe2\x80\x99m 不确定第一个猜想，并且根据与@AsadSaeeduddin 的讨论，\xe2\x80\x99s 可能很难证明，但第二个猜想是正确的。要了解原因，请考虑StrongApplicative法律husk . unhusk == id；也就是说，对于所有x :: f (), husk (unhusk x) == x. 但在 Haskell 中，unhusk == const ()，因此该定律相当于对所有人说x :: f ()，husk () == x。但这又意味着只能存在一个不同的类型值f ()：如果有两个值x, y :: f ()，则x == husk ()和husk () == y, so x == y。但如果只有一个可能的f ()值，则f必须具有固定的形状。（例如data Pair a = Pair a a，对于 ，只有一个 类型的值Pair ()，即Pair () ()，但有多个Maybe ()或类型的值[()]。）因此husk . unhusk == id意味着f必须具有固定的形状。

\n