{-# LANGUAGE AllowAmbiguousTypes #-}

module Pandora.Paradigm.Structure.Interface.Set where

import Pandora.Core.Functor (type (:=))
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.Function ((!), (%))
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.Functor.Product (attached)
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 :: * -> * -> *). Category m => m ~~> m
$ \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
!= 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
->> forall a2.
(Morphable ('Find f) t,
 Morphing ('Find f) t ~ ((Predicate <:.:> Maybe) := (->))) =>
Predicate a2 -> t a2 -> Maybe a2
forall a1 (f :: a1) (t :: * -> *) (u :: * -> *) a2.
(Morphable ('Find f) t,
 Morphing ('Find f) t ~ ((Predicate <:.:> u) := (->))) =>
Predicate a2 -> t a2 -> u 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.
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 -> 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.
Category 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 :: * -> * -> *). Category m => m ~~> m
$ t a
s t a
-> (a -> State Numerator Numerator)
-> State Numerator (t Numerator)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := 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
!)