scala - 在Coalgebras上使用Tagless Final(对象代数)可以吗？

Question

背景

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

在CS-理论栈交换上问问题What Category are Tagless Final Algebras Final In，我得到了一个很好的答案，指向此博客文章Final Algebra Semantics is Observational Equivalence。因此，这些确实是最终的代数，但与初始代数不在同一类代数中。

题

但是，当我们研究如何使用最终的无标签时，我们发现它经常应用于看起来像代数的事物。例如，请参见The False Hope of Managing Effects with Tagless-Final in Scala的第1部分中的Console或UserRepository的两个示例。

因此，看起来像许多人将F与Coalgebras（即地图F(X) ⟹ X）一起使用，并且表示过程，而不是使用在类别论中用endofunctors final tagless表示的代数以X ⟹ F(X)形式表示。这些真的是同一回事吗？还是这里发生了其他事情？

ADT和最终无标签

在代数上

让我们从Olivier Blanvillain的Scala translation of examples taken from coursework on in Haskell对最终无标签的解释开始。一个人注意到这始于一个代数数据类型，它确实是一个代数结构的原型：一个组。

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

ℤ×ℤ + ℤ + 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年的 The Algebra of Programming, by Richard Bird and 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 2 implicit中）。

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

煤Coal论

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

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

显然（对于任何阅读过Bart Jacobs从 Objects and Classes Coalgebraically开始的作品的人），状态 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的著作，例如他的 Tutorial on (co)Algebras and (co)Induction或 this Twitter thread。

从本质上讲，我们有一个过程，例如UserRepository或Console，它们具有状态并且可以更改状态，而思考是没有意义的
状态改变的数目。

现在确实是在UserRepository的Tagless Final示例中，它是由Functor 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是身份函子怎么办？然后我们有前面的情况。

从Final Tagless到ADT，应该问 UserRepository的ADT是什么？
（我自己写过类似的东西来模拟更改 a remote RDF database的命令，发现确实很有帮助，但是我不确定这在数学上是否正确。）

其他参考


颇具影响力的Haskell Typed Tagless Final Interpreters讲义
该文章对Scala（Dotty） Revisiting Tagless Final Interpreters的翻译
博客文章 From Object Algebras to Finally Tagless Interpreters证明了对象代数等效于Tagless Final。
它引用了纸张 Extensibility for the Masses, practical extensibility with Object Algebras。


Tagless Final的两个优势是


它使测试变得容易：通过使用界面编程可以
轻松创建接口的模拟实现以测试代码，例如数据库访问，IO等。
它是可扩展的：可以通过克服已知的表达问题的新方法轻松地扩展“代数”。 （在博客文章 From Object Algebras to Finally Tagless Interpreters中很好地说明了表达问题）。


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

最近的文章 Codata in Action声称，codata（合并的概念）是功能编程和OO编程之间的桥梁，并且实际上使用描述的访问者模式（也在 Extensibility for the Masses中使用）在数据和codata之间进行映射。 see illustration。对codata的要求是程序抽象的语言不可知的表示（在上面称为模块性），并且可测试性来自Jacobs所描述的接口的多种实现，其中该接口描述了一个代数。

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]
}

如果我们抛开 how final tagless relates to algebras问题并接受它们与GADT同构，则可以用代数来重新表述该问题。看来Andrej Bauer已在2019年3月的 What is Algebraic about Effects and Handlers讲义中详细解答了这个问题。

从签名开始，安德烈·鲍尔（Andrej Bauer）清楚地解释了什么是代数，然后继续解释了理论的解释和模型。
然后，他继续进行“第2节：作为代数运算的计算效应”，以通过对代数进行参数化来对有效的计算进行建模。完成后，我们得到的代数与我想知道的代数非常相似。

在“第4节”中，关于代数效应和处理程序的结余是什么？他展示了此类参数化代数的对偶如何为我们提供了非常清晰的代数的共同解释，共同模型和合作。

有人告诉我这些处理效果的方法与使用monad不同，我需要弄清楚差异是什么，以及这是否会影响问题。