karpal_core/
conclude.rs

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

karpal_core/
conclude.rs
