| 1 | /*! |
|---|
| 2 | @file |
|---|
| 3 | Forward declares `boost::hana::Logical`. |
|---|
| 4 | |
|---|
| 5 | Copyright Louis Dionne 2013-2022 |
|---|
| 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 | namespace boost { namespace hana { |
|---|
| 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 | }} // end namespace boost::hana |
|---|
| 165 | |
|---|
| 166 | #endif // !BOOST_HANA_FWD_CONCEPT_LOGICAL_HPP |
|---|
| 167 | |
|---|
