module Data.Functor.Invariant.Night (
Night(..)
, Not(..), refuted
, night
, runNightAlt
, runNightDecide
, toCoNight
, toCoNight_
, toContraNight
, assoc, unassoc
, intro1, intro2
, elim1, elim2
, swapped
, trans1, trans2
, NightChain
, pattern Swerve, pattern Reject
, runCoNightChain
, runContraNightChain
, chainListF
, chainListF_
, chainDec
, assembleNightChain
, concatNightChain
, 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
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
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
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)
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)
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
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
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
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)
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)
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
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
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
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
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
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
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
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)
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)
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
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
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)
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)
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
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
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
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
type NightChain = Chain Night Not
type NightChain1 = Chain1 Night
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)
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 #-}
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
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
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
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
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