LB
Ну ведь void это и есть боттом-тип в этом случае? Если хаскелевый Void смотреть, а не сишный void, который ()
Я тоже примерно это же место читаю/смотрю. Как я понял, bottom есть у всех типов . Но ботом это не воид
Size: a a a
2019 November 22
t
Я тоже примерно это же место читаю/смотрю. Как я понял, bottom есть у всех типов . Но ботом это не воид
А тогда чем они отличаются? Оба ведь пустое множество, или?..
LB
Ботом это хак чтобы стройная мат теория не разбилась о суровую реальность Тьюринг машин :)
t
Ботом это хак чтобы стройная мат теория не разбилась о суровую реальность Тьюринг машин :)
Т.е. это два разных названия для одного типа/вычисления, но Void - это «запланированный» бот, который «отрицание существования пруфа», а бот _|_ - это техническое проявление неразрешимости теоремы останова?
LB
Т.е. это два разных названия для одного типа/вычисления, но Void - это «запланированный» бот, который «отрицание существования пруфа», а бот _|_ - это техническое проявление неразрешимости теоремы останова?
Да. Получается что у каждого типа есть | _|_ приписка, но ее в рассуждениях не учитываем
KV
А тогда чем они отличаются? Оба ведь пустое множество, или?..
Я вообще не слышал, чтобы пустой тип называли или обозначали как bottom. Обычно bottom — это значение, населяющее все типы, как тут уже говорилось
Oℕ
Я вообще не слышал, чтобы пустой тип называли или обозначали как bottom. Обычно bottom — это значение, населяющее все типы, как тут уже говорилось
В логике и теории типов bottom / bottom type так и называют
KV
А, ну обозначение через falsum видел, действительно
LB
Требования к категориям и к моноидам выглядят удивительно похожими. Моноид хочет ассоциативность и нулевой элемент , категория хочет ассоциативность и identity (ну и правило композиции). Получается каждая категория это моноид?
ТИ
Моноид - категория, в которой только один обьект
ТИ
Категория с большим количеством обьектов уже не будет моноидом
LB
А Monoidal category это какой-то другой термин ?
KN
А Monoidal category это какой-то другой термин ?
скорее на enriched category стоит посмотреть
LB
Читаю про product и coproduct, пишет что они формируют monoidal category , сейчас только заметил приписку "о которых более формально расскажу позже"
Oℕ
А Monoidal category это какой-то другой термин ?
да
KV
В категории-моноиде с одним объектом элементы моноида — это стрелки этого объекта, а в моноидальной категории элементы — сами объекты
AG
МБ
Категория - это монада разве?
NI
Категория - это монада разве?
Можно так определить, как монаду в бикатегории спанов.