什么是范畴论 POV 中的 Applicative Functor 定义? [英] What is Applicative Functor definition from the category theory POV?

问题描述

我能够通过以下方式将 Functor 的定义从范畴论映射到 Haskell 的定义:由于 Hask 的对象是类型，因此函子 F

I was able to map Functor's definition from category theory to Haskell's definition in the following way: since objects of Hask are types, the functor F

• 将 Hask 的每个类型 a 映射到新类型 F a ，粗略地说，在它前面加上F".
• 映射每个态射 a ->Hask 的 b 到新的态射 F a ->F b 使用 fmap :: (a -> b) ->(f a -> f b).

• maps every type a of Hask to the new type F a by, roughly saying, prepending "F " to it.
• maps every morphism a -> b of Hask to the new morphism F a -> F b using fmap :: (a -> b) -> (f a -> f b).

到目前为止，一切都很好.现在我进入了Applicative，在教科书中找不到任何提到这样一个概念的地方.通过查看它添加到 Functor 中的内容，ap :: f (a -> b) ->f a ->f b，我试着想出我自己的定义.

So far, so good. Now I get to the Applicative, and can't find any mention of such a concept in textbooks. By looking at what it adds to Functor, ap :: f (a -> b) -> f a -> f b, I tried to come up with my own definition.

首先，我注意到由于 (->) 也是一个类型，Hask 的态射也是它的对象.有鉴于此，我提出了一个建议，applicative functor 是一种也可以将源类别的箭头"对象映射到目标类别的态射的函子.

First, I noticed that since (->) is also a type, morphisms of Hask are objects of it too. In light of this, I made a suggestion that applicative functor is a functor that also can map "arrow"-objects of source category into morphisms of the destination one.

这是正确的直觉吗?你能提供一个更正式、更严格的定义吗?

Is this a right intuition? Can you provide a more formal and rigorous definition?

推荐答案

理解应用函子的关键是弄清楚它们保留了什么结构.

The key to understanding applicative functors is to figure out what structure they preserve.

正则函子保留了基本的范畴结构:它们在范畴之间映射对象和态射，并且他们保留范畴的法则(结合性和恒等性).

Regular functors preserve the basic categorical structure: they map objects and morphisms between categories, and they preserve the laws of the category (associativity and identity).

但是一个类别可能有更多的结构.例如，它可能允许定义类似于态射但带有多个参数的映射.这种映射是通过柯里化定义的:例如，一个有两个参数的函数被定义为一个参数返回另一个函数的函数.如果您可以定义表示函数类型的对象，则这是可能的.通常，这个对象被称为指数(在 Haskell 中，它只是类型 b->c).然后我们可以有从一个对象到一个指数的态射，并将其称为双参数态射.

But a category may have more structure. For instance, it may allow the definition of mappings that are like morphisms but take multiple arguments. Such mappings are defined by currying: e.g., a function of two arguments is defined as a function of one argument returning another function. This is possible if you can define an object that represents a function type. In general, this object is called an exponential (in Haskell, it's just the type b->c). We can then have morphisms from one object to an exponential and call it a two-argument morphism.

Haskell 中应用函子的传统定义基于多参数映射函数的思想.但是有一个等效的定义将多参数函数沿不同的边界拆分.您可以将这样的函数视为将 product(Haskell 中的一对)映射到另一种类型(此处为 c).

The traditional definition of an applicative functor in Haskell is based on the idea of mapping functions of multiple arguments. But there is an equivalent definition that splits the multi-argument function along a different boundary. You can look at such a function as a mapping of a product (a pair, in Haskell) to another type (here, c).

a -> (b -> c)  ~  (a, b) -> c

这使我们可以将应用函子视为保留乘积的函子.但乘积只是所谓的幺半群结构的一个例子.

That allows us to look at applicative functors as functors that preserve the product. But a product is just one example of what is called a monoidal structure.

一般而言，幺半群类别是配备张量积和单位对象的类别.例如，在 Haskell 中，这可能是笛卡尔积(一对)和单位类型 ().但是请注意，幺半群定律(结合律和单位定律)仅在同构之前有效.例如:

In general, a monoidal category is a category equipped with a tensor product and a unit object. In Haskell, this could be, for instance, the cartesian product (a pair) and the unit type (). Notice, however that monoidal laws (associativity and unit laws) are valid only up to an isomorphism. For instance:

(a, ())  ~  a

一个应用函子可以被定义为一个保持幺半群结构的函子.特别是，它应该保存单位和产品.我们是在应用函子之前还是之后进行乘法"并不重要.结果应该是同构的.

An applicative functor could then be defined as a functor that preserves monoidal structure. In particular, it should preserve the unit and the product. It shouldn't matter whether we do the "multiplication" before or after applying the functor. The results should be isomorphic.

然而，我们并不真的需要一个成熟的幺半群函子.我们只需要两个态射(与同构相反)——一个用于乘法，一个用于单位.这种半保留幺半群结构的函子称为松散幺半群函子.因此，替代定义:

However, we don't really need a full-blown monoidal functor. All we need is two morphisms (as opposed to isomorphisms) -- one for multiplication and one for unit. Such a functor that half-preserves the monoidal structure is called a lax monoidal functor. Hence the alternative definition:

class Functor f => Monoidal f where
  unit :: f ()
  (**) :: f a -> f b -> f (a, b)

很容易证明Monoidal 等价于Applicative.例如，我们可以从 unit 得到 pure，反之亦然:

It's easy to show that Monoidal is equivalent to Applicative. For instance, we can get pure from unit and vice versa:

pure x = fmap (const x) unit
unit = pure ()

应用定律简单地遵循幺半群定律(结合律和单位定律).

The applicative laws follow simply from the preservation of monoid laws (associativity and unit laws).

在范畴论中，幺半群结构的保存与张量强度有关，因此应用函子也被称为强松散幺半群函子.但是，在 Hask 中，每个函子都具有与乘积相关的规范强度，因此该属性不会向定义添加任何内容.

In category theory, preservation of monoidal structure is related to tensorial strength, so an applicative functor is also known as a strong lax monoidal functor. However, in Hask, every functor has canonical strength with respect to the product, so this property doesn't add anything to the definition.

现在，如果您熟悉作为内函子范畴中的幺半群的单子的定义，你可能有兴趣知道应用程序是类似地属于内函子范畴中的幺半群，其中张量积是 Day卷积.但这更难解释.

Now, if you're familiar with the definition of a monad as a monoid in the category of endofunctors, you might be interested to know that applicatives are, similarly, monoids in the category of endofunctors where the tensor product is the Day convolution. But that's much harder to explain.

这篇关于什么是范畴论 POV 中的 Applicative Functor 定义?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！