M>По ссылке не вижу ничего подобного. Более того, я вижу там банальное if typeof(Object) == что-то там Только присыпанное синтаксическим сахаром

void printIfPrintable(Object obj) {
    if (is Printable obj) {
        obj.printObject();
    }
}

void Func1(MyObj obj)
{
  if (obj.Prop == 3 && ....  // тут много проверок
    Use(obj);
}

void Func2(MyObj obj)
{
  if (obj.Prop == 3 && obj.Prop2 == 4 && ....  // тут те же проверки, и еще пара других
    Use(obj);
}

MyObj obj = GetMyObj();
Func1(obj);
Func2(obj);


// предлагаемый вариант (псевдокод)

type MyCoolObj = MyObj where obj.Prop == 3 && ...   // тут все проверки

void Func1(MyCoolObj obj)
{
  Use(obj);  // проверок нет
}

void Func2(MyCoolObj obj)
{
  if (obj.Prop2 == 4 && ....  // тут только пара "лишних" проверок
    Use(obj);
}

MyObj obj = GetMyObj();
if (obj is MyCoolObj)    // все проверки в типе, тут ничего нет
{
  Func1(obj);
  Func2(obj);
}

В этих обстоятельствах одна и та же ошибка может быть проверена и с помощью утверждения, и обработчиком ошибок. Так, в исходном коде Microsoft Word условия, которые должны быть истинными, сперва помещаются в утверждения, а затем и в коде обработки ошибок рассматривается ситуация, когда утверждение ложно. В столь сложных и долгоживущих приложениях, как Word, утверждения служат для выявления как можно большего числа ошибок периода разработки. Но поскольку приложение очень сложное (миллионы строк кода) и прошло через столько изменений, неразумно ожидать обнаружения и исправления всех мыслимых ошибок до начала поставки приложения пользователям. Поэтому ошибки должны обрабатываться и в промышленной версии системы.

M>Которая на практике выстреливает раз в год Не говоря уже о том, что всю эту логику, навороченную в типе еще тоже надо проверить каким-то образом.

M>Тогда нафига козе баян? Ну и как это? Меня тут активно пытались убедить, что все прекрасно, и чуть ли ен все можно в типы запихнуть

M>public Order[*] read_order_from_db(OrderId id);

M>// каким образом тут компилятор проверит, что за Order сюда идет?
M>// заказ же из базы читается
M>change_order_amount(Order, Amount)
M>

read_order_from_db :: OrderId -> Either NewOrder ProcessedOrder

A>read_order_from_db :: OrderId -> Either NewOrder ProcessedOrder
A>

Только вот незадача-то. Объект у нас одного типа — заказ.

И дальше над ним может идти очень длинная последовательность действий. Где в одном действии ему надо быть уже отосланным, в другом — неотосланным, в пятом — отосланным, но неоплаченным, в десятом — просто не иметь статуса "fraud". Как предлагаешь поступать? Писать стопятьсот типов на каждый чих и комбинацию, а потом стопятьсот if'ов, инициализаторов и кастований из одного в другое?

updateOrder :: Int -> Order -> Maybe Done
updateOrder amount = check1 amount >=> check2 >=> update >=> writeOrder

check1 :: Int -> Order -> Maybe Checked1
check2 :: Checked1 -> Maybe Checked2
update :: Checked2 -> Maybe Updated
writeOrder :: Updated -> Maybe Done

M>Да не показано нигде. Идут сплошные сказки и рассказы про то, как все будет зашибись, и я в это должен верить Как магическая система типов все сома отловит, как невозможно будет написать неправильный код и т.п.