在更广泛的背景下的自然变形。

Question

我一直在通过Haskell中的一些类别理论来创建更多通用的Monads。

在我进入下一步之前，我需要能够使用自然转换。

现在，常规的自然转换 Functor很简单，它们只是函数

trans :: forall a . F a -> G a

(其中 F 和 G 是 Functor(s)，但附加限制条件是

fmap f . trans = trans . fmap f

等价于换向图。

但是当我继续研究更多的分类漏斗时...

class
  ( Category cat1
  , Category cat2
  )
    => Functor cat1 cat2 f
  where
    map :: cat1 a b -> cat2 (f a) (f b)

我不知道如何增强自然转换的定义才能跟上。

图中暗示

trans :: forall a . cat2 (F a) (G a)

哪儿

Functor cat1  cat2 F
Functor cat1' cat2 G

然而，我不清楚一定是这样的情况： cat1 ~ cat1'. 或者说，这两个漏斗的转换和前类之间的关系是什么。

在Haskell的更广泛的语境中，自然转换是什么样子的呢？Functor而不是更通用的类别？

Answer 1

然而，我并不清楚必须是 cat1 ~ cat1'的情况。

自然变换的定义中，漏子F和G有相同的域和同域。来自nlab:

给定类别C和D，以及漏斗F，G : C -> D。

所以在Haskell中的定义的直接翻译是，漏斗器之间的自然转换是 F, G 带域 cat1 和代码域 cat2 是作为一个多态项，是一个形态族 cat2 (F a) (G a) 按对象索引 a:

n :: forall a. cat2 (F a) (G a)

使得某图对所有的 f :: cat1 a b即，我们有以下公式，其中 (.) 是组成 cat2:

fmap f . n = n . fmap f

其中 n 擅长类型 a 在左边，在类型 b 在右边。

请注意，这种编码在表现力上是有限的，因为Haskell的 forall 与英语中的 "for all "不完全相同。的行为。n :: forall a. ... 靠不住 a. forall 意味着一种 "统一性"(又称参数性)的形式，这在 "自然变换 "的定义中是找不到的。