s
У них же уже ПТСР от слов вроде «функтор» или «монада»!
Ну... Считается, что слушатель знаком с понятием предпучок. И не только из ТК, кстати. Страшно не будет, если объяснить.
И что? Куча математиков ничего не знают о функторах и монадах.
Size: a a a
2021 March 26
s
Ну... Считается, что слушатель знаком с понятием предпучок. И не только из ТК, кстати. Страшно не будет, если объяснить.
И что? Куча математиков ничего не знают о функторах и монадах.
И что? Куча математиков ничего не знают о функторах и монадах.
Слово предпучок не просто так содержит в себе слово пучок.
МБ
Слово предпучок не просто так содержит в себе слово пучок.
И? Думаете, все без исключения математики в курсе?
s
При этом никто не переименовывает предпучки, чтобы люди, незнакомые с понятием пучка, чувствовали себя увереннее.
МБ
При этом никто не переименовывает предпучки, чтобы люди, незнакомые с понятием пучка, чувствовали себя увереннее.
Эмс... Переименовывают. Точнее, называют иначе.
s
Эмс... Переименовывают. Точнее, называют иначе.
Ммм, примеры? Всюду я видел только presheaf.
s
Есть вещи, которые в математике называются по разному (те хе монады, например), но вроде как предпучок это не одна из них.
МБ
Пучки обобщают кучу предыдущих понятий. И многие математики предпочтут работать с дифференцируемыми векторными полями, а не с пучками.
МБ
Сама по себе теория пучков, конечно, интересна, но не всегда релевантна предметной области. И в этой области, наверняка, какой-нибудь пучок накостылят и назовут специально. 🤷♂ Обязаны ли люди обязательно видеть в своей конструкции пучок? Как программисты в своих кванторы? Если без этого работает - ну, разве, плохо?
s
Частные случаи это всё-таки не то же самое, что синонимы.
МБ
Ну... Да. Но в языках частные случаи тоже, ведь. Кванторы там далеки от общих понятий.
AT
Сама по себе теория пучков, конечно, интересна, но не всегда релевантна предметной области. И в этой области, наверняка, какой-нибудь пучок накостылят и назовут специально. 🤷♂ Обязаны ли люди обязательно видеть в своей конструкции пучок? Как программисты в своих кванторы? Если без этого работает - ну, разве, плохо?
Напомню контекст. В Ada завезли (потырили из Eiffel?) конструкции типа
for all x of some_set => foo(x). for all они там нифига не переизобрели, а взяли прямо из исчисления предикатов первого порядка, как Вы понимаете.МБ
Напомню контекст. В Ada завезли (потырили из Eiffel?) конструкции типа
for all x of some_set => foo(x). for all они там нифига не переизобрели, а взяли прямо из исчисления предикатов первого порядка, как Вы понимаете.Ага, я нашёл. Авторы Ada 2012, конечно, утверждают, что это кванторы. Но по смыслу, всё же, это просто циклы. Скорее уж оригинал вводит пользователя в заблуждение. Если следовать оригиналу, надо квантифицировать. Но я бы сделал замечание, что это не настоящая квантифокация.
МР
Ага, я нашёл. Авторы Ada 2012, конечно, утверждают, что это кванторы. Но по смыслу, всё же, это просто циклы. Скорее уж оригинал вводит пользователя в заблуждение. Если следовать оригиналу, надо квантифицировать. Но я бы сделал замечание, что это не настоящая квантифокация.
А почему она не настоящая? Как выглядит настоящая?
МР
PS
Максим Резник
@true_grue Можете посмотреть как будет время: https://github.com/true-grue/Compiler-Development/pull/9
Спасибо, уже видел, доберусь до компьютера — поправлю!
МБ
Максим Резник
А почему она не настоящая? Как выглядит настоящая?
Ну, как в ЯП с зависимыми типами. Или как в illative lambda calculus. Последнее плохо изучено.
В завтипах - это зависимое произведение: forall x:A. P(x) - это такой тип, а не runtime конструкция. И зависимая пара: exists x:A. P(x) - тоже тип.
Первое - тип функции. Второе - тип пары значений.
Ну, то есть, это не циклы, как в Ada.
В завтипах - это зависимое произведение: forall x:A. P(x) - это такой тип, а не runtime конструкция. И зависимая пара: exists x:A. P(x) - тоже тип.
Первое - тип функции. Второе - тип пары значений.
Ну, то есть, это не циклы, как в Ada.
AT
Ну, как в ЯП с зависимыми типами. Или как в illative lambda calculus. Последнее плохо изучено.
В завтипах - это зависимое произведение: forall x:A. P(x) - это такой тип, а не runtime конструкция. И зависимая пара: exists x:A. P(x) - тоже тип.
Первое - тип функции. Второе - тип пары значений.
Ну, то есть, это не циклы, как в Ada.
В завтипах - это зависимое произведение: forall x:A. P(x) - это такой тип, а не runtime конструкция. И зависимая пара: exists x:A. P(x) - тоже тип.
Первое - тип функции. Второе - тип пары значений.
Ну, то есть, это не циклы, как в Ada.
Справедливости ради, зав. типы – это higher-order logic, а Ada – first order. 🙂
K
Напомню контекст. В Ada завезли (потырили из Eiffel?) конструкции типа
for all x of some_set => foo(x). for all они там нифига не переизобрели, а взяли прямо из исчисления предикатов первого порядка, как Вы понимаете.Лучше б они foldMap и ленивое исполнение завезли. Или, хотя бы,
all/any как HOF, а не как конструкты