-- |
-- Module      : Data.Functor.Invariant.Night
-- Copyright   : (c) Justin Le 2019
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Provides an 'Invariant' version of a Day convolution over 'Either'.
--
-- @since 0.3.0.0
module Data.Functor.Invariant.Night (
    Night(..)
  , Not(..), refuted
  , night
  , runNight
  , nerve
  , runNightAlt
  , runNightDecide
  , toCoNight
  , toCoNight_
  , toContraNight
  , assoc, unassoc
  , intro1, intro2
  , elim1, elim2
  , swapped
  , trans1, trans2
  ) where

import           Control.Natural
import           Data.Bifunctor
import           Data.Functor.Alt
import           Data.Functor.Contravariant.Decide
import           Data.Functor.Contravariant.Night  (Not(..), refuted)
import           Data.Functor.Invariant
import           Data.Functor.Invariant.Internative
import           Data.Kind
import           Data.Void
import           GHC.Generics
import qualified Data.Bifunctor.Assoc              as B
import qualified Data.Bifunctor.Swap               as B
import qualified Data.Functor.Contravariant.Night  as CN
import qualified Data.Functor.Coyoneda             as CY

-- | A pairing of invariant functors to create a new invariant functor that
-- represents the "choice" between the two.
--
-- A @'Night' f g a@ is a invariant "consumer" and "producer" of @a@, and
-- it does this by either feeding the @a@ to @f@, or feeding the @a@ to
-- @g@, and then collecting the result from whichever one it was fed to.
-- Which decision of which path to takes happens at runtime depending
-- /what/ @a@ is actually given.
--
-- For example, if we have @x :: f a@ and @y :: g b@, then @'night' x y ::
-- 'Night' f g ('Either' a b)@.  This is a consumer/producer of @'Either' a b@s, and
-- it consumes 'Left' branches by feeding it to @x@, and 'Right' branches
-- by feeding it to @y@.  It then passes back the single result from the one of
-- the two that was chosen.
--
-- Mathematically, this is a invariant day convolution, except with
-- a different choice of bifunctor ('Either') than the typical one we talk
-- about in Haskell (which uses @(,)@).  Therefore, it is an alternative to
-- the typical 'Data.Functor.Day' convolution --- hence, the name 'Night'.
data Night :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
    Night :: f b
          -> g c
          -> (b -> a)
          -> (c -> a)
          -> (a -> Either b c)
          -> Night f g a

instance Invariant (Night f g) where
    invmap :: forall a b. (a -> b) -> (b -> a) -> Night f g a -> Night f g b
invmap a -> b
f b -> a
g (Night f b
x g c
y b -> a
h c -> a
j a -> Either b c
k) = forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x g c
y (a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
h) (a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> a
j) (a -> Either b c
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g)

-- | Pair two invariant actions together into a 'Night'; assigns the first
-- one to 'Left' inputs and outputs and the second one to 'Right' inputs
-- and outputs.
night :: f a -> g b -> Night f g (Either a b)
night :: forall (f :: * -> *) a (g :: * -> *) b.
f a -> g b -> Night f g (Either a b)
night f a
x g b
y = forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f a
x g b
y forall a b. a -> Either a b
Left forall a b. b -> Either a b
Right forall a. a -> a
id

-- | Interpret the covariant part of a 'Night' into a target context @h@,
-- as long as the context is an instance of 'Alt'.  The 'Alt' is used to
-- combine results back together, chosen by '<!>'.
runNightAlt
    :: forall f g h. Alt h
    => f ~> h
    -> g ~> h
    -> Night f g ~> h
runNightAlt :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Alt h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightAlt f ~> h
f g ~> h
g (Night f b
x g c
y b -> x
h c -> x
j x -> Either b c
_) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> x
h (f ~> h
f f b
x) forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> x
j (g ~> h
g g c
y)

-- | Interpret the contravariant part of a 'Night' into a target context
-- @h@, as long as the context is an instance of 'Decide'.  The 'Decide' is
-- used to pick which part to feed the input to.
runNightDecide
    :: forall f g h. Decide h
    => f ~> h
    -> g ~> h
    -> Night f g ~> h
runNightDecide :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Decide h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightDecide f ~> h
f g ~> h
g (Night f b
x g c
y b -> x
_ c -> x
_ x -> Either b c
k) = forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either b c
k (f ~> h
f f b
x) (g ~> h
g g c
y)

-- | Convert an invariant 'Night' into the covariant version, dropping the
-- contravariant part.
--
-- Note that there is no covariant version of 'Night' defined in any common
-- library, so we use an equivalent type (if @f@ and @g@ are 'Functor's) @f
-- ':*:' g@.
toCoNight :: (Functor f, Functor g) => Night f g ~> f :*: g
toCoNight :: forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g) =>
Night f g ~> (f :*: g)
toCoNight (Night f b
x g c
y b -> x
f c -> x
g x -> Either b c
_) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> x
f f b
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> x
g g c
y

-- | Convert an invariant 'Night' into the covariant version, dropping the
-- contravariant part.
--
-- This version does not require a 'Functor' constraint because it converts
-- to the coyoneda-wrapped product, which is more accurately the covariant
-- 'Night' convolution.
--
-- @since 0.3.2.0
toCoNight_ :: Night f g ~> CY.Coyoneda f :*: CY.Coyoneda g
toCoNight_ :: forall (f :: * -> *) (g :: * -> *).
Night f g ~> (Coyoneda f :*: Coyoneda g)
toCoNight_ (Night f b
x g c
y b -> x
f c -> x
g x -> Either b c
_) = forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b -> x
f f b
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda c -> x
g g c
y


-- | Convert an invariant 'Night' into the contravariant version, dropping
-- the covariant part.
toContraNight :: Night f g ~> CN.Night f g
toContraNight :: forall (f :: * -> *) (g :: * -> *). Night f g ~> Night f g
toContraNight (Night f b
x g c
y b -> x
_ c -> x
_ x -> Either b c
h) = forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1 -> b c1 -> (c -> Either b1 c1) -> Night a b c
CN.Night f b
x g c
y x -> Either b c
h

-- | Interpret out of a 'Night' into any instance of 'Inalt' by providing
-- two interpreting functions.
--
-- @since 0.4.0.0
runNight
    :: Inalt h
    => (f ~> h)
    -> (g ~> h)
    -> Night f g ~> h
runNight :: forall (h :: * -> *) (f :: * -> *) (g :: * -> *).
Inalt h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNight f ~> h
f g ~> h
g (Night f b
x g c
y b -> x
a c -> x
b x -> Either b c
c) = forall (f :: * -> *) b a c.
Inalt f =>
(b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> f c -> f a
swerve b -> x
a c -> x
b x -> Either b c
c (f ~> h
f f b
x) (g ~> h
g g c
y)

-- | Squash the two items in a 'Night' using their natural 'Inalt'
-- instances.
--
-- @since 0.4.0.0
nerve
    :: Inalt f
    => Night f f ~> f
nerve :: forall (f :: * -> *). Inalt f => Night f f ~> f
nerve (Night f b
x f c
y b -> x
a c -> x
b x -> Either b c
c) = forall (f :: * -> *) b a c.
Inalt f =>
(b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> f c -> f a
swerve b -> x
a c -> x
b x -> Either b c
c f b
x f c
y

-- | 'Night' is associative.
assoc :: Night f (Night g h) ~> Night (Night f g) h
assoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Night f (Night g h) ~> Night (Night f g) h
assoc (Night f b
x (Night g b
y h c
z b -> c
f c -> c
g c -> Either b c
h) b -> x
j c -> x
k x -> Either b c
l) =
    forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night (forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x g b
y forall a b. a -> Either a b
Left forall a b. b -> Either a b
Right forall a. a -> a
id) h c
z
      (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> x
j (c -> x
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
f))
      (c -> x
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> c
g)
      (forall (p :: * -> * -> *) a b c.
Assoc p =>
p a (p b c) -> p (p a b) c
B.unassoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second c -> Either b c
h forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
l)

-- | 'Night' is associative.
unassoc :: Night (Night f g) h ~> Night f (Night g h)
unassoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Night (Night f g) h ~> Night f (Night g h)
unassoc (Night (Night f b
x g c
y b -> b
f c -> b
g b -> Either b c
h) h c
z b -> x
j c -> x
k x -> Either b c
l) =
    forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x (forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night g c
y h c
z forall a b. a -> Either a b
Left forall a b. b -> Either a b
Right forall a. a -> a
id)
      (b -> x
j forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b
f)
      (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> x
j forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> b
g) c -> x
k)
      (forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> Either b c
h forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
l)
      -- (k . g)
      -- (either (k . h) l)

-- | The left identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
intro1 :: g ~> Night Not g
intro1 :: forall (g :: * -> *). g ~> Night Not g
intro1 g x
y = forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night Not Void
refuted g x
y forall a. Void -> a
absurd forall a. a -> a
id forall a b. b -> Either a b
Right

-- | The right identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
intro2 :: f ~> Night f Not
intro2 :: forall (f :: * -> *). f ~> Night f Not
intro2 f x
x = forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f x
x Not Void
refuted forall a. a -> a
id forall a. Void -> a
absurd forall a b. a -> Either a b
Left

-- | The left identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
elim1 :: Invariant g => Night Not g ~> g
elim1 :: forall (g :: * -> *). Invariant g => Night Not g ~> g
elim1 (Night Not b
x g c
y b -> x
_ c -> x
g x -> Either b c
h) = forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap c -> x
g (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. Void -> a
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Not a -> a -> Void
refute Not b
x) forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
h) g c
y

-- | The right identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
elim2 :: Invariant f => Night f Not ~> f
elim2 :: forall (f :: * -> *). Invariant f => Night f Not ~> f
elim2 (Night f b
x Not c
y b -> x
f c -> x
_ x -> Either b c
h) = forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap b -> x
f (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id (forall a. Void -> a
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Not a -> a -> Void
refute Not c
y) forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
h) f b
x

-- | The two sides of a 'Night' can be swapped.
swapped :: Night f g ~> Night g f
swapped :: forall (f :: * -> *) (g :: * -> *). Night f g ~> Night g f
swapped (Night f b
x g c
y b -> x
f c -> x
g x -> Either b c
h) = forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night g c
y f b
x c -> x
g b -> x
f (forall (p :: * -> * -> *) a b. Swap p => p a b -> p b a
B.swap forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
h)

-- | Hoist a function over the left side of a 'Night'.
trans1 :: f ~> h -> Night f g ~> Night h g
trans1 :: forall (f :: * -> *) (h :: * -> *) (g :: * -> *).
(f ~> h) -> Night f g ~> Night h g
trans1 f ~> h
f (Night f b
x g c
y b -> x
g c -> x
h x -> Either b c
j) = forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night (f ~> h
f f b
x) g c
y b -> x
g c -> x
h x -> Either b c
j

-- | Hoist a function over the right side of a 'Night'.
trans2 :: g ~> h -> Night f g ~> Night f h
trans2 :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *).
(g ~> h) -> Night f g ~> Night f h
trans2 g ~> h
f (Night f b
x g c
y b -> x
g c -> x
h x -> Either b c
j) = forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x (g ~> h
f g c
y) b -> x
g c -> x
h x -> Either b c
j