什么是类别理论POV的应用Functor定义?

arr*_*owd 24 haskell category-theory applicative

我能够通过以下方式将Functor的定义从类别理论映射到Haskell的定义:因为Hask类型的对象,仿函数F

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

到现在为止还挺好.现在我到了Applicative,在教科书中找不到任何提及这样的概念.通过查看它增加了Functor,ap :: f (a -> b) -> f a -> f b我试着拿出我自己的定义.

首先,我注意到,因为(->)它也是一种类型,态射Hask也是它的对象.鉴于此,我提出了一个建议,即应用仿函数是一个仿函数,它也可以将"箭头" - 源类别的对象映射到目标类型的态射.

这是正确的直觉吗?你能提供更正式和严谨的定义吗?

Bar*_*ski 34

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

常规仿函数保留了基本的分类结构:它们在类别之间映射对象和态射,并且它们保留了类别的规律(关联性和身份).

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

Haskell中的applicative functor的传统定义基于映射多个参数的函数的想法.但是有一个等价的定义,它将多参数函数沿着不同的边界分开.您可以将这样的函数看作产品(一对,在Haskell中)到另一种类型(此处c)的映射.

a -> (b -> c)  ~  (a, b) -> c
Run Code Online (Sandbox Code Playgroud)

这使我们可以将应用仿函数看作保留产品的仿函数.但产品只是所谓的幺半群结构的一个例子.

通常,幺半群类别是配备有张量积和单位对象的类别.例如,在Haskell中,这可能是笛卡尔积(一对)和单位类型().但请注意,幺半群定律(相关性和单位定律)仅在同构时有效.例如:

(a, ())  ~  a
Run Code Online (Sandbox Code Playgroud)

然后可以将应用仿函数定义为保留幺半群结构的仿函数.特别是,它应该保留单元和产品.在应用仿函数之前或之后我们是否进行"乘法"并不重要.结果应该是同构的.

但是,我们并不需要一个完整的monoidal仿函数.我们所需要的只是两个态射(与同构相反) - 一个用于乘法,一个用于单位.这种半保留幺半群结构的仿函数称为松散幺半群仿函数.因此另一种定义:

class Functor f => Monoidal f where
  unit :: f ()
  (**) :: f a -> f b -> f (a, b)
Run Code Online (Sandbox Code Playgroud)

它很容易表明Monoidal相当于Applicative.例如,我们可以从中获得pure,unit反之亦然:

pure x = fmap (const x) unit
unit = pure ()
Run Code Online (Sandbox Code Playgroud)

适用法律仅遵循保护幺半群法律(相关性和单位法).

在类别理论中,幺半群结构的保持与张力强度有关,因此应用函子也被称为强松弛幺半群算.但是,在Hask中,每个仿函数都具有与产品相关的规范强度,因此该属性不会在定义中添加任何内容.

现在,如果你熟悉monad作为endofunctor类别中的monoid的定义,你可能会有兴趣知道类似于endofunctors类别中的应用程序,其中张量积是Day卷积.但这更难以解释.

  • 我个人更喜欢将应用仿函数视为"封闭仿函数"而不是单一仿函数.它们是幺半群的事实或多或少是巧合,并且由于保留指数而强迫,这就是为什么'Monoidal'编码的东西感觉如此混乱,而`(<*>):: f(a - > b ) - > fa - > fb` combinator,我们使用的恰好是指数的映射!考虑Applicative的另一种方式是关于(协变)Day卷积的monoid对象.这种观点的好处在于它阐明了寻找逆变形式的Applicative的道路. (7认同)
  • 当我在心理上没有发现`(**)`到`(fa,fb) - > f(a,b)`时,它对我来说更有意义.我想知道你为什么不把它写在第一位呢. (2认同)

lef*_*out 12

你说得对,Applicative转化小于直接地FunctorMonad.但实质上,它是一类半群仿函数:

class Functor f => Monoidal f where
  pureUnit :: f ()
  fzip :: f a -> f b -> f (a,b)
Run Code Online (Sandbox Code Playgroud)

从那你可以定义 - 在Hask内-

pure x = fmap (const x) pureUnit
Run Code Online (Sandbox Code Playgroud)

fs <*> xs = fmap (uncurry ($)) $ fzip fs xs
Run Code Online (Sandbox Code Playgroud)