type_proof/
boolean.rs

1//! Defines Boolean values and operations as types.
2//!
3//! There are types [`True`] and [`False`], and operations such as [`Not`], [`And`] and [`Or`]. These type operations
4//! work via type aliases, so the result of the operations is still one of [`True`] or [`False`].
5//!
6//! # Example
7//!
8//! ```
9//! use type_proof::{
10//!     boolean::{And, False, True},
11//!     type_utils::assert_type_eq,
12//! };
13//!
14//! assert_type_eq::<And<False, True>, False>();
15//! ```
16
17/// A Boolean value, encoded as a type.
18pub trait Bool {
19    /// The Boolean value as a [`bool`].
20    const VALUE: bool;
21
22    /// The negation of the Boolean value.
23    ///
24    /// The type alias [`Not<B>`] is a nicer way to access this.
25    type Not: Bool;
26
27    /// The value of `Self -> B`.
28    ///
29    /// The type alias [`Implies<A, B>`] is a nicer way to access this.
30    type Implies<B: Bool>: Bool;
31}
32
33/// The Boolean value True.
34pub struct True {}
35
36impl Bool for True {
37    const VALUE: bool = true;
38
39    type Not = False;
40
41    type Implies<B: Bool> = B;
42}
43
44/// The Boolean value False.
45pub struct False {}
46
47impl Bool for False {
48    const VALUE: bool = false;
49
50    type Not = True;
51
52    type Implies<B: Bool> = True;
53}
54
55/// Boolean negation:
56/// `¬B`
57#[allow(type_alias_bounds)]
58pub type Not<B>
59where
60    B: Bool,
61= <B as Bool>::Not;
62
63/// Boolean implication:
64/// `A -> B`
65#[allow(type_alias_bounds)]
66pub type Implies<A, B>
67where
68    A: Bool,
69    B: Bool,
70= <A as Bool>::Implies<B>;
71
72/// Boolean and:
73/// `A ∧ B`
74#[allow(type_alias_bounds)]
75pub type And<A, B>
76where
77    A: Bool,
78    B: Bool,
79= Not<Implies<A, Not<B>>>;
80
81/// Boolean or:
82/// `A ∨ B`
83#[allow(type_alias_bounds)]
84pub type Or<A, B>
85where
86    A: Bool,
87    B: Bool,
88= Not<And<Not<A>, Not<B>>>; // using De Morgan's laws
89
90/// Boolean xor:
91/// `A ⊕ B`
92#[allow(type_alias_bounds)]
93pub type Xor<A, B>
94where
95    A: Bool,
96    B: Bool,
97= And<Or<A, B>, Not<And<A, B>>>;
98
99/// Boolean equivalence:
100/// `A <-> B`, or equivalently, `A = B`
101#[allow(type_alias_bounds)]
102pub type Iff<A, B>
103where
104    A: Bool,
105    B: Bool,
106= And<Implies<A, B>, Implies<B, A>>;
107
108#[cfg(test)]
109mod tests {
110    use crate::type_utils::assert_type_eq;
111
112    use super::*;
113
114    #[test]
115    #[allow(clippy::bool_assert_comparison)]
116    fn value() {
117        assert_eq!(True::VALUE, true);
118        assert_eq!(False::VALUE, false);
119    }
120
121    #[test]
122    fn not() {
123        assert_type_eq::<False, Not<True>>();
124        assert_type_eq::<True, Not<False>>();
125    }
126
127    #[test]
128    fn and() {
129        assert_type_eq::<True, And<True, True>>();
130        assert_type_eq::<False, And<False, True>>();
131        assert_type_eq::<False, And<True, False>>();
132        assert_type_eq::<False, And<False, False>>();
133    }
134
135    #[test]
136    fn or() {
137        assert_type_eq::<True, Or<True, True>>();
138        assert_type_eq::<True, Or<False, True>>();
139        assert_type_eq::<True, Or<True, False>>();
140        assert_type_eq::<False, Or<False, False>>();
141    }
142
143    #[test]
144    fn xor() {
145        assert_type_eq::<False, Xor<True, True>>();
146        assert_type_eq::<True, Xor<False, True>>();
147        assert_type_eq::<True, Xor<True, False>>();
148        assert_type_eq::<False, Xor<False, False>>();
149    }
150
151    #[test]
152    fn implies() {
153        assert_type_eq::<True, Implies<True, True>>();
154        assert_type_eq::<True, Implies<False, True>>();
155        assert_type_eq::<False, Implies<True, False>>();
156        assert_type_eq::<True, Implies<False, False>>();
157    }
158}
type_proof/boolean.rs

type_proof/
boolean.rs
