什么是来自类别理论POV的Applicative Functor定义？ [英] What is Applicative Functor definition from the category theory POV?

问题描述

我能够以以下方式将Functor的定义从类别理论映射到Haskell的定义：由于 Hask 的对象是类型，函数 F

• 映射每个类型 a of Hask 添加到新类型 F a 中，粗略地说，在它前面加上F。
• 映射每个态射 a - > b of Hask 到新的态射 F a - > F b 使用 fmap ::（a - > b） - > （f a - > f b）。



到目前为止，现在我来到 Applicative ，在教科书中找不到任何这样的概念。通过查看它添加到 Functor ， ap :: f（a - > b） - > f a - > fb ，我试图想出自己的定义。

首先，我注意到自（ - > ）也是一个类型， Hask 的态射也是它的对象。鉴于此，我提出了一个建议，即应用函子是一个函子，它也可以将源类别的箭头对象映射到目的地的射线。

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

解决方案

理解应用函数的关键是找出它们保留的结构。



常规仿函数保留了基本的分类结构：它们在类别之间映射对象和态射，并保留类别的规律（关联性和同一性）。



但是一个类别可能有更多的结构。例如，它可以允许像态射一样定义映射，但需要多个参数。这种映射由柯里格定义：例如，两个参数的函数被定义为返回另一个函数的一个参数的函数。如果你可以定义一个代表函数类型的对象，这是可能的。一般来说，这个对象被称为指数（在Haskell中，它只是 b-> c 类型）。然后，我们可以从一个对象的态射到一个指数，并将它称为两个参数的态射。

Haskell中一个应用函子的传统定义是基于映射多个参数的函数。但是有一个等价的定义将多参数函数沿不同的边界分开。您可以将这样的函数看作是 product （一对，在Haskell中）到另一个类型（这里是 c ）的映射。

  a  - > （b→c）〜（a，b）→> c 
  

这允许我们将应用函数看作保留产品的函数。但是产品只是所谓的monoidal结构的一个例子。

一般来说，monoidal类别是配备张量积和单位对象的类别。在Haskell中，这可能是，例如，笛卡尔积（一对）和单位类型（）。不过要注意的是，monoidal法则（结合性和单位法则）只有达到同构才有效。例如：

 （a，（））〜a 
  

然后可以将一个应用函数定义为保留monoidal结构的函子。特别是，它应该保留单位和产品。在应用函数之前或之后，我们是否应该进行乘法并不重要。结果应该是同构的。

然而，我们并不需要一个完整的monoidal函子。我们需要的是两个态射（与同构相反） - 一个用于乘法，另一个用于单位。这种半保留monoidal结构的函子被称为 lax monoidal functor 。因此，替代定义：

  class Functor f => Monoidal f其中
 unit :: f（）
（**）:: f a  - > f b  - > f（a，b）
  

很容易显示 Monoidal 相当于 Applicative 。例如，我们可以从 unit 获取 pure ，反之亦然：



 纯x = fmap（常x）单位
单位=纯（）
  

应用法则仅仅遵循幺半律的保留（结合性和单位法则）。在分类理论中，monoidal结构的保存与张量强度有关，所以一个可应用的函子也被称为强分散monoidal函子。然而，在 Hask 中，每个函数都具有关于产品的规范强度，所以此属性不会向定义添加任何内容。

现在，如果您熟悉monode在endofunctors范畴中的定义，那么您可能有兴趣知道applicatives同样也是monotypeid，它属于endofunctors类别，其中tensor乘积是Day卷积。但这很难解释。

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

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

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.

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

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.

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.

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)

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

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.

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