Фон
Сообщество Haskell и Scala в последнее время очень очаровано тем, что они называют безметочным окончательным «шаблоном» программирования.На них ссылаются как на двойные по отношению к начальным свободным алгебрам, поэтому мне было интересно, какой финал Tagless был финальным.На ncatlab можно говорить только о конечных коалгебрах, а не о конечных алгебрах.
Задавая вопрос Какие категории являются финальными Алгебрами без тэгов В на обмене стеками теории CS Я получил очень хороший ответ, указывая на это сообщение в блоге Семантика конечной алгебры - это наблюдательная эквивалентность .Таким образом, это действительно конечные алгебры, но не в той же категории, что и начальные ...
Вопрос
Тем не менее, когда мы посмотрим, как окончательный без тегов используется используется , мы находим, что это очень часто применяется для вещей, которые похожи на коалгебры.См., Например, два примера Console или UserRepository в части 1 Ложная надежда на управление эффектами с помощью Tagless-Final в Scala .
Таким образом, вместо того, чтобы иметь алгебры, которые в теории категорий выражаются эндофункторами F в качестве карт вида F(X) ⟹ X, похоже, что многие используют final tagless с коалгебрами, которые являются картами X ⟹ F(X), и представляютпроцессы.Это действительно одно и то же?Или здесь что-то еще происходит?
ADT и окончательный тэг
на алгебрах
Давайте начнем с объяснений окончательного тэга, данного Оливье Бланвьеном перевода 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).Этот морфизм известен как складка.(См. Книгу 1997 года Алгебра программирования Ричарда Берда и Эге де Моора )
В финале без тегов это превращается в черту
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, к окончательной версии без тегов.(См. Обсуждение теории о том, что это такое ).
О коалгебрах
Теперь, если мы возьмем пример UserRepository из Ложная надежда на управлениеЭффекты с Tagless-Final в Scala , у нас есть
trait UserRepository {
def getUserById(id: UserID): User
def getUserProfile(user: User): UserProfile
def updateUserProfile(user: User, profile: UserProfile): Unit
}
Это ясно (для тех, кто читал некоторые работы Барта Джейкобса, начиная с Объекты и классы, коалгебраически )коалгебра по состоянию S UserRepository.Коалгебра двойственна алгебре: стрелки обратные.Начиная с Functor F и определенного типа S, коалгебра представляет собой функцию S ⟹ F[S]
В случае пользовательского хранилища мы можем видеть, что это будет
S ⟹ (Uid → User) × (User → Profile) × (User × Profile → S)
Здесь функторF(X) переводит любой тип X в три набора функций.Коалгебра - это такой функтор F, множество состояний S и морфизм перехода S ⟹ F(S).У нас есть 2 метода наблюдения getUserById и getUserProfile и один изменяющий состояние один updateUserProfile, также известный как установщик.Изменяя тип состояний, мы меняем коалгебру.Если мы посмотрим на все коалгебры на таком функторе F и на морфизмы между ними, мы получим категорию коалгебр.Из них наиболее важным является последний, который дает структуру всех наблюдений за коалгебрами этого функтора.
Для получения дополнительной информации о коалгебрах и их связи с ОО см. Работы Барта Джейкобса, такие как его Учебник по (со) алгебрам и (со) индукции или этой ветке Twitter .
По сути, у нас есть такой процесс, как UserRepository или Console, которые имеют состояние и могутизменить состояние, тогда как не имеет смысла думать об изменении состояния для числа.
Теперь верно, что в последнем примере TagRepository из UserRepository он генерируется с помощью 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 - функтор Identity?Тогда у нас есть предыдущий случай.
Если пойти по другому пути, от Final Tagless до ADT, следует спросить, что это будет за ADT для UserRepository?(Я сам написал нечто подобное для моделирования команд для изменения удаленной базы данных RDF и нашел это действительно полезным, но я не уверен, что это правильно математически.)
Дополнительные ссылки
Два преимущества, заявленные в Tagless Final:
- упрощают тестирование: переходя к программированию с интерфейсами, можно легко создаватьмакетные реализации интерфейса для тестирования кода, такие как доступ к базе данных, ввод-вывод и т. д ...
- он расширяемый: одинможет легко расширить «алгебру» новыми методами, преодолевая то, что известно как проблема выражения.(Проблема выражения хорошо проиллюстрирована в сообщении в блоге От алгебр объектов до окончательных интерпретаторов без тегов ).
Следующее выглядит так, как будто оно может дать подсказку:
В недавней статье Codata in Action утверждается, что codata (коалгебраическая концепция) является мостом между функциональным и ОО-программированием и фактически использует описанный шаблон посетителей (также используемый в Расширяемость для масс * 1163).*) для сопоставления данных и кодатов. см. Иллюстрацию .Заявки на codata являются независимым от языка представлением процедурной абстракции (выше названной модульностью), а тестируемость происходит из множества реализаций интерфейса, который Джейкобс описывает с категорией для коалгебры.