{-|
Module: Data.Type.Predicate
Description: statically analyzable predicates on generic types
Maintainer: Olaf Klinke
Stability: experimental

This module defines the GADT 'Predicate' 
and the category of predicate transformers.
-}
{-# LANGUAGE GADTs, PolyKinds, KindSignatures, TypeOperators, RankNTypes, ScopedTypeVariables #-}
module Data.Type.Predicate (
    -- * Predicates on polynomial types
    Predicate(..),
    eval,
    -- * Predicate transformers
    insL,
    insR,
    first,
    second,
    mapRec,
    mapMeta,
    mapConst,
    GStone(..),
    gDomain,
    -- * universal properties
    universalProd,
    universalUnion) where
import Type.Reflection (Typeable,SomeTypeRep,someTypeRep)
import Data.Kind (Type)
import Data.Proxy (Proxy(..))
import GHC.Generics
import Control.Applicative (liftA2)
import qualified Control.Category as Cat

-- | Predicates on Generic representations of polynomial types.
-- The only way to evaluate predicates on unions is to do 'Case' analysis.
-- All predicates on products must eventually extract the first or second component. 
data Predicate :: (Type -> Type) -> Type where
    Wildcard :: Predicate ty -- ^ the wildcard pattern
    Neg :: Predicate ty -> Predicate ty -- ^ logical negation
    (:\/) :: Predicate ty -> Predicate ty -> Predicate ty -- ^ logical disjunction
    (:/\) :: Predicate ty -> Predicate ty -> Predicate ty -- ^ logical conjunction
    Fst :: Predicate f -> Predicate (f :*: g)
    Snd :: Predicate g -> Predicate (f :*: g)
    Case :: Predicate f -> Predicate g -> Predicate (f :+: g)
    RecP :: Predicate f -> Predicate (Rec1 f)
    MetaP :: Predicate f -> Predicate (M1 i m f)
    ConstP :: (Generic c, Rep c ~ f) => Predicate f -> Predicate (K1 i c)
    
-- | evaluate a predicate
eval :: Predicate ty -> ty p -> Bool
eval :: forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate ty
Wildcard  ty p
_ = Bool
True
eval (Neg Predicate ty
p) ty p
x = Bool -> Bool
not (Predicate ty -> ty p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate ty
p ty p
x)
eval (Predicate ty
p :\/ Predicate ty
q) ty p
x = Predicate ty -> ty p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate ty
p ty p
x Bool -> Bool -> Bool
|| Predicate ty -> ty p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate ty
q ty p
x
eval (Predicate ty
p :/\ Predicate ty
q) ty p
x = Predicate ty -> ty p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate ty
p ty p
x Bool -> Bool -> Bool
&& Predicate ty -> ty p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate ty
q ty p
x
eval (Fst Predicate f
p) (f p
x :*: g p
_) = Predicate f -> f p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate f
p f p
x
eval (Snd Predicate g
p) (f p
_ :*: g p
x) = Predicate g -> g p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate g
p g p
x
eval (Case Predicate f
p Predicate g
_) (L1 f p
x) = Predicate f -> f p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate f
p f p
x
eval (Case Predicate f
_ Predicate g
p) (R1 g p
x) = Predicate g -> g p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate g
p g p
x
eval (RecP Predicate f
p) (Rec1 f p
x) = Predicate f -> f p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate f
p f p
x
eval (MetaP Predicate f
p) (M1 f p
x)  = Predicate f -> f p -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate f
p f p
x
eval (ConstP Predicate f
p) (K1 c
x) = Predicate f -> f Any -> Bool
forall (ty :: * -> *) p. Predicate ty -> ty p -> Bool
eval Predicate f
p (c -> Rep c Any
forall x. c -> Rep c x
forall a x. Generic a => a -> Rep a x
from c
x)

-- | universal property of the product @:*:@
-- and Stone dual of @(Control.Arrow.&&&)@. 
-- Notice that 'Fst' and 'Snd' are the Stone duals 
-- of 'fst' and 'snd', respectively. 
-- Accordingly, 
-- @'universalProd' 'Fst' 'Snd'@ 
-- is the identity.
universalProd :: 
    (Predicate a -> Predicate z) -> 
    (Predicate b -> Predicate z) -> 
    Predicate (a :*: b) -> Predicate z
universalProd :: forall (a :: * -> *) (z :: * -> *) (b :: * -> *).
(Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
_ (Fst Predicate f
p) = Predicate a -> Predicate z
f Predicate a
Predicate f
p
universalProd Predicate a -> Predicate z
_ Predicate b -> Predicate z
f (Snd Predicate g
p) = Predicate b -> Predicate z
f Predicate b
Predicate g
p
universalProd Predicate a -> Predicate z
_ Predicate b -> Predicate z
_ Predicate (a :*: b)
Wildcard = Predicate z
forall (ty :: * -> *). Predicate ty
Wildcard
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g (Neg Predicate (a :*: b)
p) = Predicate z -> Predicate z
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg ((Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
forall (a :: * -> *) (z :: * -> *) (b :: * -> *).
(Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g Predicate (a :*: b)
p)
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g (Predicate (a :*: b)
p :\/ Predicate (a :*: b)
q) = (Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
forall (a :: * -> *) (z :: * -> *) (b :: * -> *).
(Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g Predicate (a :*: b)
p Predicate z -> Predicate z -> Predicate z
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ (Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
forall (a :: * -> *) (z :: * -> *) (b :: * -> *).
(Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g Predicate (a :*: b)
q
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g (Predicate (a :*: b)
p :/\ Predicate (a :*: b)
q) = (Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
forall (a :: * -> *) (z :: * -> *) (b :: * -> *).
(Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g Predicate (a :*: b)
p Predicate z -> Predicate z -> Predicate z
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ (Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
forall (a :: * -> *) (z :: * -> *) (b :: * -> *).
(Predicate a -> Predicate z)
-> (Predicate b -> Predicate z)
-> Predicate (a :*: b)
-> Predicate z
universalProd Predicate a -> Predicate z
f Predicate b -> Predicate z
g Predicate (a :*: b)
q

-- | universal property of the union @:+:@
universalUnion :: 
    (Predicate z -> Predicate a) -> 
    (Predicate z -> Predicate b) -> 
    Predicate z -> Predicate (a :+: b)
universalUnion :: forall (z :: * -> *) (a :: * -> *) (b :: * -> *).
(Predicate z -> Predicate a)
-> (Predicate z -> Predicate b)
-> Predicate z
-> Predicate (a :+: b)
universalUnion = (Predicate a -> Predicate b -> Predicate (a :+: b))
-> (Predicate z -> Predicate a)
-> (Predicate z -> Predicate b)
-> Predicate z
-> Predicate (a :+: b)
forall a b c.
(a -> b -> c)
-> (Predicate z -> a) -> (Predicate z -> b) -> Predicate z -> c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Predicate a -> Predicate b -> Predicate (a :+: b)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate f -> Predicate (g :+: f)
Case

-- * Predicate transformers 

-- | Predicate transformers form a cartesian category.
-- We can regard an element of @'GStone' ('Rep' x) ('Rep' y)@
-- as the Stone dual of a function @x -> y@.
-- Instead of the pair @(,)@ in this category 
-- @:*:@ plays the role of the cartesian product. 
newtype GStone f g = GStone (Predicate g -> Predicate f)
instance Cat.Category GStone where
    id :: forall (a :: * -> *). GStone a a
id = (Predicate a -> Predicate a) -> GStone a a
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone Predicate a -> Predicate a
forall a. a -> a
id
    (GStone Predicate c -> Predicate b
h) . :: forall (b :: * -> *) (c :: * -> *) (a :: * -> *).
GStone b c -> GStone a b -> GStone a c
. (GStone Predicate b -> Predicate a
g) = (Predicate c -> Predicate a) -> GStone a c
forall (f :: * -> *) (g :: * -> *).
(Predicate g -> Predicate f) -> GStone f g
GStone (Predicate b -> Predicate a
g(Predicate b -> Predicate a)
-> (Predicate c -> Predicate b) -> Predicate c -> Predicate a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Predicate c -> Predicate b
h)

-- | The monomorphic type representation 
-- of the domain @f@ of the morphism,
-- instantiated at parameter @()@.
gDomain :: forall f g. Typeable (f ()) => GStone f g -> SomeTypeRep
gDomain :: forall (f :: * -> *) (g :: * -> *).
Typeable (f ()) =>
GStone f g -> SomeTypeRep
gDomain GStone f g
_ = Proxy (f ()) -> SomeTypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> SomeTypeRep
someTypeRep (Proxy (f ())
forall {k} (t :: k). Proxy t
Proxy :: Proxy (f ()))

-- | 'insL' witnesses the inclusion of @f@ into @f :+: g@.
-- Stone dual of 'Left'.
insL :: Predicate (f :+: g) -> Predicate f
insL :: forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
p = case Predicate (f :+: g)
p of
    Predicate (f :+: g)
Wildcard -> Predicate f
forall (ty :: * -> *). Predicate ty
Wildcard
    Neg Predicate (f :+: g)
q -> Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg (Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
q)
    Predicate (f :+: g)
q :\/ Predicate (f :+: g)
r -> Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
q Predicate f -> Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
r
    Predicate (f :+: g)
q :/\ Predicate (f :+: g)
r -> Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
q Predicate f -> Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ Predicate (f :+: g) -> Predicate f
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate f
insL Predicate (f :+: g)
r
    Case Predicate f
q Predicate g
_ -> Predicate f
Predicate f
q

-- | 'insR' witnesses the inclusion of @g@ into @f :+: g@.
-- Stone dual of 'Right'.
insR :: Predicate (f :+: g) -> Predicate g
insR :: forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
p = case Predicate (f :+: g)
p of
    Predicate (f :+: g)
Wildcard -> Predicate g
forall (ty :: * -> *). Predicate ty
Wildcard
    Neg Predicate (f :+: g)
q -> Predicate g -> Predicate g
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg (Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
q)
    Predicate (f :+: g)
q :\/ Predicate (f :+: g)
r -> Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
q Predicate g -> Predicate g -> Predicate g
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
r
    Predicate (f :+: g)
q :/\ Predicate (f :+: g)
r -> Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
q Predicate g -> Predicate g -> Predicate g
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ Predicate (f :+: g) -> Predicate g
forall (f :: * -> *) (g :: * -> *).
Predicate (f :+: g) -> Predicate g
insR Predicate (f :+: g)
r
    Case Predicate f
_ Predicate g
q -> Predicate g
Predicate g
q

-- | inverse to 'RecP'
mapRec :: Predicate (Rec1 f) -> Predicate f
mapRec :: forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec Predicate (Rec1 f)
Wildcard = Predicate f
forall (ty :: * -> *). Predicate ty
Wildcard
mapRec (Neg Predicate (Rec1 f)
p) = Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg (Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec Predicate (Rec1 f)
p)
mapRec (Predicate (Rec1 f)
p :\/ Predicate (Rec1 f)
q) = Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec Predicate (Rec1 f)
p Predicate f -> Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec Predicate (Rec1 f)
q
mapRec (Predicate (Rec1 f)
p :/\ Predicate (Rec1 f)
q) = Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec Predicate (Rec1 f)
p Predicate f -> Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ Predicate (Rec1 f) -> Predicate f
forall (f :: * -> *). Predicate (Rec1 f) -> Predicate f
mapRec Predicate (Rec1 f)
q
mapRec (RecP Predicate f
p) = Predicate f
Predicate f
p

-- | inverse to 'MetaP'
mapMeta :: Predicate (M1 i m f) -> Predicate f
mapMeta :: forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta Predicate (M1 i m f)
Wildcard = Predicate f
forall (ty :: * -> *). Predicate ty
Wildcard
mapMeta (Neg Predicate (M1 i m f)
p) = Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg (Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta Predicate (M1 i m f)
p)
mapMeta (Predicate (M1 i m f)
p :\/ Predicate (M1 i m f)
q) = Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta Predicate (M1 i m f)
p Predicate f -> Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta Predicate (M1 i m f)
q
mapMeta (Predicate (M1 i m f)
p :/\ Predicate (M1 i m f)
q) = Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta Predicate (M1 i m f)
p Predicate f -> Predicate f -> Predicate f
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ Predicate (M1 i m f) -> Predicate f
forall i (m :: Meta) (f :: * -> *).
Predicate (M1 i m f) -> Predicate f
mapMeta Predicate (M1 i m f)
q
mapMeta (MetaP Predicate f
p) = Predicate f
Predicate f
p

-- | inverse to 'ConstP'
mapConst :: Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst :: forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst Predicate (K1 i c)
Wildcard = Predicate (Rep c)
forall (ty :: * -> *). Predicate ty
Wildcard
mapConst (Neg Predicate (K1 i c)
p) = Predicate (Rep c) -> Predicate (Rep c)
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg (Predicate (K1 i c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst Predicate (K1 i c)
p)
mapConst (Predicate (K1 i c)
p :\/ Predicate (K1 i c)
q) = Predicate (K1 i c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst Predicate (K1 i c)
p Predicate (Rep c) -> Predicate (Rep c) -> Predicate (Rep c)
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ Predicate (K1 i c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst Predicate (K1 i c)
q
mapConst (Predicate (K1 i c)
p :/\ Predicate (K1 i c)
q) = Predicate (K1 i c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst Predicate (K1 i c)
p Predicate (Rep c) -> Predicate (Rep c) -> Predicate (Rep c)
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ Predicate (K1 i c) -> Predicate (Rep c)
forall c i. Generic c => Predicate (K1 i c) -> Predicate (Rep c)
mapConst Predicate (K1 i c)
q
mapConst (ConstP Predicate f
p) = Predicate f
Predicate (Rep c)
p 

-- | Stone dual of @Control.Arrow.first@
first :: (Predicate f -> Predicate g) -> Predicate (f :*: h) -> Predicate (g :*: h)
first :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
first Predicate f -> Predicate g
_ Predicate (f :*: h)
Wildcard = Predicate (g :*: h)
forall (ty :: * -> *). Predicate ty
Wildcard
first Predicate f -> Predicate g
f (Neg Predicate (f :*: h)
p) = Predicate (g :*: h) -> Predicate (g :*: h)
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg ((Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
first Predicate f -> Predicate g
f Predicate (f :*: h)
p)
first Predicate f -> Predicate g
f (Predicate (f :*: h)
p :/\ Predicate (f :*: h)
q) = (Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
first Predicate f -> Predicate g
f Predicate (f :*: h)
p Predicate (g :*: h) -> Predicate (g :*: h) -> Predicate (g :*: h)
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ (Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
first Predicate f -> Predicate g
f Predicate (f :*: h)
q
first Predicate f -> Predicate g
f (Predicate (f :*: h)
p :\/ Predicate (f :*: h)
q) = (Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
first Predicate f -> Predicate g
f Predicate (f :*: h)
p Predicate (g :*: h) -> Predicate (g :*: h) -> Predicate (g :*: h)
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ (Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (f :*: h) -> Predicate (g :*: h)
first Predicate f -> Predicate g
f Predicate (f :*: h)
q
first Predicate f -> Predicate g
f (Fst Predicate f
p) = Predicate g -> Predicate (g :*: h)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate (g :*: f)
Fst (Predicate f -> Predicate g
f Predicate f
Predicate f
p)
first Predicate f -> Predicate g
_ (Snd Predicate g
q) = Predicate h -> Predicate (g :*: h)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate (f :*: g)
Snd Predicate h
Predicate g
q

-- | Stone dual of @Control.Arrow.second@
second :: (Predicate f -> Predicate g) -> Predicate (h :*: f) -> Predicate (h :*: g)
second :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
second Predicate f -> Predicate g
_ Predicate (h :*: f)
Wildcard = Predicate (h :*: g)
forall (ty :: * -> *). Predicate ty
Wildcard
second Predicate f -> Predicate g
f (Neg Predicate (h :*: f)
p) = Predicate (h :*: g) -> Predicate (h :*: g)
forall (ty :: * -> *). Predicate ty -> Predicate ty
Neg ((Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
second Predicate f -> Predicate g
f Predicate (h :*: f)
p)
second Predicate f -> Predicate g
f (Predicate (h :*: f)
p :/\ Predicate (h :*: f)
q) = (Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
second Predicate f -> Predicate g
f Predicate (h :*: f)
p Predicate (h :*: g) -> Predicate (h :*: g) -> Predicate (h :*: g)
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:/\ (Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
second Predicate f -> Predicate g
f Predicate (h :*: f)
q
second Predicate f -> Predicate g
f (Predicate (h :*: f)
p :\/ Predicate (h :*: f)
q) = (Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
second Predicate f -> Predicate g
f Predicate (h :*: f)
p Predicate (h :*: g) -> Predicate (h :*: g) -> Predicate (h :*: g)
forall (ty :: * -> *). Predicate ty -> Predicate ty -> Predicate ty
:\/ (Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
(Predicate f -> Predicate g)
-> Predicate (h :*: f) -> Predicate (h :*: g)
second Predicate f -> Predicate g
f Predicate (h :*: f)
q
second Predicate f -> Predicate g
_ (Fst Predicate f
p) = Predicate h -> Predicate (h :*: g)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate (g :*: f)
Fst Predicate h
Predicate f
p
second Predicate f -> Predicate g
f (Snd Predicate g
q) = Predicate g -> Predicate (h :*: g)
forall (g :: * -> *) (f :: * -> *).
Predicate g -> Predicate (f :*: g)
Snd (Predicate f -> Predicate g
f Predicate f
Predicate g
q)

{-- TODO: does not compile
-- | Stone dual of @(Control.Arrow.***)@
pair :: (Predicate f -> Predicate f') -> 
    (Predicate g -> Predicate g') ->
    Predicate (f :*: f') -> Predicate (g :*: g')
pair _ _ Wildcard = Wildcard
pair f g (Neg p) = Neg (pair f g p)
pair f g (p :/\ q) = pair f g p :/\ pair f g q
pair f g (p :\/ q) = pair f g p :\/ pair f g q
pair f _ (Fst p) = Fst (f p)
pair _ g (Snd q) = Snd (g q)
--}