Oℕ
А как в хаскелле
а в хаскеле не индуктивные
Size: a a a
2019 December 17
Oℕ
а что?
тензорное произведение объекта самого на себя
KV
Я сказал "индуктивные"? Ну блин
CE
а в хаскеле не индуктивные
А что такое индуктивные тогда?
Oℕ
что например композиция функторов
Oℕ
А что такое индуктивные тогда?
хочу подготовиться и ответить завтра
CE
Ух, хорошо, спасибо. А то я что-то не видел какого-то понятного мне определения
KV
Как минимум индуктивные типы должны идти в комплекте с принципом индукции, а он невыразим
YS
тензорное произведение объекта самого на себя
оно совпадает с композицией функторов?
ЕО
Опять ваши спекуляции на тему сильно неформализованную
МБ
оно совпадает с композицией функторов?
В категории функторов
ЕО
В целом можно сказать одно: монада в ТК понятие параметризованное категорией, а монада в хаскеле над определенной "категорией"
YS
В категории функторов
то есть Хаскель — скучный срез ТК?
AG
то есть Хаскель — скучный срез ТК?
ну да там же одна категория
AG
ну ещё можно подкатегории выделять
ЕО
ну да там же одна категория
Ну там щас Type:Type есть, так что "выделять подкатегории" это довольно сильный инструмент
ЕО
Предлагаю собраться как-нибудь и попробовать формализовать категорно функциональный язык программирования с ленивой редукцией и Type:Type
МБ
то есть Хаскель — скучный срез ТК?
Надо определить "скучный". ТК, конечно, шире применяется.
ЕО
Предлагаю собраться как-нибудь и попробовать формализовать категорно функциональный язык программирования с ленивой редукцией и Type:Type
Как DCPO-ENRICHED категорию, а потом показать, что можно с её помощью рассуждать о хаскеле
МБ
Предлагаю собраться как-нибудь и попробовать формализовать категорно функциональный язык программирования с ленивой редукцией и Type:Type
А Воеводский ещё этого не сделал?