所有固定大小的容器都是强幺半群仿函数吗，and/or 反之亦然？

Question

Applicative 类型class 表示松弛幺半群函子，它在类型函数的类别上保留了笛卡尔幺半群结构。

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

-- 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及其规律可以等价地写成这样：

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 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

上面的第一条定律是微不足道的，因为 () -> () 类型的唯一居民是 ().

上的身份函数

然而，其余三个定律，以及子class本身，并非微不足道。具体来说，并非每个 Applicative 都是此 class.

的合法实例

这里有一些 Applicative 仿函数，我们可以为其声明 StrongApplicative 的合法实例：

Identity
VoidF
(->) r
~~Monoid m => (,) m~~（查看答案）
Vec (n :: Nat)
Stream（无限）

这里有一些 Applicative 我们无法做到的：

[]
Either e
Maybe
NonEmptyList

这里的模式表明 StrongApplicative class 在某种意义上是 FixedSize class，其中 "fixed size" ^*表示f a的居民中a的居民的多重性^**是固定的。

这可以表述为两种猜想：

每个 Applicative 表示其类型参数的元素的 "fixed size" 容器是 StrongApplicative
不存在 StrongApplicative 的实例，其中 a 的出现次数可以变化

谁能想出反驳这些猜想的反例，或者能证明这些猜想对错的令人信服的推理？

* 我意识到我没有正确定义形容词 "fixed size"。不幸的是，这个任务有点循环。我不知道 "fixed size" 容器有任何正式描述，我正在尝试提出一个。 StrongApplicative 是我迄今为止最好的尝试。

然而，为了评估这是否是一个好的定义，我需要一些东西来与之进行比较。给定一些 formal/informal 定义函子相对于其类型参数的居民具有给定大小或多重性意味着什么，问题是 StrongApplicative 实例的存在是否精确地区分固定的函子和不同的大小。

由于不知道现有的正式定义，我在使用术语 "fixed size" 时求助于直觉。但是，如果有人已经知道关于函子大小的现有形式主义并且可以将 StrongApplicative 与之进行比较，那就更好了。

** "multiplicity" 我指的是 "how many" 仿函数参数类型的任意元素出现在仿函数的共域类型的居民中。这是 不考虑 应用仿函数的特定类型，因此不考虑参数类型的任何特定居民。

关于这一点的不准确导致了评论中的一些混乱，所以这里有一些我认为各种仿函数的 size/multiplicity 的例子：

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

我们至少可以回答以下问题之一是否定的：

Every Applicative representing a "fixed size" container of elements of its type argument is an instance of StrongApplicative

其实原题中一个合法的例子StrongApplicative是错误的。作者应用 Monoid => (,) m 不是 StrongApplicative，因为例如 husk $ unhusk $ ("foo", ()) == ("", ()) /= ("foo", ()).

同理，固定尺寸容器的例子：

data Strange a = L a | R a

of fixed multiplicity 1, 不是很强的应用，因为如果我们定义 husk = Left 那么 husk $ unhusk $ Right () /= Right ()，反之亦然。一种等效的查看方式是，这只是适用于您在 Bool.

上选择幺半群的作者

因此存在 "fixed size" 个不是 StrongApplicative 的应用程序。是否所有 StrongApplicative 都是固定大小还有待观察。

Answer 2

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?

我不确定第一个猜想，根据与@AsadSaeeduddin 的讨论，它可能很难证明，但第二个猜想是正确的。要了解原因，请考虑 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，因此 x == y.但如果只有一个可能的 f () 值，那么 f 必须是固定形状。（例如，对于 data Pair a = Pair a a，只有一个 Pair () 类型的值，即 Pair () ()，但有多个 Maybe () 或 [()] 类型的值。）因此 husk . unhusk == id 意味着 f 必须是固定形状。

Answer 3

让我们把可表示函子作为我们对"fixed size container"的定义：

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

真正的 Representable 有一些规律和超类，但为了这个答案的目的，我们实际上只需要两个属性：

tabulate . index = id
index . tabulate = id

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

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

Every Applicative representing a "fixed size" container of elements of its type argument is an [law-abiding] instance of 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 等，以便您可以跟踪其中是哪个。（这样就很容易验证我们没有把我们试图证明的东西当作假设！在证明 unhuskr . huskr = id 时使用 unhuskf . huskf = 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)

所有固定大小的容器都是强幺半群仿函数吗，and/or 反之亦然？

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

haskell

functor

category-theory

applicative