"если описывать X-в-жизни, то это моделируется удобно Y-из-теории" — тут это обзывают онтологическим рассуждением и немедленно объявляют оффтопом )))
Но я ровно вот про такие рассуждения спрашивал несколько дней назад (вопрос был "есть ли какие-то исследования, обобщающие и раскрывающие понятие "удобно" в моделировании X-из-жизни понятиями Y-из-теории?").
Молчу-молчу )))

Да это просто разговор сейчас был не о зависимых, а о других типах

О недозависимых ;-)

Так мои вопросы были про все типы и бестипья. Заодно и выяснилось бы, как часто зависимые типы имеют конкурентное преимущество в ответе на подобные вопросы — если чуток доопределить (даже не формализовывать) это понятие "удобно моделировать" для уменьшения количества споров, то потом просто или наслаждаться, что в ответ на каждый такой вопрос удобней оказываются зависимые типы, или печалиться, что они для всего оказываются неудобны кроме специально придумываемых искусственных ситуаций "не-из-жизни".

Зависимые типы имеют преимущество почти всегда.
Поскольку, хоть и не всегда удаётся придумать, как удобно описать ими что-то, но вообще описать можно ну почти всегда.
С гомотопическими типами с унивалентностью ещё круче —
это уже нехилая претензия на новые основания математики.

Внезапно, забивать гвозди можно не только молотком

В этом-то и штука, что машина Тьюринга теоретически описывает всё, только пользоваться ей невозможно. Поэтому то, что зависимые типы всемогущи, если не рассматривать понятие "удобство моделирования", меня сильно смущает.

Я поэтому и зацепился за слово "удобно".

Новые основания математики это очень хорошо. Но если забивать гвозди можно не только молотком, но и микроскопами, камнями и всем подряд менее удобным, то может всё-таки лучше забивать молотком?

Так что я свой тезис про "удобство моделирования" оставляю.

А если микроскопом удобнее, чем отдельно взятым молотком?

В каком-то смысле, тут можно сделать ассоциацию удобство—идиоматичность.
Про гомотопические типы, можно сказать, что ну вот это математика. И если в математике что-то можно описать, то и там тоже.
Что-то описывается удобнее, есть разрешимая проверка типов, возможен и достаточно развитый (но неразрешимый!) вывод типов.

Тогда это очень интересно! Осталось понять, что такое "удобнее". Например, машина Тьюринга была удобней для доказательства универсальности вычислений. Но для самих вычислений неудобна. Так что я бы всё-таки уточнял про "удобнее" — что имеется ввиду.

Про бизнес-процессы и около, вспоминается пи-исчисление и около, которое эволюционировало, в конце концов, в биграфовые модели.
Там многое вполне так идиоматично для "процессов", только с доказательствами всё очень туго, почти никак, я бы сказал.
Линейщина претендует на то, чтоб сделать такое же, но с доказательствами и всеми удобствами современных зависимых типов. Но пока не придумали полностью, только по кускам.

Про зависимые то же самое можно сказать. Как показывает ковыряние в литературе конструктивных вычислимых логик, как минимум, 5 видов: множества, типы зависимые и гомотопические, реализуемость и illative комбинаторы. И каждая даёт осмысленный фрагмент математикм. Эх... Блин. Как бы заставить чиновников переписать программы курсов по матлогике...

С "просто" зависимыми, проблема начинается вот прям с вещественных чисел.
Что-то сделать можно, но всё это будет слишком более другой математикой, чем "классическая".

Описание организационных процессов (какой там "бизнес"! Слёзы одни при описании "процесса уборки помещения") меня в последнюю очередь интересует. Ибо все эти пошаговые процедуры в жизни не выполняются обычно. Можно поговорить про то, как это всё описывается, но в современном производстве или у тебя завод-автомат  и там "обычное программирование из айти", или какая-нибудь больница, где привозят пациента, и каждый следующий шаг в лечении решает консилиум, никакого предварительного описания процесса, всё "полный agile", тьфу, case management. И биграфовые модели со всякими BPMN теперь популярны только в очень узком кругу самых далёких от жизни программистов. И не работают. А работают как раз описания объектов из domain, над которыми on the fly определяются разные операции без предварительного их планирования, динамически.

А вот про "удобство зависимых типов" как идиоматичность — вот непонятно мне это. Интуитивно понятно, что "зависимость типа" это как раз вот это позволение что-то делать "на лету", и это вполне то, что нужно.

Но когда оказывается, что это удобство-1 описания математики, а потом берите математику и с удобством-2 описывайте мир, я опять напрягаюсь.

> "зависимость типа" это как раз вот это позволение что-то делать "на лету"

Скорее, с точностью до наоборот: зав. типы - про статические проверки, т.е. на "этапе компиляции", до "на лету".

> И биграфовые модели со всякими BPMN
> теперь популярны только в очень узком кругу
> самых далёких от жизни программистов.
> И не работают.
Я чуток имел с подобным дело (только тогда не знал, что такое биграфы) и не совсем согласен.
Полностью детализованно пытаться что-то прописывать, это ерунда, конечно.
Но до какого-то уровня, нутипааа "Plan-Do-Check-Act", описать можно. И даже дальше.
Очевидно, что чем точнее описание, тем больше ограничений (которые никто исполнять не будет).

Фишка в том, что первый раз дело делается с планированием на лету каждого шага, и журналируется ручное выполнение. А второй раз — это выполняется обычно чуток модифицированный шаблон первого выполнения. Сами же эти "дела" (cases) состоят из других дел. В основе описания же — практики, ассоциируемые не с шагами процесса, а с domain. Можно считать так, что они все задаются декларативно (есть предусловия и постусловия, и задействуются практики при выполнении предусловий, когда бы они ни возникли). То есть есть практика "если поцарапалось — закрась. И обычно наблюдай, поцарапалось ли". И нет явно прописанного процесса, где это было бы шагом. Но в жизни люди начинают замечать, что где-то поцарапалось — и закрашивают. Но это вообще уже оффтоп к дискуссии о типах в языках программирования, но не о типах в моделировании.

В архитектурных языках архитектуры предприятия (типа ArchiMate) есть два элемента: один "процесс" для императивного процесса из шагов, а другой "функция" для вот такой вот "практики". Это всё описано у меня в учебнике "Системное мышление" — https://yadi.sk/i/aaZBihiJhw6i8w

Если считать, что языки программирования, моделирования, онтологизирования это одно (а я так считаю), то это тогда валидная дискуссия для группы. Если считать, что это всё разные языки (например, язык программирования исполняется фон-неймановским процессором, архитектурный язык головой человека, онтологический язык логическим процессором — что для меня смешные различия), то тогда тут такое обсуждение оффтоп.

> есть предусловия и постусловия
Чтоб с этим нормально работать, хорошие типы уже нужны ;-)
Хотя и если просто описать операционно, конечно, требований к типам гораздо меньше.

Вот смотрите, как различаются описания Idris и Julia в их сравнении: https://www.slant.co/versus/133/5275/~julia_vs_idris

У Idris как раз  "Pro
Domain driven design and type driven development

Because of full dependent types in Idris, the programmer can focus more on modelling the domain with types and waste less time fixing common bugs that the type checker will catch. Dependent types help apply type driven development and a lot of code auto generation, making the compiler and type checker an ally in developing working software instead of just getting in the way" — это ровно то, зачем я пришёл в чатик по зависимым типам. Ибо я считал (зря считал), что подобные вопросы в сообществе любителей Idris не оффтоп.

В Julia "Pro
Strong dynamic typing

Dynamic and high level, but does not isolate the user from properly thinking about types. Can do explicit type signatures which is great for teaching structured thinking" — ничего про лёгкость domain driven design мы не слышим. Хотя это по факту не так, ибо там очень хорошая работа с пакетами — ты добавляешь описания мира с разных сторон, не перекомпилируя каждый раз всё заново вместе с библиотеками.

два очень разных языка