Здравствуйте, genre, Вы писали:
G>Это все как-бы да. Я там выше с подобного примера и начал. Но как только я начинаю пытаться представлять как это все будет работать при воркфлоу сложнее линейного, а особенно если есть циклы, то сам выпадаю по StackOverflow.
Как я понимаю, весь смысл статической проверки — в том, чтобы получить некоторые гарантии. Т.е. мы отлавливаем заведомые противоречия в программе. И весь вопрос — в том, какие противоречия мы хотим отловить.
Классический пример — сложение строк с числами. Или секунд с килограммами. Или параметров с sql стейтментом.
Чтобы противоречие вообще обнаружилось, нам нужно хотя бы два несогласующихся "утверждения".
Т.е. вот мы в строке 1 предполагаем, что а — это строка, в строке 1111 умножаем а на 3.1415926, как будто это real.
Такие вещи компилятор нам поможет отловить.
Но если мы это a используем строго один раз — то ему нечему противоречить. Ну, вот если мы использовали 3.1415926 ровно один раз, то мы запросто можем в нём опечататься, и никакой компилятор нам не поможет. Он поможет если мы Pi используем 100500 раз — тогда мы можем заменить 100500 вхождений константы 3.1415926 на идентификатор Pi, и будем иметь гарантию хотя бы того, что во всей программе значение Pi одно и то же. Опечатки в названии идентификатора компилятор нам отловит.

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

Здравствуйте, Sinclair, Вы писали:

S>Именно поэтому компилятор вряд ли поможет отловить ошибки в бизнес-логике. Там основные ошибки — это противоречие программы и спецификации, и противоречие спецификации и того, чего хотел бизнес.

О чем и речь.

Здравствуйте, Sinclair, Вы писали:

S>Как я понимаю, весь смысл статической проверки — в том, чтобы получить некоторые гарантии. Т.е. мы отлавливаем заведомые противоречия в программе. И весь вопрос — в том, какие противоречия мы хотим отловить.

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

Здравствуйте, genre, Вы писали:
G>Ну как раз обсуждение о том, насколько много ошибок можно отловить с помощью продвинутой статической типизации. Вроде как и много, даже логику на типах можно, но насколько реально это применимо в больших системах так и непонятно.
Ещё раз подчеркну: саму по себе логику на типах реализовывать малоинтересно. Просто потому, что это не даст преимуществ. Нет ничего ракетного в реализации компайл-тайм целочисленной арифметики на шаблонах С++, но она никак не поможет исправить ошибку в самой формуле. Она не будет лучше банального int a = 2*2-3.
Интересно ловить какие-нибудь "свойства" этой логики. Например, соответствие размерностей в инженерных вычислениях.
Или, например, отсутствие JS и SQL injections в коде странички.
Тут — то же самое: есть одно правило типа "нельзя склеивать экранированные строки с неэкранированными", и очень много операций склейки, которые должны этому правилу удовлетворять.
Вот тут поддержка компилятора — самое то.

Здравствуйте, Mamut, Вы писали:

M>Охо-хо. Логическая ошибка — это когда ты считаешь пеню в размере 50% от стоимости товара, а не 0.5%.
Ок. А есть формальный критерий определения того, что эта пеня — ошибочная?
Компилятору не может "не нравиться А". Он может только сравнивать А и Б.
У вас в примере есть только А.
Т.е. либо у нас есть более жёсткое правило, типа "пеня не может быть больше 5%", которое меняется гораздо реже чем правило типа "размер пени с 01.01.2011 равен 0.5%", либо есть ещё какой-то критерий проверки значения пени на корректность.

M>Логическая ошибка — это когда позволяешь поднимать сумму в заказе выше определенной суммы, забыв проверить одно из условий.
Если подъём суммы в заказе происходит в N местах, то статическая проверка может, к примеру, убедиться, что все условия всегда применены.
А если подъем суммы происходит ровно в 1 месте, то ни статика, ни динамика никак не помогут ничего проверить.
Собственно, тестирование — это и есть дописывание A' к тем А, для которых нету Б для сравнения.

M>Да-да. Замени синус на товар
А чем плохо? Можно очень много вещей провалидировать статически. Например, что ордер, отданный в процессинг — непустой (есть хотя бы один line item).
Если в вашей системе есть куча мест, где из ордера по разным правилам изымаются позиции (сплит по поставщикам/складам; выбрасывание позиций, отсутствующих на складе на момент отправки, етк), то такая банальщина поможет предотвратить "array index out of bounds" где-то в недрах этого спагетти.

M>>Охо-хо. Логическая ошибка — это когда ты считаешь пеню в размере 50% от стоимости товара, а не 0.5%.
S>Ок. А есть формальный критерий определения того, что эта пеня — ошибочная?

Есть: бизнес-задача.

Или, если процитировать презентацию банка:

Often working from verbal, ad hoc evolving spec. And at best from informal functional specs....
[types..] Make wrong code impossible to write

А бизнес-задача реально приходит в виде тикета, в котором написано что-то типа: «согласно изменению наших правил/законов/левой задней пятки мы должны установить пеню за просроченные более, чем на 30 дней, оплаты пеню в размере не больше 5% от оригинальной стоимости заказа».

После чего хорошо если этот тикет кто-то заметит и начнет задавать доп. вопросы: а что делать, если заказ проведен в системе X (они обрабатываются оп-другому), а что если заказ оплачен частично, а что если заказ отправлен частями, а что если заказ находится в одном из статусов. Или прекрасное: а что, если между первой оплатой и «просроченной» человек стал protected person (политики, люди, находящиеся в программе защиты свидетелей и т.п.). То есть мы не знаем его адреса и не можем выслать ему предупреждение и т.п.

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

S>Компилятору не может "не нравиться А". Он может только сравнивать А и Б.
S>У вас в примере есть только А.
S>Т.е. либо у нас есть более жёсткое правило, типа "пеня не может быть больше 5%", которое меняется гораздо реже чем правило типа "размер пени с 01.01.2011 равен 0.5%", либо есть ещё какой-то критерий проверки значения пени на корректность.

Нет, у нас есть правило «пеня не может быть больше 5%» Иногда (как описал выше) есть доп. условия, но в реальности оно выглядит примерно так: http://rsdn.ru/forum/philosophy/5946213.1

Автор: Mamut
Дата: 06.02.15

(это восстановлено по коду, потому что этого описания нет в одном месте).

M>>Логическая ошибка — это когда позволяешь поднимать сумму в заказе выше определенной суммы, забыв проверить одно из условий.
S>Если подъём суммы в заказе происходит в N местах, то статическая проверка может, к примеру, убедиться, что все условия всегда применены.
S>А если подъем суммы происходит ровно в 1 месте, то ни статика, ни динамика никак не помогут ничего проверить.
S>Собственно, тестирование — это и есть дописывание A' к тем А, для которых нету Б для сравнения.

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

M>>Да-да. Замени синус на товар
S>А чем плохо? Можно очень много вещей провалидировать статически. Например, что ордер, отданный в процессинг — непустой (есть хотя бы один line item).
S>Если в вашей системе есть куча мест, где из ордера по разным правилам изымаются позиции (сплит по поставщикам/складам; выбрасывание позиций, отсутствующих на складе на момент отправки, етк), то такая банальщина поможет предотвратить "array index out of bounds" где-то в недрах этого спагетти.

Куча мест есть, но они упакованы в один API в модуле Goods Максимум, что туда передается, это заказ и новые/изменяемые товары У нас на удивление мало случаев, когда какие-то проверки на какие-то условия копипастой раскиданы по ста местам. Обычно есть некий API, куда передается объект и проверки делаются там.

Ой. Кстати. Только сегодня пришел баг с прекрасным примером именно логической ошибки.

Когда мы отправляем физическое письмо с информацией про товар, мы выставляем счет за отсылку этого письма продавцу. Если это письмо повторно отсылается нашей тех. поддержкой из нашего внутреннего CRM, то этот счет не выставляется. Появился REST API, который позволяет это сделать из новой CRM, которая сейчас пилится. ВНЕЗАПНО оказалось, что вызов REST API выставляет счет за письма, хотя не должен.

А все просто

%% используемый по всей системе код
order_communication:send_invoice() ->
   ....
   FactoringFees = config:read(Merchant, factoring_fees),
   Inv = invoice:set_factoring_fee(OriginalInvoice, FactoringFees),
   invoice_send:send(Inv).


%% код на странице CRM'а
order_show_yaws:send_mail(SiteState) ->
  ...
  Inv = case is_customer_support(SiteState) of
           true -> OriginalInvoice;
           false ->
             FactoringFees = config:read(Merchant, factoring_fees),
             invoice:set_factoring_fee(Invoice, FactoringFees),
        end,
  invoice_send:send(Inv).

%% код в новом вызове REST API
restapi_order_mail:call() ->
  ...
  order_communication:send_invoice(Inv).

Тут не спасет ничего, кроме живительного осинового кола, направленного далеко не в сердце. Самое страшное, что этот первые два куска кода были написаны гуру Эрланга, имена которых выбиты в скрижалях по всему Эрлангу (его библиотекам, документации и т.п.)

Здравствуйте, Sinclair, Вы писали:

S>Ещё раз подчеркну: саму по себе логику на типах реализовывать малоинтересно. Просто потому, что это не даст преимуществ. Нет ничего ракетного в реализации компайл-тайм целочисленной арифметики на шаблонах С++, но она никак не поможет исправить ошибку в самой формуле. Она не будет лучше банального int a = 2*2-3.

Какая-то странная постановка вопроса. Кодируя целочисленную арифметику в типах мы получаем возможность проверить свойства целочисленной арифметики.

Допустим, мы закодировали целые числа как типы Z и S (n :: Nat) и кайнд Nat:

data Nat = Z | S Nat

У нас есть библиотека (singletons), которая нагенерит нам для этих типов всякого бойлерплейта, и библиотеки со всякими утилитами, которые понадобится для дальнейших "доказательств" (насколько вообще можно говорить о доказательствах в языке без проверки тотальности).
так же мы можем в типах и арифметику закодировать:

singletons [d|
 (+) :: Nat -> Nat -> Nat
 Z   + n = n
 S m + n = S (m + n)

 (-) :: Nat -> Nat -> Nat
 n   - Z   = n
 S n - S m = n - m
 Z   - S _ = Z

 (*) :: Nat -> Nat -> Nat
 Z   * _ = Z
 S n * m = n * m + m
 |]

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

plusZL :: SNat n -> Z :+: n :=: n -- то, что мы доказываем 0 + n = n
plusZL _ = Refl -- компилятор конструирует доказательство сам (думаю, понятно почему)

В других случаях доказательство придется конструировать вручную. Ассоциативность, например:

plusAssociative :: SNat n -> SNat m -> SNat l
                -> n :+: (m :+: l) :=: (n :+: m) :+: l
plusAssociative SZ     _ _ = Refl
plusAssociative (SS n) m l =
  start (sS n %+ (m %+ l))
    =~= sS (n %+ (m %+ l))
    === sS ((n %+ m) %+ l)  `because` cong' sS (plusAssociative n m l)
    =~= sS (n %+ m) %+ l
    =~= (sS n %+ m) %+ l

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

Здравствуйте, Klapaucius, Вы писали:

K>Какая-то странная постановка вопроса. Кодируя целочисленную арифметику в типах мы получаем возможность проверить свойства целочисленной арифметики.
К счастью, обычно свойства целочисленной арифметики входят в поставку компилятора, и шансов поломать их неожиданной программой у нас мало.
Вот, допустим, перед вами поставили задачу "решить квадратное уравнение".
То есть на входе — коэффициенты a, b, c, на выходе — все корни уравнения.

Максимум, который сможет нам дать тайпчекер — предотвратить попытку извлечения квадратного корня из отрицательного детерминанта.
А вот, скажем, то, что вместо 4 я опечатаюсь и напишу 3, никакой тайпчекер не отловит. Или я ошибаюсь?

Здравствуйте, Sinclair, Вы писали:

S>Максимум, который сможет нам дать тайпчекер — предотвратить попытку извлечения квадратного корня из отрицательного детерминанта.
S>А вот, скажем, то, что вместо 4 я опечатаюсь и напишу 3, никакой тайпчекер не отловит. Или я ошибаюсь?

По идее, мы можем в типе функии указать "возвращает такое число х, что х*х = input", тогда при ошибке в формуле код не скомпилируется. Только вот с вещественными числами так работать дело гиблое, в задачах с целыми оно реальнее.

Например, функция поиска подстроки на ATS у меня такой тип имела:

fn search {n,m:nat | m <= n}
  (str : string n, sub : string m) : [p:int | p <= n - m] int p

Т.е. "возвращает такое целое p, что оно не больше n — m, где n и m это длины переданных строк".

Здравствуйте, Sinclair, Вы писали:

S>К счастью, обычно свойства целочисленной арифметики входят в поставку компилятора

Вернее, в поставку компилятора входит реализация целочисленной арифметики (обычно кольца вычетов, конечно), для которой эти свойства выполняются.

S>и шансов поломать их неожиданной программой у нас мало.

Ну так в моем посте буквально это и написано + плюс ответ на возражение, хотя возможно и недостаточно развернутый:

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

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

S>Вот, допустим, перед вами поставили задачу "решить квадратное уравнение".
S>То есть на входе — коэффициенты a, b, c, на выходе — все корни уравнения.

S>Максимум, который сможет нам дать тайпчекер — предотвратить попытку извлечения квадратного корня из отрицательного детерминанта.
S>А вот, скажем, то, что вместо 4 я опечатаюсь и напишу 3, никакой тайпчекер не отловит. Или я ошибаюсь?

Какие пред или пост условия заданы для функции — то и проверит.
Т.е. разница между этими вашими примерами не столько возможностями тайпчекера определяется, сколько вашей способностью сформулировать проверяемые свойства. Для функции, которая из a b и дискриминанта вычисляет корни уравнения, вы сформулировали условие D >= 0. Значит есть что проверять. А если вы условия не формулируете — то тут и проверять нечего, хоть тайпчекером, хоть тестами, с той поправкой, что какие-то условия могут быть выведены без всякого указания. Т.е. есть всякие средства получения таких условий без вашей помощи вроде систем вывода типов, в том числе и refinement типов (на подобии {p:int | p <= n — m} из соседнего поста) вроде liquid types. Есть еще всякие системы эвристического поиска свойств для некоего набора функций. Так вот, эти средства получения условий для проверки автоматически — действительно ограничены и далеко без помощи человека не уходят. В полуавтоматическом же режиме, т.е. с помощью человека как при формулировании условий, так и при доказательстве можно зайти, наоборот, очень далеко.
Другое дело, что перспективы что-то проверить, "доказать", о чем-то рассуждать и вообще сохранить рассудок в случае плавучки не радужные.

Здравствуйте, Sinclair, Вы писали:

S>Ещё раз подчеркну: саму по себе логику на типах реализовывать малоинтересно. Просто потому, что это не даст преимуществ. Нет ничего ракетного в реализации компайл-тайм целочисленной арифметики на шаблонах С++, но она никак не поможет исправить ошибку в самой формуле. Она не будет лучше банального int a = 2*2-3.

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

В примере же с ордером условная "правая часть" вычисляется в одном месте, а подаётся в условную "левую часть" в другом месте. Типы должны соответствовать друг другу.


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

Тип текущего результата вычислений тоже может обладать размерностью.
ИМХО, вряд ли у того же ордера будет более десятка размерностей.

Вот, поупражнялся:

using System;

namespace StrongTypedOrder
{
    public class Any<T> {}
    public class Not<T> : Any<T> { }

    public class Checked : Any<Checked> { }
    public class Approved : Any<Approved> { }
    public class Closed : Any<Closed> { }

    class OrderProcessor
    {
        public void SendInvoice<X>(Order<Checked, X, Not<Closed>> o) 
            where X : Any<Approved>
        {
            OrderData od = o.Data;
            Console.WriteLine("Send Address: {0}, amount: {1}", od.Address, od.Amount);
        }

        public void Execute(Order<Checked, Approved, Not<Closed>> o)
        {
            OrderData od = o.Data;
            Console.WriteLine("Execute Address: {0}, amount: {1}", od.Address, od.Amount);
        }

        public void Archive(Order<Checked, Approved, Closed> o)
        {
            OrderData od = o.Data;
            Console.WriteLine("Archive Address: {0}, amount: {1}", od.Address, od.Amount);
        }
        
        public Order<Checked, X, Not<Closed>> 
            Check<X>(Order<Not<Checked>, X, Not<Closed>> o)
            where X : Any<Approved>
        {
            return new Order<Checked, X, Not<Closed>>(o.Data);
        }

        public Order<Checked, Approved, Not<Closed>>
            Approve(Order<Checked, Not<Approved>, Not<Closed>> o)
        {
            return new Order<Checked, Approved, Not<Closed>>(o.Data);
        }

        public Order<X, Y, Closed>
            Close<X, Y>(Order<X, Y, Not<Closed>> o)
            where X : Any<Checked>
            where Y : Any<Approved>
        {
            return new Order<X, Y, Closed>(o.Data);
        }

        public Order<Not<Checked>, Not<Approved>, Not<Closed>> 
            Create()
        {
            return new Order<Not<Checked>, Not<Approved>, Not<Closed>>(new OrderData());
        }
    }

    public class OrderData
    {
        public double Amount { get; set; }
        public string Address { get; set; }
    }

    public struct Order<TChecked, TApproved, TClosed>
        where TChecked : Any<Checked>
        where TApproved : Any<Approved>
        where TClosed : Any<Closed>
    {
        internal Order(OrderData data)
            : this()
        {
            this.Data = data;
        }

        public OrderData Data { get; private set; }
    }

    class Program
    {
        static void Main(string[] args)
        {
            var p = new OrderProcessor();
            var order = p.Create();

            order.Data.Address = "XXX";
            order.Data.Amount = 42;

            // p.SendInvoice(order);        // compilation error

            var checkedOrder = p.Check(order);
            p.SendInvoice(checkedOrder);    // OK

            // p.Execute(checkedOrder);     // compilation error

            var approvedOrder = p.Approve(checkedOrder);
            p.Execute(approvedOrder);       // OK

            // p.Archive(approvedOrder);    // compilation error

            var closedOrder = p.Close(approvedOrder);
            p.Archive(closedOrder);         // OK
        }
    }
}

Здравствуйте, vdimas, Вы писали:

V>В примере же с ордером условная "правая часть" вычисляется в одном месте, а подаётся в условную "левую часть" в другом месте. Типы должны соответствовать друг другу.
Не факт.

V>Тип текущего результата вычислений тоже может обладать размерностью.
V>ИМХО, вряд ли у того же ордера будет более десятка размерностей.

V>

    class Program
V>    {
V>        static void Main(string[] args)
V>        {
V>            var p = new OrderProcessor();
V>            var order = p.Create();

V>            order.Data.Address = "XXX";
V>            order.Data.Amount = 42;

V>            // p.SendInvoice(order);        // compilation error

V>            var checkedOrder = p.Check(order);
V>            p.SendInvoice(checkedOrder);    // OK

V>            // p.Execute(checkedOrder);     // compilation error

V>            var approvedOrder = p.Approve(checkedOrder);
V>            p.Execute(approvedOrder);       // OK

V>            // p.Archive(approvedOrder);    // compilation error

V>            var closedOrder = p.Close(approvedOrder);
V>            p.Archive(closedOrder);         // OK
V>        }
V>    }
V>}
V>

И какие классы ошибок мы отловим? Отправку инвоиса по непроверенному ордеру? Ну так у нас ровно две строки кода: отправка и проверка. С тем же успехом мы можем просто забыть поставить в сигнатуре SendInvoice нужный предикат.
Такая проверка имеет смысл тогда, когда у нас есть условия, которые можно проверить многократно — например, куча путей исполнения, в которых может то встречаться, то не встречаться Check. Тогда компилятор поможет нам убедиться, что нет таких путей, которые ... и так далее.
А в реальном order flow всё скорее всего ещё неинтереснее — разные этапы этого workflow берут ордер не из параметров, а из базы, и там никаких статически верифицируемых свойств нету.

Здравствуйте, Sinclair, Вы писали:

S>И какие классы ошибок мы отловим? Отправку инвоиса по непроверенному ордеру? Ну так у нас ровно две строки кода: отправка и проверка. С тем же успехом мы можем просто забыть поставить в сигнатуре SendInvoice нужный предикат.

Можем. Тут же дело (как ты правильно ранее заметил) в масштабируемости. Если SendInvoice вызывается более, чем из одного места, то вот тебе и профит. А если взять десяток координат (а не 3), то получим пространство в 1024 комбинации. А кол-во возможных переходов (путей) — еще на многие-многие порядки больше. Комбинаторика-с. На типах же достаточно будет проверить всего столько кейзов, сколько существует БАЗОВЫХ операций над ордером, двигающих его из начального состояния во все достижимые в пространстве состояний, закодированных типами. Т.е. это будет некий "пояс безопасности", которым может оперировать уже вышестоящая логика сколь угодно высокой комбинаторной сложности, где разница статики vs динамики будет в полный рост. Например, в какой-то ветке сложного "слаботипизированного" решения по цепочке if-ов никогда не доходили до SendInvoice в тестах в одном из самых сложных алгоритмов, а потом у заказчика всё упало в боевых условиях на самой важной "сделке века".


S>Такая проверка имеет смысл тогда, когда у нас есть условия, которые можно проверить многократно — например, куча путей исполнения, в которых может то встречаться, то не встречаться Check. Тогда компилятор поможет нам убедиться, что нет таких путей, которые ... и так далее.

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


S>А в реальном order flow всё скорее всего ещё неинтереснее — разные этапы этого workflow берут ордер не из параметров, а из базы, и там никаких статически верифицируемых свойств нету.

Есть. ))

        public Order<Checked, AnyApproved, AnyClosed>
            MakeChecked<AnyApproved, AnyClosed>(Order<Not<Checked>, AnyApproved, AnyClosed> o)
            where AnyApproved : Any<Approved>
            where AnyClosed : Any<Closed>
        {
            return new Order<Checked, AnyApproved, AnyClosed>(o.Data);
        }

Разумеется, есть много техник перехода тип <=> данные и наоборот (визитор, размеченное объединение, всевозможные виды IoC, в т.ч. некоторые с громкими аббревиатурами в ФП, которые делают вид, будто они вовсе не IoC, а нечто самостоятельно существующее). ))

Но не в этом суть. Это две противоборствующие парадигмы (кодировать признак в тип или в данные?), где в реальной разработке используется некий компромисс. Чем больше закодировано в данных, тем больше рантайм-полиморфизма требуется, но и доступно тоже, т.е. тем выше уровень абстракции на уровне объектов/интерфейсов в смысле абстракций ООП, что есть бенефит для, скажем, многих чисто-ООП паттернов и дизайнов на их основе. Скажем, AST, построенное на абстрактной базе, должно явно кодировать информацию о типах узлов в данных (или в виртуальных методах, что одно и то же), чтобы это AST было пригодно для полезной обработки. Я называю такой подход "сливать в бутылочное горлышко, а затем разливать из него". Кста, как раз тот случай, когда паттерн-матчинг заруливает визитор. В случае же строго-типизированного AST, проход по нему возможен только через различные техники визиторов/колбэков/IoC, что не всегда удобно, но зато имеем лучшую типобезопасность. В общем, в реальной большой проге обычно встречаются оба подхода и оба являются компромиссами, ес-но, в рамках имеющихся мейнстримовых языков, без явной поддержки зависимых типов.

Здравствуйте, Sinclair, Вы писали:

S>А в реальном order flow всё скорее всего ещё неинтереснее — разные этапы этого workflow берут ордер не из параметров, а из базы, и там никаких статически верифицируемых свойств нету.

Есть, через if, как вот здесь:
http://rsdn.ru/forum/philosophy/5949645.1

Автор: jazzer
Дата: 10.02.15

You will always get what you always got
  If you always do  what you always did

Здравствуйте, jazzer, Вы писали:

J>Здравствуйте, Sinclair, Вы писали:

S>>А в реальном order flow всё скорее всего ещё неинтереснее — разные этапы этого workflow берут ордер не из параметров, а из базы, и там никаких статически верифицируемых свойств нету.

J>Есть, через if, как вот здесь:
J>http://rsdn.ru/forum/philosophy/5949645.1

Автор: jazzer
Дата: 10.02.15

Не нашёл.
Упрощу вопрос: вот у нас есть метод LoadOrder(int orderId). Какой тип он возвращает?

S>Упрощу вопрос: вот у нас есть метод LoadOrder(int orderId). Какой тип он возвращает?

Дай я тебе отвечу Wolfhound'ом

Автор: WolfHound
Дата: 09.02.15

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

©

Здравствуйте, Sinclair, Вы писали:

J>>Есть, через if, как вот здесь:
J>>http://rsdn.ru/forum/philosophy/5949645.1

Автор: jazzer
Дата: 10.02.15

S>Не нашёл.
S>Упрощу вопрос: вот у нас есть метод LoadOrder(int orderId). Какой тип он возвращает?

Ну тут много вариантов.
Можно вернуть вариант (хм... непереводимая игра слов ), в котором будет зашит статический тип ордера. Это если мы хотим все свойства проверить в самом LoadOrder (что маловероятно — все-таки нам что-то делать с ордером хочется каждый раз разное — нет смысла пихать все это в LoadOrder).
После этого, если это правильный вариант (т.е. со статическим диспатчем, как в Boost.Variant), у нас появляется возможность переложить контроль на компилятор. Но это не такой хороший варинат, как мой — так как нужно предусмотреть ветки визитора варианта для "неправильного" типа, а мы хотим, что оно вообще не компилировалось.
Другой вариант — это передавать continuation в LoadOrder — тогда он будет называться LoadAndProcessOrder(int orderId, function whatToDo). Но, опять же, в С++ это напрямую не сработает из-за энергичной стратегии воплощения шаблонов — будет сделана попытка скомпилировать все ветки, и с правильным типом, и с неправильным, и будет выдана ошибка, либо же нам надо предусмотреть какие-то обходные пути, типа "компилируется, но ничего не делает" — что просто замаскирует ошибку, либо "компилируется, но бросает исключение" — но это рантайм, а мы же боремся за проверку во время компиляции...

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

You will always get what you always got
  If you always do  what you always did

Здравствуйте, jazzer, Вы писали:

J>Но, опять же, в С++ это напрямую не сработает из-за энергичной стратегии воплощения шаблонов — будет сделана попытка скомпилировать все ветки, и с правильным типом, и с неправильным, и будет выдана ошибка, либо же нам надо предусмотреть какие-то обходные пути, типа "компилируется, но ничего не делает" — что просто замаскирует ошибку, либо "компилируется, но бросает исключение" — но это рантайм, а мы же боремся за проверку во время компиляции...

Если обработка ордера не требует наличия тех или иных свойств — то никаких ошибок не будет, точно также как и в твоём варианте не нужно будет писать PROP_IF/PROP_ELSE.
Если же при обработке ордера нужно будет вызывать функцию у которой в precondition будет требование конкретного свойства (типа order_is_processed) — то компилятор заставит пользователя продумать и описать реакцию на разные состояния, и нарушение precondtion в runtime не пройдёт. Точно также как и в твоём варианте компилятор заставит пользователя продумать содержание веток PROP_IF + PROP_ELSE.
Никакой концептуальной разницы я здесь не вижу. Разница только в синтаксическом сахаре

Здравствуйте, Evgeny.Panasyuk, Вы писали:

EP>Если же при обработке ордера нужно будет вызывать функцию у которой в precondition будет требование конкретного свойства (типа order_is_processed) — то компилятор заставит пользователя продумать и описать реакцию на разные состояния, и нарушение precondtion в runtime не пройдёт. Точно также как и в твоём варианте компилятор заставит пользователя продумать содержание веток PROP_IF + PROP_ELSE.
EP>Никакой концептуальной разницы я здесь не вижу. Разница только в синтаксическом сахаре

Разница в том, что _все_ функции придется написать компилируемыми на _все_ возможные состояния ордера (например, static_visitor должен быть компилируемым со всеми типами варианта) — в то время как мы хотели бы получать ошибку при попытке вызвать функцию для неправильного ордера. Моей первой идеей было как раз сделать все на continuations — и я столкнулся именно с этой проблемой: функция-продолжение должна быть компилируемой и с правильным типом, и с неправильным, причем под компилируемостью подразумевается и отсутствие static_assert.
Единственный действительно рабочий вариант, который я нашел — это разнести типы синтаксически (по веткам if/else). Он не такой элегантный, как с продолжениями (хотя тоже как посмотреть — он обеспечивает естественный if/else flow), но дает именно то, что нужно.
Мы ведь хотим получать ошибку компиляции при попытке позвать не ту функцию, а с continuations мы передаем ее всегда, независимо от типа — и она должна всегда компилироваться, для всех вариантов свойств.

Разве что ты имеешь в виду разбить этот if/else по веткам static_visitor-а варианта (и тогда будет ошибка компиляции при попытке вызова ограниченной функции не из той ветки визитора) — но это, имхо, менее наглядно, чем прямой if/else. Но работать будет.

You will always get what you always got
  If you always do  what you always did

Здравствуйте, jazzer, Вы писали:

J>Разве что ты имеешь в виду разбить этот if/else по веткам static_visitor-а варианта (и тогда будет ошибка компиляции при попытке вызова ограниченной функции не из той ветки визитора)

Да, именно так. То есть в случае variant/continuation будет код вида:

void function_which_requires_processed_order(Order<prcoessed> &x);

// ...
{
    apply(order, [](Order<prcoessed> &x)
    {
        function_which_requires_processed_order(x);
        // ...
    },
    [](auto &x)
    {
        // "ELSE" branch
        // special processing, noop, exception or whatever
    });
}

А в случае PROP_IF:

template<typename O>
enable_if_t<Processed<O>> function_which_requires_processed_order(O &o);

// ...
{
    PROP_IF(order, Processed)
    {
        function_which_requires_processed_order(order);
        // ...
    }
    PROP_ELSE
    {
        // "ELSE" branch
        // special processing, noop, exception or whatever
    };
}

То есть структура и возможности по обработке веток примерно одинаковые.

J>- но это, имхо, менее наглядно, чем прямой if/else. Но работать будет.

Несомненно это менее наглядно и удобно. И если есть какая-то логика которая хорошо ложится на зависимые типы — то хорошо бы иметь библиотеку типа PROP_IF.
variant и continuation я показывал как примеры техник реализации — то что это вообще возможно (ведь высказывались сомнения на этот счёт) — а не как законченные решения.