Информация об изменениях

Сообщение Про типы и логику - С++ от 10.02.2015 8:11

Изменено 10.02.2015 8:44 jazzer

Старый текст
Новый текст
Разница

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

В каком-то смысле это попытка реализации зависимых типов на С++, я ее начал писать очень давно (еще до С++11, так что кое-что будет излишне многословно), когда заинтересовался бурным обсуждением зависимых типов здесь; но вот с подачи Мамута подвернулась относительно реальная задача, на которой можно проверить мои построения.

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

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

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

Не рассчитывая на честное судейство, покажу то, что у меня есть (весь код ниже рабочий, ошибки компиляции реальны).
Пусть у нас есть ордер:

struct Order
{
  int id;
  bool shipped, prepaid_, risk;
  double amount;

  // эти строчки просто для разных способов определения свойств ордера, помимо o.shipped
  bool prepaid() const { return prepaid_; }
  friend bool has_risk(const Order& o) { return o.risk; }
};

Это базовый тип, и на него мы будем навешивать свойства. Тип ордера со свойствами (в каком-то виде это зависимый тип из агды и т.п.) будет выглядеть так: Type<Order, Properties>, где Properties — это просто compile-time map, например Type<Order&, boost::mpl::map<_{HasRisk:false_ }, _{Shipped:false_}, _{Prepaid:false_}> > (тут, для краткости, _{K:V} — это boost::mpl::pair<K,V>). Метафункции для добавления/убирания/изменения/проверки свойств пишутся элементарно, так что я их тут не привожу.

Теперь делаем функцию increase_amount(Order), которая будет проверять, обладает ли ордер нужными свойствами. Проверку можно написать прямо в определении функции, а можно вынести отдельной метафункцией (потому что автоматически появтся возможность написать для нее юнит-тесты):

struct HasRisk; // Свойство, которое мы хотим проверять в compile time

// предикат (CheckExact - это проверка того, что свойство HasRisk строго равно false.
//           понятно, что можно сделать другие предикаты, типа AtLeast и т.п.)
template<class O> using can_increase_amount = CheckExact< O, HasRisk, bm::false_ >;

//разрешаем (enable_if) функцию только если проверка прошла
template<class O>
typename boost::enable_if< can_increase_amount<O>, O >::type
increase_amount(O o, double incr)
{
  QTLOG << "increasing amount of order " << unwrap(o) << " by " << incr;
  unwrap(o).amount += incr;
  return o;
}

// ругнемся, чтоб программеру было понятно, что он написал что-то не то.
// в принципе, эту функцию можно и не писать, но тогда сообщение об ошибке 
// будет слишком загадочным ("функция не найдена")
template<class O>
typename boost::disable_if< can_increase_amount<O>, O >::type
increase_amount(O o, double incr)
{
  BOOST_MPL_ASSERT_MSG(false, YOU_CANT_INCREASE_AMOUNT_FOR_SUCH_ORDER, (O));
  return o;
}

Теперь пишем функцию, в которой мы хотим увеличивать amount ордера (это реальный работающий код, если что):

void try_to_change_amount(Order& o)
{
  //increase_amount(o, 2.71);  - не скомпилируется: мы ничего не знаем о риске
  
  PROP_IF(o, has_risk(o), HasRisk) {
    //increase_amount(o, 2.71); - не скомпилируется: ордер помечен как рисковый
  }
  PROP_ELSE(o) {
    increase_amount(o, 2.71);
  };

Что делает PROP_IF — он навершивает свойство HasRisk в соответствии с проверкой has_risk(o), и дальше внутри if и else объект o будет обладать этим свойством. Это приведет к тому, что вызов increase_amount скомпилируется только внутри ветки else. Если раскомментировать вызов внутри ветки if или вызов за пределами if — будет ошибка компиляции:

error: ************::YOU_CANT_INCREASE_AMOUNT_FOR_SUCH_ORDER::************(Type<Order&, mpl::map<_{HasRisk:true_ }> >)

Это была реализация требования

если товар помечен, как risk, то изменять сумму нельзя

Теперь добавим следующее требование:

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

В коде это приведет просто к добавлению этого требования к предикату:

struct Shipped; // новое свойство

template<class O> using can_increase_amount =
    bm::and_< CheckExact< O, HasRisk, bm::false_ >
            , CheckExact< O, Shipped, bm::false_ > // новое ad-hoc требование
            >;

запускаем компиляцию — опаньки, не компилируется:

error: ************::YOU_CANT_INCREASE_AMOUNT_FOR_SUCH_ORDER::************(Type<Order&, mpl::map<_{HasRisk:false_ }> >)

Не компилируется потому, что требуется проверить свойство Shipped, а его нет.
Идем туда, где не компилируется, добавляем соответствующий PROP_IF:

void try_to_change_amount(Order& o)
{
  PROP_IF(o, has_risk(o), HasRisk) {
    // сообщить об ошибке
  }
  PROP_ELSE(o) {
    // increase_amount(o, 2.71); -- больше не работает: надо проверять Shipped
    PROP_IF(o, o.shipped, Shipped ) {
      //increase_amount(o, 2.71); // (*)
      // сообщить об ошибке
    }
    PROP_ELSE(o) {
      increase_amount(o, 2.71);
    };
  };

если раскомментировать вызов increase_amount внутри Shipped==true (*) — получим, опять же, ошибку компиляции:

error: ************::YOU_CANT_INCREASE_AMOUNT_FOR_SUCH_ORDER::************(Type<Order&, mpl::map<_{HasRisk:false_ }, _{Shipped:true_}> >)

Вместо раскомментирования может быть неудачный copy-paste, например, или неудачный merge.

Надеюсь, идея понятна. Дополнительные требования навешиваются аналогично. Если элементарных свойств/требований становится слишком много, то можно их просто упаковать в мета-свойство IncreaseAmountOK, которое будет взводиться теперь уже обычной функцией bool can_increase_amount(Order, amount) (да, тут в проверке появился amount; и аналогично появятся какие-то другие внешние вещи из конфигурации, БД и прочая) — и таким образом мы вернемся к простому первоначальному варианту, только вместо HasRisk/has_risk(o) будет это мета-свойство и функция-предикат, соответственно.

Естественно, это не убережет нас от ошибок в реализации can_increase_amount (или has_risk выше) — но компилятор не пропустит вызова increase_amount для ордера, у которого не прошла соответствующая проверка, какой бы они не была. Компилятор теперь будет гарантировать, что increase_amount может быть вызван только для ордера со свойством IncreaseAmountOK=true:

template<class O>
typename boost::enable_if< IncreaseAmountOK<O>, O >::type
increase_amount(O o, double incr);

void try_to_change_amount(Order& o, double new_amt)
{
  PROP_IF(o, can_increase_amount(o, new_amt), IncreaseAmountOK) {
    increase_amount(o, new_amt);
  };
}

попытка вставить вызов increase_amount в любое другое место за пределами сработавшего if вызовет ошибку компиляции. Именно благодаря типам.

Более того, можно в PROP_IF навесить свойство не только на ордер, но и на new_amt, с которым прошла проверка, или даже на пару order+new_amt — чтобы было невозможно позвать increase_amount с другой суммой new_amt2, которая проверку не проходила:

template<class OrderAndAmount>
typename boost::enable_if< IncreaseAmountOK<OrderAndAmount>, OrderAndAmount >::type
increase_amount(OrderAndAmount oa)
{
  unwrap(oa.order).amount += oa.amount;
}

void try_to_change_amount(Order& o, double new_amt)
{
  PROP_IF(order_and_amount, can_increase_amount(o, new_amt), IncreaseAmountOK) {
    increase_amount(order_and_amount);
  };
}

И не сказать, что кода стало на 100500 порядков больше, чем с решением в лоб.
Обрати внимание, логика в смысле того, что происходит внутри change_amount, внутри can_increase_amount, внутри has_risk, и даже внутри try_to_change_amount в смысле вызовов проверок/предикатов, генерации разнообразных сообщений об ошибках входных данных и прочая, на типах не пишется.
На типах пишется логика ограничений: когда, что и как может быть вызвано.
И проверяет их компилятор за нас, автоматически, и не пропустит ни строчки кода, не соответствующего требуемым (или изменившимся) ограничениям.

Про типы и логику - С++

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

В каком-то смысле это попытка реализации зависимых типов на С++, я ее начал писать очень давно (еще до С++11, так что кое-что будет излишне многословно), когда заинтересовался бурным обсуждением зависимых типов здесь; но вот с подачи Мамута подвернулась относительно реальная задача, на которой можно проверить мои построения.

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

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

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

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

Не рассчитывая на честное судейство, покажу то, что у меня есть (весь код ниже рабочий, ошибки компиляции реальны).
Пусть у нас есть ордер:

struct Order
{
  int id;
  bool shipped, prepaid_, risk;
  double amount;

  // эти строчки просто для разных способов определения свойств ордера, помимо o.shipped
  bool prepaid() const { return prepaid_; }
  friend bool has_risk(const Order& o) { return o.risk; }
};

Это базовый тип, и на него мы будем навешивать свойства. Тип ордера со свойствами (в каком-то виде это зависимый тип) будет выглядеть так: Type<Order, Properties>, где Properties — это просто compile-time map, например Type<Order&, boost::mpl::map<_{HasRisk:false_ }, _{Shipped:false_}, _{Prepaid:false_}> > (тут, для краткости, _{K:V} — это boost::mpl::pair<K,V>). Метафункции для добавления/убирания/изменения/проверки свойств пишутся элементарно, так что я их тут не привожу.

Теперь делаем функцию increase_amount(Order), которая будет проверять, обладает ли ордер нужными свойствами. Проверку можно написать прямо в определении функции, а можно вынести отдельной метафункцией (потому что автоматически появтся возможность написать для нее юнит-тесты):

struct HasRisk; // Свойство, которое мы хотим проверять в compile time

// предикат (CheckExact - это проверка того, что свойство HasRisk строго равно false.
//           понятно, что можно сделать другие предикаты, типа AtLeast и т.п.)
template<class O> using can_increase_amount = CheckExact< O, HasRisk, bm::false_ >;

//разрешаем (enable_if) функцию только если проверка прошла
template<class O>
typename boost::enable_if< can_increase_amount<O>, O >::type
increase_amount(O o, double incr)
{
  std::cout << "increasing amount of order " << unwrap(o) << " by " << incr << std::endl;
  unwrap(o).amount += incr;
  return o;
}

// ругнемся, чтоб программеру было понятно, что он написал что-то не то.
// в принципе, эту функцию можно и не писать, но тогда сообщение об ошибке 
// будет слишком загадочным ("функция не найдена")
template<class O>
typename boost::disable_if< can_increase_amount<O>, O >::type
increase_amount(O o, double incr)
{
  BOOST_MPL_ASSERT_MSG(false, YOU_CANT_INCREASE_AMOUNT_FOR_SUCH_ORDER, (O));
  return o;
}