karpal_core/
conclude.rs

1use crate::contravariant::PredicateF;
2use crate::decide::Decide;
3#[cfg(all(not(feature = "std"), feature = "alloc"))]
4use alloc::boxed::Box;
5
6/// Conclude: the contravariant analogue of Plus.
7///
8/// Adds a `conclude` operation (the identity for `choose`).
9/// `conclude` takes a function `A -> Infallible`, witnessing that `A` is
10/// uninhabited — so the resulting predicate is vacuously true.
11///
12/// Laws:
13/// - Left identity: `choose(f, conclude(absurd), fa) ≈ contramap(from_right . f, fa)`
14/// - Right identity: `choose(f, fa, conclude(absurd)) ≈ contramap(from_left . f, fa)`
15pub trait Conclude: Decide {
16    fn conclude<A: 'static>(f: impl Fn(A) -> core::convert::Infallible + 'static) -> Self::Of<A>;
17}
18
19impl Conclude for PredicateF {
20    fn conclude<A: 'static>(
21        _f: impl Fn(A) -> core::convert::Infallible + 'static,
22    ) -> Box<dyn Fn(A) -> bool> {
23        // Vacuously true: if `f` could produce Infallible, `A` is uninhabited,
24        // so this predicate will never actually be called with a real value.
25        // For inhabited types, the predicate is simply always true.
26        Box::new(|_| true)
27    }
28}
29
30#[cfg(test)]
31mod tests {
32    use super::*;
33
34    #[test]
35    fn predicate_conclude() {
36        // For any inhabited type, conclude gives a predicate that's always true
37        let p: Box<dyn Fn(i32) -> bool> = PredicateF::conclude(|_: i32| unreachable!());
38        // We can't actually call it with the intent of testing the Infallible path,
39        // but we can test that the predicate is true for any value
40        assert!(p(42));
41        assert!(p(-1));
42    }
43}
44
45#[cfg(test)]
46mod law_tests {
47    use super::*;
48    use proptest::prelude::*;
49
50    proptest! {
51        // Left identity: choose(|a| Err(a), conclude(absurd), fa)(x) == fa(x)
52        #[test]
53        fn predicate_left_identity(x in any::<i32>()) {
54            let fa: Box<dyn Fn(i32) -> bool> = Box::new(|a| a > 0);
55            let expected = fa(x);
56
57            let fa2: Box<dyn Fn(i32) -> bool> = Box::new(|a| a > 0);
58            let result = PredicateF::choose(
59                |a: i32| -> Result<core::convert::Infallible, i32> { Err(a) },
60                PredicateF::conclude(|i: core::convert::Infallible| -> core::convert::Infallible { i }),
61                fa2,
62            );
63            prop_assert_eq!(result(x), expected);
64        }
65
66        // Right identity: choose(|a| Ok(a), fa, conclude(absurd))(x) == fa(x)
67        #[test]
68        fn predicate_right_identity(x in any::<i32>()) {
69            let fa: Box<dyn Fn(i32) -> bool> = Box::new(|a| a > 0);
70            let expected = fa(x);
71
72            let fa2: Box<dyn Fn(i32) -> bool> = Box::new(|a| a > 0);
73            let result = PredicateF::choose(
74                |a: i32| -> Result<i32, core::convert::Infallible> { Ok(a) },
75                fa2,
76                PredicateF::conclude(|i: core::convert::Infallible| -> core::convert::Infallible { i }),
77            );
78            prop_assert_eq!(result(x), expected);
79        }
80    }
81}
karpal_core/conclude.rs

karpal_core/
conclude.rs
