ARK>Рассматриваю для простоты только первые две строчки.

Действительно. Дальше же работа с конфигурацией идет, там уже все не так весело


ARK>Псевдокод:

ARK>

ARK>  type SentOrder is Order where Sent = true;
ARK>  type UnsentOrder is Order where Sent = false;

ARK>  function ChangeOrderSum(order: UnsentOrder, newSum: Money): UnsentOrder is    // эту функцию нельзя вызвать для заказа, у которого Sent равно true!
ARK>    ...
ARK>  end;

Чем это принципиально отличается от API с такими же условиями?

ARK>  var order := CreateOrder(1, 12000.00);
ARK>  order := ChangeOrderSum(order, 2800.23);
ARK>  order := SendOrder(order);
ARK>//  order := ChangeOrderSum(order, 5555.00);    // error
ARK>  PrintOrderDetails(order);    // OK

ARK>

Да-да. Error. Потому что в реальности все так и происходит, ага-ага

В реальности происходит так:

Order = read_order_from_db(OrderId),
checnge_order_amount(Order, Amount).

Ой. Внезапно на этапе компиляции мы даже не знаем, будет заказ отправелнным или неотправленным. Какая печаль!


ARK>Таким образом, тут мы "закодировали в типах" требование "Пока заказ не помечен, как отправленный, можно уменьшать и увеличивать сумму заказа". Компилятор запрещает нарушать его.

Вау. Ага. Так как мне поможет компилятор в тех двух строчках кода, что я привел?

ARK>Могли ли мы ошибиться при реализации этого требования? Могли.

Я об этом (среди прочего) и говорю уже пятнадцать сообщения подряд Нет, «магический тайпчекер все проверит»

ARK>Но все равно существует вероятность обнаружения ошибки компилятором, есть шанс, что где-то какие-то типы "не срастутся".

«Есть вероятность», «есть шанс»... Это не аргументы — это вера.

ARK>В данном случае, чтобы компилятор ничего не заподозрил, нам пришлось бы ошибиться сразу в двух сигнатурах функций (в SendOrder+ChangeOrderSum, или в ChangeOrderSum+PrintOrderDetails). Но, конечно, какая-то "отладка типов" тоже нужна, да.

Какая? Я уже пятнадцать раз спросил, как, реализовав логику на типах, люди собираются ее проверять?

ARK>Рассматриваю для простоты только первые две строчки.

Действительно. Дальше же работа с конфигурацией идет, там уже все не так весело


ARK>Псевдокод:

ARK>

ARK>  type SentOrder is Order where Sent = true;
ARK>  type UnsentOrder is Order where Sent = false;

ARK>  function ChangeOrderSum(order: UnsentOrder, newSum: Money): UnsentOrder is    // эту функцию нельзя вызвать для заказа, у которого Sent равно true!
ARK>    ...
ARK>  end;

Чем это принципиально отличается от API с такими же условиями?

ARK>  var order := CreateOrder(1, 12000.00);
ARK>  order := ChangeOrderSum(order, 2800.23);
ARK>  order := SendOrder(order);
ARK>//  order := ChangeOrderSum(order, 5555.00);    // error
ARK>  PrintOrderDetails(order);    // OK

ARK>

Да-да. Error. Потому что в реальности все так и происходит, ага-ага

В реальности происходит так:

Order = read_order_from_db(OrderId),
change_order_amount(Order, Amount).

Ой. Внезапно на этапе компиляции мы даже не знаем, будет заказ отправелнным или неотправленным. Какая печаль!


ARK>Таким образом, тут мы "закодировали в типах" требование "Пока заказ не помечен, как отправленный, можно уменьшать и увеличивать сумму заказа". Компилятор запрещает нарушать его.

Вау. Ага. Так как мне поможет компилятор в тех двух строчках кода, что я привел?

ARK>Могли ли мы ошибиться при реализации этого требования? Могли.

Я об этом (среди прочего) и говорю уже пятнадцать сообщения подряд Нет, «магический тайпчекер все проверит»

ARK>Но все равно существует вероятность обнаружения ошибки компилятором, есть шанс, что где-то какие-то типы "не срастутся".

«Есть вероятность», «есть шанс»... Это не аргументы — это вера.

ARK>В данном случае, чтобы компилятор ничего не заподозрил, нам пришлось бы ошибиться сразу в двух сигнатурах функций (в SendOrder+ChangeOrderSum, или в ChangeOrderSum+PrintOrderDetails). Но, конечно, какая-то "отладка типов" тоже нужна, да.

Какая? Я уже пятнадцать раз спросил, как, реализовав логику на типах, люди собираются ее проверять?