module Pandora.Paradigm.Primary.Functor.Predicate where import Pandora.Core.Functor (type (~>), type (:=>)) import Pandora.Core.Interpreted (Interpreted (Primary, run, unite)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category ((<--)) import Pandora.Pattern.Morphism.Straight (Straight (Straight)) import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-))) import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult)) import Pandora.Pattern.Functor.Monoidal (Monoidal (unit)) import Pandora.Pattern.Object.Setoid (Setoid ((==))) import Pandora.Pattern.Object.Ringoid (Ringoid ((*))) import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False), bool) import Pandora.Paradigm.Algebraic.Product ((:*:)((:*:))) import Pandora.Paradigm.Algebraic.Sum ((:+:)(Option, Adoption)) import Pandora.Paradigm.Algebraic.Exponential (type (-->), type (<--)) newtype Predicate a = Predicate (a -> Boolean) instance Interpreted (->) Predicate where type Primary Predicate a = a -> Boolean run :: ((->) < Predicate a) < Primary Predicate a run ~(Predicate a -> Boolean f) = Primary Predicate a a -> Boolean f unite :: ((->) < Primary Predicate a) < Predicate a unite = ((->) < Primary Predicate a) < Predicate a forall a. (a -> Boolean) -> Predicate a Predicate instance Contravariant (->) (->) Predicate where a -> b f >-|- :: (a -> b) -> Predicate b -> Predicate a >-|- Predicate b -> Boolean g = (a -> Boolean) -> Predicate a forall a. (a -> Boolean) -> Predicate a Predicate ((a -> Boolean) -> Predicate a) -> (a -> Boolean) -> Predicate a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- b -> Boolean g (b -> Boolean) -> (a -> b) -> a -> Boolean forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> b f instance Semimonoidal (-->) (:*:) (:*:) Predicate where mult :: (Predicate a :*: Predicate b) --> Predicate (a :*: b) mult = ((Predicate a :*: Predicate b) -> Predicate (a :*: b)) -> (Predicate a :*: Predicate b) --> Predicate (a :*: b) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Predicate a :*: Predicate b) -> Predicate (a :*: b)) -> (Predicate a :*: Predicate b) --> Predicate (a :*: b)) -> ((Predicate a :*: Predicate b) -> Predicate (a :*: b)) -> (Predicate a :*: Predicate b) --> Predicate (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Predicate a -> Boolean f :*: Predicate b -> Boolean g) -> ((a :*: b) -> Boolean) -> Predicate (a :*: b) forall a. (a -> Boolean) -> Predicate a Predicate (((a :*: b) -> Boolean) -> Predicate (a :*: b)) -> ((a :*: b) -> Boolean) -> Predicate (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(a x :*: b y) -> a -> Boolean f a x Boolean -> Boolean -> Boolean forall a. Ringoid a => a -> a -> a * b -> Boolean g b y instance Monoidal (-->) (<--) (:*:) (:*:) Predicate where unit :: Proxy (:*:) -> (Unit (:*:) <-- a) --> Predicate a unit Proxy (:*:) _ = ((Unit (:*:) <-- a) -> Predicate a) -> (Unit (:*:) <-- a) --> Predicate a forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Unit (:*:) <-- a) -> Predicate a) -> (Unit (:*:) <-- a) --> Predicate a) -> ((Unit (:*:) <-- a) -> Predicate a) -> (Unit (:*:) <-- a) --> Predicate a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \Unit (:*:) <-- a _ -> (a -> Boolean) -> Predicate a forall a. (a -> Boolean) -> Predicate a Predicate ((a -> Boolean) -> Predicate a) -> (a -> Boolean) -> Predicate a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \a _ -> Boolean True instance Semimonoidal (-->) (:*:) (:+:) Predicate where mult :: (Predicate a :*: Predicate b) --> Predicate (a :+: b) mult = ((Predicate a :*: Predicate b) -> Predicate (a :+: b)) -> (Predicate a :*: Predicate b) --> Predicate (a :+: b) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Predicate a :*: Predicate b) -> Predicate (a :+: b)) -> (Predicate a :*: Predicate b) --> Predicate (a :+: b)) -> ((Predicate a :*: Predicate b) -> Predicate (a :+: b)) -> (Predicate a :*: Predicate b) --> Predicate (a :+: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Predicate a -> Boolean f :*: Predicate b -> Boolean g) -> ((a :+: b) -> Boolean) -> Predicate (a :+: b) forall a. (a -> Boolean) -> Predicate a Predicate (((a :+: b) -> Boolean) -> Predicate (a :+: b)) -> ((a :+: b) -> Boolean) -> Predicate (a :+: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \case Option a x -> a -> Boolean f a x Adoption b y -> b -> Boolean g b y equate :: Setoid a => a :=> Predicate equate :: a :=> Predicate equate a x = (a -> Boolean) -> Predicate a forall a. (a -> Boolean) -> Predicate a Predicate (a -> a -> Boolean forall a. Setoid a => a -> a -> Boolean == a x) not :: Predicate ~> Predicate not :: Predicate a -> Predicate a not (Predicate a -> Boolean p) = (a -> Boolean) -> Predicate a forall a. (a -> Boolean) -> Predicate a Predicate ((a -> Boolean) -> Predicate a) -> (a -> Boolean) -> Predicate a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- Boolean -> Boolean -> Boolean -> Boolean forall a. a -> a -> Boolean -> a bool Boolean True Boolean False (Boolean -> Boolean) -> (a -> Boolean) -> a -> Boolean forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . a -> Boolean p