所有固定大小的容器是否都具有很强的单曲面函子，反之亦然? [英] Are all fixed size containers strong monoidal functors, and/or vice versa?

问题描述

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

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

人们可能会想知道，对于同一结构，为 oplax 单项式的函子可能是什么样的:

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

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

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

但是，尽管每个Applicative函子(实际上是任何Functor)都是琐碎的OpApplicative，但Applicative松驰度和OpApplicative松驰度之间不一定存在良好的关系.因此，我们可以使用笛卡尔单曲面结构寻找强单曲面函子:

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

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

However, the remaining three laws, and hence the subclass itself, is not trivial. Specifically, not every Applicative is a lawful instance of this class.

以下是一些Applicative仿函数，我们可以为其声明StrongApplicative的合法实例:

Here are some Applicative functors for which we can declare lawful instances of StrongApplicative:

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

• Identity
• VoidF
• (->) r
• Monoid m => (,) m (see answers)
• Vec (n :: Nat)
• Stream (infinite)

这是一些我们不能为其提供的Applicative:

And here are some Applicatives for which we cannot:

• []
• Either e
• Maybe
• NonEmptyList

• []
• Either e
• Maybe
• NonEmptyList

此处的模式表明StrongApplicative类在某种意义上是FixedSize类，其中固定大小" ^* 表示...的多重性 ^** f a居民中的a居民是固定的.

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.

这可以说是两个推测:

• 每个Applicative代表类型参数的元素的固定大小"容器都是StrongApplicative
的一个实例.
• 不存在任何StrongApplicative实例，其中a的出现次数可以变化

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

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

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

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

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.

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

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:固定，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

• 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

推荐答案

• 每个Applicative代表类型参数的元素的固定大小"容器都是StrongApplicative
的一个实例.
• 不存在任何StrongApplicative实例，其中a的出现次数可以变化

• 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必须形状固定.

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.

这篇关于所有固定大小的容器是否都具有很强的单曲面函子，反之亦然?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！