module Pandora.Paradigm.Structure.Interface.Set where import Pandora.Core.Morphism ((!), (%)) import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Traversable (Traversable ((->>))) import Pandora.Pattern.Object.Setoid (Setoid ((/=))) import Pandora.Pattern.Object.Semigroup ((+)) import Pandora.Pattern.Object.Quasiring (one) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Nothing)) import Pandora.Paradigm.Primary.Functor.Predicate (equate) import Pandora.Paradigm.Primary.Functor.Product (attached) import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False)) import Pandora.Paradigm.Primary.Object.Natural (Natural (Zero)) import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce), find) import Pandora.Paradigm.Inventory.State (State, modify) import Pandora.Paradigm.Controlflow.Effect (run) member :: forall e a . (Setoid a, Monotonic e a) => a -> e -> Boolean member :: a -> e -> Boolean member a x = (a -> Boolean -> Boolean) -> Boolean -> Maybe a -> Boolean forall e a r. Monotonic e a => (a -> r -> r) -> r -> e -> r reduce @(Maybe a) @a (\a _ Boolean _ -> Boolean True) Boolean False (Maybe a -> Boolean) -> (e -> Maybe a) -> e -> Boolean forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Predicate a -> e -> Maybe a forall e a (t :: * -> *). (Monotonic e a, Pointable t, Avoidable t) => Predicate a -> e -> t a find (a |-> Predicate forall a. Setoid a => a |-> Predicate equate a x) subset :: (Monotonic (t a) a, Traversable t, Setoid a, Setoid (t a)) => t a -> t a -> Boolean subset :: t a -> t a -> Boolean subset t a ss t a s = Maybe (t a) forall a. Maybe a Nothing Maybe (t a) -> Maybe (t a) -> Boolean forall a. Setoid a => a -> a -> Boolean /= (t a ss t a -> (a -> Maybe a) -> Maybe (t a) forall (t :: * -> *) (u :: * -> *) a b. (Traversable t, Pointable u, Applicative u) => t a -> (a -> u b) -> (u :. t) := b ->> Predicate a -> t a -> Maybe a forall e a (t :: * -> *). (Monotonic e a, Pointable t, Avoidable t) => Predicate a -> e -> t a find (Predicate a -> t a -> Maybe a) -> t a -> Predicate a -> Maybe a forall a b c. (a -> b -> c) -> b -> a -> c % t a s (Predicate a -> Maybe a) -> (a -> Predicate a) -> a -> Maybe a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Predicate a forall a. Setoid a => a |-> Predicate equate) cardinality :: Traversable t => t a -> Natural cardinality :: t a -> Natural cardinality t a s = (Natural :*: t ()) -> Natural forall a b. (a :*: b) -> a attached ((Natural :*: t ()) -> Natural) -> (State Natural (t ()) -> Natural :*: t ()) -> State Natural (t ()) -> Natural forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . forall a. Interpreted (State Natural) => State Natural a -> Primary (State Natural) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run @(State _) (State Natural (t ()) -> ((->) Natural :. (:*:) Natural) := t ()) -> Natural -> State Natural (t ()) -> Natural :*: t () forall a b c. (a -> b -> c) -> b -> a -> c % Natural Zero (State Natural (t ()) -> Natural) -> State Natural (t ()) -> Natural forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ t a s t a -> (a -> State Natural ()) -> State Natural (t ()) forall (t :: * -> *) (u :: * -> *) a b. (Traversable t, Pointable u, Applicative u) => t a -> (a -> u b) -> (u :. t) := b ->> (!) ((Natural -> Natural) -> State Natural () forall s (t :: * -> *). Stateful s t => (s -> s) -> t () modify @Natural (Natural -> Natural -> Natural forall a. Semigroup a => a -> a -> a + Natural forall a. Quasiring a => a one))