在Coalgebras上使用Tagless Final（对象代数）可以吗？

Question

背景

Haskell和Scala社区最近对他们所谓的无标签最终编程“模式” 非常着迷。这些被称为初始自由代数的对偶，所以我想知道Tagless Final是最终的。在ncatlab上，仅能找到最终的代数，而不是最终的代数。

问一个问题什么是无标签的最终代数最终在 CS-理论栈交换中，我得到了一个很好的答案，指向此博客文章《最终代数语义是观察上的等效性》。因此，这些确实是最终代数，但与初始代数不在同一类代数中。

题

然而，当我们看看如何最终无标签的使用，我们发现，这是很经常应用于东西看起来像余代数。例如，请参阅Scala中使用Tagless-Final管理效果的虚假希望的第1部分中a Console或a 的两个示例。UserRepository

因此，看起来像代数论一样，它并没有F像在分类论中用endofunctors 形式表达的代数作为形式的映射F(X) ? X那样，而是像许多final tagless与Coalgebras 一样使用，它们是映射X ? F(X)，并表示过程。这些真的是同一回事吗？还是这里发生了其他事情？

ADT和最终无标签

在代数上

让我们从Olivier Blanvillain的Scala译文中对最终无标签的解释开始，这些范例摘自Haskell的课程。一个人注意到这始于一个代数数据类型，它确实是一个代数结构的原型：一个组。

在类别中，可以用多项式函子构建一个组，该多项式函子 F[X] = X×X + X + 1可以将任意类型的类型作为该类型对或该类型对或1的类型。然后为X选择一个特定类型，例如A代数是一个函数F[A] ? A。最广为人知的组是正负自然数的集合，0表示？，因此我们的代数为：

?×? + ? + 1 ? ? 

代数可以被分解成3个功能+: ?×? ? ?，-: ? ? ?和常数zero: 1 ? ?。如果我们改变类型X，我们将得到不同的代数，并且这些代数形成一个类别，它们之间具有同态射态，其中最重要的是初始代数。

最初的代数是免费的，它使人们能够构建所有结构而不会丢失任何信息。在Scala 3中，我们可以为这样的组建立初始代数：

?×? + ? + 1 ? ? 

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

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

该fe结构然后可以通过创建函数被解释IExp => Int或IExp => String，这是在代数的类别，其中态射到达一个由解构ADT，并递归地对特定X（例如映射到这些的代数String或Int）。这种形态被称为折叠。（请参阅Richard Bird和Oege de Moor在1997年出版的《编程的代数》一书）

在无标签决赛中，这转变成特质

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))))

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

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中2 implicit）中的上下文。

因此，在这里，我们正从最初的ADT表示的代数结构过渡到最终的无标签版本。（请参阅有关cstheory的讨论）。

煤Coal论

现在，如果我们以Scala中使用Tagless-Final管理效果的错误希望UserRepository为例，

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

显然（对于任何阅读过Bart Jacobs的一些从Objects and Classes Coalgebraically入手的人），状态S的合并代数UserRepository。代数是代数的对偶：箭头相反。从Functor F到特定的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）Algebras和（co）Induction教程或此Twitter线程。

从本质上讲，我们有一个诸如UserRepository或Console之类的进程，它们具有状态并且可以更改状态，而考虑数字的状态更改是没有意义的。

现在确实如此，在UserRepository的Tagless Final示例中，它是由Functor生成的F[_]，如下所示：

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

这足以将UserRepository更改为代数吗？在某种程度上，函数看起来都具有相同的F [_]类型范围，但这确实有效吗？如果F是身份函子怎么办？然后我们有前面的情况。

换一种方式，从最终无标签到ADT，应该问问ADT的用途是UserRepository什么？（我自己写过类似的东西来建模用于更改远程RDF数据库的命令的模型，发现这确实很有用，但是我不确定这在数学上是否正确。）

其他参考

• 颇具影响力的Haskell 类型无标签最终口译员讲义
• Scala（Dotty）再次探讨无标签最终口译员的文章翻译
• 从对象代数到Finalless无标记解释器的博客文章证明了Object代数等同于Tagless Final。
• 它引用了《论文的质量可扩展性》，《对象代数的实际可扩展性》。

无标签决赛的两个优势是

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

以下看起来可以提供一个线索：

最近的文章中行动CODATA声称CODATA（一个coalgebraic概念）是功能性的和OO编程之间的桥梁，并且实际使用中描述的访问者模式（在也用于扩展用于大量数据的）数据和CODATA之间进行映射。参见插图。对codata的声明是过程抽象的语言不可知的表示（在上面称为模块性），并且可测试性来自Jacobs所描述的接口的多种实现，其中该接口描述了共同代数的类别。

Answer 1

两种类型的代数之间的区别是有效代数和无效代数之间的区别。事实上，我们也可以在 Dotty (Scala3) 中使用 GADT 编写 UserRepo，如下所示：

\n\n

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

\n\n

如果我们抛开最终 tagless 与代数如何相关的问题并接受它们与 GADT 同构，那么我们可以用代数来重新表述该问题。看起来 Andrej Bauer 在 2019 年 3 月的讲义中详细回答了这个问题What is Algebraic about Effects and Handlers。

\n\n

Andrej Bauer 从签名开始清楚地解释了什么是代数，然后解释什么是理论的解释和模型。\n然后他在“\xc2\xa72 作为代数运算的计算效应”中继续通过参数化来模拟有效的计算代数。完成后，我们得到的代数与我想知道的代数非常相似。

\n\n

在“\xc2\xa74 关于代数效应和处理程序的余代数是什么？” 他展示了这种参数化代数的对偶如何为我们提供对显然是余代数的共同解释、共同模型和合作。

\n\n

我被告知这些处理效果的方法与使用 monad 不同，我需要找出区别是什么，以及这是否会影响问题。

\n