module Data.Bifunctor.Conjunction
( -- * Conjunctions
  Conj(..)
, exlF
, exrF
, deMorganConj
) where

import Control.Applicative (liftA2)
import Data.Functor.Continuation

-- Conjunctions

class Conj c where
  (>!!<) :: Applicative f => f a -> f b -> f (a `c` b)
  infixr 3 >!!<
  exl :: Contravariant k => k a -> k (a `c` b)
  exr :: Contravariant k => k b -> k (a `c` b)

instance Conj (,) where
  >!!< :: f a -> f b -> f (a, b)
(>!!<) = (a -> b -> (a, b)) -> f a -> f b -> f (a, b)
forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,)
  exl :: k a -> k (a, b)
exl = ((a, b) -> a) -> k a -> k (a, b)
forall (f :: Type -> Type) a b.
Contravariant f =>
(a -> b) -> f b -> f a
contramap (a, b) -> a
forall a b. (a, b) -> a
fst
  exr :: k b -> k (a, b)
exr = ((a, b) -> b) -> k b -> k (a, b)
forall (f :: Type -> Type) a b.
Contravariant f =>
(a -> b) -> f b -> f a
contramap (a, b) -> b
forall a b. (a, b) -> b
snd


exlF :: (Functor f, Conj c) => f (a `c` b) -> f a
exlF :: f (c a b) -> f a
exlF = (c a b -> a) -> f (c a b) -> f a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a ! a) -> a ! c a b
forall (c :: Type -> Type -> Type) (k :: Type -> Type) a b.
(Conj c, Contravariant k) =>
k a -> k (c a b)
exl a ! a
forall a. a ! a
idK (a ! c a b) -> c a b -> a
forall r a. (r ! a) -> a -> r
!)

exrF :: (Functor f, Conj c) => f (a `c` b) -> f b
exrF :: f (c a b) -> f b
exrF = (c a b -> b) -> f (c a b) -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b ! b) -> b ! c a b
forall (c :: Type -> Type -> Type) (k :: Type -> Type) b a.
(Conj c, Contravariant k) =>
k b -> k (c a b)
exr b ! b
forall a. a ! a
idK (b ! c a b) -> c a b -> b
forall r a. (r ! a) -> a -> r
!)


deMorganConj :: (Contravariant k, Conj c) => Either (k a) (k b) -> k (a `c` b)
deMorganConj :: Either (k a) (k b) -> k (c a b)
deMorganConj = k a -> k (c a b)
forall (c :: Type -> Type -> Type) (k :: Type -> Type) a b.
(Conj c, Contravariant k) =>
k a -> k (c a b)
exl (k a -> k (c a b))
-> (k b -> k (c a b)) -> Either (k a) (k b) -> k (c a b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
`either` k b -> k (c a b)
forall (c :: Type -> Type -> Type) (k :: Type -> Type) b a.
(Conj c, Contravariant k) =>
k b -> k (c a b)
exr