MG
How to design world рассказывает про то, как сделать интерактивную программу. Не про то.
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
384 membersпожаловаться на группу
2019 August 24
AT
Alexander Tchitchigin in Типы в языках программирования, моделирования, представления знаний и жизни
Не очень удачный пример с налогами. Традиционный пример — это замена насоса на нефтеперерабатывающем заводе. Был насос одного производителя, поломался — его заменили на насос другого производителя, но на чертежах ведь всё осталось то же самое. У насоса тем самым есть несколько имён: комплектующее, которое на чертежах, предмет закупки (всё, что закупили для этой позиции на чертеже) и установленное оборудование (тот насос, который сейчас работает). С этим всем нужно работать: три системы учёта одного и того же насоса. Нужно, чтобы учёт не развалился, ибо насосов пара десятков тысяч, всё время что-то ломается, а вот ещё технари удумали один мощный насос двумя маломощными заменить — и нужно как-то и это отразить. Какую конструкцию из каких типов нужно для этого предложить, и почему?
Интересный вопрос. Начинает проясняться, где собака зарыта.
А можете сразу сказать в каких местах вылазят косяки и какие при "типичном" моделировании как делают сейчас?
А можете сразу сказать в каких местах вылазят косяки и какие при "типичном" моделировании как делают сейчас?
AG
смахивает на сеть петри
MG
@GabrielFallen Пару типичных косяков я привёл выше: забывают про время и про то, что физические объекты меняют свои роли.
AT
Alexander Tchitchigin in Типы в языках программирования, моделирования, представления знаний и жизни
Не очень удачный пример с налогами. Традиционный пример — это замена насоса на нефтеперерабатывающем заводе. Был насос одного производителя, поломался — его заменили на насос другого производителя, но на чертежах ведь всё осталось то же самое. У насоса тем самым есть несколько имён: комплектующее, которое на чертежах, предмет закупки (всё, что закупили для этой позиции на чертеже) и установленное оборудование (тот насос, который сейчас работает). С этим всем нужно работать: три системы учёта одного и того же насоса. Нужно, чтобы учёт не развалился, ибо насосов пара десятков тысяч, всё время что-то ломается, а вот ещё технари удумали один мощный насос двумя маломощными заменить — и нужно как-то и это отразить. Какую конструкцию из каких типов нужно для этого предложить, и почему?
При этом Вы написали "три системы учёта" - это три отдельных программы? Мы хотим придумать систему типов, выходящую за пределы одной программы?
AL
Интересный вопрос. Начинает проясняться, где собака зарыта.
А можете сразу сказать в каких местах вылазят косяки и какие при "типичном" моделировании как делают сейчас?
А можете сразу сказать в каких местах вылазят косяки и какие при "типичном" моделировании как делают сейчас?
Вот вся книжка BORO как раз про то, где и какие вылезают косяки при ООП и реляционном/табличном моделировании. И предлагает решение.
Дальше кривизна начинается в тот момент, когда это решение перекладывают в логику первого порядка и реализуют триплами. Об этом хорошо пишет Валерий Крылов, он давал пояснения в чате зависимых типов. Повторю одну из его записей 2012 года: https://justy-tylor.livejournal.com/171175.html
Дальше кривизна начинается в тот момент, когда это решение перекладывают в логику первого порядка и реализуют триплами. Об этом хорошо пишет Валерий Крылов, он давал пояснения в чате зависимых типов. Повторю одну из его записей 2012 года: https://justy-tylor.livejournal.com/171175.html
AL
При этом Вы написали "три системы учёта" - это три отдельных программы? Мы хотим придумать систему типов, выходящую за пределы одной программы?
Бинго! Это и есть "программирование в большом" )))
MG
При этом Вы написали "три системы учёта" - это три отдельных программы? Мы хотим придумать систему типов, выходящую за пределы одной программы?
Да. А то внутри программ линейные типы на зависимых ездят и всё красиво, а как граница процесса пересекается - так JSON или реляционка.
AL
@GabrielFallen Пару типичных косяков я привёл выше: забывают про время и про то, что физические объекты меняют свои роли.
Более мелко нужно говорить: отдельно объекты (которые существуют в физическом мире под разными именами и играют разные роли), отдельно роли, отдельно имена объектов и их ролей.
Про именование в этом чудесном мире тоже есть литература. Например, вот.
Про именование в этом чудесном мире тоже есть литература. Например, вот.
AG
ну, мы вроде говорили уже, для распределенных систем вам нужны сессионные типы, то есть все та же кодата и линейщина
AL
Да. А то внутри программ линейные типы на зависимых ездят и всё красиво, а как граница процесса пересекается - так JSON или реляционка.
Вот! И очень много людей, у которых это абсолютно актуальная головная боль, и переход от XML к JSON является просто головокружительным улучшением! )))
AG
если хотите моделировать локальность, то и модальные типы
AG
а там и до пучков рукой подать :D
MG
Сессионные типы - это про протоколы коммуникации? А про общую модель данных что-нибудь есть?
NI
смахивает на сеть петри
Ну вот сети Петри, наверное, можно отнести к той линейщине, о которой я говорю.
Всё же, с ними работать сильно попроще, чем с биграфами.
Всё же, с ними работать сильно попроще, чем с биграфами.
MG
@clayrat Пучки как по-английски?
AL
если хотите моделировать локальность, то и модальные типы
Я вот сильно напрягаюсь при этом. Ибо "модальность" пришла как раз от онтологов, но в последнее время онтологи склоняются к тому, чтобы заменить модальности "просто типами" — классифицировать высказывания об объектах типами этих высказываний, не прибегая к понятию модальности. И нужно отдельно разбираться, что там такое с "модальностью" происходит в последнее время.
MG
Я очень по верхам пробежался, и мне кажется, что sheaves и session types - это про то, как писать софт, а не про то, как моделировать мир. Я неправ?
AL
а там и до пучков рукой подать :D
Лучше бы подать куда-нибудь поближе к тому, как эти пучки прилепить к выражению в языке программирования смены насоса, когда есть программа учёта чертежей (PLM), программа учёта закупок (ERP) и программа эксплуатационного учёта (EAM). И как эти пучки использовать для того, чтобы учёт при замене насоса слесарем Васей не развалился. Если пучки для этого не помогают, то к чёрту пучки.