Но это же не связано с изначальным утверждением, что язык

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

Или я не понимаю вашу логику?

Не могу сказать связано или не связано, зато точно могу ответить что "язык с ограничениями в виде той же системы типов обязательно не позволяет выразить какие-то вполне корректные программы, выразимые, не будь этих ограничений". Это свойство называется "полнота" (aka completeness). Если система типов (или любая другая система ограничений) полна, это значит, что можно написать все корректные программы. Среди динамических (runtime) систем ограничений/проверок/мониторов встречаются полные, среди статических — нет. Во всяком случае таких чтобы sound and complete не встречается. Зато среди SAST-систем подавляющее большинство (все промышленные, КМК) — и unsound, и incomplete.

А можно пример "полной динамической системы"? Насколько я понимаю, даже типичный ассемблер не полный.

Я имел в виду "динамические мониторы", которые в рантайме следят. В известном смысле, таким монитором можно считать ОС, и она полна в некотором смысле. Помнится, бывают мониторы, полные по отношению к некоторому классу ошибок многопоточности.

> Если система типов (или любая другая система ограничений) полна, это значит, что можно написать все корректные программы. Не понял: корректные программы с какой точки зрения? А если не полна?

С той самой, которую Вы читали у Пирса: https://t.me/symboliclogic/7354 Грубо говоря, не зацикливаются, не бросают исключений, не выполняют "недопустимых операций". А если не полна, то забракует часть корректных программ.

То есть не полная система может забраковать программы, даже те которые удовлетворяют ограничениям которые накладываются этой системой?

Нет. Ограничения (синтаксические) накладываются системой типов или ещё чем. А корректность определяется runtime поведением программы. Очевидно, что система ограничений пропускает все программы, которые удовлетворяют её ограничениям. Но это ничего не говорит (само по себе) про корректность runtime-поведения этих программ. Про связь с корректностью говорят теоремы soundness and completeness.

Те, которые удовлетворяют, она забраковать не может, по определению. Может она корректные программы, которые не удовлетворяют.

Вот не понятно: как программы могут быть корректными если они не удовлетворяют ограничениям. Опять таки, корректные с какой точки зрения? Блин, я чего-то недопонимаю, но не могу понять что именно🤪

Функции g f = (f 1, f "foo") невозможно приписать тип в рамках Rank1 системы. Но возможно в хаскелле со всключённым RankNTypes g :: (forall x. x -> x) -> (Int, String) g f = (f 1, f "foo") где forall n . type - это аналог генерика. Rank1 разрешает генерик-аргументам объявляться только для всей функции разом, а RankN - для любой части её сигнатуры. Например, g :: forall x. (x -> x) -> (Int, String) g f = (f 1, f "foo") не скомпилируется, потому что тайпчекер будучи внутри forall x заменит x -> x на x0 -> x0, т.е., освежит переменную типа и не сможет найти решение, так как x0 ~ Int, x0 ~ String. В варианте с внутренним forall тайпчерек заменит x два раза: x -> x -> x0 -> x0 и x -> x -> x1 -> x1 и будет удовлетворён набором констрейнтов x0 ~ Int, x1 ~ String.

Сильно!

Ну вы нормы ГТО удовлетворяете? А полезным человеком являетесь.

> Пирс написал, что корректные программы (в лямбда-исчислении) — это те, которые редуцируются в значения. Вот после этой фразы у меня почти сложилась картинка. Напоследок, маленький вопрос: "Недопустимые операции" это например какие?

В лямбда-исчислении это все те, для которых нет правил редукции. "В жизни" — всё то самое, что вызывает "системную ошибку" или "необрабатываемое исключение": division by zero, null pointer dereference, out-of-bounds access и далее по списку.

Во! Спасибо😊

Дежурное напоминание, что зацикливание (бесконечное) сюда тоже относится (строго говоря).

мне кажется, это скорее про бесконечные циклы

И про них тоже: https://t.me/CompilerDev/94569

Ну вообще, скорее нет, обычно все таки разделяют safety и liveness свойства, бесконечные циклы это про liveness как раз

Смотря где разделяют. В другом месте разделяют partial correctness и total correctness примерно по той же линии. Но мое мнение -- что "по честному" зацикливание тоже нужно считать за проблему. По крайней мере там, где зацикливание не было преднамеренным. А это на практике -- везде, потому что нужен аккуратный shutdown всего по пинку.

Нет, посылкой WM_EXIT или какого-то подобного сообщения, по которому этот бесконечный цикл заканчивается.

> бесконечный цикл > заканчивается Ну, что и требовалось доказать. 😂

Это вы про то, что в подлунном мире всё преходяще?