karpal_core/
conclude.rs

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

karpal_core/
conclude.rs
