Про типы и логику
От: Mamut Швеция http://dmitriid.com
Дата: 05.02.15 15:40
Оценка: 37 (4) -1
Выношу из соседнего обсуждения
Автор: Mamut
Дата: 02.02.15
, так как там много флейма и отсутсвие конструктива.

Мне просто действительно интересно. Многие утверждают, что типы помогают (чуть ли не) во всем, вплоть до того, что «тайпчекер проверяет именно логику».

У меня есть простейшая задача, мне просто интересно, как она будет решаться типами, и/или как типы могут помочь ее решить. Самое главное, если вся логика упаковывается в типы, каким образом проверяется правильность реализации этой логики на типах? Свое решение «в лоб» я тоже напишу, естественно Языки программирования — любые Но желательно приближенные к реальному миру (то есть те, что хоть в какой-то мере используются в природе).

Исходные данные:
— есть заказ
-- он может быть отправлен или неотправлен
-- он может быть предоплачен или не предоплачен
-- он может быть помечен, как несущий риск или не помечен

Что с заказом можно сделать:

— Можно изменить сумму заказа: увеличить или уменьшить (в реальности это конечно сложнее, так как изменяется не сумма, а товары в заказе: они могут добавляться, изменяться, добавляться скидки и штрафы и многое другое. И сумма заказа — это сумма товаров. Но для простоты возьмем именно этот случай).


Собственно задача. Мы будем эмулировать реальную разработку, в которой требования меняются. Мне интересно, как будет меняться реализация с типами по мере изменения требований. Все крутится вокруг изменения суммы. Для спортивности: не смотрите в следующий шаг, пока не реализован первый шаг.

Шаг 1.

  • если заказ неотправлен и непредоплачен, можно увеличивать и уменьшать
  • если заказ отправлен, нельзя увеличивать, можно уменьшать
  • если сумма увеличивается, мы должны провести risk check. если risk check не проходит, товар никак не помечается, но изменение суммы не проходит
  • если товар помечен, как risk, то изменять сумму нельзя

    Шаг 2.

    Изменение суммы:

    Все то же самое, что и в шаге первом, только:

  • увеличивать можно на max(фиксированная сумма1, процент1 от оригинальной суммы заказа)
  • уменьшать можно на max(фиксированная сумма2, процент2 от оригинальной суммы заказа),
    где сумма1, сумма2, процент1, процент2 — это конфигурация, считываемая из базы данных

    Если изменение не попадает в эти рамки, то увеличить/уменьшить нельзя


    Шаг 3.

    Все то же самое, что и в шаге 2. Дополнительно:

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


  • dmitriid.comGitHubLinkedIn
    Re: Про типы и логику
    От: nikov США http://www.linkedin.com/in/nikov
    Дата: 05.02.15 16:53
    Оценка: 43 (2) +13
    Здравствуйте, Mamut, Вы писали:

    M>Исходные данные:

    M>- есть заказ
    M>-- он может быть отправлен или неотправлен
    M>-- он может быть предоплачен или не предоплачен
    M>-- он может быть помечен, как несущий риск или не помечен

    Высокоуровневую логику на типах писать сложно и обычно нерентабельно, и это обычно никто не делает. Но вот пример ошибки в твоей задаче, с которой типы могут помочь: представь, что все три флага выше имеют просто тип boolean. Программист может случайно ошибиться, например, в порядке аргументов, и вместо того, чтобы пометить заказ как "предоплачен", пометить его как "отправлен". Если же вместо boolean мы будем использовать три разных типа, с двумя значениями каждый, такую ошибку будет очень трудно совершить случайно. Точно так же, можно использовать разные типы для количества и цены товара, и т.д. Компилятор может проверять, что мы случайно не складываем погонные метры с килограммами, или что мы не ищем значение в килограммах внутри списка, элементы которого являются "количеством ящиков".
    Отредактировано 05.02.2015 16:58 nikov . Предыдущая версия .
    Re: Про типы и логику
    От: Sinix  
    Дата: 05.02.15 17:05
    Оценка: 38 (1)
    Здравствуйте, Mamut, Вы писали:

    M> меня есть простейшая задача, мне просто интересно, как она будет решаться типами, и/или как типы могут помочь ее решить. Самое главное, если вся логика упаковывается в типы, каким образом проверяется правильность реализации этой логики на типах?

    Я видно не понимаю контекста, но зачем тут именно типы?

    Для примитивного опердня за глаза хватит обычных ассертов.

    Для чего-то покритичнее нужны контракты + smt-солвер для верификации пост/предусловий + ассерты, чтобы покрыть условия, которые солвер не может вывести автоматически. Или (вариант для бедных), реврайтер чтобы подставлять условия-инварианты в каждый метод + тесты с более-менее полноценным покрытием кода.

    Не, при желании система типов может быть расширена так, чтобы передаваемое значение аннотировалось контрактами метода, этакий adt на стероидах. Но на практике это приведёт к дичайшему гемморою из-за high cohesion: контракты расползаются по всему коду и поменять их ничего не поломав — тот ещё квест.
    Re[2]: Про типы и логику
    От: Mamut Швеция http://dmitriid.com
    Дата: 05.02.15 19:45
    Оценка:
    N>Высокоуровневую логику на типах писать сложно и обычно нерентабельно, и это обычно никто не делает.

    Но как же! Мне тут рядом все уши прожужжали, что надо как можно больше логики складывать в типы!

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


    Да. Это, безусловно, подспорье. Но на практике (80% кода в логике изменения не менялись уже лет пять, остальные 20% менялись этой весной) такое возникает исчезающе редко, особенно если заказ предоставлен черным ящиком, из которого наружу торчат is_processed, is_risk и т.п.

    У нас гораздо больше проблем именно с высокоуровневой логикой.


    dmitriid.comGitHubLinkedIn
    Re[2]: Про типы и логику
    От: Mamut Швеция http://dmitriid.com
    Дата: 05.02.15 19:55
    Оценка: +1
    S>Я видно не понимаю контекста, но зачем тут именно типы?

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

    S>Для примитивного опердня за глаза хватит обычных ассертов.


    S>Для чего-то покритичнее нужны контракты + smt-солвер для верификации пост/предусловий + ассерты, чтобы покрыть условия, которые солвер не может вывести автоматически. Или (вариант для бедных), реврайтер чтобы подставлять условия-инварианты в каждый метод + тесты с более-менее полноценным покрытием кода.


    Ой 0_о

    Ну, в целом я на самом деле согласен. У нас, правда, данный конкретный случай решено, по сути, if'ами В change_sum там три функции is_fobidden_1, is_fobidden_2 и is_fobidden_3 где-то на сто строчек После чего происходит собственно увеличение суммы (которое тоже может происходить по-разному из-за всякого разного).

    Хотя да, скажем передвижение заказа по dunning'у у нас описано развесистой машиной состояний, с интересными проверками там и тут и прочими плюшками.

    S>Не, при желании система типов может быть расширена так, чтобы передаваемое значение аннотировалось контрактами метода, этакий adt на стероидах. Но на практике это приведёт к дичайшему гемморою из-за high cohesion: контракты расползаются по всему коду и поменять их ничего не поломав — тот ещё квест.


    Ой. А мне утверждали, что придется меняться не во всем коде, а только в одном месте


    dmitriid.comGitHubLinkedIn
    Re: Про типы и логику
    От: kaa.python Ниоткуда РСДН профессионально мёртв и завален ватой.
    Дата: 06.02.15 02:19
    Оценка: 43 (2)
    Здравствуйте, Mamut, Вы писали:

    M>Выношу из соседнего обсуждения
    Автор: Mamut
    Дата: 02.02.15
    , так как там много флейма и отсутсвие конструктива.

    M>Мне просто действительно интересно. Многие утверждают, что типы помогают (чуть ли не) во всем, вплоть до того, что «тайпчекер проверяет именно логику».

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

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

    Само собой, если язык легко позволяет творить с типами что угодно через приведение к void*, то мы получаем дополнительные места с неочевидным поведением, но они хотя бы локализованны и и проще покрыть тестами.

    Как-то так...
    Re: Про типы и логику
    От: IT Россия linq2db.com
    Дата: 06.02.15 04:40
    Оценка: 6 (1) +4
    Здравствуйте, Mamut, Вы писали:

    M>У меня есть простейшая задача, мне просто интересно, как она будет решаться типами, и/или как типы могут помочь ее решить.


    Простейшая задача, выковырянная неизвестно из какого места, да ещё и адаптированная под точку зрения автора, ничего не доказывает.

    Если ты когда-нибудь собирал мозаичные пазлы, то должен был заметить, что различная форма фрагментов рисунка позволяет избежать большинства ошибок и резко ускорить выполнение задачи. Типы в любой логике выполняют примерно туже самую роль.
    Если нам не помогут, то мы тоже никого не пощадим.
    Re[2]: Про типы и логику
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 07:20
    Оценка: 5 (1) -2 :)
    M>>У меня есть простейшая задача, мне просто интересно, как она будет решаться типами, и/или как типы могут помочь ее решить.
    IT>Простейшая задача, выковырянная неизвестно из какого места, да ещё и адаптированная под точку зрения автора, ничего не доказывает.

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

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

    IT>Если ты когда-нибудь собирал мозаичные пазлы, то должен был заметить, что различная форма фрагментов рисунка позволяет избежать большинства ошибок и резко ускорить выполнение задачи. Типы в любой логике выполняют примерно туже самую роль.


    Демагогия.

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

    Но зато при постоянных пафосных заявлениях про мозаику, тайпчекер проверит логику и прочая и прочая.

    http://rsdn.ru/forum/philosophy/5945470.1
    Автор: genre
    Дата: 05.02.15
    (на стопятидесятом сообщении в топике)

    Вот это все настолько красиво звучит, что было бы здорово увидеть пример, как запросто отразить это в определении типа.


    Ответ? Все будет зашиьись, верь мне
    Автор: jazzer
    Дата: 05.02.15
    .


    dmitriid.comGitHubLinkedIn
    Re[2]: Про типы и логику
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 07:21
    Оценка:
    KP>позволят не писать ряд тестов для проверки корректности поведения с не подходящими типами

    Например?


    dmitriid.comGitHubLinkedIn
    Re[3]: Про типы и логику
    От: kaa.python Ниоткуда РСДН профессионально мёртв и завален ватой.
    Дата: 06.02.15 07:35
    Оценка: 38 (1) +3
    Здравствуйте, Mamut, Вы писали:

    M>Например?


    У нас есть функция и типы данных:
    struct bar{ void f1(){}; void f2(){};}
    struct zoo{void f1(){};}
    
    void foo(bar data);

    Если ты пишешь на языке не поддерживющем проверку типов на этапе сборки, ты должен написать тест который докажет что foo() не поплохеет если в нее по ошибке будет скормлен объект типа zoo. Проверка типа во время компиляции убережет тебя от, во-первых, написания теста, во-вторых от добавления лишней защитной логики в foo(). Мы же явно не хотим что бы foo() падала или как-то еще непортребно себя вела при получении неверного типа в качестве входных данных.
    Re[4]: Про типы и логику
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 08:38
    Оценка:
    KP>Мы же явно не хотим что бы foo() падала или как-то еще непортребно себя вела при получении неверного типа в качестве входных данных.

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

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


    dmitriid.comGitHubLinkedIn
    Re: Ах да, мое решение :)
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 09:22
    Оценка: 48 (2)
    Одна из проблем, в котором я столкнулся в обсуждении в соседней ветке — это какой-то мегастранный подход апологетов типизации к решению задачи. Почему-то несколько раз для них являлось откровением, что все проверки можно и нужно делать не в местах, откуда вызывается change_amount, а внутри самой функции change_amount. Или, например, что в таком случае можно возвращать внятные ошибки

    Несмотря на жалобы IT
    Автор: IT
    Дата: 06.02.15
    , эта задача — реальная задача, решаемая нашей компанией тысячи раз в день. Выросла она на основе тех самых "ad-hoc and often informal specifications", о которых говорится в презентации тут
    Автор: jazzer
    Дата: 30.01.15
    . Почему-то, несмотря на презентацию, и уверенность в «компиляторе, проверяющем мозаику», никто так и не осилил решить эту задачу типами

    Вы думаете, задачи в Standard Chartered Bank сильно отличаются от такой? Вы сильно заблуждаетесь.

    В общем, решение в лоб. Примерно в таком виде оно существует и у нас, работает, проблем не вызывает. Изменение суммы производится путем вызова order:change_amount. Эта функция вызывается из трех мест. Все, что в нее передается — это заказ и новая сумма. На выходе — {ok, UpdatedOrder} или {error, Reason}.

    Код полупсевдокод (знающие Erlang поймут, почему — в if guard'ах нельзя кастомные функции). Код писал вручную прямо в редакторе сообщений RSDN, так что могут быть ошибки, естественно

    Естественно, к коду еще будут приложены тесты, проверяющие ожидаемое поведение для заказов в разных состояниях. Как unit-тесты, проверяющие, правильно ли реализована функция, так и integration-тесты, проверяющие поведение всей системы. А у вас не так?

    M>Шаг 1.


    M>[*] если заказ неотправлен и непредоплачен, можно увеличивать и уменьшать

    M>[*] если заказ отправлен, нельзя увеличивать, можно уменьшать
    M>[*] если сумма увеличивается, мы должны провести risk check. если risk check не проходит, товар никак не помечается, но изменение суммы не проходит
    M>[*] если товар помечен, как risk, то изменять сумму нельзя

    change_amount(Order, NewAmount) ->
      case is_forbidden(Order, NewAmount) of
        {error, Reason} ->
          {error, Reason};
        ok ->
          case risk_check(Order, NewAmount) of
            {error, Reason} -> {error, Reason};
            ok -> {ok, Order#order{amount = NewAmount}
          end
      end.
    
    is_forbidden(Order, NewAmount) ->
      if
        is_risk(Order) ->
          {error, risk};
        not is_shipped(Order) andalso not is_prepaid(Order) ->
          ok;
        is_shipped(Order) andalso NewAmount > amount(Order) ->
          {error, amount}
        true ->
          ok
      end.
    
    risk_check(Order, NewAmount) ->
      case amount(Order) < Amount of
        true -> risk:risk_check(Order, Amount);
        ok
      end.



    M>Шаг 2.


    M>Изменение суммы:


    M>Все то же самое, что и в шаге первом, только:


    M>[*] увеличивать можно на max(фиксированная сумма1, процент1 от оригинальной суммы заказа)

    M>[*] уменьшать можно на max(фиксированная сумма2, процент2 от оригинальной суммы заказа),
    M>где сумма1, сумма2, процент1, процент2 — это конфигурация, считываемая из базы данных

    M>Если изменение не попадает в эти рамки, то увеличить/уменьшить нельзя


    Добавляется одна функция и вызов этой функции. Все остальное без изменений.

    change_amount(Order, NewAmount) ->
      case is_forbidden(Order, NewAmount) of
        ...
        ok ->
          case risk_check(Order, NewAmount) of
            ...
            ok -> 
              update_amount(Order, NewAmount)
          end
      end.
    
    ...
    
    update_amount(Order, NewAmount) when amount(Order) > NewAmount ->
       Estore = get_estore(Order)
       Max = config:read(Estore, max_decrease),
       MaxPct = config:read(Estore, max_increase_pct),
       AmountDiff = abs(amount(Order) - NewAmount),
    
       case AmountDiff > Max andalso AmountDiff/amount(Order) > MaxPct of
         true -> {error, amount};
         false -> {ok, Order#order{amount = NewAmount}}
       end;
    update_amount(Order, NewAmount) ->
       %% то же самое, только для max_increase и max_increase_pct
       end.


    M>Шаг 3.


    M>Все то же самое, что и в шаге 2. Дополнительно:


    M>[*] если заказ предоплачен (неважно, отправлен или нет), можно увеличивать сумму, если это разрешено конфигурацией магазина. Сумма, на которую можно увеличивать высчитывается, как в шаге 2

    M>[*] если заказ предоплачен, неотправлен, и сумма увеличивается, надо сделать auth-запрос в банк. если он не срабатывает, увеличить нельзя.
    M>[*] если заказ предоплачен, отправлен, и сумма увеличивается, надо сделать auth-запрос в банк на разницу в сумме, а потом сделать capture запрос на всю сумму. Если хоть один из них не срабатывает, увеличить нельзя.

    Меняются некоторые условия, добавляются функции. В реальности проверок is_forbidden еще около десятка. Полный код.

    change_amount(Order, NewAmount) ->
      case is_forbidden(Order, NewAmount) of
        {error, Reason} ->
          {error, Reason};
        ok ->
          case risk_check(Order, NewAmount) of
            {error, Reason} -> {error, Reason};
            ok -> update_amount(Order, NewAmount)
          end
      end.
    
    is_forbidden(Order, NewAmount) ->
      if
        is_risk(Order) ->
          {error, risk};
        is_prepaid(Order) andalso NewAmount > amount(Order) ->
          can_raise_prepaid_order(Order, NewAmount);
        is_shipped(Order) andalso NewAmount > amount(Order) ->
          {error, amount}
        true ->
          ok
      end.
    
    can_raise_prepaid_order(Order, NewAmount) ->
      Estore = get_estore(Order),
      case config:get_config(Estore, can_raise_prepaid) of
        false -> {error, amount};
        true -> ok
      end.  
    
    risk_check(Order, NewAmount) ->
      case amount(Order) < Amount of
        true -> risk:risk_check(Order, Amount);
        ok
      end.
    
    update_amount(Order, NewAmount) ->
       Estore = get_estore(Order)
       Max = config:read(Estore, case amount(Order) > NewAmount of true -> max_decrease; false -> max_increase end),
       MaxPct = config:read(Estore, case amount(Order) > NewAmount of true -> max_decrease_pct; false -> max_increase_pct end),
       AmountDiff = abs(amount(Order) - NewAmount),
    
       case AmountDiff > Max andalso AmountDiff/amount(Order) > MaxPct of
         true -> {error, amount};
         false -> 
            auth_and_capture(Order, NewAmount)
       end.
    
    auth_and_capture(Order, NewAmount) ->
      case is_prepaid(Order) of
        false ->
          {ok, Order#order{amount = NewAmount};
        true ->
          case NewAmount > amount(Order) of
            true ->
              case payments:auth(Order, NewAmount - amount(Order)) of
                {error, Reason} -> {error, Reason};
                ok -> capture(Order, NewAmount)
              end;
            false ->
               capture(Order, NewAmount)
          end
      end.
    
    capture(Order, NewAmount) ->
      case is_shipped(Order) of
        false -> {ok, Order#order{amount = NewAmount};
        true ->
          case payment:capture(Order, NewAmount) of
            {error, Reason} -> {error, Reason};
            ok -> {ok, Order#order{amount = NewAmount}
          end
      end.


    dmitriid.comGitHubLinkedIn
    Re[2]: Ну и в реальности
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 10:27
    Оценка:
    M>В реальности проверок is_forbidden еще около десятка.

    Условия на запрет изменения

  • если заказ помечен как кредит
  • если заказ помечен как удаленный
  • если заказ помечен как пассивный
  • если заказ помечен как замороженный
  • если заказ помечен как предоплата
  • если заказ помечен как оплаченный по предоплате
  • если в заказе нет товаров, которые можно вернуть

  • если это аггрегированный заказ с прошедшим сроком оплаты
  • если это архивный заказ при условии, что он оплачивается через account
  • если сумма увеличивается, а это запрещено настройками заказа
  • если сумма увеличивается, а мы уже отослали запрос на оплату в банк клиента
  • если сумма увеличивается на сумму большую, чем указано в настройках (относительно оригинальной суммы заказа)

  • если сумма увеличивается, а заказ проведен через новую систему
  • если мы возвращаем деньги клиенту, заказ находится в одном из трех статусов, не является кредитом, и возвращаемая сумма меньше, чем максимальная разрешенная к возврату сумма


  • только после этого будет предпринята попытка изменить сумму заказа. Причем само изменение суммы — это тоже не шубу в трусы заправлять. Это надо сделать запись в бухгалтерию, передвинуть заказ по dunning chain, если надо, сделать нужные записи в кредитной истории, устроить risk check'и, и прочая и прочая.


    dmitriid.comGitHubLinkedIn
    Re[3]: Про типы и логику
    От: Sinix  
    Дата: 06.02.15 11:03
    Оценка: 27 (2)
    Здравствуйте, Mamut, Вы писали:

    S>>Я видно не понимаю контекста, но зачем тут именно типы?


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

    А, тогда ой. Я что-то не соображу, что тут можно придумать кроме очевидных и нужных not-null и типов-размерностей. Тоже интересно было бы посмотреть.

    S>>Для чего-то покритичнее нужны контракты + ...

    M>Ой 0_о
    Ага Даже простые trait/variant особо популярности не набрали, что уж тут говорить о статической верификации на типах.

    Я кстати уже который год внимательно смотрю за CodeContracts. Очень интересная попытка протащить статические контракты в мейнстрим малой кровью. Поначалу "малой кровью" не выходило, контракты надо было прописывать в каждом методе (и обновлять всю цепочку вызовов при любом изменении контракта). Плюс куча мелких косяков реврайтера, плюс поддержка только премиум-версии студии и тыды и тыпы.
    Короче, штука только для поиграться была.

    А где-то год назад в контракты добавили автоматический вывод контрактов и к прошлой осени допилили его до практически рабочего состояния. Например:
        static void Example()
        {
            // Warning: CodeContracts: requires is false: !string.IsNullOrEmpty(s).
            // This sequence of invocations will bring to an error Example -> TestWithContract -> TestWithContract2 -> TestWithContract3 -> TestWithContract4, condition !string.IsNullOrEmpty(s)
            TestWithContract(""); 
        }
        
        private static void TestWithContract(string s)
        {
            TestWithContract2(s);
        }
        private static void TestWithContract2(string s)
        {
            TestWithContract3(s);
        }
        private static void TestWithContract3(string s)
        {
            TestWithContract4(s);
        }
        private static void TestWithContract4(string s)
        {
            TestWithContractCore(s);
        }
        private static void TestWithContractCore(string s)
        {
            Contract.Requires(!string.IsNullOrEmpty(s));
            Console.WriteLine(s);
        }

    + поддержка в VS Community + недавное выкладывание CC в опенсорс... молодцы, короче

    Два недостатка:
    * не работает вывод по if-then-throw, только для контрактов через Contract.Requires(),
    * сборка с проверкой всех контрактов может занимать дофигищща времени.
    Ну, и надо аккуратно настраивать параметры верификации для каждого проекта + повозиться с билд-сервером, но это уже мелочи.

    Уже всерьёз думаю полноценно опробовать в продакшне, если будет возможность


    M>Ну, в целом я на самом деле согласен. У нас, правда, данный конкретный случай решено, по сути, if'ами В change_sum там три функции is_fobidden_1, is_fobidden_2 и is_fobidden_3 где-то на сто строчек После чего происходит собственно увеличение суммы (которое тоже может происходить по-разному из-за всякого разного).


    Угу. В текущем проекте контракты не используются, зато вовсю используются отладочные ассерты. Безумно удобная штука: пишешь код, закладываешься на какое-то поведение (например, на order.State == State.Processed), добавил в код что-то типа
    DebugCode.AssertBusiness(order.State == State.Processed, "бла-бла-бла");

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

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

    M>Хотя да, скажем передвижение заказа по dunning'у у нас описано развесистой машиной состояний, с интересными проверками там и тут и прочими плюшками.

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



    S>>Не, при желании система типов может быть расширена так, чтобы передаваемое значение аннотировалось контрактами метода, этакий adt на стероидах. Но на практике это приведёт к дичайшему гемморою из-за high cohesion: контракты расползаются по всему коду и поменять их ничего не поломав — тот ещё квест.


    M>Ой. А мне утверждали, что придется меняться не во всем коде, а только в одном месте

    Проблемы с расползанием будут, если контракты прописывать явно, как у тебя в стартовом сообщении. А если выводить автоматически (что насколько я знаю, умеет только code contracts, по крайней мере из более-менее мейнстрима) — то совсем другое дело
    Re[4]: Про типы и логику
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 12:32
    Оценка: 30 (1) :)
    M>>Хотя да, скажем передвижение заказа по dunning'у у нас описано развесистой машиной состояний, с интересными проверками там и тут и прочими плюшками.
    S>Что-то такое тоже есть в паре мест. Особенно удобно в отладочных сборках навесить на изменение текущего состояния все возможные проверки. Пару раз спасало от багов из разряда "фиг найдёшь".

    У нас в итоге «фиг найдешь баги» появились из-за новых требований к определенному классу заказов.

    То есть в целом для dunning'а не имеет значения, кто и когда откуда заказ сделал, главное — какой способ оплаты выбран. И потом заказ перемещается по состояниям A -> B -> C -> D и т.п.

    Но появился новый тип интеграции в котором как всегда ВНЕЗАПНО (a.k.a. ad-hoc) надо было поломать state-машину примерно так:
    
    A -> B -> C  -> D -> E -> F
         \              /
          -(if X) - - -



    Это обходило пару проверок, которые были указаны в C и D, и которые рушили представления о заказе, когда заказ из F, например, перемещался обратно в C. И таких сокращений из-за новой интеграции было несколько штук Слава богу, когда от интеграции отказались, вычищать эти проблемы пришлось не мне


    dmitriid.comGitHubLinkedIn
    Re[2]: Про типы и логику
    От: Кодт Россия  
    Дата: 06.02.15 12:47
    Оценка:
    Здравствуйте, nikov, Вы писали:

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

    N>Высокоуровневую логику на типах писать сложно и обычно нерентабельно, и это обычно никто не делает. Но вот пример ошибки в твоей задаче, с которой типы могут помочь: представь, что все три флага выше имеют просто тип boolean. Программист может случайно ошибиться, например, в порядке аргументов, и вместо того, чтобы пометить заказ как "предоплачен", пометить его как "отправлен".

    Спасают именованные аргументы вместо позиционных. Структуры с геттерами-сеттерами вместо тупых кортежей.

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


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

    Именованные аргументы тоже многословны, да ещё и в разных языках может возникать разная нагрузка на рантайм (передача хештаблицы вместо кортежа аргументов — в питоне).
    Перекуём баги на фичи!
    Re: Про типы и логику
    От: Кодт Россия  
    Дата: 06.02.15 13:39
    Оценка: 21 (1)
    Здравствуйте, Mamut, Вы писали:

    M>Собственно задача. Мы будем эмулировать реальную разработку, в которой требования меняются. Мне интересно, как будет меняться реализация с типами по мере изменения требований. Все крутится вокруг изменения суммы. Для спортивности: не смотрите в следующий шаг, пока не реализован первый шаг.


    Если с самого начала знать, что шаги будут "в ассортименте", то можно упаковать все условия в утино-типизированный кортеж времени компиляции.
    Тогда получишь фантомные типы вокруг одного и того же нетто-типа.

    template<class Netto, class Phantom> struct phantom_type
    {
      typedef Phantom phantom;
      Netto value;
      phantom_type(Netto v) : value(v) {}
    };
    
    // нетто
    typedef int Good; // товар (в штуках)
    
    // операции
    unspecified1<Good> start(Good value);
    unspecified1<Good> increase(unspecified0<Good> good);
    unspecified1<Good> decrease(unspecified0<Good> good);
    unspecified1<Good> increase(unspecified0<Good> good);
    unspecified1<Good> riskcheck(unspecified0<Good> good); // здесь мы влезаем в полиморфизм времени исполнения
                                                           // так что - или делаем на продолжениях, или на полиморфных значениях
    unspecified1<Good> pay(unspecified0<Good> good);
    unspecified1<Good> send(unspecified0<Good> good);


    Как это сделать _красиво_ — тут надо подумать.
    То, что потребуются функторы — безусловно.
    Какой-то небольшой фреймворчик, реализующий аппликативные функторы. В хаскелле, так, всё из коробки будет (я так думаю), а камле, скале и плюсах придётся немножко попотеть.
    Перекуём баги на фичи!
    Re[2]: Про типы и логику
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 13:57
    Оценка:
    К>Какой-то небольшой фреймворчик, реализующий аппликативные функторы. В хаскелле, так, всё из коробки будет (я так думаю), а камле, скале и плюсах придётся немножко попотеть.

    Ни у конечно вопрос, надо ли потеть?


    dmitriid.comGitHubLinkedIn
    Re[2]: Ах да, мое решение :)
    От: jazzer Россия Skype: enerjazzer
    Дата: 06.02.15 14:51
    Оценка:
    Здравствуйте, Mamut, Вы писали:

    M>В общем, решение в лоб. Примерно в таком виде оно существует и у нас, работает, проблем не вызывает.


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

    Типы не решают задачу решения задачи в лоб. Они решают задачу бана неправильного кода, где правильность закодирована в определении. У тебя такого бана нету. Можно проверить is_forbidden и тут же дернуть update_amount, и компилятор и не почешется на эту тему, и останется только уповать на тесты.
    jazzer (Skype: enerjazzer) Ночная тема для RSDN
    Автор: jazzer
    Дата: 26.11.09

    You will always get what you always got
      If you always do  what you always did
    Re[3]: Ах да, мое решение :)
    От: Mamut Швеция http://dmitriid.com
    Дата: 06.02.15 15:01
    Оценка: :)
    J>Типы не решают задачу решения задачи в лоб. Они решают задачу бана неправильного кода, где правильность закодирована в определении. У тебя такого бана нету. Можно проверить is_forbidden и тут же дернуть update_amount, и компилятор и не почешется на эту тему, и останется только уповать на тесты.

    Общие фразы ни о чем продолжаются.

    Да можно. Да, не почешется. Только код работает уже много лет и проблем не вызывает. От апологетов типизации слышны только рассказы о том, как типы везде во всем помогут и как все плохо в коде без типов И ни одного внятного примера сложнее, чем hello, world.

    Не говоря уже про смешное
    Автор: jazzer
    Дата: 05.02.15

    Так ведь дело-то в том, что проверку-то ты вставишь, а дальше-то что делать будешь с результатом этой проверки? что в check должно происходить? исключение? ведь надо же как-то наверх сообщить, что облом?




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

    Пока что многие говорят, что нет, типы
    Автор: nikov
    Дата: 05.02.15
    тут не помогут
    Автор: Sinix
    Дата: 05.02.15
    никак
    Автор: kaa.python
    Дата: 06.02.15
    , кроме как на самом низком уровне, проверять что мы не складываем километры с килограммами и т.п.



    dmitriid.comGitHubLinkedIn
    Подождите ...
    Wait...
    Пока на собственное сообщение не было ответов, его можно удалить.