module Data.Bifunctor.Disjunction
( -- * Disjunctions
  Disj(..)
, inlK
, inrK
, deMorganDisj
) where

import Data.Functor.Continuation
import Data.Functor.Identity (Identity(..))

-- Disjunctions

class Disj d where
  inl :: Functor f => f a -> f (a `d` b)
  inr :: Functor f => f b -> f (a `d` b)
  (<!!>) :: Representable k => k a -> k b -> k (a `d` b)
  infixr 3 <!!>

instance Disj Either where
  inl :: f a -> f (Either a b)
inl = (a -> Either a b) -> f a -> f (Either a b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a b
forall a b. a -> Either a b
Left
  inr :: f b -> f (Either a b)
inr = (b -> Either a b) -> f b -> f (Either a b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either a b
forall a b. b -> Either a b
Right
  k a
a <!!> :: k a -> k b -> k (Either a b)
<!!> k b
b = (Either a b -> Rep k) -> k (Either a b)
forall (f :: Type -> Type) a.
Representable f =>
(a -> Rep f) -> f a
tabulate ((a -> Rep k) -> (b -> Rep k) -> Either a b -> Rep k
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (k a -> a -> Rep k
forall (f :: Type -> Type) a. Representable f => f a -> a -> Rep f
index k a
a) (k b -> b -> Rep k
forall (f :: Type -> Type) a. Representable f => f a -> a -> Rep f
index k b
b))


inlK :: (Contravariant k, Disj d) => k (a `d` b) -> k a
inlK :: k (d a b) -> k a
inlK = (a -> d a b) -> k (d a b) -> k a
forall (f :: Type -> Type) a b.
Contravariant f =>
(a -> b) -> f b -> f a
contramap (Identity (d a b) -> d a b
forall a. Identity a -> a
runIdentity (Identity (d a b) -> d a b)
-> (a -> Identity (d a b)) -> a -> d a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity a -> Identity (d a b)
forall (d :: Type -> Type -> Type) (f :: Type -> Type) a b.
(Disj d, Functor f) =>
f a -> f (d a b)
inl (Identity a -> Identity (d a b))
-> (a -> Identity a) -> a -> Identity (d a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall a. a -> Identity a
Identity)

inrK :: (Contravariant k, Disj d) => k (a `d` b) -> k b
inrK :: k (d a b) -> k b
inrK = (b -> d a b) -> k (d a b) -> k b
forall (f :: Type -> Type) a b.
Contravariant f =>
(a -> b) -> f b -> f a
contramap (Identity (d a b) -> d a b
forall a. Identity a -> a
runIdentity (Identity (d a b) -> d a b)
-> (b -> Identity (d a b)) -> b -> d a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity b -> Identity (d a b)
forall (d :: Type -> Type -> Type) (f :: Type -> Type) b a.
(Disj d, Functor f) =>
f b -> f (d a b)
inr (Identity b -> Identity (d a b))
-> (b -> Identity b) -> b -> Identity (d a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Identity b
forall a. a -> Identity a
Identity)


deMorganDisj :: (Representable k, Disj d) => (k a, k b) -> k (a `d` b)
deMorganDisj :: (k a, k b) -> k (d a b)
deMorganDisj = (k a -> k b -> k (d a b)) -> (k a, k b) -> k (d a b)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry k a -> k b -> k (d a b)
forall (d :: Type -> Type -> Type) (k :: Type -> Type) a b.
(Disj d, Representable k) =>
k a -> k b -> k (d a b)
(<!!>)