{-# LANGUAGE AllowAmbiguousTypes #-} module Pandora.Paradigm.Structure.Interface.Set where import Pandora.Core.Functor (type (>), type (>>>>>>)) import Pandora.Core.Interpreted ((<~~)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category ((<--), (<---)) import Pandora.Pattern.Kernel (constant) 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.Algebraic () import Pandora.Paradigm.Algebraic.Product (attached) import Pandora.Paradigm.Algebraic.Exponential ((%)) import Pandora.Paradigm.Primary.Functor.Convergence (Convergence (Convergence)) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Nothing)) import Pandora.Paradigm.Primary.Functor.Predicate (Predicate, equate) import Pandora.Paradigm.Primary.Object.Boolean (Boolean) import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Zero)) import Pandora.Paradigm.Schemes.T_U (type (<:.:>)) import Pandora.Paradigm.Inventory.Ability.Modifiable (modify) import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing), Morph (Find), find) import Pandora.Paradigm.Inventory.Some.State (State) type Set t f a = (Traversable (->) (->) t, Setoid a, Setoid (t a), Morphable (Find f) t) subset :: forall t f a . (Set t f a, Morphing (Find f) t ~ (Predicate <:.:> Maybe >>>>>> (->))) => Convergence Boolean > t a subset :: Convergence Boolean > t a subset = (t a -> t a -> Boolean) -> Convergence Boolean > t a forall r a. (a -> a -> r) -> Convergence r a Convergence ((t a -> t a -> Boolean) -> Convergence Boolean > t a) -> (t a -> t a -> Boolean) -> Convergence Boolean > t a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \t a s t a ss -> Maybe (t a) forall a. Maybe a Nothing Maybe (t a) -> Maybe (t a) -> Boolean forall a. Setoid a => a -> a -> Boolean != ((forall a2. Morphed ('Find f) t ((Predicate <:.:> Maybe) >>>>>> (->)) => Predicate a2 -> t a2 -> Maybe a2 forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2. Morphed ('Find mod) struct ((Predicate <:.:> result) >>>>>> (->)) => Predicate a2 -> struct a2 -> result a2 find @f @t @Maybe (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. Semigroupoid m => m b c -> m a b -> m a c . a -> Predicate a forall a. Setoid a => a :=> Predicate equate (a -> Maybe a) -> t a -> Maybe (t a) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Traversable source target t, Covariant source target u, Monoidal (Straight source) (Straight target) (:*:) (:*:) u) => source a (u b) -> target (t a) (u (t b)) <<- t a ss) cardinality :: Traversable (->) (->) t => t a -> Numerator cardinality :: t a -> Numerator cardinality t a s = (Numerator :*: t Numerator) -> Numerator forall a b. (a :*: b) -> a attached ((Numerator :*: t Numerator) -> Numerator) -> (Numerator :*: t Numerator) -> Numerator forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <--- State Numerator Numerator -> a -> State Numerator Numerator forall (m :: * -> * -> *) a i. Kernel m => m a (m i a) constant ((Numerator -> Numerator) -> State Numerator Numerator forall k (i :: k) e r. Modifiable i => Modification i e r modify @State (Numerator -> Numerator -> Numerator forall a. Semigroup a => a -> a -> a + Numerator forall a. Quasiring a => a one)) (a -> State Numerator Numerator) -> t a -> State Numerator (t Numerator) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Traversable source target t, Covariant source target u, Monoidal (Straight source) (Straight target) (:*:) (:*:) u) => source a (u b) -> target (t a) (u (t b)) <<- t a s State Numerator (t Numerator) -> ((->) Numerator :. (:*:) Numerator) >>> t Numerator forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a <~~ Numerator Zero