logical.hpp 7.0 KB

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