]>
Commit | Line | Data |
---|---|---|
7c673cae FG |
1 | /*! |
2 | @file | |
3 | Forward declares `boost::hana::Logical`. | |
4 | ||
b32b8144 | 5 | @copyright Louis Dionne 2013-2017 |
7c673cae FG |
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 |