-- |
-- 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
  , runNightAlt
  , runNightDecide
  , toCoNight
  , toCoNight_
  , toContraNight
  , assoc, unassoc
  , intro1, intro2
  , elim1, elim2
  , swapped
  , trans1, trans2
  -- * Chain
  , NightChain
  , pattern Swerve, pattern Reject
  , runCoNightChain
  , runContraNightChain
  , chainListF
  , chainListF_
  , chainDec
  , assembleNightChain
  , concatNightChain
  -- * Nonempty Chain
  , NightChain1
  , pattern NightChain1
  , runCoNightChain1
  , runContraNightChain1
  , chainNonEmptyF
  , chainNonEmptyF_
  , chainDec1
  , assembleNightChain1
  , concatNightChain1
  ) where

import           Control.Applicative.ListF
import           Control.Natural
import           Control.Natural.IsoF
import           Data.Bifunctor
import           Data.Functor.Alt
import           Data.Functor.Contravariant.Conclude
import           Data.Functor.Contravariant.Decide
import           Data.Functor.Contravariant.Divisible.Free
import           Data.Functor.Contravariant.Night          (Not(..), refuted)
import           Data.Functor.Invariant
import           Data.Functor.Plus
import           Data.HBifunctor
import           Data.HBifunctor.Associative hiding        (assoc)
import           Data.HBifunctor.Tensor hiding             (elim1, elim2, intro1, intro2)
import           Data.HFunctor
import           Data.HFunctor.Chain
import           Data.Kind
import           Data.SOP
import           Data.Void
import           GHC.Generics
import qualified Control.Monad.Trans.Compose               as CT
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
import qualified Data.HBifunctor.Tensor                    as T
import qualified Data.List.NonEmpty                        as NE

-- | 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
          -> (a -> Either b c)
          -> (b -> a)
          -> (c -> a)
          -> Night f g a

-- | 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 :: f a -> g b -> Night f g (Either a b)
night x :: f a
x y :: g b
y = f a
-> g b
-> (Either a b -> Either a b)
-> (a -> Either a b)
-> (b -> Either a b)
-> Night f g (Either a b)
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f a
x g b
y Either a b -> Either a b
forall a. a -> a
id a -> Either a b
forall a b. a -> Either a b
Left b -> Either a b
forall a b. b -> Either a b
Right

-- | 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 :: (f ~> h) -> (g ~> h) -> Night f g ~> h
runNightAlt f :: f ~> h
f g :: g ~> h
g (Night x :: f b
x y :: g c
y _ j :: b -> x
j k :: c -> x
k) = (b -> x) -> h b -> h x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> x
j (f b -> h b
f ~> h
f f b
x) h x -> h x -> h x
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!> (c -> x) -> h c -> h x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> x
k (g c -> h c
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 :: (f ~> h) -> (g ~> h) -> Night f g ~> h
runNightDecide f :: f ~> h
f g :: g ~> h
g (Night x :: f b
x y :: g c
y h :: x -> Either b c
h _ _) = (x -> Either b c) -> h b -> h c -> h x
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either b c
h (f b -> h b
f ~> h
f f b
x) (g c -> h c
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 :: Night f g ~> (f :*: g)
toCoNight (Night x :: f b
x y :: g c
y _ f :: b -> x
f g :: c -> x
g) = (b -> x) -> f b -> f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> x
f f b
x f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (c -> x) -> g c -> g x
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_ :: Night f g x -> (:*:) (Coyoneda f) (Coyoneda g) x
toCoNight_ (Night x :: f b
x y :: g c
y _ f :: b -> x
f g :: c -> x
g) = (b -> x) -> f b -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b -> x
f f b
x Coyoneda f x -> Coyoneda g x -> (:*:) (Coyoneda f) (Coyoneda g) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (c -> x) -> g c -> Coyoneda g x
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 :: Night f g x -> Night f g x
toContraNight (Night x :: f b
x y :: g c
y f :: x -> Either b c
f _ _) = f b -> g c -> (x -> Either b c) -> Night f g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
CN.Night f b
x g c
y x -> Either b c
f

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

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

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

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

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

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

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

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

-- | In the covariant direction, we can interpret out of a 'Chain1' of 'Night'
-- into any 'Alt'.
runCoNightChain1
    :: forall f g. Alt g
    => f ~> g
    -> NightChain1 f ~> g
runCoNightChain1 :: (f ~> g) -> NightChain1 f ~> g
runCoNightChain1 f :: f ~> g
f = (f ~> g) -> (Night f g ~> g) -> NightChain1 f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> g
f ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Alt h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightAlt f ~> g
f forall a. a -> a
g ~> g
id)

-- | In the contravariant direction, we can interpret out of a 'Chain1' of
-- 'Night' into any 'Decide'.
runContraNightChain1
    :: forall f g. Decide g
    => f ~> g
    -> NightChain1 f ~> g
runContraNightChain1 :: (f ~> g) -> NightChain1 f ~> g
runContraNightChain1 f :: f ~> g
f = (f ~> g) -> (Night f g ~> g) -> NightChain1 f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> g
f ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Decide h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightDecide f ~> g
f forall a. a -> a
g ~> g
id)

-- | Extract the 'Dec' part out of a 'NightChain', shedding the
-- covariant bits.
chainDec :: NightChain f ~> Dec f
chainDec :: NightChain f x -> Dec f x
chainDec = (f ~> Dec f) -> NightChain f ~> Dec f
forall (f :: * -> *) (g :: * -> *).
Conclude g =>
(f ~> g) -> NightChain f ~> g
runContraNightChain f ~> Dec f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | Extract the 'Dec1' part out of a 'NightChain1', shedding the
-- covariant bits.
chainDec1 :: NightChain1 f ~> Dec1 f
chainDec1 :: NightChain1 f x -> Dec1 f x
chainDec1 = (f ~> Dec1 f) -> NightChain1 f ~> Dec1 f
forall (f :: * -> *) (g :: * -> *).
Decide g =>
(f ~> g) -> NightChain1 f ~> g
runContraNightChain1 f ~> Dec1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | In the covariant direction, we can interpret out of a 'Chain' of 'Night'
-- into any 'Plus'.
runCoNightChain
    :: forall f g. Plus g
    => f ~> g
    -> NightChain f ~> g
runCoNightChain :: (f ~> g) -> NightChain f ~> g
runCoNightChain f :: f ~> g
f = (Not ~> g) -> (Night f g ~> g) -> NightChain f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
       (f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain (g x -> Not x -> g x
forall a b. a -> b -> a
const g x
forall (f :: * -> *) a. Plus f => f a
zero) ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Alt h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightAlt f ~> g
f forall a. a -> a
g ~> g
id)

-- | In the contravariant direction, we can interpret out of a 'Chain' of
-- 'Night' into any 'Conclude'.
runContraNightChain
    :: forall f g. Conclude g
    => f ~> g
    -> NightChain f ~> g
runContraNightChain :: (f ~> g) -> NightChain f ~> g
runContraNightChain f :: f ~> g
f = (Not ~> g) -> (Night f g ~> g) -> NightChain f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
       (f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain ((x -> Void) -> g x
forall (f :: * -> *) a. Conclude f => (a -> Void) -> f a
conclude ((x -> Void) -> g x) -> (Not x -> x -> Void) -> Not x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not x -> x -> Void
forall a. Not a -> a -> Void
refute) ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Decide h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightDecide f ~> g
f forall a. a -> a
g ~> g
id)

-- | Extract the 'ListF' part out of a 'NightChain', shedding the
-- contravariant bits.
--
-- @since 0.3.2.0
chainListF :: Functor f => NightChain f ~> ListF f
chainListF :: NightChain f ~> ListF f
chainListF = (f ~> ListF f) -> NightChain f ~> ListF f
forall (f :: * -> *) (g :: * -> *).
Plus g =>
(f ~> g) -> NightChain f ~> g
runCoNightChain f ~> ListF f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | Extract the 'ListF' part out of a 'NightChain', shedding the
-- contravariant bits.
--
-- This version does not require a 'Functor' constraint because it converts
-- to the coyoneda-wrapped product, which is more accurately the true
-- conversion to a covariant chain.
--
-- @since 0.3.2.0
chainListF_ :: NightChain f ~> CT.ComposeT ListF CY.Coyoneda f
chainListF_ :: NightChain f x -> ComposeT ListF Coyoneda f x
chainListF_ = (Not ~> ComposeT ListF Coyoneda f)
-> (Night f (ComposeT ListF Coyoneda f)
    ~> ComposeT ListF Coyoneda f)
-> Chain Night Not f ~> ComposeT ListF Coyoneda f
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
       (f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain (ComposeT ListF Coyoneda f x -> Not x -> ComposeT ListF Coyoneda f x
forall a b. a -> b -> a
const (ListF (Coyoneda f) x -> ComposeT ListF Coyoneda f x
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
f (g m) a -> ComposeT f g m a
CT.ComposeT ([Coyoneda f x] -> ListF (Coyoneda f) x
forall k (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF []))) ((Night f (ComposeT ListF Coyoneda f) ~> ComposeT ListF Coyoneda f)
 -> NightChain f x -> ComposeT ListF Coyoneda f x)
-> (Night f (ComposeT ListF Coyoneda f)
    ~> ComposeT ListF Coyoneda f)
-> NightChain f x
-> ComposeT ListF Coyoneda f x
forall a b. (a -> b) -> a -> b
$ \case
    Night x (CT.ComposeT (ListF xs)) _ f g -> ListF (Coyoneda f) x -> ComposeT ListF Coyoneda f x
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
f (g m) a -> ComposeT f g m a
CT.ComposeT (ListF (Coyoneda f) x -> ComposeT ListF Coyoneda f x)
-> ([Coyoneda f x] -> ListF (Coyoneda f) x)
-> [Coyoneda f x]
-> ComposeT ListF Coyoneda f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Coyoneda f x] -> ListF (Coyoneda f) x
forall k (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([Coyoneda f x] -> ComposeT ListF Coyoneda f x)
-> [Coyoneda f x] -> ComposeT ListF Coyoneda f x
forall a b. (a -> b) -> a -> b
$
      (b -> x) -> f b -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b -> x
f f b
x Coyoneda f x -> [Coyoneda f x] -> [Coyoneda f x]
forall a. a -> [a] -> [a]
: ((Coyoneda f c -> Coyoneda f x) -> [Coyoneda f c] -> [Coyoneda f x]
forall a b. (a -> b) -> [a] -> [b]
map ((Coyoneda f c -> Coyoneda f x)
 -> [Coyoneda f c] -> [Coyoneda f x])
-> ((c -> x) -> Coyoneda f c -> Coyoneda f x)
-> (c -> x)
-> [Coyoneda f c]
-> [Coyoneda f x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> x) -> Coyoneda f c -> Coyoneda f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) c -> x
g [Coyoneda f c]
xs

-- | Extract the 'NonEmptyF' part out of a 'NightChain1', shedding the
-- contravariant bits.
--
-- @since 0.3.2.0
chainNonEmptyF :: Functor f => NightChain1 f ~> NonEmptyF f
chainNonEmptyF :: NightChain1 f ~> NonEmptyF f
chainNonEmptyF = (f ~> NonEmptyF f) -> NightChain1 f ~> NonEmptyF f
forall (f :: * -> *) (g :: * -> *).
Alt g =>
(f ~> g) -> NightChain1 f ~> g
runCoNightChain1 f ~> NonEmptyF f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | Extract the 'NonEmptyF' part out of a 'NightChain1', shedding the
-- contravariant bits.
--
-- This version does not require a 'Functor' constraint because it converts
-- to the coyoneda-wrapped product, which is more accurately the true
-- conversion to a covariant chain.
--
-- @since 0.3.2.0
chainNonEmptyF_ :: NightChain1 f ~> CT.ComposeT NonEmptyF CY.Coyoneda f
chainNonEmptyF_ :: NightChain1 f x -> ComposeT NonEmptyF Coyoneda f x
chainNonEmptyF_ = (f ~> ComposeT NonEmptyF Coyoneda f)
-> (Night f (ComposeT NonEmptyF Coyoneda f)
    ~> ComposeT NonEmptyF Coyoneda f)
-> Chain1 Night f ~> ComposeT NonEmptyF Coyoneda f
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> ComposeT NonEmptyF Coyoneda f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject ((Night f (ComposeT NonEmptyF Coyoneda f)
  ~> ComposeT NonEmptyF Coyoneda f)
 -> NightChain1 f x -> ComposeT NonEmptyF Coyoneda f x)
-> (Night f (ComposeT NonEmptyF Coyoneda f)
    ~> ComposeT NonEmptyF Coyoneda f)
-> NightChain1 f x
-> ComposeT NonEmptyF Coyoneda f x
forall a b. (a -> b) -> a -> b
$ \case
    Night x (CT.ComposeT (NonEmptyF xs)) _ f g -> NonEmptyF (Coyoneda f) x -> ComposeT NonEmptyF Coyoneda f x
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
f (g m) a -> ComposeT f g m a
CT.ComposeT (NonEmptyF (Coyoneda f) x -> ComposeT NonEmptyF Coyoneda f x)
-> (NonEmpty (Coyoneda f x) -> NonEmptyF (Coyoneda f) x)
-> NonEmpty (Coyoneda f x)
-> ComposeT NonEmptyF Coyoneda f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Coyoneda f x) -> NonEmptyF (Coyoneda f) x
forall k (f :: k -> *) (a :: k). NonEmpty (f a) -> NonEmptyF f a
NonEmptyF (NonEmpty (Coyoneda f x) -> ComposeT NonEmptyF Coyoneda f x)
-> NonEmpty (Coyoneda f x) -> ComposeT NonEmptyF Coyoneda f x
forall a b. (a -> b) -> a -> b
$
      (b -> x) -> f b -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b -> x
f f b
x Coyoneda f x -> NonEmpty (Coyoneda f x) -> NonEmpty (Coyoneda f x)
forall a. a -> NonEmpty a -> NonEmpty a
NE.<| ((Coyoneda f c -> Coyoneda f x)
-> NonEmpty (Coyoneda f c) -> NonEmpty (Coyoneda f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Coyoneda f c -> Coyoneda f x)
 -> NonEmpty (Coyoneda f c) -> NonEmpty (Coyoneda f x))
-> ((c -> x) -> Coyoneda f c -> Coyoneda f x)
-> (c -> x)
-> NonEmpty (Coyoneda f c)
-> NonEmpty (Coyoneda f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> x) -> Coyoneda f c -> Coyoneda f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) c -> x
g NonEmpty (Coyoneda f c)
xs


-- | Instead of defining yet another separate free monoid like
-- 'Control.Applicative.Free.Ap',
-- 'Data.Functor.Contravariant.Divisible.Free.Div', or
-- 'Data.Functor.Contravariant.Divisible.Free.Dec', we re-use 'Chain'.
--
-- You can assemble values using the combinators in "Data.HFunctor.Chain",
-- and then tear them down/interpret them using 'runCoNightChain' and
-- 'runContraNightChain'.  There is no general invariant interpreter (and so no
-- 'MonoidIn' instance for 'Night') because the typeclasses used to express
-- the target contexts are probably not worth defining given how little the
-- Haskell ecosystem uses invariant functors as an abstraction.
type NightChain  = Chain Night Not

-- | Instead of defining yet another separate free semigroup like
-- 'Data.Functor.Apply.Free.Ap1',
-- 'Data.Functor.Contravariant.Divisible.Free.Div1', or
-- 'Data.Functor.Contravariant.Divisible.Free.Dec1', we re-use 'Chain1'.
--
-- You can assemble values using the combinators in "Data.HFunctor.Chain",
-- and then tear them down/interpret them using 'runCoNightChain1' and
-- 'runContraNightChain1'.  There is no general invariant interpreter (and so no
-- 'SemigroupIn' instance for 'Night') because the typeclasses used to
-- express the target contexts are probably not worth defining given how
-- little the Haskell ecosystem uses invariant functors as an abstraction.
type NightChain1 = Chain1 Night

-- | Match on a non-empty 'NightChain'; contains the splitting function,
-- the two rejoining functions, the first @f@, and the rest of the chain.
-- Analogous to the 'Data.Functor.Contravariant.Divisible.Free.Choose'
-- constructor.
pattern Swerve :: (a -> Either b c) -> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain f a
pattern $bSwerve :: (a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain f a
$mSwerve :: forall r a (f :: * -> *).
NightChain f a
-> (forall b c.
    (a -> Either b c)
    -> (b -> a) -> (c -> a) -> f b -> NightChain f c -> r)
-> (Void# -> r)
-> r
Swerve f g h x xs = More (Night x xs f g h)

-- | Match on an "empty" 'NightChain'; contains no @f@s, but only the
-- terminal value.  Analogous to the
-- 'Data.Functor.Contravariant.Divisible.Free.Lose' constructor.
pattern Reject :: (a -> Void) -> NightChain f a
pattern $bReject :: (a -> Void) -> NightChain f a
$mReject :: forall r a (f :: * -> *).
NightChain f a -> ((a -> Void) -> r) -> (Void# -> r) -> r
Reject x = Done (Not x)
{-# COMPLETE Swerve, Reject #-}

-- | Match on a 'NightChain1' to get the head and the rest of the items.
-- Analogous to the 'Data.Functor.Contravariant.Divisible.Free.Dec1'
-- constructor.
pattern NightChain1 :: Invariant f => (a -> Either b c) -> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain1 f a
pattern $bNightChain1 :: (a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain1 f a
$mNightChain1 :: forall r (f :: * -> *) a.
Invariant f =>
NightChain1 f a
-> (forall b c.
    (a -> Either b c)
    -> (b -> a) -> (c -> a) -> f b -> NightChain f c -> r)
-> (Void# -> r)
-> r
NightChain1 f g h x xs <- (splitChain1->Night x xs f g h)
  where
    NightChain1 f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: f b
x xs :: NightChain f c
xs = Night f (ListBy Night f) a -> NightChain1 f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE (Night f (ListBy Night f) a -> NightChain1 f a)
-> Night f (ListBy Night f) a -> NightChain1 f a
forall a b. (a -> b) -> a -> b
$ f b
-> NightChain f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night f (Chain Night Not f) a
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f b
x NightChain f c
xs a -> Either b c
f b -> a
g c -> a
h
{-# COMPLETE NightChain1 #-}

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

instance HFunctor (Night f) where
    hmap :: (f ~> g) -> Night f f ~> Night f g
hmap f :: f ~> g
f = (f ~> f) -> (f ~> g) -> Night f f ~> Night f g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (j :: k -> *) (g :: k -> *) (l :: k -> *).
HBifunctor t =>
(f ~> j) -> (g ~> l) -> t f g ~> t j l
hbimap forall a. a -> a
f ~> f
id f ~> g
f

instance HBifunctor Night where
    hbimap :: (f ~> j) -> (g ~> l) -> Night f g ~> Night j l
hbimap f :: f ~> j
f g :: g ~> l
g (Night x :: f b
x y :: g c
y h :: x -> Either b c
h j :: b -> x
j k :: c -> x
k) = j b
-> l c -> (x -> Either b c) -> (b -> x) -> (c -> x) -> Night j l x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night (f b -> j b
f ~> j
f f b
x) (g c -> l c
g ~> l
g g c
y) x -> Either b c
h b -> x
j c -> x
k

instance Associative Night where
    type NonEmptyBy Night = NightChain1
    type FunctorBy Night = Invariant
    associating :: Night f (Night g h) <~> Night (Night f g) h
associating = (Night f (Night g h) ~> Night (Night f g) h)
-> (Night (Night f g) h ~> Night f (Night g h))
-> Night f (Night g h) <~> Night (Night f g) h
forall k (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF Night f (Night g h) ~> Night (Night f g) h
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Night f (Night g h) ~> Night (Night f g) h
assoc Night (Night f g) h ~> Night f (Night g h)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Night (Night f g) h ~> Night f (Night g h)
unassoc

    appendNE :: Night (NonEmptyBy Night f) (NonEmptyBy Night f) x
-> NonEmptyBy Night f x
appendNE (Night xs :: NonEmptyBy Night f b
xs ys :: NonEmptyBy Night f c
ys f :: x -> Either b c
f g :: b -> x
g h :: c -> x
h) = case NonEmptyBy Night f b
xs of
      Done1 x                  -> Night f (Chain1 Night f) x -> Chain1 Night f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (f b
-> Chain1 Night f c
-> (x -> Either b c)
-> (b -> x)
-> (c -> x)
-> Night f (Chain1 Night f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f b
x NonEmptyBy Night f c
Chain1 Night f c
ys x -> Either b c
f b -> x
g c -> x
h)
      More1 (Night z zs j k l) -> Night f (Chain1 Night f) x -> NonEmptyBy Night f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (Night f (Chain1 Night f) x -> NonEmptyBy Night f x)
-> Night f (Chain1 Night f) x -> NonEmptyBy Night f x
forall a b. (a -> b) -> a -> b
$
        f b
-> Chain1 Night f (Either c c)
-> (x -> Either b (Either c c))
-> (b -> x)
-> (Either c c -> x)
-> Night f (Chain1 Night f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f b
z (Night (NonEmptyBy Night f) (NonEmptyBy Night f) (Either c c)
-> NonEmptyBy Night f (Either c c)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
Associative t =>
t (NonEmptyBy t f) (NonEmptyBy t f) ~> NonEmptyBy t f
appendNE (Chain1 Night f c
-> Chain1 Night f c
-> (Either c c -> Either c c)
-> (c -> Either c c)
-> (c -> Either c c)
-> Night (Chain1 Night f) (Chain1 Night f) (Either c c)
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night Chain1 Night f c
zs NonEmptyBy Night f c
Chain1 Night f c
ys Either c c -> Either c c
forall a. a -> a
id c -> Either c c
forall a b. a -> Either a b
Left c -> Either c c
forall a b. b -> Either a b
Right))
          (Either (Either b c) c -> Either b (Either c c)
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc (Either (Either b c) c -> Either b (Either c c))
-> (x -> Either (Either b c) c) -> x -> Either b (Either c c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Either b c) -> Either b c -> Either (Either b c) c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> Either b c
j (Either b c -> Either (Either b c) c)
-> (x -> Either b c) -> x -> Either (Either b c) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
f)
          (b -> x
g (b -> x) -> (b -> b) -> b -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b
k)
          ((c -> x) -> (c -> x) -> Either c c -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> x
g (b -> x) -> (c -> b) -> c -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> b
l) c -> x
h)
    matchNE :: NonEmptyBy Night f ~> (f :+: Night f (NonEmptyBy Night f))
matchNE = NonEmptyBy Night f x -> (:+:) f (Night f (NonEmptyBy Night f)) x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *).
Chain1 t f ~> (f :+: t f (Chain1 t f))
matchChain1

    consNE :: Night f (NonEmptyBy Night f) x -> NonEmptyBy Night f x
consNE = Night f (NonEmptyBy Night f) x -> NonEmptyBy Night f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1
    toNonEmptyBy :: Night f f x -> NonEmptyBy Night f x
toNonEmptyBy = Night f f x -> NonEmptyBy Night f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *).
HBifunctor t =>
t f f ~> Chain1 t f
toChain1

instance Tensor Night Not where
    type ListBy Night = NightChain

    intro1 :: f x -> Night f Not x
intro1 = f x -> Night f Not x
forall (f :: * -> *). f ~> Night f Not
intro2
    intro2 :: g x -> Night Not g x
intro2 = g x -> Night Not g x
forall (g :: * -> *). g ~> Night Not g
intro1
    elim1 :: Night f Not ~> f
elim1 = Night f Not x -> f x
forall (f :: * -> *). Invariant f => Night f Not ~> f
elim2
    elim2 :: Night Not g ~> g
elim2 = Night Not g x -> g x
forall (g :: * -> *). Invariant g => Night Not g ~> g
elim1

    appendLB :: Night (ListBy Night f) (ListBy Night f) x -> ListBy Night f x
appendLB = Night (ListBy Night f) (ListBy Night f) x -> ListBy Night f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain
    splitNE :: NonEmptyBy Night f x -> Night f (ListBy Night f) x
splitNE = NonEmptyBy Night f x -> Night f (ListBy Night f) x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
Chain1 t f ~> t f (Chain t i f)
splitChain1
    splittingLB :: p ((:+:) Not (Night f (ListBy Night f)) a)
  ((:+:) Not (Night f (ListBy Night f)) a)
-> p (ListBy Night f a) (ListBy Night f a)
splittingLB = p ((:+:) Not (Night f (ListBy Night f)) a)
  ((:+:) Not (Night f (ListBy Night f)) a)
-> p (ListBy Night f a) (ListBy Night f a)
forall k1 k2 (t :: k1 -> (k2 -> *) -> k2 -> *) (i :: k2 -> *)
       (f :: k1).
Chain t i f <~> (i :+: t f (Chain t i f))
splittingChain

    toListBy :: Night f f x -> ListBy Night f x
toListBy = Night f f x -> ListBy Night f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t f f ~> Chain t i f
toChain

instance Matchable Night Not where
    unsplitNE :: Night f (ListBy Night f) ~> NonEmptyBy Night f
unsplitNE (Night x :: f b
x xs :: ListBy Night f c
xs f :: x -> Either b c
f g :: b -> x
g h :: c -> x
h) = case ListBy Night f c
xs of
      Done r  -> f x -> NonEmptyBy Night f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
f a -> Chain1 t f a
Done1 (f x -> NonEmptyBy Night f x) -> f x -> NonEmptyBy Night f x
forall a b. (a -> b) -> a -> b
$ (b -> x) -> (x -> b) -> f b -> f x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap b -> x
g ((b -> b) -> (c -> b) -> Either b c -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
id (Void -> b
forall a. Void -> a
absurd (Void -> b) -> (c -> Void) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not c -> c -> Void
forall a. Not a -> a -> Void
refute Not c
r) (Either b c -> b) -> (x -> Either b c) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
f) f b
x
      More ys -> Night f (Chain1 Night f) x -> NonEmptyBy Night f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (Night f (Chain1 Night f) x -> NonEmptyBy Night f x)
-> Night f (Chain1 Night f) x -> NonEmptyBy Night f x
forall a b. (a -> b) -> a -> b
$ f b
-> Chain1 Night f c
-> (x -> Either b c)
-> (b -> x)
-> (c -> x)
-> Night f (Chain1 Night f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f b
x (Night f (ListBy Night f) c -> NonEmptyBy Night f c
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE Night f (ListBy Night f) c
Night f (Chain Night Not f) c
ys) x -> Either b c
f b -> x
g c -> x
h
    matchLB :: ListBy Night f ~> (Not :+: NonEmptyBy Night f)
matchLB = \case
      Done x  -> Not x -> (:+:) Not (Chain1 Night f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Not x
x
      More xs -> Chain1 Night f x -> (:+:) Not (NonEmptyBy Night f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Chain1 Night f x -> (:+:) Not (NonEmptyBy Night f) x)
-> Chain1 Night f x -> (:+:) Not (NonEmptyBy Night f) x
forall a b. (a -> b) -> a -> b
$ Night f (ListBy Night f) x -> NonEmptyBy Night f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE Night f (ListBy Night f) x
Night f (Chain Night Not f) x
xs

-- | Convenient wrapper to build up a 'NightChain' on by providing each
-- component of it.  This makes it much easier to build up longer chains
-- because you would only need to write the splitting/joining functions in
-- one place.
--
-- For example, if you had a data type
--
-- @
-- data MyType = MTI Int | MTB Bool | MTS String
-- @
--
-- and an invariant functor @Prim@ (representing, say, a bidirectional
-- parser, where @Prim Int@ is a bidirectional parser for an 'Int'@),
-- then you could assemble a bidirectional parser for a @MyType@ using:
--
-- @
-- invmap (\case MTI x -> Z (I x); MTB y -> S (Z (I y)); MTS z -> S (S (Z (I z))))
--        (\case Z (I x) -> MTI x; S (Z (I y)) -> MTB y; S (S (Z (I z))) -> MTS z) $
--   assembleNightChain $ intPrim
--                     :* boolPrim
--                     :* stringPrim
--                     :* Nil
-- @
--
-- Some notes on usefulness depending on how many components you have:
--
-- *    If you have 0 components, use 'Reject' directly.
-- *    If you have 1 component, use 'inject' or 'injectChain' directly.
-- *    If you have 2 components, use 'toListBy' or 'toChain'.
-- *    If you have 3 or more components, these combinators may be useful;
--      otherwise you'd need to manually peel off eithers one-by-one.
assembleNightChain
    :: NP f as
    -> NightChain f (NS I as)
assembleNightChain :: NP f as -> NightChain f (NS I as)
assembleNightChain = \case
    Nil     -> Not (NS I as) -> NightChain f (NS I as)
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
       (a :: k).
i a -> Chain t i f a
Done (Not (NS I as) -> NightChain f (NS I as))
-> Not (NS I as) -> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ (NS I as -> Void) -> Not (NS I as)
forall a. (a -> Void) -> Not a
Not (\case {})
    x :: f x
x :* xs :: NP f xs
xs -> Night f (Chain Night Not f) (NS I (x : xs))
-> NightChain f (NS I as)
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
       (a :: k).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) (NS I (x : xs))
 -> NightChain f (NS I as))
-> Night f (Chain Night Not f) (NS I (x : xs))
-> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ f x
-> Chain Night Not f (NS I xs)
-> (NS I (x : xs) -> Either x (NS I xs))
-> (x -> NS I (x : xs))
-> (NS I xs -> NS I (x : xs))
-> Night f (Chain Night Not f) (NS I (x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
      f x
x
      (NP f xs -> Chain Night Not f (NS I xs)
forall (f :: * -> *) (as :: [*]). NP f as -> NightChain f (NS I as)
assembleNightChain NP f xs
xs)
      NS I (x : xs) -> Either x (NS I xs)
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
      (I x -> NS I (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : xs)) -> (x -> I x) -> x -> NS I (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
      NS I xs -> NS I (x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S

-- | A version of 'assembleNightChain' where each component is itself
-- a 'NightChain'.
--
-- @
-- assembleNightChain (x :* y :* z :* Nil)
--   = concatNightChain (injectChain x :* injectChain y :* injectChain z :* Nil)
-- @
concatNightChain
    :: NP (NightChain f) as
    -> NightChain f (NS I as)
concatNightChain :: NP (NightChain f) as -> NightChain f (NS I as)
concatNightChain = \case
    Nil     -> Not (NS I as) -> NightChain f (NS I as)
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
       (a :: k).
i a -> Chain t i f a
Done (Not (NS I as) -> NightChain f (NS I as))
-> Not (NS I as) -> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ (NS I as -> Void) -> Not (NS I as)
forall a. (a -> Void) -> Not a
Not (\case {})
    x :: NightChain f x
x :* xs :: NP (NightChain f) xs
xs -> Night (NightChain f) (NightChain f) (NS I (x : xs))
-> NightChain f (NS I as)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain (Night (NightChain f) (NightChain f) (NS I (x : xs))
 -> NightChain f (NS I as))
-> Night (NightChain f) (NightChain f) (NS I (x : xs))
-> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ NightChain f x
-> Chain Night Not f (NS I xs)
-> (NS I (x : xs) -> Either x (NS I xs))
-> (x -> NS I (x : xs))
-> (NS I xs -> NS I (x : xs))
-> Night (NightChain f) (NightChain f) (NS I (x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
      NightChain f x
x
      (NP (NightChain f) xs -> Chain Night Not f (NS I xs)
forall (f :: * -> *) (as :: [*]).
NP (NightChain f) as -> NightChain f (NS I as)
concatNightChain NP (NightChain f) xs
xs)
      NS I (x : xs) -> Either x (NS I xs)
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
      (I x -> NS I (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : xs)) -> (x -> I x) -> x -> NS I (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
      NS I xs -> NS I (x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S

-- | A version of 'assembleNightChain' but for 'NightChain1' instead.  Can
-- be useful if you intend on interpreting it into something with only
-- a 'Decide' or 'Alt' instance, but no
-- 'Data.Functor.Contravariant.Divisible.Decidable' or 'Plus' or
-- 'Control.Applicative.Alternative'.
assembleNightChain1
    :: Invariant f
    => NP f (a ': as)
    -> NightChain1 f (NS I (a ': as))
assembleNightChain1 :: NP f (a : as) -> NightChain1 f (NS I (a : as))
assembleNightChain1 = \case
    x :: f x
x :* xs :: NP f xs
xs -> case NP f xs
xs of
      Nil    -> f (NS I '[x]) -> NightChain1 f (NS I (a : as))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
f a -> Chain1 t f a
Done1 (f (NS I '[x]) -> NightChain1 f (NS I (a : as)))
-> f (NS I '[x]) -> NightChain1 f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ (x -> NS I '[x]) -> (NS I '[x] -> x) -> f x -> f (NS I '[x])
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (I x -> NS I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I '[x]) -> (x -> I x) -> x -> NS I '[x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I) (I x -> x
forall a. I a -> a
unI (I x -> x) -> (NS I '[x] -> I x) -> NS I '[x] -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS I '[x] -> I x
forall k (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ) f x
x
      _ :* _ -> Night f (Chain1 Night f) (NS I (x : x : xs))
-> NightChain1 f (NS I (a : as))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (Night f (Chain1 Night f) (NS I (x : x : xs))
 -> NightChain1 f (NS I (a : as)))
-> Night f (Chain1 Night f) (NS I (x : x : xs))
-> NightChain1 f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ f x
-> Chain1 Night f (NS I (x : xs))
-> (NS I (x : x : xs) -> Either x (NS I (x : xs)))
-> (x -> NS I (x : x : xs))
-> (NS I (x : xs) -> NS I (x : x : xs))
-> Night f (Chain1 Night f) (NS I (x : x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
        f x
x
        (NP f (x : xs) -> Chain1 Night f (NS I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> NightChain1 f (NS I (a : as))
assembleNightChain1 NP f xs
NP f (x : xs)
xs)
        NS I (x : x : xs) -> Either x (NS I (x : xs))
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
        (I x -> NS I (x : x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : x : xs)) -> (x -> I x) -> x -> NS I (x : x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
        NS I (x : xs) -> NS I (x : x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S

-- | A version of 'concatNightChain' but for 'NightChain1' instead.  Can be
-- useful if you intend on interpreting it into something with only
-- a 'Decide' or 'Alt' instance, but no
-- 'Data.Functor.Contravariant.Divisible.Decidable' or 'Plus' or
-- 'Control.Applicative.Alternative'.
concatNightChain1
    :: Invariant f
    => NP (NightChain1 f) (a ': as)
    -> NightChain1 f (NS I (a ': as))
concatNightChain1 :: NP (NightChain1 f) (a : as) -> NightChain1 f (NS I (a : as))
concatNightChain1 = \case
    x :: NightChain1 f x
x :* xs :: NP (NightChain1 f) xs
xs -> case NP (NightChain1 f) xs
xs of
      Nil    -> (x -> NS I '[x])
-> (NS I '[x] -> x)
-> NightChain1 f x
-> Chain1 Night f (NS I '[x])
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (I x -> NS I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I '[x]) -> (x -> I x) -> x -> NS I '[x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I) (I x -> x
forall a. I a -> a
unI (I x -> x) -> (NS I '[x] -> I x) -> NS I '[x] -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS I '[x] -> I x
forall k (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ) NightChain1 f x
x
      _ :* _ -> Night (NightChain1 f) (NightChain1 f) (NS I (x : x : xs))
-> NightChain1 f (NS I (a : as))
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
(Associative t, FunctorBy t f) =>
t (Chain1 t f) (Chain1 t f) ~> Chain1 t f
appendChain1 (Night (NightChain1 f) (NightChain1 f) (NS I (x : x : xs))
 -> NightChain1 f (NS I (a : as)))
-> Night (NightChain1 f) (NightChain1 f) (NS I (x : x : xs))
-> NightChain1 f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ NightChain1 f x
-> Chain1 Night f (NS I (x : xs))
-> (NS I (x : x : xs) -> Either x (NS I (x : xs)))
-> (x -> NS I (x : x : xs))
-> (NS I (x : xs) -> NS I (x : x : xs))
-> Night (NightChain1 f) (NightChain1 f) (NS I (x : x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
        NightChain1 f x
x
        (NP (NightChain1 f) (x : xs) -> Chain1 Night f (NS I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP (NightChain1 f) (a : as) -> NightChain1 f (NS I (a : as))
concatNightChain1 NP (NightChain1 f) xs
NP (NightChain1 f) (x : xs)
xs)
        NS I (x : x : xs) -> Either x (NS I (x : xs))
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
        (I x -> NS I (x : x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : x : xs)) -> (x -> I x) -> x -> NS I (x : x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
        NS I (x : xs) -> NS I (x : x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S

unconsNSI :: NS I (a ': as) -> Either a (NS I as)
unconsNSI :: NS I (a : as) -> Either a (NS I as)
unconsNSI = \case
  Z (I x :: x
x) -> x -> Either x (NS I as)
forall a b. a -> Either a b
Left x
x
  S xs :: NS I xs
xs    -> NS I xs -> Either a (NS I xs)
forall a b. b -> Either a b
Right NS I xs
xs