{-# LANGUAGE AllowAmbiguousTypes #-}

module Pandora.Paradigm.Structure.Interface.Set where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Semigroupoid ((.))
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.Algebraic ()
import Pandora.Paradigm.Primary.Algebraic.Product (attached)
import Pandora.Paradigm.Primary.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.Structure.Ability.Morphable (Morphable (Morphing), Morph (Find), find)
import Pandora.Paradigm.Inventory.State (State, modify)
import Pandora.Paradigm.Controlflow.Effect (run)

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 source 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)
-> (State Numerator (t Numerator) -> Numerator :*: t Numerator)
-> State Numerator (t Numerator)
-> Numerator
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State Numerator) =>
State Numerator a -> Primary (State Numerator) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _) (State Numerator (t Numerator)
 -> ((->) Numerator :. (:*:) Numerator) := t Numerator)
-> Numerator
-> State Numerator (t Numerator)
-> Numerator :*: t Numerator
forall a b c. (a -> b -> c) -> b -> a -> c
% Numerator
Zero (State Numerator (t Numerator) -> Numerator)
-> State Numerator (t Numerator) -> Numerator
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ ((Numerator -> Numerator) -> State Numerator Numerator
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify @Numerator (Numerator -> Numerator -> Numerator
forall a. Semigroup a => a -> a -> a
+ Numerator
forall a. Quasiring a => a
one) State Numerator Numerator -> a -> State Numerator Numerator
forall a b. a -> b -> a
!.) (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 source target (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- t a
s