问题标签 [category-theory]

在范畴论中，函子是两个范畴之间的同态。在 Haskell 中，据说应用函子允许我们在“函子内部”应用函数。有人可以将“函子内部的函数”这个词翻译回数学或提供其他一些见解吗？（我知道函子可以是Maybe，[]等等，但仍然很难理解这个概念。）

在范畴论中，一个单子可以由两个伴随函子构成。特别是，如果C和D是类别，并且 F : C --> D和G : D --> C是伴随函子，在某种意义上是双射

hom(FX,Y) = hom(X,GY)

对于C中的每个X和D中的Y，则组合G o F : C --> C是一个单子。

一对这样的伴随函子可以通过固定类型b和取F和G来给出

并且通过currying给出hom集之间的双射（模构造函数）：

在这种情况下，相应的单子是

我不知道这个 monad 的名字应该是什么，除了它似乎是一个带有可覆盖信息的 reader monad（编辑： dbaupp 在评论中指出这是Statemonad. )

所以State单子可以被“分解”为一对伴随函子Fand G，我们可以写

到现在为止还挺好。

我现在正试图弄清楚如何将其他常见的单子分解为成对的伴随函子 - 例如Maybe, [], Reader, Writer, Cont- 但我无法弄清楚我们可以将它们“分解”成的伴随函子对是什么。

唯一简单的情况似乎是Identitymonad，它可以分解为任何一对仿函数，F并且与（特别是，你可以只取and ）相反。GFGF = IdentityG = Identity

任何人都可以解释一下吗？

好吧，我正在研究 Haskell Monads。当我阅读维基百科分类理论文章时，我发现单子态射的签名看起来很像逻辑中的重言式，但你需要转换M a为~~A，这里~是逻辑否定。

其他操作也是重言式：

也可以理解为，根据普通函数式语言的Curry-Howard对应是直觉逻辑，而不是经典逻辑，所以不能指望像重言式一样~~A => A可以有对应。

但我在想别的东西。为什么单子只能与双重否定有关？单一否定的对应关系是什么？这使我得到以下类定义：

这里我定义了一个叫做“Nomad”的概念，它支持两种操作（都与直觉逻辑中的一个逻辑公理有关）。请注意，“rfmap”这个名称意味着它的签名类似于 functor 的fmap，但结果中a和的顺序b相反。现在我可以用它们重新定义 Monad 操作，用 replace M ato n (n a)。

那么现在让我们进入问题部分。Monad是范畴论的一个概念，这似乎意味着我的“Nomad”也是一个范畴论的概念。那是什么？有用吗？该课题是否有论文或研究成果？

在之前的回答中，Petr PudlakCFunctor为除从Hask到Hask的函子之外的函子定义了该类。使用类型族重新编写它，它看起来像

看起来像的实例，例如

在范畴论中，只要F : C --> D是函子且G : D --> E是函子，则组合GF : C --> E也是函子。

我想用 Haskell 来表达这一点。因为我不会写instance CFunctor (f . g)，所以我介绍一个包装类：

在写这个CFunctor实例时，我得到了

但我无法弄清楚cmap应该是什么。有什么建议吗？

PS这一切的最终原因是还引入了一个Adjunction带有方法的类unitand counit，然后自动从附属词中派生monad实例。但首先，我需要向编译器展示两个仿函数的组合也是一个仿函数。

我知道我可以cmap.cmap在类型的对象上使用g (f a)它并且会起作用，但这看起来有点像作弊 - 当然函子只是一个函子，编译器不必知道它实际上是两个的组合其他函子？

Haskell 中的产品类型很容易定义：

是两种类型的产品。两种类型的联产品是

但是，虽然产品很容易扩展到三种或更多类型，但对于副产品来说似乎并不那么简单。这种差异背后是否有理论依据，或者纯粹是技术原因？

根据这篇关于haskell中指称语义的文章， 所有类型都有底部，如果函数f：A->B将类型A的底部映射到类型B的底部，则它是严格的，否则称为非严格。

（这让人联想到态射保留基点的尖锐类别）。

为什么 Haskell 有非严格函数，而标准 ML 没有？

根据维基百科对自由对象的定义，在我看来，Hask 中的每个 Functor 都是免费的。相反，每个自由对象也应该是一个 Functor。这是正确的，还是我误解了？

据我了解，仿函数是两个类别之间的映射，例如从对象 in到where和are 类别的对象。

在 Haskell 中有Hask，其中对象是 Haskell 类型，而态射是 Haskell 函数。但是，Functor类型类有一个函数fmap在这些类型之间进行映射（因此它们是对象而不是类别本身）：

f a并且f b都是Hask中的对象。这是否意味着 Haskell 中的每个实例Functor都是一个内函子，如果不是Functor真的代表一个函子？

我在这里想念什么？Haskell中的类型也是类别吗？

我正在玩一些类似免费的想法，发现了这个：

我想找到可以编写函数的条件：

但我一直无法找到一个有意义的结构f（除了一个简单的结构，其中mkFree是 的一种方法???），它允许编写这个函数。特别是，如果这个结构没有提到Free类型，我的审美会更喜欢。

有没有人见过这样的东西？这种概括可能吗？在我还没有想到的方向上是否有一个已知的概括？

我有点不确定这是一个 math.SE 问题还是一个 SO 问题，但我怀疑数学家一般不太可能特别了解或关心这一类别，而 Haskell 程序员可能会这样做。

因此，我们知道Hask 或多或少有产品（当然，我在这里使用的是理想化的 Hask）。我对它是否有均衡器很感兴趣（在这种情况下它会有所有有限的限制）。

直觉上似乎不是，因为你不能像在集合上那样进行分离，所以子对象通常似乎很难构造。但是对于您想提出的任何特定情况，似乎您可以通过在Set中计算均衡器并对其进行计数来破解它（毕竟，每种 Haskell 类型都是可数的，并且每个可数集都是同构于有限类型或自然数，Haskell 都有）。所以我看不出我将如何寻找反例。

现在，Agda 似乎更有希望了：在那里形成子对象相对容易。明显的 sigma 类型Σ A (λ x → f x == g x)是均衡器吗？如果细节不起作用，它在道德上是一个均衡器吗？