问题标签 [category-theory]

查看Haskell文档，提升似乎基本上是 的概括fmap，允许映射具有多个参数的函数。

然而，关于提升的Wikipedia文章给出了不同的观点，根据类别中的态射定义“提升”，以及它与类别中的其他对象和态射的关系（我不会在此提供详细信息）。我想如果我们正在考虑 Cat （类别的类别，从而使我们的态射函子），这可能与 Haskell 的情况有关，但我看不出这种升力的类别理论概念如何与 Haskell 中的根据链接的文章，如果有的话。

如果这两个概念并不真正相关，只是名称相似，那么 Haskell 中是否使用了电梯（范畴论）？

我正试图了解 F 代数，这篇文章做得很好。我理解范畴论中对偶的概念，但我很难理解 F-coalgebras（F-algebras 的对偶）如何与 Haskell 中的惰性数据结构相关联。

F-代数用具有以下功能的内函子来描述：F a -> a，如果您将 F a 视为一个表达式，并且 a 是对该表达式求值的结果，那么这是有道理的，正如链接文章所解释的那样。

作为 F 代数的对偶，F 代数的对应函数是 a -> F a。维基百科说 F-coalgebras 可以用来创建无限的惰性数据结构。a -> F a 函数如何允许创建无限的惰性数据结构？此外，考虑到这一点，由于 Haskell 的核心是惰性的，Haskell F-coalgebras 中的大多数数据类型是不是 F-algebras？F-代数不是惰性求值吗？

如果数据类型（或至少能够处理无限数据的数据类型）基于 Haskell 中的 F 代数，例如，列表的 a -> F a 函数是什么？列表的终端 F 代数是什么？

在 Haskell 中创建一个无限列表 [1,2,3,4...] 可能如下所示：

这是否以某种方式使用 F 代数？无限数据结构在使用 F 代数的同时需要惰性求值和递归的概念吗？我在这里错过了什么吗？

我创建了一个either<l, r>类似于 Haskell 的类Either a b。我也在map课堂上直接实现了一个功能；这就是代码的样子：

现在我想隔离map函数以创建一个名为的抽象基类functor

either将继承这个类：

但是这是无效的 C++，因为模板成员函数不能是虚拟的。

此外，我试图测试是否<r, either<l, r>>可以匹配<a, derived<a>>（functor<r, either<l, r>>或任何其他模板）但由于它有两个模板参数而无法匹配。另请注意，仿函数的其他派生类可能具有与仿函数无关的不同数量的模板参数。

函子基类可以用 C++ 模板表达吗？

APipe可以分为两部分：生成器部分 ( yield) 和消费者部分 ( await)。

如果你有一个Pipe只使用它的生成器一半，并且只返回()（或从不返回），那么它可以表示为“ListT正确完成”。事实证明，它MonadPlus可以用来表示像 ListT-done-right 这样的任何东西。引用 Gabriel Gonzalez 的话：

请注意，您可以ListT仅使用转换器依赖项构建任何（不仅仅是管道中的）。例如，以下是您将如何实现的ListT模拟Pipes.Prelude.stdinLn：

这将像任何类型一样输入 checkListT并为所有这些做正确的事情。

ListT所以我的问题是这样的：管道的MonadPlus消费者部分是否有双重关系？

要求：

• 一个从不使用yield，只返回()（或从不返回）但确实使用的管道await可以表示为这个“对 ListT”。
• “dual to ListT”可以推广到“dual of MonadPlus”

我正在尝试为双类别定义一个类型类，并使用类别、函子和自然转换的双类别对其进行实例化。

这是类别的类：

这是函子的类：

下面是函子的组成：

两个函子的组合应该是一个函子。但是，Haskell 不接受以下实例化，因为f并且g不在范围内。你怎么定义fmap这里？

以下是自然变换（此处未使用参数 c，但对下面的下一个实例化很有用。）：

这是双类别的类（运算符.|和.-分别是 2 单元格的垂直和水平组合）：

范畴、函子和自然变换应该形成一个双范畴。但是，Haskell 不接受以下实例化，因为在.-自然变换的水平组合的定义中，g 不在范围内。您如何定义(.-)此处的水平构图？

如果我们将我们对类别的理解限制为CategoryHaskell 中的普通类：

然后假设 anArrow是一个Categorywhich can 另外：

我们可以很容易地得出：

或者我们可以(***)从firstand派生second：

我们还可以得出：

或者我们可以推导出(&&&)给定的dupand (***)：

我的观点是什么，我的问题是什么？是这样的：

Arrow没有什么arr？它似乎完全连贯且有用。是否有任何箭头法则（除了类别法则之外）不涉及arr并且在这里保持完整？这在范畴论中意味着什么？

我基本上从reddit偷了这个问题，但对其进行了概括和阐述： http ://www.reddit.com/r/haskell/comments/2e0ane/category_with_fanout_and_split_but_not_an_arrow/

是否有任何“推荐”的库可以在 Agda 中提供易于使用的基本范畴理论形式化？Agda 标准库似乎在这方面提供的很少。

我正在寻找入门门槛低的东西，类似于使用Semigroup标准库中定义的代数结构的方式。

例如，在我当前的项目中有几个态射概念，重载合成和恒等式的语法变得很尴尬。很自然的做法是引入一个合适的记录类型并使用 Agda 的“实例参数”机制来模拟一个Morphism类型类。但毫无疑问，这一定是一个发明了很多次的轮子。（好吧，标准库中调用Morphism了一个结构，也许可以适应这个目的，所以这不一定是最好的例子，但你明白了。）

我知道这个库，它看起来很全面，但似乎并不是特别活跃。

我们可以有两种类型f, g :: * -> *，它们不是单子，但它们的组合是。例如对于任意固定s：

g a不是 monad（除非我们限制s为 monoid），而是f (g a)状态 monad s -> (s, a)。（不像函子和应用函子，即使两者f和g都是单子，它们的组合也可能不是。）

函子或应用函子有类似的例子吗？那就是组成fand的组合g是一个函子（或应用函子），即使

1. 之一fandg不是（应用）函子，另一个是，或
2. 它们都不是（应用）函子，

在LYHFGG中，作者指出“单子只是支持 >>= 的应用函子”（见下图）。如果我看一下Monad type class的定义，我看不出这句话怎么可能是真的。

Monad 类型类似乎与Control.Applicative类型类没有任何关系，例如 Monad 类型类不是 Applicative 的子类型。所以很明显，从技术上讲，在 Haskell 中，Monads 和 Applicative 函子是完全独立的类型类。因此，如果作者的陈述是真实的，那么它在不同的上下文中一定是真实的。

有人可以通过这个看似不真实的陈述来解释本书作者的意思吗？

他的陈述应该如何解释？在什么情况下？也许在范畴论的背景下？

换句话说： 我看不出如何将任何给定的 Monad 变成 Applicative 函子。因为如果作者的陈述是真的，那么每个 Monad 都可以机械地（通过使用算法）变成 Applicative 函子。但真的有可能做到吗？如果是，如何？

迄今为止的故事——

...

问题，

现在就这一切而言，有两个目标，首先我有兴趣在 scala 中实现 2 类（到目前为止我已经非常成功{我认为程序可能是由在合适的类别中绘制和组合图表 Scala 具有我观察到的 BiCCC 2-Category 结构（至少我很确定）}），第二个通用编程，Free Monad 是更高阶的 monad HMonadyoneda 和 coyoneda 有HFunctor实例，并且我想知道 aHKleisli会是什么样子。

现在，我遇到了A参数相互遮蔽并创建 F[A]-not-F[A] 问题的问题。现在我的第一个想法是添加一个隐式Leibniz[F[A], F[A']]（A' 是伪代码）并使用，希望我可以用它来见证 [A]F[A] [A']F[A'] 的相等性，但我没有'还没有弄清楚它是如何工作的，或者它是否足够，我也想知道我是否只是在这个问题上钻了太久，并且错过了一些明显的重写，这些重写让我到达了我想要去的地方我在这里向好人开放。我希望能提供任何帮助，并尽可能详细地说明如何实现这一点，我希望能分享关于高阶分类抽象的任何想法。