ceph/src/boost/boost/hana/fwd/concept/logical.hpp

   1 /*!
   2 @file
   3 Forward declares `boost::hana::Logical`.
   4
   5 @copyright Louis Dionne 2013-2017
   6 Distributed under the Boost Software License, Version 1.0.
   7 (See accompanying file LICENSE.md or copy at http://boost.org/LICENSE_1_0.txt)
   8  */
   9
  10 #ifndef BOOST_HANA_FWD_CONCEPT_LOGICAL_HPP
  11 #define BOOST_HANA_FWD_CONCEPT_LOGICAL_HPP
  12
  13 #include <boost/hana/config.hpp>
  14
  15
  16 BOOST_HANA_NAMESPACE_BEGIN
  17     //! @ingroup group-concepts
  18     //! @defgroup group-Logical Logical
  19     //! The `Logical` concept represents types with a truth value.
  20     //!
  21     //! Intuitively, a `Logical` is just a `bool`, or something that can act
  22     //! like one. However, in the context of programming with heterogeneous
  23     //! objects, it becomes extremely important to distinguish between those
  24     //! objects whose truth value is known at compile-time, and those whose
  25     //! truth value is only known at runtime. The reason why this is so
  26     //! important is because it is possible to branch at compile-time on
  27     //! a condition whose truth value is known at compile-time, and hence
  28     //! the return type of the enclosing function can depend on that truth
  29     //! value. However, if the truth value is only known at runtime, then
  30     //! the compiler has to compile both branches (because any or both of
  31     //! them may end up being used), which creates the additional requirement
  32     //! that both branches must evaluate to the same type.
  33     //!
  34     //! More specifically, `Logical` (almost) represents a [boolean algebra][1],
  35     //! which is a mathematical structure encoding the usual properties that
  36     //! allow us to reason with `bool`. The exact properties that must be
  37     //! satisfied by any model of `Logical` are rigorously stated in the laws
  38     //! below.
  39     //!
  40     //!
  41     //! Truth, falsity and logical equivalence
  42     //! --------------------------------------
  43     //! A `Logical` `x` is said to be _true-valued_, or sometimes also just
  44     //! _true_ as an abuse of notation, if
  45     //! @code
  46     //!     if_(x, true, false) == true
  47     //! @endcode
  48     //!
  49     //! Similarly, `x` is _false-valued_, or sometimes just _false_, if
  50     //! @code
  51     //!     if_(x, true, false) == false
  52     //! @endcode
  53     //!
  54     //! This provides a standard way of converting any `Logical` to a straight
  55     //! `bool`. The notion of truth value suggests another definition, which
  56     //! is that of logical equivalence. We will say that two `Logical`s `x`
  57     //! and `y` are _logically equivalent_ if they have the same truth value.
  58     //! To denote that some expressions `p` and `q` of a Logical data type are
  59     //! logically equivalent, we will sometimes also write
  60     //! @code
  61     //!     p   if and only if   q
  62     //! @endcode
  63     //! which is very common in mathematics. The intuition behind this notation
  64     //! is that whenever `p` is true-valued, then `q` should be; but when `p`
  65     //! is false-valued, then `q` should be too. Hence, `p` should be
  66     //! true-valued when (and only when) `q` is true-valued.
  67     //!
  68     //!
  69     //! Minimal complete definition
  70     //! ---------------------------
  71     //! `eval_if`, `not_` and `while_`
  72     //!
  73     //! All the other functions can be defined in those terms:
  74     //! @code
  75     //!     if_(cond, x, y) = eval_if(cond, lazy(x), lazy(y))
  76     //!     and_(x, y) = if_(x, y, x)
  77     //!     or_(x, y) = if_(x, x, y)
  78     //!     etc...
  79     //! @endcode
  80     //!
  81     //!
  82     //! Laws
  83     //! ----
  84     //! As outlined above, the `Logical` concept almost represents a boolean
  85     //! algebra. The rationale for this laxity is to allow things like integers
  86     //! to act like `Logical`s, which is aligned with C++, even though they do
  87     //! not form a boolean algebra. Even though we depart from the usual
  88     //! axiomatization of boolean algebras, we have found through experience
  89     //! that the definition of a Logical given here is largely compatible with
  90     //! intuition.
  91     //!
  92     //! The following laws must be satisfied for any data type `L` modeling
  93     //! the `Logical` concept. Let `a`, `b` and `c` be objects of a `Logical`
  94     //! data type, and let `t` and `f` be arbitrary _true-valued_ and
  95     //! _false-valued_ `Logical`s of that data type, respectively. Then,
  96     //! @code
  97     //!     // associativity
  98     //!     or_(a, or_(b, c))   == or_(or_(a, b), c)
  99     //!     and_(a, and_(b, c)) == and_(and_(a, b), c)
 100     //!
 101     //!     // equivalence through commutativity
 102     //!     or_(a, b)   if and only if   or_(b, a)
 103     //!     and_(a, b)  if and only if   and_(b, a)
 104     //!
 105     //!     // absorption
 106     //!     or_(a, and_(a, b)) == a
 107     //!     and_(a, or_(a, b)) == a
 108     //!
 109     //!     // left identity
 110     //!     or_(a, f)  == a
 111     //!     and_(a, t) == a
 112     //!
 113     //!     // distributivity
 114     //!     or_(a, and_(b, c)) == and_(or_(a, b), or_(a, c))
 115     //!     and_(a, or_(b, c)) == or_(and_(a, b), and_(a, c))
 116     //!
 117     //!     // complements
 118     //!     or_(a, not_(a))  is true-valued
 119     //!     and_(a, not_(a)) is false-valued
 120     //! @endcode
 121     //!
 122     //! > #### Why is the above not a boolean algebra?
 123     //! > If you look closely, you will find that we depart from the usual
 124     //! > boolean algebras because:
 125     //! > 1. we do not require the elements representing truth and falsity to
 126     //! >    be unique
 127     //! > 2. we do not enforce commutativity of the `and_` and `or_` operations
 128     //! > 3. because we do not enforce commutativity, the identity laws become
 129     //! >    left-identity laws
 130     //!
 131     //!
 132     //! Concrete models
 133     //! ---------------
 134     //! `hana::integral_constant`
 135     //!
 136     //!
 137     //! Free model for arithmetic data types
 138     //! ------------------------------------
 139     //! A data type `T` is arithmetic if `std::is_arithmetic<T>::%value` is
 140     //! true. For an arithmetic data type `T`, a model of `Logical` is
 141     //! provided automatically by using the result of the builtin implicit
 142     //! conversion to `bool` as a truth value. Specifically, the minimal
 143     //! complete definition for those data types is
 144     //! @code
 145     //!     eval_if(cond, then, else_) = cond ? then(id) : else(id)
 146     //!     not_(cond) = static_cast<T>(cond ? false : true)
 147     //!     while_(pred, state, f) = equivalent to a normal while loop
 148     //! @endcode
 149     //!
 150     //! > #### Rationale for not providing a model for all contextually convertible to bool data types
 151     //! > The `not_` method can not be implemented in a meaningful way for all
 152     //! > of those types. For example, one can not cast a pointer type `T*`
 153     //! > to bool and then back again to `T*` in a meaningful way. With an
 154     //! > arithmetic type `T`, however, it is possible to cast from `T` to
 155     //! > bool and then to `T` again; the result will be `0` or `1` depending
 156     //! > on the truth value. If you want to use a pointer type or something
 157     //! > similar in a conditional, it is suggested to explicitly convert it
 158     //! > to bool by using `to<bool>`.
 159     //!
 160     //!
 161     //! [1]: http://en.wikipedia.org/wiki/Boolean_algebra_(structure)
 162     template <typename L>
 163     struct Logical;
 164 BOOST_HANA_NAMESPACE_END
 165
 166 #endif // !BOOST_HANA_FWD_CONCEPT_LOGICAL_HPP