KV
Ну когда на бифункторы смотрят как на операции (и наоборот)
Size: a a a
2018 October 05
NI
Например?
KV
Моноидальные категории...
KV
Ну и вообще, внутренние алгебры
KV
Или даже внутренние логики
NI
В общем, это вполне согласуется с моим тезисом о том, что типы, это функторы.
И соответственный подход к их морфизмам ;-)
И соответственный подход к их морфизмам ;-)
KV
NI
Не всё ;-) Какие-то из тех примеров в тему, а какие-то нет.
NI
Я думаю, что понял, о чём речь.
KV
В общем, это вполне согласуется с моим тезисом о том, что типы, это функторы.
И соответственный подход к их морфизмам ;-)
И соответственный подход к их морфизмам ;-)
Меня натолкнули на мысль метафоры, представленные Бартошем Милевским в его книге. Функторы сопровождаются отображениями, сохраняющими структуру, но меняющими содержимое, а естественные преобразования меняют структуру (сам функтор), но не меняют содержимое. Это все в рамках одного и того же программистского подхода, да
к
Естественные преобразования вроде как вполне могут менять содержимое, не меняют содержимое естественные изоморфизмы
ЗП
Естественные преобразования вроде как вполне могут менять содержимое, не меняют содержимое естественные изоморфизмы
естественные преобразование в точности до изоморфизма, да не могут менять
KV
Естественные преобразования вроде как вполне могут менять содержимое, не меняют содержимое естественные изоморфизмы
Ну это вопрос терминологии. Преобразование из List в Maybe, конечно, теряет информацию, но что сохраняет, то сохраняет как есть, без изменений
к
Контрпример: константный функтор, который все в один объект сводит, он ничего не сохраняет
NI
Можно так сказать — сохраняет то, что ещё как-то можно сохранить ;-)
В случае константного, убивается всё напрочь ;-)
В случае константного, убивается всё напрочь ;-)
KV
Контрпример: константный функтор, который все в один объект сводит, он ничего не сохраняет
У этого функтора пустая структура, поэтому можно сказать, что преобразование в него сохраняет содержимое тривиально
KV
Это как "для любого х из пустого множества" - тривиально истинно
KV
Ну ваще, это же метафора, зачем её терзать. Истины тут все равно нет.
к
Правилен ли мой вывод, что раз константый функтор все сводит в один объект и из любого функтора есть нат преобразование (есть у этого короткий термин?), то объект, в который сводит конст - терминальный?
KV
Правилен ли мой вывод, что раз константый функтор все сводит в один объект и из любого функтора есть нат преобразование (есть у этого короткий термин?), то объект, в который сводит конст - терминальный?
По-моему, там нарушается условие единственности