fp_library/types/
conjunctive.rs

1//! A newtype wrapper whose [`Semigroup`](crate::classes::Semigroup) and [`Monoid`](crate::classes::Monoid) instances use
2//! conjunction from [`HeytingAlgebra`](crate::classes::HeytingAlgebra).
3//!
4//! ### Examples
5//!
6//! ```
7//! use fp_library::{
8//! 	functions::*,
9//! 	types::Conjunctive,
10//! };
11//!
12//! assert_eq!(append(Conjunctive(true), Conjunctive(false)), Conjunctive(false));
13//! assert_eq!(empty::<Conjunctive<bool>>(), Conjunctive(true));
14//! ```
15
16#[fp_macros::document_module]
17mod inner {
18	use {
19		crate::classes::*,
20		fp_macros::*,
21	};
22
23	/// A newtype wrapper whose [`Semigroup`] instance uses
24	/// [`HeytingAlgebra::conjoin`].
25	///
26	/// This provides a [`Monoid`] based on logical conjunction (AND),
27	/// with [`HeytingAlgebra::true_value`] as the identity element.
28	#[document_examples]
29	///
30	/// ```
31	/// use fp_library::{
32	/// 	functions::*,
33	/// 	types::Conjunctive,
34	/// };
35	///
36	/// assert_eq!(append(Conjunctive(true), Conjunctive(true)), Conjunctive(true));
37	/// assert_eq!(append(Conjunctive(true), Conjunctive(false)), Conjunctive(false));
38	/// assert_eq!(empty::<Conjunctive<bool>>(), Conjunctive(true));
39	/// ```
40	#[derive(Clone, Copy, Debug, Default, Eq, Hash, Ord, PartialEq, PartialOrd)]
41	pub struct Conjunctive<A>(
42		/// The wrapped value.
43		pub A,
44	);
45
46	#[document_type_parameters("The Heyting algebra type.")]
47	impl<A: HeytingAlgebra> Semigroup for Conjunctive<A> {
48		/// Combines two values using [`HeytingAlgebra::conjoin`].
49		#[document_signature]
50		///
51		#[document_parameters("The first conjunctive value.", "The second conjunctive value.")]
52		///
53		#[document_returns("The conjunction wrapped in `Conjunctive`.")]
54		#[document_examples]
55		///
56		/// ```
57		/// use fp_library::{
58		/// 	functions::*,
59		/// 	types::Conjunctive,
60		/// };
61		///
62		/// assert_eq!(append(Conjunctive(true), Conjunctive(true)), Conjunctive(true));
63		/// ```
64		fn append(
65			a: Self,
66			b: Self,
67		) -> Self {
68			Conjunctive(A::conjoin(a.0, b.0))
69		}
70	}
71
72	#[document_type_parameters("The Heyting algebra type.")]
73	impl<A: HeytingAlgebra> Monoid for Conjunctive<A> {
74		/// Returns `Conjunctive(true_value())`.
75		#[document_signature]
76		///
77		#[document_returns("The top element wrapped in `Conjunctive`.")]
78		#[document_examples]
79		///
80		/// ```
81		/// use fp_library::{
82		/// 	functions::*,
83		/// 	types::Conjunctive,
84		/// };
85		///
86		/// assert_eq!(empty::<Conjunctive<bool>>(), Conjunctive(true));
87		/// ```
88		fn empty() -> Self {
89			Conjunctive(A::true_value())
90		}
91	}
92}
93
94pub use inner::*;
95
96#[cfg(test)]
97mod tests {
98	use {
99		super::*,
100		crate::functions::*,
101		quickcheck_macros::quickcheck,
102	};
103
104	#[quickcheck]
105	fn semigroup_associativity(
106		a: bool,
107		b: bool,
108		c: bool,
109	) -> bool {
110		let x = Conjunctive(a);
111		let y = Conjunctive(b);
112		let z = Conjunctive(c);
113		append(x, append(y, z)) == append(append(x, y), z)
114	}
115
116	#[quickcheck]
117	fn monoid_left_identity(a: bool) -> bool {
118		let x = Conjunctive(a);
119		append(empty::<Conjunctive<bool>>(), x) == x
120	}
121
122	#[quickcheck]
123	fn monoid_right_identity(a: bool) -> bool {
124		let x = Conjunctive(a);
125		append(x, empty::<Conjunctive<bool>>()) == x
126	}
127}
fp_library/types/conjunctive.rs

fp_library/types/
conjunctive.rs
