是否可以在煤代数上使用无标签最终(对象代数)

Question

Background

Haskell和Scala社区最近非常迷恋他们所谓的无标签最终编程"模式"。这些被引用为初始自由代数的对偶，所以我想知道无标签最终是什么。在ncatlab上，人们只能找到最终代数的讨论，而不是最终代数。

问问题 无标签最终代数是什么类别 最终在 CS 理论堆栈交换中，我得到了一个非常好的答案，指向这篇博文 最终代数语义是观察等价。所以这些确实是最终代数，但与初始代数不属于同一类别的代数......

问题

然而，当我们查看最终无标签的使用方式时，我们发现它经常应用于看起来像代数的东西。例如，参见 Scala 中 The False Hope of Management Effects with Tagless-Final 第 1 部分中的两个Console或UserRepository示例。

因此，代数不是在范畴论中用内函子表示的代数F作为F(X) ⟹ X形式的映射，而是看起来许多人使用final tagless与X ⟹ F(X)映射并表示过程的Coalgebras一起使用。这些真的是一回事吗？还是这里发生了其他事情？

ADT 和最终无标签

关于代数

让我们从Olivier Blanvillain的Scala翻译的最终无标签的解释开始，这些解释取自Haskell的课程作业中的例子。人们注意到，这始于代数数据类型，它确实是代数结构的原型：群。

在类别中，群可以由多项式函子构建F[X] = X×X + X + 1将任何类型带到该类型或该类型的对或 1 的类型。然后为 X 选择一个特定的类型，比如 A 代数是一个函数F[A] ⟹ A。最广为人知的群是正自然数和负自然数的集合，0 表示 Z，因此我们的代数是：

ℤ×ℤ + ℤ + 1 ⟹ ℤ 

代数可以分解为3个函数+: ℤ×ℤ ⟹ ℤ、-: ℤ ⟹ ℤ和常数zero: 1 ⟹ ℤ。如果我们改变X类型，我们会得到不同的代数，这些代数形成一个类别，它们之间有态射，其中最重要的一个是初始代数。

初始代数是免费的代数，它允许人们在不丢失任何信息的情况下构建所有结构。在 Scala 3 中，我们可以为这样的群构建初始代数：

enum IExp {
case Lit(i: Int)
case Neg(e: IExp)
case Add(r: IExp, l: IExp)
}

我们可以使用它构建一个简单的结构：

import IExp._
val fe: IExp = Add(Lit(8), Neg(Add(Lit(1), Lit(2))))

然后可以通过创建函数来解释fe结构IExp => Int或IExp => String，它们是代数范畴中的态射，通过解构 ADT 并递归映射这些到达哪个 到一个代数，用于特定的X(例如String或Int)。这种态射称为折叠。(参见1997年Richard Bird和Oege de Moor的《编程代数》一书)

在无标签决赛中，这转化为特征

trait Exp[T] {
def lit(i: Int): T
def neg(t: T): T
def add(l: T, r: T): T
}

就像一组三个函数一样，它们都返回相同的类型。 表达式是函数应用程序

def tf0[T] given (e: Exp[T]): T =
import e._
add(lit(8), neg(add(lit(1), lit(2))))

这些可以用给定的实例来解释

given as Exp[Int] {
def lit(i: Int): Int = i
def neg(t: Int): Int = -t
def add(l: Int, r: Int): Int = l + r
}
tf0[Int]  // 5

本质上解释是接口的实现Exp在上下文中given(或在 Scala 2implicit中)。

因此，在这里，我们正在从从初始ADT表示的代数结构转向最终的无标签版本。(请参阅关于 cstheory 的讨论，了解这是什么)。

关于煤代数

现在，如果我们以 Scala 中 The False Hope of Management Effects with Tagless-Final 中的UserRepository为例，我们有

trait UserRepository {
def getUserById(id: UserID): User
def getUserProfile(user: User): UserProfile
def updateUserProfile(user: User, profile: UserProfile): Unit
}

这显然是(对于任何读过巴特·雅各布斯(Bart Jacobs)从《对象和类代数》开始的作品的人来说)是关于UserRepository状态S的代数。 Coalgebra是代数的对偶：箭头是相反的。 从函子 F 开始，特定类型 S 开始，从代数的特定类型 S 开始 是一个函数S ⟹ F[S]

在用户存储库的情况下，我们可以看到这是

S ⟹ (Uid → User) × (User → Profile) × (User × Profile → S) 

在这里，函子F(X)将任何类型的函数X带到 3 元组函数。 代数就是这样一个函子 F，一组状态 S，并且 过渡态射S ⟹ F(S). 我们有 2 种观察方法getUserById和getUserProfile以及一种状态改变一种updateUserProfile也称为二传手。通过改变状态的类型 我们改变煤代数。如果我们查看这样一个函子 F 上的所有代数，以及它们之间的态射，我们得到一类代数。其中最重要的一个是最后一个，它给出了对该函子的煤代数的所有观察的结构。

有关代数及其与OO的关系的更多信息，请参阅Bart Jacobs的工作，例如他的(co)代数和(co)Induction Tutorial或此Twitter帖子。

本质上，我们有一个进程，例如UserRepository或Console，它们具有状态并且可以更改状态，而认为这是没有意义的。 数字的状态更改。

现在确实在UserRepository的无标签最终示例中，它是由函子F[_]泛型的，如下所示：

trait UserRepository[F[_]] {
def getUserById(id: UserID): F[User]
def getUserProfile(user: User): F[UserProfile]
def updateUserProfile(user: User, profile: UserProfile): F[Unit]
}

这足以将UserRepository更改为代数吗？在某种程度上，看起来这些函数都具有相同的类型 F[_]，但这真的有效吗？如果 F 是恒等函子怎么办？然后我们有前一个案例。

反过来说，从最终无标签到ADT，人们应该问UserRepository有一个ADT会是什么？(我自己也写过类似的东西来建模更改远程RDF数据库的命令，发现这真的很有帮助，但我不确定这在数学上是否正确。

更多参考资料

• 颇具影响力的Haskell打字无标签最终口译员讲义
• 该文章的翻译为 Scala (Dotty) 重访无标签最终解释器
• 一篇博客文章《从对象代数到最终无标签解释器》指出，对象代数等价于无标签最终。
• 它引用了论文《大众的扩展性，对象代数的实际可扩展性》。

无标签决赛声称的两个优点是

• 它使测试变得容易：通过转向使用接口进行编程，可以 轻松创建接口的模拟实现，以测试代码，例如数据库访问，IO等...
• 它是可扩展的：人们可以很容易地用新的方法来扩展"代数"，克服所谓的表达式问题。(表达式问题在博客文章《从对象代数到最终无标签解释器》中有很好的说明)。

以下内容似乎可以提供线索：

最近的文章Codata in Action声称codata(一个代数概念)是函数式编程和OO编程之间的桥梁，并且实际上使用描述的访问者模式(也用于大众的扩展性)在数据和codata之间进行映射。 见图示。codata的声明是过程抽象的语言不可知表示(上面称为模块化)，可测试性来自Jacobs使用coalgebra类别划分的接口的多个实现。

Answer 1

两种代数之间的区别是有效代数和非有效代数之间的区别。事实上，人们也可以在Dotty(Scala3)中使用GADT编写UserRepo，就像这样：

enum UserRepo[A]{
case GetUserById(id: UserID) extends UserRepo[User]
case GetUserProfile(user: User) extends  UserRepo[UserProfile]
case UpdateUserProfile(user: User, profile: UserProfile) extends UserRepo[Unit]
}

如果我们撇开最终无标签与代数的关系问题，并接受它们与GADT同构，那么我们可以用代数来重新表述这个问题。看起来安德烈·鲍尔(Andrej Bauer)在2019年3月的讲义中详细回答了这个问题 什么是关于效果和处理程序的代数。

安德烈·鲍尔(Andrej Bauer)清楚地解释了代数是什么，从签名开始，然后继续解释理论的解释和模型是什么。 然后，他继续在"§2 作为代数运算的计算效应"中，通过代数的参数化来建模有效的计算。完成后，我们得到的代数与我想知道的代数非常相似。

在"§4 关于代数效应和处理程序的代数是什么？"中，他展示了这种参数化代数的对偶如何为我们提供共同解释、协同模型和协同工作，

而这些东西显然是煤数。我被告知这些处理效果的方法与使用 monads 不同，我需要弄清楚有什么区别，以及这是否会影响问题。