"Состояние" объектов замечательно моделируются либо Хагиновыми терминальными F,G-диалгебрами, либо просто терминальными коалгебрами, когда в правой части может стоять экспонента. Получается, какбе, чисто. Не знаю, будет ли сиять ;-)
На самом деле, F,G-диалгебры выглядят более естественно, но терминальные коалгебры во многих случаях позволяют сделать то же самое, если только в правой части может быть экспонента.
Например, сигнатуры типа (Self, A) -> (Self, D, E, F, G) которые можно записать только диалгебрами, коалгебрами можно записать, как Self -> A -> (Self, D, E, F, G) Не совсем по-категорному, но наверное, понятно.
Насчёт диалгебр такой косяк, что их существование, зачастую, как в данном примере, эквивалентно существованию некоторых сопряжённостей, а не все сопряжённости одинаково полезны. Например, существование правого сопряжённого к data-функтору списка приводит к вырожденности категории (все объекты изоморфны). Это у Хагино доказывается, вроде, несложно.
Есть Фрейдовые диалгебры, они, в некоторм смысле, обобщают понятия "начальный-терминальный", это алгебры от дифунктора (профунктора), то есть, A x A^op -> A В основном, пользуются для простоты работы с разными вариантностями. F,G-диалгебры обощают алгебры и коалгебры. Интересно было бы скрестить Фрейдовые и Хагиновые диалгебры, чтобы избежать неприятной возни с вариантностями у Хагино. Только вот, определять ограничения будет ещё сложнее.
Немного Фрейдовые диалгебры упоминается у Varmo Vene Categorical Programming With Inductive and Coinductive types в главе про Mendler'овые схемы рекурсии. Ну и у самого Фрейда, вроде, в его Algebraically Complete Categories Статья, на мой взгляд, очень любопытная.
F,G-диалгебры по Hagino описаны они в его статье A Categorical Programming Language Там много пурги, но думаю, её будет быстро пролистать. В 3-й главе чуть подробнее говорится по F,G-диалгебры и приводится пример, что любые они нам не нужны, ибо слишком нехорошие объекты ими можно описать.
Ещё одна статья, где Hagino создаёт свою лямбду, и замахивается на дальнейшее усовершенствование ML A Typed Lambda Calculus with Categorical Type Constructors. Там же он рассказывает про F,G-диалгебры, и пожалуй, стоит читать именно её, только вот, примера про вырожденность категории, где есть правый сопряжённый к data-функтору списка (и ещё какой-то пример), нет.
Ну и ещё несколько статеек на тему и близко.
Erik Poll and Jan Zwanenburg, From Algebras and Coalgebras to Dialgebras Тут кратенько рассказывается про F,G-диалгебры, и про чего-то, около интерфейсов класса, которые ими можно описывать. Вроде, там они для полиномиальных функторов.
Ещё две, парочка немного любопытных статей от Hendrik Tews:
Coalgebras for Binary Methods: Properties of Bisimulation and Invariants
Greatest Bisimulation for Binary Methods
ИМХО, с категорной стороны, нормально написана из этих статей только статья Фрейда. Вторая статья Хагино, где он описывает реализацию своих затей в виде типизированной лямбды тоже интересна, но только тем, что так даётся нечто законченное.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2010-02-27 07:16 am (UTC)no subject
Date: 2010-02-27 08:39 am (UTC)либо Хагиновыми терминальными F,G-диалгебрами,
либо просто терминальными коалгебрами, когда
в правой части может стоять экспонента.
Получается, какбе, чисто.
Не знаю, будет ли сиять ;-)
no subject
Date: 2010-02-27 03:23 pm (UTC)no subject
Date: 2010-02-27 03:35 pm (UTC)но терминальные коалгебры во многих случаях позволяют сделать
то же самое, если только в правой части может быть экспонента.
Например, сигнатуры типа
(Self, A) -> (Self, D, E, F, G)
которые можно записать только диалгебрами,
коалгебрами можно записать, как
Self -> A -> (Self, D, E, F, G)
Не совсем по-категорному, но наверное, понятно.
Насчёт диалгебр такой косяк, что их существование, зачастую,
как в данном примере, эквивалентно существованию некоторых сопряжённостей,
а не все сопряжённости одинаково полезны.
Например, существование правого сопряжённого к data-функтору списка
приводит к вырожденности категории (все объекты изоморфны).
Это у Хагино доказывается, вроде, несложно.
no subject
Date: 2010-02-28 04:23 pm (UTC)no subject
Date: 2010-03-02 09:58 am (UTC)Есть Фрейдовые диалгебры, они, в некоторм смысле,
обобщают понятия "начальный-терминальный",
это алгебры от дифунктора (профунктора), то есть,
A x A^op -> A
В основном, пользуются для простоты
работы с разными вариантностями.
F,G-диалгебры обощают алгебры и коалгебры.
Интересно было бы скрестить Фрейдовые и Хагиновые диалгебры,
чтобы избежать неприятной возни с вариантностями у Хагино.
Только вот, определять ограничения будет ещё сложнее.
Немного Фрейдовые диалгебры упоминается у Varmo Vene
Categorical Programming With Inductive and Coinductive types
в главе про Mendler'овые схемы рекурсии.
Ну и у самого Фрейда, вроде, в его
Algebraically Complete Categories
Статья, на мой взгляд, очень любопытная.
F,G-диалгебры по Hagino описаны они в его статье
A Categorical Programming Language
Там много пурги, но думаю, её будет быстро пролистать.
В 3-й главе чуть подробнее говорится по F,G-диалгебры
и приводится пример, что любые они нам не нужны,
ибо слишком нехорошие объекты ими можно описать.
Ещё одна статья, где Hagino создаёт свою лямбду,
и замахивается на дальнейшее усовершенствование ML
A Typed Lambda Calculus with Categorical Type Constructors.
Там же он рассказывает про F,G-диалгебры, и пожалуй,
стоит читать именно её, только вот, примера про
вырожденность категории, где есть правый сопряжённый
к data-функтору списка (и ещё какой-то пример), нет.
Ну и ещё несколько статеек на тему и близко.
Erik Poll and Jan Zwanenburg,
From Algebras and Coalgebras to Dialgebras
Тут кратенько рассказывается про F,G-диалгебры,
и про чего-то, около интерфейсов класса,
которые ими можно описывать.
Вроде, там они для полиномиальных функторов.
Ещё две, парочка немного любопытных статей от Hendrik Tews:
Coalgebras for Binary Methods:
Properties of Bisimulation and Invariants
Greatest Bisimulation for Binary Methods
ИМХО, с категорной стороны, нормально написана
из этих статей только статья Фрейда.
Вторая статья Хагино, где он описывает реализацию
своих затей в виде типизированной лямбды тоже интересна,
но только тем, что так даётся нечто законченное.
no subject
Date: 2010-03-02 09:59 am (UTC)тогда могу где-нибудь выложить или куда-нибудь выслать.