Можно ли использовать финал без тегов (объектные алгебры) на коалгебрах?

Question

Задний план

Сообщество Haskell и Scala в последнее время очень увлечено тем, что они называют окончательным "шаблоном" программирования без тегов. На них ссылаются как на двойственные к исходным свободным алгебрам, поэтому мне было интересно, чем был финал без тегов. На ncatlab можно найти разговоры только о конечных коалгебрах, но не об окончательных алгебрах.

Задавая вопрос, какая категория является финальной алгеброй без тегов Final In on CS-Theory Stack Exchange, я получил очень хороший ответ, указывающий на это сообщение в блоге. Окончательная семантика алгебры - это наблюдательная эквивалентность. Так что это действительно конечные алгебры, но не из той же категории алгебр, что и исходная...

Вопрос

Тем не менее, когда мы смотрим на то, как окончательный tagless будет использоваться, мы находим, что она очень часто применяются для вещей, которые выглядят как коалгебры. См., Например, два примераConsole или UserRepositoryв части 1 книги "Ложная надежда на управление эффектами с помощью Tagless-Final в Scala".

Поэтому вместо алгебр, которые в теории категорий выражаются эндофункторами F как карты формы F(X) ⟹ X, похоже, многие используют final tagless с коалгебрами, которые являются картами X ⟹ F(X), и представляют процессы. Неужели это одно и то же? Или здесь что-то еще происходит?

ADT и Final Tagless

Об алгебрах

Давайте начнем с объяснений final tagless, данных в переводе Оливье Бланвиллена на Scala примеров, взятых из курсовой работы на 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). This morphism is known as a fold. (See the 1997 book The Algebra of Programming, by Richard Bird and Oege de Moor)

In Tagless final this is transformed into the trait

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

As is a set of three functions all returning the same type. Expressions are function applications

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

and these can be interpreted with a given instance

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

Essentially the interpretation is the implementation of the interface Exp that is given (or in Scala 2 implicit) in the context.

So here we are moving from an algebraic structure expressed from an initial ADT to a final tagless version. (See the discussion on cstheory on what that is).

On Coalgebras

Now if we take the UserRepository example from The False Hope of Managing Effects with Tagless-Final in Scala, we have

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

this is clearly (for anyone who has read some of Bart Jacobs' work starting with Objects and Classes Coalgebraically) a coalgebra on the state S of UserRepository. A Coalgebra is the dual of an Algebra: the arrows are reversed. Starting from a Functor F, and a specific type S an coalgebra is a function S ⟹ F[S]

In the case of a user repository we can see this to be

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

Here the functor F(X) takes any type X to a 3-tuple of functions. The coalgebra is such a functor F, a set of states S, and a transition morphism S ⟹ F(S). We have 2 observational methods getUserById and getUserProfile and one state changing one updateUserProfile also known as a setter. By varying the type of states we vary the coalgebra. If we look at all coalgebras on such a functor F, and the morphisms between them, we get a category of coalgebras. Of which the most important one is the final one which gives the structure of all observations on the coalgebras of that functor.

For more info on coalgebras and their relation to OO see the work by Bart Jacobs such as his Tutorial on (co)Algebras and (co)Induction or this Twitter thread.

Essentially we have a process such as a UserRepository or a Console that have state and can change state, whereas it does not make sense to think of change of state for a number.

Now it is true that in the Tagless Final example of UserRepository it is Genericised by a Functor F[_], like this:

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, следует спросить, что было бы иметь ADT для UserRepository? (Я сам написал нечто подобное для моделирования команд для изменения удаленной базы данных RDF и обнаружил, что это действительно полезно, но я не уверен, правильно ли это математически.)

Дальнейшие ссылки

• Заметки к лекциям влиятельного Haskell Typed Final Interpreters
• Перевод этой статьи для Scala (Dotty) Revisiting Final Interpreters без тегов
• Сообщение в блоге " От объектных алгебр до интерпретаторов без тегов" утверждает, что объектные алгебры эквивалентны Final без тегов.
• Он цитирует статью " Расширяемость для масс, практическая расширяемость с помощью объектных алгебр".

Два заявленных преимущества финала без тегов:

• это упрощает тестирование: переходя к программированию с интерфейсами, можно легко создать фиктивные реализации интерфейса для тестирования кода, такого как доступ к базе данных, ввод-вывод и т. д.
• она расширяема: можно легко расширить "алгебру" с помощью новых методов, преодолевающих так называемую проблему выражения. (Проблема с выражениями хорошо проиллюстрирована в сообщении блога " От объектных алгебр до, наконец, интерпретаторов без тегов").

Похоже, следующее может дать ключ к разгадке:

В недавней статье Codata in Action утверждается, что codata (коалгебраическая концепция) является мостом между функциональным и объектно-ориентированным программированием и фактически использует описанный шаблон посетителя (также используемый в Extensibility for the Masses) для сопоставления данных и кодированных. см. иллюстрацию. Заявления о кодах - это не зависящее от языка представление процедурной абстракции (названное выше модульностью), а тестируемость обеспечивается множественными реализациями интерфейса, который Якобс описывает с категорией для коалгебры.

Answer 1

Разница между этими двумя типами алгебр заключается в том, что они действуют между эффективными и неэффективными алгебрами. Действительно, можно написать UserRepo с помощью GADT в Dotty (Scala3), например, так:

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

Если оставить в стороне проблему того, как final tagless относится к алгебрам, и принять, что они изоморфны GADT, то мы можем перефразировать проблему в терминах алгебр. Похоже, что Андрей Бауэр подробно ответил на проблему в лекциях за март 2019 г. Что такое алгебраические эффекты и обработчики.

Андрей Бауэр ясно объясняет, что такое алгебры, начиная с сигнатур, и переходит к объяснению того, что такое интерпретации и модели теории. Затем он переходит к "§2 Вычислительные эффекты как алгебраические операции", чтобы моделировать эффективные вычисления путем параметризации алгебр. Когда это будет сделано, мы получим алгебры, очень похожие на те, которые меня интересовали.

В "§4. Что такое коалгебраическое в алгебраических эффектах и ​​обработчиках?" он показывает, как двойственные к таким параметризованным алгебрам дают нам соинтерпретации, совместные модели и кооперации для того, что совершенно очевидно является коалгебрами.

Мне сказали, что эти способы обработки эффектов не совпадают с использованием монад, и мне нужно выяснить, в чем разница, и влияет ли это на проблему.