在余代数上使用无标记的Final（对象代数）可以吗？

Question

然而，当我们研究如何使用final tagless时，我们发现它经常应用于看起来像余代数的事情。例如，请参见Scala中使用Tagless-Final管理效果的错误希望第1部分中的控制台或userrepository的两个示例。

因此，在范畴理论中，代数用内函数F表示为F(X)X形式的映射，而不是用F(X)形式的映射，看起来许多代数使用final less，而余代数是映射X F(X)，并表示过程。这些真的是一回事吗？还是这里发生了别的什么事？

让我们从Olivier Blanvillain对final tagless的解释开始，他的Scala翻译摘自Haskell课程中的例子。我们会注意到，这是从一个代数数据类型开始的，它实际上是一个代数结构的原型：一个组。

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

ℤ×ℤ + ℤ + 1 ⟹ ℤ 

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

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

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

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

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

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，即给定（或在Scala2隐式)。

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

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

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

在这里，函数f(X)将任何类型X转换为一个3元组函数。余代数是这样一个函子F，一个状态集S和一个转移态射S F(S)。我们有两个观察方法getUserByID和getUserProfile，还有一个状态更改方法UpdateUserProfile，也称为setter。通过改变状态的类型，我们改变了余代数。如果我们研究这样一个函子F上的所有余代数，以及它们之间的态射，我们得到了一个余代数范畴。其中最重要的一个是最后一个，它给出了该函子的余代数上所有观测的结构。

关于余代数及其与面向对象关系的更多信息，请参见Bart Jacobs的工作，如他的（共）代数和（共）归纳法教程，或者这条Twitter线程。

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是什么？（我自己编写了类似的代码，用于对更改远程RDF数据库的命令进行建模，并发现这确实很有帮助，但我不确定这在数学上是否正确。）

• 有影响力的Haskell打印了无标签的最终口译员课堂讲稿
• 那篇文章的Scala翻译（Dotty）重访无标签最终解释器
• 一篇从对象代数到最终无标记解释器的博客文章说明了对象代数等同于无标记最终解释器。
• 引用了论文中关于质量的可扩展性和关于对象代数的实用可扩展性。

null

最近的文章Codata in Action声称，Codata（一个共代数概念）是函数式编程和面向对象编程之间的桥梁，并且实际上使用所描述的访问者模式（也用于面向大众的可扩展性）在数据和Codata之间进行映射。见插图。对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]
}

如果我们撇开最终无标记如何与代数相关的问题，并接受它们与GADTs同构，那么我们就可以用代数来重新表述这个问题。在那里，安德烈·鲍尔（Andrej Bauer）似乎已经在2019年3月的课堂讲稿中详细回答了这个问题，什么是关于效果和处理程序的代数。

安德烈·鲍尔清楚地解释了什么是代数，从签名开始，然后解释了什么是理论的解释和模型。然后，他在“§2作为代数运算的计算效果”中继续通过代数的参数化来为有效的计算建模。当这样做的时候，我们得到的代数看起来和我想知道的代数非常相似。