{-# OPTIONS_GHC -Wno-orphans #-}
module Data.HBifunctor.Tensor (
  
    Tensor(..)
  , rightIdentity
  , leftIdentity
  , sumLeftIdentity
  , sumRightIdentity
  , prodLeftIdentity
  , prodRightIdentity
  
  , MonoidIn(..)
  , nilLB
  , consLB
  , unconsLB
  , retractLB
  , interpretLB
  
  , inL
  , inR
  , outL
  , outR
  , prodOutL
  , prodOutR
  , WrapF(..)
  , WrapLB(..)
  
  , Matchable(..)
  , splittingNE
  , matchingLB
  ) where
import           Control.Applicative.Free
import           Control.Applicative.ListF
import           Control.Applicative.Step
import           Control.Monad.Freer.Church
import           Control.Monad.Trans.Compose
import           Control.Natural
import           Control.Natural.IsoF
import           Data.Bifunctor
import           Data.Coerce
import           Data.Data
import           Data.Function
import           Data.Functor.Apply.Free
import           Data.Functor.Bind
import           Data.Functor.Classes
import           Data.Functor.Contravariant
import           Data.Functor.Contravariant.Conclude
import           Data.Functor.Contravariant.Decide
import           Data.Functor.Contravariant.Divise
import           Data.Functor.Contravariant.Divisible
import           Data.Functor.Contravariant.Divisible.Free
import           Data.Functor.Contravariant.Night          (Night(..), Not(..))
import           Data.Functor.Day                          (Day(..))
import           Data.Functor.Identity
import           Data.Functor.Invariant
import           Data.Functor.Invariant.Internative
import           Data.Functor.Invariant.Inplicative
import           Data.Functor.Plus
import           Data.Functor.Product
import           Data.Functor.Sum
import           Data.Functor.These
import           Data.HBifunctor
import           Data.HBifunctor.Associative
import           Data.HBifunctor.Tensor.Internal
import           Data.HFunctor
import           Data.HFunctor.Chain.Internal
import           Data.HFunctor.Internal
import           Data.HFunctor.Interpret
import           Data.List.NonEmpty                        (NonEmpty(..))
import           Data.Void
import           GHC.Generics
import qualified Data.Bifunctor.Assoc                      as B
import qualified Data.Functor.Contravariant.Coyoneda       as CCY
import qualified Data.Functor.Contravariant.Day            as CD
import qualified Data.Functor.Contravariant.Night          as N
import qualified Data.Functor.Day                          as D
import qualified Data.Functor.Invariant.Day                as ID
import qualified Data.Functor.Invariant.Night              as IN
import qualified Data.Map.NonEmpty                         as NEM
rightIdentity :: (Tensor t i, FunctorBy t f) => f <~> t f i
rightIdentity :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Tensor t i, FunctorBy t f) =>
f <~> t f i
rightIdentity = (f ~> t f i) -> (t f i ~> f) -> f <~> t f i
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF f x -> t f i x
f ~> t f i
forall (f :: * -> *). f ~> t f i
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
f ~> t f i
intro1 t f i x -> f x
t f i ~> f
forall (f :: * -> *). FunctorBy t f => t f i ~> f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Tensor t i, FunctorBy t f) =>
t f i ~> f
elim1
leftIdentity  :: (Tensor t i, FunctorBy t g) => g <~> t i g
leftIdentity :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *).
(Tensor t i, FunctorBy t g) =>
g <~> t i g
leftIdentity = (g ~> t i g) -> (t i g ~> g) -> g <~> t i g
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF g x -> t i g x
g ~> t i g
forall (g :: * -> *). g ~> t i g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *).
Tensor t i =>
g ~> t i g
intro2 t i g x -> g x
t i g ~> g
forall (g :: * -> *). FunctorBy t g => t i g ~> g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *).
(Tensor t i, FunctorBy t g) =>
t i g ~> g
elim2
sumLeftIdentity :: f <~> V1 :+: f
sumLeftIdentity :: forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:+:) V1 f a) ((:+:) V1 f a) -> p (f a) (f a)
sumLeftIdentity = (f ~> (V1 :+: f)) -> ((V1 :+: f) ~> f) -> f <~> (V1 :+: f)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF f x -> (:+:) V1 f x
f ~> (V1 :+: f)
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (V1 x -> f x
forall {x :: k}. V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 (forall {x :: k}. V1 x -> f x) -> (f ~> f) -> (V1 :+: f) ~> f
forall {k} (f :: k -> *) (h :: k -> *) (g :: k -> *).
(f ~> h) -> (g ~> h) -> (f :+: g) ~> h
!+! f x -> f x
f ~> f
forall a. a -> a
id)
sumRightIdentity :: f <~> f :+: V1
sumRightIdentity :: forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:+:) f V1 a) ((:+:) f V1 a) -> p (f a) (f a)
sumRightIdentity = (f ~> (f :+: V1)) -> ((f :+: V1) ~> f) -> f <~> (f :+: V1)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF f x -> (:+:) f V1 x
f ~> (f :+: V1)
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f x -> f x
forall {x :: k}. f x -> f x
forall a. a -> a
id (forall {x :: k}. f x -> f x) -> (V1 ~> f) -> (f :+: V1) ~> f
forall {k} (f :: k -> *) (h :: k -> *) (g :: k -> *).
(f ~> h) -> (g ~> h) -> (f :+: g) ~> h
!+! V1 x -> f x
V1 ~> f
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1)
prodLeftIdentity :: f <~> Proxy :*: f
prodLeftIdentity :: forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:*:) Proxy f a) ((:*:) Proxy f a) -> p (f a) (f a)
prodLeftIdentity = (f ~> (Proxy :*: f)) -> ((Proxy :*: f) ~> f) -> f <~> (Proxy :*: f)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (Proxy x
forall {k} (t :: k). Proxy t
Proxy Proxy x -> f x -> (:*:) Proxy f x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:) (\case Proxy x
_ :*: f x
y -> f x
y)
prodRightIdentity :: g <~> g :*: Proxy
prodRightIdentity :: forall {k} (g :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:*:) g Proxy a) ((:*:) g Proxy a) -> p (g a) (g a)
prodRightIdentity = (g ~> (g :*: Proxy)) -> ((g :*: Proxy) ~> g) -> g <~> (g :*: Proxy)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (g x -> Proxy x -> (:*:) g Proxy x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy x
forall {k} (t :: k). Proxy t
Proxy) (\case g x
x :*: Proxy x
_ -> g x
x)
prodOutL :: f :*: g ~> f
prodOutL :: forall {k} (f :: k -> *) (g :: k -> *) (x :: k). (:*:) f g x -> f x
prodOutL (f x
x :*: g x
_) = f x
x
prodOutR :: f :*: g ~> g
prodOutR :: forall {k} (f :: k -> *) (g :: k -> *) (x :: k). (:*:) f g x -> g x
prodOutR (f x
_ :*: g x
y) = g x
y
class (Tensor t i, SemigroupIn t f) => MonoidIn t i f where
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    pureT  :: i ~> f
    default pureT :: Interpret (ListBy t) f => i ~> f
    pureT  = ListBy t f x -> f x
ListBy t f ~> f
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Interpret t f =>
t f ~> f
retract (ListBy t f x -> f x) -> (i x -> ListBy t f x) -> i x -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ListBy t f <~> (i :+: t f (ListBy t f)))
-> (i :+: t f (ListBy t f)) ~> ListBy t f
forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
ListBy t f <~> (i :+: t f (ListBy t f))
splittingLB @t) ((:+:) i (t f (ListBy t f)) x -> ListBy t f x)
-> (i x -> (:+:) i (t f (ListBy t f)) x) -> i x -> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i x -> (:+:) i (t f (ListBy t f)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1
retractLB :: forall t i f. MonoidIn t i f => ListBy t f ~> f
retractLB :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
MonoidIn t i f =>
ListBy t f ~> f
retractLB = (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
MonoidIn t i f =>
i ~> f
pureT @t (i ~> f)
-> (t f (ListBy t f) ~> f) -> (i :+: t f (ListBy t f)) ~> f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *).
SemigroupIn t h =>
(f ~> h) -> (g ~> h) -> t f g ~> h
!*! forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
SemigroupIn t f =>
t f f ~> f
biretract @t (t f f x -> f x)
-> (t f (ListBy t f) x -> t f f x) -> t f (ListBy t f) x -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ListBy t f ~> f) -> t f (ListBy t f) ~> t f f
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> t f g ~> t f l
hright (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
MonoidIn t i f =>
ListBy t f ~> f
retractLB @t))
              ((:+:) i (t f (ListBy t f)) x -> f x)
-> (ListBy t f x -> (:+:) i (t f (ListBy t f)) x)
-> ListBy t f x
-> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
ListBy t f ~> (i :+: t f (ListBy t f))
unconsLB @t
interpretLB :: forall t i g f. MonoidIn t i f => (g ~> f) -> ListBy t g ~> f
interpretLB :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *) (f :: * -> *).
MonoidIn t i f =>
(g ~> f) -> ListBy t g ~> f
interpretLB g ~> f
f = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
MonoidIn t i f =>
ListBy t f ~> f
retractLB @t (ListBy t f x -> f x)
-> (ListBy t g x -> ListBy t f x) -> ListBy t g x -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (g ~> f) -> ListBy t g ~> ListBy t f
forall {k} {k1} (t :: (k -> *) -> k1 -> *) (f :: k -> *)
       (g :: k -> *).
HFunctor t =>
(f ~> g) -> t f ~> t g
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> ListBy t f ~> ListBy t g
hmap g x -> f x
g ~> f
f
inL
    :: forall t i f g. MonoidIn t i g
    => f ~> t f g
inL :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *) (g :: * -> *).
MonoidIn t i g =>
f ~> t f g
inL = (i ~> g) -> t f i ~> t f g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> t f g ~> t f l
hright (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
MonoidIn t i f =>
i ~> f
pureT @t) (t f i x -> t f g x) -> (f x -> t f i x) -> f x -> t f g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> t f i x
forall (f :: * -> *). f ~> t f i
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
f ~> t f i
intro1
inR
    :: forall t i f g. MonoidIn t i f
    => g ~> t f g
inR :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *) (g :: * -> *).
MonoidIn t i f =>
g ~> t f g
inR = (i ~> f) -> t i g ~> t f g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
forall (f :: * -> *) (j :: * -> *) (g :: * -> *).
(f ~> j) -> t f g ~> t j g
hleft (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
MonoidIn t i f =>
i ~> f
pureT @t) (t i g x -> t f g x) -> (g x -> t i g x) -> g x -> t f g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> t i g x
forall (g :: * -> *). g ~> t i g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *).
Tensor t i =>
g ~> t i g
intro2
outL
    :: (Tensor t Proxy, FunctorBy t f)
    => t f g ~> f
outL :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
       (g :: * -> *).
(Tensor t Proxy, FunctorBy t f) =>
t f g ~> f
outL = t f Proxy x -> f x
t f Proxy ~> f
forall (f :: * -> *). FunctorBy t f => t f Proxy ~> f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Tensor t i, FunctorBy t f) =>
t f i ~> f
elim1 (t f Proxy x -> f x) -> (t f g x -> t f Proxy x) -> t f g x -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (g ~> Proxy) -> t f g ~> t f Proxy
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> t f g ~> t f l
hright g x -> Proxy x
g ~> Proxy
forall {k} (f :: k -> *) (x :: k). f x -> Proxy x
absorb
outR
    :: (Tensor t Proxy, FunctorBy t g)
    => t f g ~> g
outR :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (g :: * -> *)
       (f :: * -> *).
(Tensor t Proxy, FunctorBy t g) =>
t f g ~> g
outR = t Proxy g x -> g x
t Proxy g ~> g
forall (g :: * -> *). FunctorBy t g => t Proxy g ~> g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *).
(Tensor t i, FunctorBy t g) =>
t i g ~> g
elim2 (t Proxy g x -> g x) -> (t f g x -> t Proxy g x) -> t f g x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f ~> Proxy) -> t f g ~> t Proxy g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
forall (f :: * -> *) (j :: * -> *) (g :: * -> *).
(f ~> j) -> t f g ~> t j g
hleft f x -> Proxy x
f ~> Proxy
forall {k} (f :: k -> *) (x :: k). f x -> Proxy x
absorb
class Tensor t i => Matchable t i where
    
    
    
    
    
    unsplitNE :: FunctorBy t f => t f (ListBy t f) ~> NonEmptyBy t f
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    matchLB   :: FunctorBy t f => ListBy t f ~> i :+: NonEmptyBy t f
splittingNE
    :: (Matchable t i, FunctorBy t f)
    => NonEmptyBy t f <~> t f (ListBy t f)
splittingNE :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
NonEmptyBy t f <~> t f (ListBy t f)
splittingNE = (NonEmptyBy t f ~> t f (ListBy t f))
-> (t f (ListBy t f) ~> NonEmptyBy t f)
-> NonEmptyBy t f <~> t f (ListBy t f)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF NonEmptyBy t f x -> t f (ListBy t f) x
NonEmptyBy t f ~> t f (ListBy t f)
forall (f :: * -> *). NonEmptyBy t f ~> t f (ListBy t f)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> t f (ListBy t f)
splitNE t f (ListBy t f) x -> NonEmptyBy t f x
t f (ListBy t f) ~> NonEmptyBy t f
forall (f :: * -> *).
FunctorBy t f =>
t f (ListBy t f) ~> NonEmptyBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE
matchingLB
    :: forall t i f. (Matchable t i, FunctorBy t f)
    => ListBy t f <~> i :+: NonEmptyBy t f
matchingLB :: forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
ListBy t f <~> (i :+: NonEmptyBy t f)
matchingLB = (ListBy t f ~> (i :+: NonEmptyBy t f))
-> ((i :+: NonEmptyBy t f) ~> ListBy t f)
-> ListBy t f <~> (i :+: NonEmptyBy t f)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
ListBy t f ~> (i :+: NonEmptyBy t f)
matchLB @t) (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
i ~> ListBy t f
nilLB @t (i ~> ListBy t f)
-> (NonEmptyBy t f ~> ListBy t f)
-> (i :+: NonEmptyBy t f) ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *).
SemigroupIn t h =>
(f ~> h) -> (g ~> h) -> t f g ~> h
!*! forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> ListBy t f
fromNE @t)
instance Tensor (:*:) Proxy where
    type ListBy (:*:) = ListF
    intro1 :: forall (f :: * -> *). f ~> (f :*: Proxy)
intro1 = (f x -> Proxy x -> (:*:) f Proxy x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Proxy x
forall {k} (t :: k). Proxy t
Proxy)
    intro2 :: forall (g :: * -> *). g ~> (Proxy :*: g)
intro2 = (Proxy x
forall {k} (t :: k). Proxy t
Proxy Proxy x -> g x -> (:*:) Proxy g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:)
    elim1 :: forall (f :: * -> *). FunctorBy (:*:) f => (f :*: Proxy) ~> f
elim1 (f x
x      :*: ~Proxy x
Proxy) = f x
x
    elim2 :: forall (g :: * -> *). FunctorBy (:*:) g => (Proxy :*: g) ~> g
elim2 (~Proxy x
Proxy :*: g x
y     ) = g x
y
    appendLB :: forall (f :: * -> *).
(ListBy (:*:) f :*: ListBy (:*:) f) ~> ListBy (:*:) f
appendLB (ListF [f x]
xs :*: ListF [f x]
ys) = [f x] -> ListF f x
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([f x]
xs [f x] -> [f x] -> [f x]
forall a. [a] -> [a] -> [a]
++ [f x]
ys)
    splitNE :: forall (f :: * -> *). NonEmptyBy (:*:) f ~> (f :*: ListBy (:*:) f)
splitNE     = NonEmptyF f x -> (:*:) f (ListF f) x
NonEmptyBy (:*:) f x -> (:*:) f (ListBy (:*:) f) x
forall {k} (f :: k -> *) (a :: k).
NonEmptyF f a -> (:*:) f (ListF f) a
nonEmptyProd
    splittingLB :: forall (f :: * -> *).
ListBy (:*:) f <~> (Proxy :+: (f :*: ListBy (:*:) f))
splittingLB = (ListF f ~> (Proxy :+: (f :*: ListF f)))
-> ((Proxy :+: (f :*: ListF f)) ~> ListF f)
-> ListF f <~> (Proxy :+: (f :*: ListF f))
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF ListF f x -> (:+:) Proxy (f :*: ListF f) x
ListF f ~> (Proxy :+: (f :*: ListF f))
forall {k} {f :: k -> *} {p :: k}.
ListF f p -> (:+:) Proxy (f :*: ListF f) p
to_ (:+:) Proxy (f :*: ListF f) x -> ListF f x
(Proxy :+: (f :*: ListF f)) ~> ListF f
forall {k} {f :: k -> *} {a :: k}.
(:+:) Proxy (f :*: ListF f) a -> ListF f a
from_
      where
        to_ :: ListF f p -> (:+:) Proxy (f :*: ListF f) p
to_ = \case
          ListF []     -> Proxy p -> (:+:) Proxy (f :*: ListF f) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Proxy p
forall {k} (t :: k). Proxy t
Proxy
          ListF (f p
x:[f p]
xs) -> (:*:) f (ListF f) p -> (:+:) Proxy (f :*: ListF f) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (f p
x f p -> ListF f p -> (:*:) f (ListF f) p
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: [f p] -> ListF f p
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF [f p]
xs)
        from_ :: (:+:) Proxy (f :*: ListF f) a -> ListF f a
from_ = \case
          L1 ~Proxy a
Proxy           -> [f a] -> ListF f a
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF []
          R1 (f a
x :*: ListF [f a]
xs) -> [f a] -> ListF f a
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF (f a
xf a -> [f a] -> [f a]
forall a. a -> [a] -> [a]
:[f a]
xs)
    toListBy :: forall (f :: * -> *). (f :*: f) ~> ListBy (:*:) f
toListBy (f x
x :*: f x
y) = [f x] -> ListF f x
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF [f x
x, f x
y]
instance Plus f => MonoidIn (:*:) Proxy f where
    pureT :: Proxy ~> f
pureT Proxy x
_        = f x
forall a. f a
forall (f :: * -> *) a. Plus f => f a
zero
instance Tensor Product Proxy where
    type ListBy Product = ListF
    intro1 :: forall (f :: * -> *). f ~> Product f Proxy
intro1 = (f x -> Proxy x -> Product f Proxy x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
`Pair` Proxy x
forall {k} (t :: k). Proxy t
Proxy)
    intro2 :: forall (g :: * -> *). g ~> Product Proxy g
intro2 = (Proxy x
forall {k} (t :: k). Proxy t
Proxy Proxy x -> g x -> Product Proxy g x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
`Pair`)
    elim1 :: forall (f :: * -> *). FunctorBy Product f => Product f Proxy ~> f
elim1 (Pair f x
x ~Proxy x
Proxy) = f x
x
    elim2 :: forall (g :: * -> *). FunctorBy Product g => Product Proxy g ~> g
elim2 (Pair ~Proxy x
Proxy g x
y) = g x
y
    appendLB :: forall (f :: * -> *).
Product (ListBy Product f) (ListBy Product f) ~> ListBy Product f
appendLB (ListF [f x]
xs `Pair` ListF [f x]
ys) = [f x] -> ListF f x
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([f x]
xs [f x] -> [f x] -> [f x]
forall a. [a] -> [a] -> [a]
++ [f x]
ys)
    splitNE :: forall (f :: * -> *).
NonEmptyBy Product f ~> Product f (ListBy Product f)
splitNE     = ((f :*: ListF f) <~> Product f (ListF f))
-> (f :*: ListF f) ~> Product f (ListF f)
forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF p (Product f (ListF f) a) (Product f (ListF f) a)
-> p ((:*:) f (ListF f) a) ((:*:) f (ListF f) a)
forall {k} (f :: k -> *) (g :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p (Product f g a) (Product f g a) -> p ((:*:) f g a) ((:*:) f g a)
(f :*: ListF f) <~> Product f (ListF f)
prodProd ((:*:) f (ListF f) x -> Product f (ListF f) x)
-> (NonEmptyF f x -> (:*:) f (ListF f) x)
-> NonEmptyF f x
-> Product f (ListF f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyF f x -> (:*:) f (ListF f) x
forall {k} (f :: k -> *) (a :: k).
NonEmptyF f a -> (:*:) f (ListF f) a
nonEmptyProd
    splittingLB :: forall (f :: * -> *).
ListBy Product f <~> (Proxy :+: Product f (ListBy Product f))
splittingLB = (ListF f ~> (Proxy :+: Product f (ListF f)))
-> ((Proxy :+: Product f (ListF f)) ~> ListF f)
-> ListF f <~> (Proxy :+: Product f (ListF f))
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF ListF f x -> (:+:) Proxy (Product f (ListF f)) x
ListF f ~> (Proxy :+: Product f (ListF f))
forall {k} {f :: k -> *} {p :: k}.
ListF f p -> (:+:) Proxy (Product f (ListF f)) p
to_ (:+:) Proxy (Product f (ListF f)) x -> ListF f x
(Proxy :+: Product f (ListF f)) ~> ListF f
forall {k} {f :: k -> *} {a :: k}.
(:+:) Proxy (Product f (ListF f)) a -> ListF f a
from_
      where
        to_ :: ListF f p -> (:+:) Proxy (Product f (ListF f)) p
to_ = \case
          ListF []     -> Proxy p -> (:+:) Proxy (Product f (ListF f)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Proxy p
forall {k} (t :: k). Proxy t
Proxy
          ListF (f p
x:[f p]
xs) -> Product f (ListF f) p -> (:+:) Proxy (Product f (ListF f)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (f p
x f p -> ListF f p -> Product f (ListF f) p
forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
`Pair` [f p] -> ListF f p
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF [f p]
xs)
        from_ :: (:+:) Proxy (Product f (ListF f)) a -> ListF f a
from_ = \case
          L1 ~Proxy a
Proxy              -> [f a] -> ListF f a
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF []
          R1 (f a
x `Pair` ListF [f a]
xs) -> [f a] -> ListF f a
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF (f a
xf a -> [f a] -> [f a]
forall a. a -> [a] -> [a]
:[f a]
xs)
    toListBy :: forall (f :: * -> *). Product f f ~> ListBy Product f
toListBy (Pair f x
x f x
y) = [f x] -> ListF f x
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF [f x
x, f x
y]
instance Plus f => MonoidIn Product Proxy f where
    pureT :: Proxy ~> f
pureT Proxy x
_         = f x
forall a. f a
forall (f :: * -> *) a. Plus f => f a
zero
instance Tensor Day Identity where
    type ListBy Day = Ap
    intro1 :: forall (f :: * -> *). f ~> Day f Identity
intro1   = f x -> Day f Identity x
forall (f :: * -> *). f ~> Day f Identity
D.intro2
    intro2 :: forall (g :: * -> *). g ~> Day Identity g
intro2   = g x -> Day Identity g x
forall (g :: * -> *). g ~> Day Identity g
D.intro1
    elim1 :: forall (f :: * -> *). FunctorBy Day f => Day f Identity ~> f
elim1    = Day f Identity x -> f x
forall (f :: * -> *) a. Functor f => Day f Identity a -> f a
D.elim2
    elim2 :: forall (g :: * -> *). FunctorBy Day g => Day Identity g ~> g
elim2    = Day Identity g x -> g x
forall (f :: * -> *) a. Functor f => Day Identity f a -> f a
D.elim1
    appendLB :: forall (f :: * -> *).
Day (ListBy Day f) (ListBy Day f) ~> ListBy Day f
appendLB (Day ListBy Day f b
x ListBy Day f c
y b -> c -> x
z) = b -> c -> x
z (b -> c -> x) -> Ap f b -> Ap f (c -> x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ap f b
ListBy Day f b
x Ap f (c -> x) -> Ap f c -> Ap f x
forall a b. Ap f (a -> b) -> Ap f a -> Ap f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ap f c
ListBy Day f c
y
    splitNE :: forall (f :: * -> *). NonEmptyBy Day f ~> Day f (ListBy Day f)
splitNE     = Ap1 f x -> Day f (Ap f) x
NonEmptyBy Day f x -> Day f (ListBy Day f) x
forall (f :: * -> *) a. Ap1 f a -> Day f (Ap f) a
ap1Day
    splittingLB :: forall (f :: * -> *).
ListBy Day f <~> (Identity :+: Day f (ListBy Day f))
splittingLB = (Ap f ~> (Identity :+: Day f (Ap f)))
-> ((Identity :+: Day f (Ap f)) ~> Ap f)
-> Ap f <~> (Identity :+: Day f (Ap f))
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF Ap f x -> (:+:) Identity (Day f (Ap f)) x
Ap f ~> (Identity :+: Day f (Ap f))
forall {f :: * -> *} {p}. Ap f p -> (:+:) Identity (Day f (Ap f)) p
to_ (:+:) Identity (Day f (Ap f)) x -> Ap f x
(Identity :+: Day f (Ap f)) ~> Ap f
forall {f :: * -> *} {a}. (:+:) Identity (Day f (Ap f)) a -> Ap f a
from_
      where
        to_ :: Ap f p -> (:+:) Identity (Day f (Ap f)) p
to_ = \case
          Pure p
x  -> Identity p -> (:+:) Identity (Day f (Ap f)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (p -> Identity p
forall a. a -> Identity a
Identity p
x)
          Ap f a1
x Ap f (a1 -> p)
xs -> Day f (Ap f) p -> (:+:) Identity (Day f (Ap f)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (f a1 -> Ap f (a1 -> p) -> (a1 -> (a1 -> p) -> p) -> Day f (Ap f) p
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
Day f a1
x Ap f (a1 -> p)
xs a1 -> (a1 -> p) -> p
forall a b. a -> (a -> b) -> b
(&))
        from_ :: (:+:) Identity (Day f (Ap f)) a -> Ap f a
from_ = \case
          L1 (Identity a
x) -> a -> Ap f a
forall a (f :: * -> *). a -> Ap f a
Pure a
x
          R1 (Day f b
x Ap f c
xs b -> c -> a
f) -> f b -> Ap f (b -> a) -> Ap f a
forall (f :: * -> *) a1 a. f a1 -> Ap f (a1 -> a) -> Ap f a
Ap f b
x ((b -> c -> a) -> c -> b -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> a
f (c -> b -> a) -> Ap f c -> Ap f (b -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ap f c
xs)
    toListBy :: forall (f :: * -> *). Day f f ~> ListBy Day f
toListBy (Day f b
x f c
y b -> c -> x
z) = f b -> Ap f (b -> x) -> Ap f x
forall (f :: * -> *) a1 a. f a1 -> Ap f (a1 -> a) -> Ap f a
Ap f b
x (f c -> Ap f (c -> b -> x) -> Ap f (b -> x)
forall (f :: * -> *) a1 a. f a1 -> Ap f (a1 -> a) -> Ap f a
Ap f c
y ((c -> b -> x) -> Ap f (c -> b -> x)
forall a (f :: * -> *). a -> Ap f a
Pure ((b -> c -> x) -> c -> b -> x
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> x
z)))
instance (Apply f, Applicative f) => MonoidIn Day Identity f where
    pureT :: Identity ~> f
pureT            = Identity x -> f x
Identity ~> f
forall (f :: * -> *). Applicative f => Identity ~> f
generalize
instance Tensor CD.Day Proxy where
    type ListBy CD.Day = Div
    intro1 :: forall (f :: * -> *). f ~> Day f Proxy
intro1 = f x -> Day f Proxy x
forall (f :: * -> *). f ~> Day f Proxy
CD.intro2
    intro2 :: forall (g :: * -> *). g ~> Day Proxy g
intro2 = g x -> Day Proxy g x
forall (g :: * -> *). g ~> Day Proxy g
CD.intro1
    elim1 :: forall (f :: * -> *). FunctorBy Day f => Day f Proxy ~> f
elim1 = Day f Proxy x -> f x
forall (f :: * -> *) (g :: * -> *) a.
Contravariant f =>
Day f g a -> f a
CD.day1
    elim2 :: forall (g :: * -> *). FunctorBy Day g => Day Proxy g ~> g
elim2 = Day Proxy g x -> g x
forall (g :: * -> *) (f :: * -> *) a.
Contravariant g =>
Day f g a -> g a
CD.day2
    appendLB :: forall (f :: * -> *).
Day (ListBy Day f) (ListBy Day f) ~> ListBy Day f
appendLB (CD.Day ListBy Day f b
x ListBy Day f c
y x -> (b, c)
z) = (x -> (b, c)) -> Div f b -> Div f c -> Div f x
forall a b c. (a -> (b, c)) -> Div f b -> Div f c -> Div f a
forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide x -> (b, c)
z Div f b
ListBy Day f b
x Div f c
ListBy Day f c
y
    splitNE :: forall (f :: * -> *). NonEmptyBy Day f ~> Day f (ListBy Day f)
splitNE = (:*:) (Coyoneda f) (ListF (Coyoneda f)) x -> Day f (Div f) x
forall {f :: * -> *} {f :: * -> *} {p}.
(:*:) (Coyoneda f) (ListF (Coyoneda f)) p -> Day f (Div f) p
go ((:*:) (Coyoneda f) (ListF (Coyoneda f)) x -> Day f (Div f) x)
-> (Div1 f x -> (:*:) (Coyoneda f) (ListF (Coyoneda f)) x)
-> Div1 f x
-> Day f (Div f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> t f (ListBy t f)
splitNE @(:*:) (NonEmptyF (Coyoneda f) x
 -> (:*:) (Coyoneda f) (ListF (Coyoneda f)) x)
-> (Div1 f x -> NonEmptyF (Coyoneda f) x)
-> Div1 f x
-> (:*:) (Coyoneda f) (ListF (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) -> NonEmptyF (Coyoneda f) x)
-> (Div1 f x -> NonEmpty (Coyoneda f x))
-> Div1 f x
-> NonEmptyF (Coyoneda f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div1 f x -> NonEmpty (Coyoneda f x)
forall (f :: * -> *) a. Div1 f a -> NonEmpty (Coyoneda f a)
unDiv1
      where
        go :: (:*:) (Coyoneda f) (ListF (Coyoneda f)) p -> Day f (Div f) p
go (CCY.Coyoneda p -> b
f f b
x :*: ListF [Coyoneda f p]
xs) = f b -> Div f p -> (p -> (b, p)) -> Day f (Div f) p
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x ([Coyoneda f p] -> Div f p
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div [Coyoneda f p]
xs) (\p
y -> (p -> b
f p
y, p
y))
    splittingLB :: forall (f :: * -> *).
ListBy Day f <~> (Proxy :+: Day f (ListBy Day f))
splittingLB = (Div f ~> ListF (Coyoneda f))
-> (ListF (Coyoneda f) ~> Div f) -> Div f <~> ListF (Coyoneda f)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF ([Coyoneda f x] -> ListF (Coyoneda f) x
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([Coyoneda f x] -> ListF (Coyoneda f) x)
-> (Div f x -> [Coyoneda f x]) -> Div f x -> ListF (Coyoneda f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div f x -> [Coyoneda f x]
forall (f :: * -> *) a. Div f a -> [Coyoneda f a]
unDiv) ([Coyoneda f x] -> Div f x
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div ([Coyoneda f x] -> Div f x)
-> (ListF (Coyoneda f) x -> [Coyoneda f x])
-> ListF (Coyoneda f) x
-> Div f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListF (Coyoneda f) x -> [Coyoneda f x]
forall {k} (f :: k -> *) (a :: k). ListF f a -> [f a]
runListF) (p (ListF (Coyoneda f) a) (ListF (Coyoneda f) a)
 -> p (Div f a) (Div f a))
-> (p ((:+:) Proxy (Day f (Div f)) a)
      ((:+:) Proxy (Day f (Div f)) a)
    -> p (ListF (Coyoneda f) a) (ListF (Coyoneda f) a))
-> p ((:+:) Proxy (Day f (Div f)) a)
     ((:+:) Proxy (Day f (Div f)) a)
-> p (Div f a) (Div f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
ListBy t f <~> (i :+: t f (ListBy t f))
splittingLB @(:*:) (p ((:+:) Proxy (Coyoneda f :*: ListF (Coyoneda f)) a)
   ((:+:) Proxy (Coyoneda f :*: ListF (Coyoneda f)) a)
 -> p (ListF (Coyoneda f) a) (ListF (Coyoneda f) a))
-> (p ((:+:) Proxy (Day f (Div f)) a)
      ((:+:) Proxy (Day f (Div f)) a)
    -> p ((:+:) Proxy (Coyoneda f :*: ListF (Coyoneda f)) a)
         ((:+:) Proxy (Coyoneda f :*: ListF (Coyoneda f)) a))
-> p ((:+:) Proxy (Day f (Div f)) a)
     ((:+:) Proxy (Day f (Div f)) a)
-> p (ListF (Coyoneda f) a) (ListF (Coyoneda f) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Proxy :+: (Coyoneda f :*: ListF (Coyoneda f)))
 ~> (Proxy :+: Day f (Div f)))
-> ((Proxy :+: Day f (Div f))
    ~> (Proxy :+: (Coyoneda f :*: ListF (Coyoneda f))))
-> (Proxy :+: (Coyoneda f :*: ListF (Coyoneda f)))
   <~> (Proxy :+: Day f (Div f))
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (((Coyoneda f :*: ListF (Coyoneda f)) ~> Day f (Div f))
-> (Proxy :+: (Coyoneda f :*: ListF (Coyoneda f)))
   ~> (Proxy :+: Day f (Div f))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> (f :+: g) ~> (f :+: l)
hright (:*:) (Coyoneda f) (ListF (Coyoneda f)) x -> Day f (Div f) x
(Coyoneda f :*: ListF (Coyoneda f)) ~> Day f (Div f)
forall {f :: * -> *} {f :: * -> *} {p}.
(:*:) (Coyoneda f) (ListF (Coyoneda f)) p -> Day f (Div f) p
to_) ((Day f (Div f) ~> (Coyoneda f :*: ListF (Coyoneda f)))
-> (Proxy :+: Day f (Div f))
   ~> (Proxy :+: (Coyoneda f :*: ListF (Coyoneda f)))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> (f :+: g) ~> (f :+: l)
hright Day f (Div f) x -> (:*:) (Coyoneda f) (ListF (Coyoneda f)) x
Day f (Div f) ~> (Coyoneda f :*: ListF (Coyoneda f))
forall {f :: * -> *} {f :: * -> *} {a}.
Day f (Div f) a -> (:*:) (Coyoneda f) (ListF (Coyoneda f)) a
from_)
      where
        to_ :: (:*:) (Coyoneda f) (ListF (Coyoneda f)) p -> Day f (Div f) p
to_   (CCY.Coyoneda p -> b
f f b
x :*: ListF [Coyoneda f p]
xs) = f b -> Div f p -> (p -> (b, p)) -> Day f (Div f) p
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x ([Coyoneda f p] -> Div f p
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div [Coyoneda f p]
xs) (\p
y -> (p -> b
f p
y, p
y))
        from_ :: Day f (Div f) a -> (:*:) (Coyoneda f) (ListF (Coyoneda f)) a
from_ (CD.Day f b
x (Div [Coyoneda f c]
xs) a -> (b, c)
f) = (a -> b) -> f b -> Coyoneda f a
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (a -> (b, c)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
f) f b
x Coyoneda f a
-> ListF (Coyoneda f) a
-> (:*:) (Coyoneda f) (ListF (Coyoneda f)) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (a -> c) -> ListF (Coyoneda f) c -> ListF (Coyoneda f) a
forall a' a.
(a' -> a) -> ListF (Coyoneda f) a -> ListF (Coyoneda f) a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (a -> (b, c)) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
f) ([Coyoneda f c] -> ListF (Coyoneda f) c
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF [Coyoneda f c]
xs)
    toListBy :: forall (f :: * -> *). Day f f ~> ListBy Day f
toListBy (CD.Day f b
x f c
y x -> (b, c)
f) = [Coyoneda f x] -> Div f x
[Coyoneda f x] -> ListBy Day f x
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div ([Coyoneda f x] -> ListBy Day f x)
-> ((:*:) (Coyoneda f) (Coyoneda f) x -> [Coyoneda f x])
-> (:*:) (Coyoneda f) (Coyoneda f) x
-> ListBy Day f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListF (Coyoneda f) x -> [Coyoneda f x]
forall {k} (f :: k -> *) (a :: k). ListF f a -> [f a]
runListF (ListF (Coyoneda f) x -> [Coyoneda f x])
-> ((:*:) (Coyoneda f) (Coyoneda f) x -> ListF (Coyoneda f) x)
-> (:*:) (Coyoneda f) (Coyoneda f) x
-> [Coyoneda f x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:*:) (Coyoneda f) (Coyoneda f) x -> ListF (Coyoneda f) x
(:*:) (Coyoneda f) (Coyoneda f) x -> ListBy (:*:) (Coyoneda f) x
forall (f :: * -> *). (f :*: f) ~> ListBy (:*:) f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t f f ~> ListBy t f
toListBy ((:*:) (Coyoneda f) (Coyoneda f) x -> ListBy Day f x)
-> (:*:) (Coyoneda f) (Coyoneda f) x -> ListBy Day f x
forall a b. (a -> b) -> a -> b
$
        (x -> b) -> f b -> Coyoneda f x
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (x -> (b, c)) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x Coyoneda f x -> Coyoneda f x -> (:*:) (Coyoneda f) (Coyoneda f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (x -> c) -> f c -> Coyoneda f x
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (x -> (b, c)) -> x -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f c
y
instance (Divise f, Divisible f) => MonoidIn CD.Day Proxy f where
    pureT :: Proxy ~> f
pureT Proxy x
_ = f x
forall a. f a
forall (f :: * -> *) a. Divisible f => f a
conquer
instance Tensor ID.Day Identity where
    type ListBy ID.Day = DivAp
    intro1 :: forall (f :: * -> *). f ~> Day f Identity
intro1 = f x -> Day f Identity x
forall (f :: * -> *). f ~> Day f Identity
ID.intro2
    intro2 :: forall (g :: * -> *). g ~> Day Identity g
intro2 = g x -> Day Identity g x
forall (g :: * -> *). g ~> Day Identity g
ID.intro1
    elim1 :: forall (f :: * -> *). FunctorBy Day f => Day f Identity ~> f
elim1 = Day f Identity x -> f x
forall (f :: * -> *) a. Invariant f => Day f Identity a -> f a
ID.elim2
    elim2 :: forall (g :: * -> *). FunctorBy Day g => Day Identity g ~> g
elim2 = Day Identity g x -> g x
forall (f :: * -> *) a. Invariant f => Day Identity f a -> f a
ID.elim1
    appendLB :: forall (f :: * -> *).
Day (ListBy Day f) (ListBy Day f) ~> ListBy Day f
appendLB (ID.Day (DivAp Chain Day Identity f b
xs) (DivAp Chain Day Identity f c
ys) b -> c -> x
f x -> (b, c)
g) = Chain Day Identity f x -> DivAp f x
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f x -> DivAp f x)
-> Chain Day Identity f x -> DivAp f x
forall a b. (a -> b) -> a -> b
$ case Chain Day Identity f b
xs of
      Done (Identity b
x)      -> (c -> x)
-> (x -> c) -> Chain Day Identity f c -> Chain Day Identity f x
forall a b.
(a -> b)
-> (b -> a) -> Chain Day Identity f a -> Chain Day Identity f b
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> x
f b
x) ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (x -> (b, c)) -> x -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
g) Chain Day Identity f c
ys
      More (ID.Day f b
z Chain Day Identity f c
zs b -> c -> b
h b -> (b, c)
j) -> Day f (Chain Day Identity f) x -> Chain Day Identity f x
forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
       (f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More (Day f (Chain Day Identity f) x -> Chain Day Identity f x)
-> Day f (Chain Day Identity f) x -> Chain Day Identity f x
forall a b. (a -> b) -> a -> b
$ f b
-> Chain Day Identity f (c, c)
-> (b -> (c, c) -> x)
-> (x -> (b, (c, c)))
-> Day f (Chain Day Identity f) x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
ID.Day
        f b
z
        (DivAp f (c, c) -> Chain Day Identity f (c, c)
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (DivAp f (c, c) -> Chain Day Identity f (c, c))
-> DivAp f (c, c) -> Chain Day Identity f (c, c)
forall a b. (a -> b) -> a -> b
$ Day (ListBy Day f) (ListBy Day f) (c, c) -> ListBy Day f (c, c)
forall (f :: * -> *).
Day (ListBy Day f) (ListBy Day f) ~> ListBy Day f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB (DivAp f c
-> DivAp f c
-> (c -> c -> (c, c))
-> ((c, c) -> (c, c))
-> Day (DivAp f) (DivAp f) (c, c)
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
ID.Day (Chain Day Identity f c -> DivAp f c
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp Chain Day Identity f c
zs) (Chain Day Identity f c -> DivAp f c
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp Chain Day Identity f c
ys) (,) (c, c) -> (c, c)
forall a. a -> a
id))
        (\b
q (c
r, c
s) -> b -> c -> x
f (b -> c -> b
h b
q c
r) c
s)
        (((b, c), c) -> (b, (c, c))
forall a b c. ((a, b), c) -> (a, (b, c))
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc (((b, c), c) -> (b, (c, c)))
-> (x -> ((b, c), c)) -> x -> (b, (c, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> (b, c)) -> (b, c) -> ((b, c), c)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> (b, c)
j ((b, c) -> ((b, c), c)) -> (x -> (b, c)) -> x -> ((b, c), c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
g)
    splitNE :: forall (f :: * -> *). NonEmptyBy Day f ~> Day f (ListBy Day f)
splitNE = (Chain1 Day f x -> Day f (Chain Day Identity f) x)
-> DivAp1 f x -> Day f (DivAp f) x
forall a b. Coercible a b => a -> b
coerce Chain1 Day f x -> Day f (Chain Day Identity f) x
Chain1 Day f ~> Day f (Chain Day Identity f)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
Chain1 t f ~> t f (Chain t i f)
splitChain1
    splittingLB :: forall (f :: * -> *).
ListBy Day f <~> (Identity :+: Day f (ListBy Day f))
splittingLB = p (Chain Day Identity f a) (Chain Day Identity f a)
-> p (DivAp f a) (DivAp f a)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
 forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
DivAp f <~> Chain Day Identity f
coercedF (p (Chain Day Identity f a) (Chain Day Identity f a)
 -> p (DivAp f a) (DivAp f a))
-> (p ((:+:) Identity (Day f (DivAp f)) a)
      ((:+:) Identity (Day f (DivAp f)) a)
    -> p (Chain Day Identity f a) (Chain Day Identity f a))
-> p ((:+:) Identity (Day f (DivAp f)) a)
     ((:+:) Identity (Day f (DivAp f)) a)
-> p (DivAp f a) (DivAp f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ((:+:) Identity (Day f (Chain Day Identity f)) a)
  ((:+:) Identity (Day f (Chain Day Identity f)) a)
-> p (Chain Day Identity f a) (Chain Day Identity f a)
forall {k1} {k2} (t :: k1 -> (k2 -> *) -> k2 -> *) (i :: k2 -> *)
       (f :: k1) (p :: * -> * -> *) (a :: k2).
Profunctor p =>
p ((:+:) i (t f (Chain t i f)) a) ((:+:) i (t f (Chain t i f)) a)
-> p (Chain t i f a) (Chain t i f a)
splittingChain (p ((:+:) Identity (Day f (Chain Day Identity f)) a)
   ((:+:) Identity (Day f (Chain Day Identity f)) a)
 -> p (Chain Day Identity f a) (Chain Day Identity f a))
-> (p ((:+:) Identity (Day f (DivAp f)) a)
      ((:+:) Identity (Day f (DivAp f)) a)
    -> p ((:+:) Identity (Day f (Chain Day Identity f)) a)
         ((:+:) Identity (Day f (Chain Day Identity f)) a))
-> p ((:+:) Identity (Day f (DivAp f)) a)
     ((:+:) Identity (Day f (DivAp f)) a)
-> p (Chain Day Identity f a) (Chain Day Identity f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ((:+:) Identity (Day f (DivAp f)) a)
  ((:+:) Identity (Day f (DivAp f)) a)
-> p ((:+:) Identity (Day f (Chain Day Identity f)) a)
     ((:+:) Identity (Day f (Chain Day Identity f)) a)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
 forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
(Identity :+: Day f (Chain Day Identity f))
<~> (Identity :+: Day f (DivAp f))
coercedF
    toListBy :: forall (f :: * -> *). Day f f ~> ListBy Day f
toListBy = Chain Day Identity f x -> DivAp f x
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f x -> DivAp f x)
-> (Day f f x -> Chain Day Identity f x) -> Day f f x -> DivAp f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day f (Chain Day Identity f) x -> Chain Day Identity f x
forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
       (f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More (Day f (Chain Day Identity f) x -> Chain Day Identity f x)
-> (Day f f x -> Day f (Chain Day Identity f) x)
-> Day f f x
-> Chain Day Identity f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f ~> Chain Day Identity f)
-> Day f f ~> Day f (Chain Day Identity f)
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> Day f g ~> Day f l
hright (DivAp f x -> Chain Day Identity f x
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (DivAp f x -> Chain Day Identity f x)
-> (f x -> DivAp f x) -> f x -> Chain Day Identity f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> DivAp f x
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> DivAp f
inject)
instance Matchable ID.Day Identity where
    unsplitNE :: forall (f :: * -> *).
FunctorBy Day f =>
Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE = (Day f (Chain Day Identity f) x -> Chain1 Day f x)
-> Day f (DivAp f) x -> DivAp1 f x
forall a b. Coercible a b => a -> b
coerce Day f (Chain Day Identity f) x -> Chain1 Day f x
Day f (Chain Day Identity f) ~> Chain1 Day f
forall (f :: * -> *).
Invariant f =>
Day f (Chain Day Identity f) ~> Chain1 Day f
unsplitNEIDay_
    matchLB :: forall (f :: * -> *).
FunctorBy Day f =>
ListBy Day f ~> (Identity :+: NonEmptyBy Day f)
matchLB = (Chain Day Identity f x -> (:+:) Identity (Chain1 Day f) x)
-> DivAp f x -> (:+:) Identity (DivAp1 f) x
forall a b. Coercible a b => a -> b
coerce Chain Day Identity f x -> (:+:) Identity (Chain1 Day f) x
Chain Day Identity f ~> (Identity :+: Chain1 Day f)
forall (f :: * -> *).
Invariant f =>
Chain Day Identity f ~> (Identity :+: Chain1 Day f)
matchLBIDay_
unsplitNEIDay_ :: Invariant f => ID.Day f (Chain ID.Day Identity f) ~> Chain1 ID.Day f
unsplitNEIDay_ :: forall (f :: * -> *).
Invariant f =>
Day f (Chain Day Identity f) ~> Chain1 Day f
unsplitNEIDay_ (ID.Day f b
x Chain Day Identity f c
xs b -> c -> x
g x -> (b, c)
f) = case Chain Day Identity f c
xs of
  Done (Identity c
r) -> f x -> Chain1 Day f x
forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
f a -> Chain1 t f a
Done1 (f x -> Chain1 Day f x) -> f x -> Chain1 Day f x
forall a b. (a -> b) -> a -> b
$ (b -> x) -> (x -> b) -> f b -> f x
forall a b. (a -> b) -> (b -> a) -> f a -> f b
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> x
`g` c
r) ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (x -> (b, c)) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x
  More Day f (Chain Day Identity f) c
ys           -> Day f (Chain1 Day f) x -> Chain1 Day f x
forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (Day f (Chain1 Day f) x -> Chain1 Day f x)
-> Day f (Chain1 Day f) x -> Chain1 Day f x
forall a b. (a -> b) -> a -> b
$ f b
-> Chain1 Day f c
-> (b -> c -> x)
-> (x -> (b, c))
-> Day f (Chain1 Day f) x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
ID.Day f b
x (Day f (Chain Day Identity f) c -> Chain1 Day f c
Day f (Chain Day Identity f) ~> Chain1 Day f
forall (f :: * -> *).
Invariant f =>
Day f (Chain Day Identity f) ~> Chain1 Day f
unsplitNEIDay_ Day f (Chain Day Identity f) c
ys) b -> c -> x
g x -> (b, c)
f
matchLBIDay_ :: Invariant f => Chain ID.Day Identity f ~> (Identity :+: Chain1 ID.Day f)
matchLBIDay_ :: forall (f :: * -> *).
Invariant f =>
Chain Day Identity f ~> (Identity :+: Chain1 Day f)
matchLBIDay_ = \case
  Done Identity x
x  -> Identity x -> (:+:) Identity (Chain1 Day f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Identity x
x
  More Day f (Chain Day Identity f) x
xs -> Chain1 Day f x -> (:+:) Identity (Chain1 Day f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Chain1 Day f x -> (:+:) Identity (Chain1 Day f) x)
-> Chain1 Day f x -> (:+:) Identity (Chain1 Day f) x
forall a b. (a -> b) -> a -> b
$ Day f (Chain Day Identity f) x -> Chain1 Day f x
Day f (Chain Day Identity f) ~> Chain1 Day f
forall (f :: * -> *).
Invariant f =>
Day f (Chain Day Identity f) ~> Chain1 Day f
unsplitNEIDay_ Day f (Chain Day Identity f) x
xs
instance Inplicative f => MonoidIn ID.Day Identity f where
    pureT :: Identity ~> f
pureT (Identity x
x) = x -> f x
forall a. a -> f a
forall (f :: * -> *) a. Inplicative f => a -> f a
knot x
x
instance Tensor IN.Night IN.Not where
    type ListBy IN.Night = DecAlt
    intro1 :: forall (f :: * -> *). f ~> Night f Not
intro1 = f x -> Night f Not x
forall (f :: * -> *). f ~> Night f Not
IN.intro2
    intro2 :: forall (g :: * -> *). g ~> Night Not g
intro2 = g x -> Night Not g x
forall (g :: * -> *). g ~> Night Not g
IN.intro1
    elim1 :: forall (f :: * -> *). FunctorBy Night f => Night f Not ~> f
elim1 = Night f Not x -> f x
Night f Not ~> f
forall (f :: * -> *). Invariant f => Night f Not ~> f
IN.elim2
    elim2 :: forall (g :: * -> *). FunctorBy Night g => Night Not g ~> g
elim2 = Night Not g x -> g x
Night Not g ~> g
forall (g :: * -> *). Invariant g => Night Not g ~> g
IN.elim1
    appendLB :: forall (f :: * -> *).
Night (ListBy Night f) (ListBy Night f) ~> ListBy Night f
appendLB (IN.Night (DecAlt Chain Night Not f b1
xs) (DecAlt Chain Night Not f c1
ys) b1 -> x
f c1 -> x
g x -> Either b1 c1
h) = Chain Night Not f x -> DecAlt f x
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt (Chain Night Not f x -> DecAlt f x)
-> Chain Night Not f x -> DecAlt f x
forall a b. (a -> b) -> a -> b
$ case Chain Night Not f b1
xs of
      Done Not b1
r      -> (c1 -> x)
-> (x -> c1) -> Chain Night Not f c1 -> Chain Night Not f x
forall a b.
(a -> b) -> (b -> a) -> Chain Night Not f a -> Chain Night Not f b
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap c1 -> x
g ((b1 -> c1) -> (c1 -> c1) -> Either b1 c1 -> c1
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> c1
forall a. Void -> a
absurd (Void -> c1) -> (b1 -> Void) -> b1 -> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not b1 -> b1 -> Void
forall a. Not a -> a -> Void
refute Not b1
r) c1 -> c1
forall a. a -> a
id (Either b1 c1 -> c1) -> (x -> Either b1 c1) -> x -> c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b1 c1
h) Chain Night Not f c1
ys
      More (IN.Night f b1
z Chain Night Not f c1
zs b1 -> b1
j c1 -> b1
k b1 -> Either b1 c1
l) -> Night f (Chain Night Not f) x -> Chain Night Not f x
forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
       (f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) x -> Chain Night Not f x)
-> Night f (Chain Night Not f) x -> Chain Night Not f x
forall a b. (a -> b) -> a -> b
$ f b1
-> Chain Night Not f (Either c1 c1)
-> (b1 -> x)
-> (Either c1 c1 -> x)
-> (x -> Either b1 (Either c1 c1))
-> Night f (Chain Night Not f) x
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
IN.Night
        f b1
z
        (DecAlt f (Either c1 c1) -> Chain Night Not f (Either c1 c1)
forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt (DecAlt f (Either c1 c1) -> Chain Night Not f (Either c1 c1))
-> DecAlt f (Either c1 c1) -> Chain Night Not f (Either c1 c1)
forall a b. (a -> b) -> a -> b
$ Night (ListBy Night f) (ListBy Night f) (Either c1 c1)
-> ListBy Night f (Either c1 c1)
forall (f :: * -> *).
Night (ListBy Night f) (ListBy Night f) ~> ListBy Night f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB (DecAlt f c1
-> DecAlt f c1
-> (c1 -> Either c1 c1)
-> (c1 -> Either c1 c1)
-> (Either c1 c1 -> Either c1 c1)
-> Night (DecAlt f) (DecAlt f) (Either c1 c1)
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
IN.Night (Chain Night Not f c1 -> DecAlt f c1
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c1
zs) (Chain Night Not f c1 -> DecAlt f c1
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c1
ys) c1 -> Either c1 c1
forall a b. a -> Either a b
Left c1 -> Either c1 c1
forall a b. b -> Either a b
Right Either c1 c1 -> Either c1 c1
forall a. a -> a
id))
        (b1 -> x
f (b1 -> x) -> (b1 -> b1) -> b1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b1 -> b1
j)
        ((c1 -> x) -> (c1 -> x) -> Either c1 c1 -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b1 -> x
f (b1 -> x) -> (c1 -> b1) -> c1 -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c1 -> b1
k) c1 -> x
g)
        (Either (Either b1 c1) c1 -> Either b1 (Either c1 c1)
forall a b c. Either (Either a b) c -> Either a (Either b c)
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc (Either (Either b1 c1) c1 -> Either b1 (Either c1 c1))
-> (x -> Either (Either b1 c1) c1) -> x -> Either b1 (Either c1 c1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b1 -> Either b1 c1) -> Either b1 c1 -> Either (Either b1 c1) c1
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b1 -> Either b1 c1
l (Either b1 c1 -> Either (Either b1 c1) c1)
-> (x -> Either b1 c1) -> x -> Either (Either b1 c1) c1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b1 c1
h)
    splitNE :: forall (f :: * -> *).
NonEmptyBy Night f ~> Night f (ListBy Night f)
splitNE = (Chain1 Night f x -> Night f (Chain Night Not f) x)
-> DecAlt1 f x -> Night f (DecAlt f) x
forall a b. Coercible a b => a -> b
coerce Chain1 Night f x -> Night f (Chain Night Not f) x
Chain1 Night f ~> Night f (Chain Night Not f)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
Chain1 t f ~> t f (Chain t i f)
splitChain1
    splittingLB :: forall (f :: * -> *).
ListBy Night f <~> (Not :+: Night f (ListBy Night f))
splittingLB = p (Chain Night Not f a) (Chain Night Not f a)
-> p (DecAlt f a) (DecAlt f a)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
 forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
DecAlt f <~> Chain Night Not f
coercedF (p (Chain Night Not f a) (Chain Night Not f a)
 -> p (DecAlt f a) (DecAlt f a))
-> (p ((:+:) Not (Night f (DecAlt f)) a)
      ((:+:) Not (Night f (DecAlt f)) a)
    -> p (Chain Night Not f a) (Chain Night Not f a))
-> p ((:+:) Not (Night f (DecAlt f)) a)
     ((:+:) Not (Night f (DecAlt f)) a)
-> p (DecAlt f a) (DecAlt f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ((:+:) Not (Night f (Chain Night Not f)) a)
  ((:+:) Not (Night f (Chain Night Not f)) a)
-> p (Chain Night Not f a) (Chain Night Not f a)
forall {k1} {k2} (t :: k1 -> (k2 -> *) -> k2 -> *) (i :: k2 -> *)
       (f :: k1) (p :: * -> * -> *) (a :: k2).
Profunctor p =>
p ((:+:) i (t f (Chain t i f)) a) ((:+:) i (t f (Chain t i f)) a)
-> p (Chain t i f a) (Chain t i f a)
splittingChain (p ((:+:) Not (Night f (Chain Night Not f)) a)
   ((:+:) Not (Night f (Chain Night Not f)) a)
 -> p (Chain Night Not f a) (Chain Night Not f a))
-> (p ((:+:) Not (Night f (DecAlt f)) a)
      ((:+:) Not (Night f (DecAlt f)) a)
    -> p ((:+:) Not (Night f (Chain Night Not f)) a)
         ((:+:) Not (Night f (Chain Night Not f)) a))
-> p ((:+:) Not (Night f (DecAlt f)) a)
     ((:+:) Not (Night f (DecAlt f)) a)
-> p (Chain Night Not f a) (Chain Night Not f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ((:+:) Not (Night f (DecAlt f)) a)
  ((:+:) Not (Night f (DecAlt f)) a)
-> p ((:+:) Not (Night f (Chain Night Not f)) a)
     ((:+:) Not (Night f (Chain Night Not f)) a)
forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
 forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
(Not :+: Night f (Chain Night Not f))
<~> (Not :+: Night f (DecAlt f))
coercedF
    toListBy :: forall (f :: * -> *). Night f f ~> ListBy Night f
toListBy = Chain Night Not f x -> DecAlt f x
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt (Chain Night Not f x -> DecAlt f x)
-> (Night f f x -> Chain Night Not f x)
-> Night f f x
-> DecAlt f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Night f (Chain Night Not f) x -> Chain Night Not f x
forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
       (f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) x -> Chain Night Not f x)
-> (Night f f x -> Night f (Chain Night Not f) x)
-> Night f f x
-> Chain Night Not f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f ~> Chain Night Not f)
-> Night f f ~> Night f (Chain Night Not f)
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> Night f g ~> Night f l
hright (DecAlt f x -> Chain Night Not f x
forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt (DecAlt f x -> Chain Night Not f x)
-> (f x -> DecAlt f x) -> f x -> Chain Night Not f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> DecAlt f x
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> DecAlt f
inject)
instance Matchable IN.Night Not where
    unsplitNE :: forall (f :: * -> *).
FunctorBy Night f =>
Night f (ListBy Night f) ~> NonEmptyBy Night f
unsplitNE = (Night f (Chain Night Not f) x -> Chain1 Night f x)
-> Night f (DecAlt f) x -> DecAlt1 f x
forall a b. Coercible a b => a -> b
coerce Night f (Chain Night Not f) x -> Chain1 Night f x
Night f (Chain Night Not f) ~> Chain1 Night f
forall (f :: * -> *).
Invariant f =>
Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_
    matchLB :: forall (f :: * -> *).
FunctorBy Night f =>
ListBy Night f ~> (Not :+: NonEmptyBy Night f)
matchLB = (Chain Night Not f x -> (:+:) Not (Chain1 Night f) x)
-> DecAlt f x -> (:+:) Not (DecAlt1 f) x
forall a b. Coercible a b => a -> b
coerce Chain Night Not f x -> (:+:) Not (Chain1 Night f) x
Chain Night Not f ~> (Not :+: Chain1 Night f)
forall (f :: * -> *).
Invariant f =>
Chain Night Not f ~> (Not :+: Chain1 Night f)
matchLBINight_
unsplitNEINight_ :: Invariant f => IN.Night f (Chain IN.Night Not f) ~> Chain1 IN.Night f
unsplitNEINight_ :: forall (f :: * -> *).
Invariant f =>
Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_ (IN.Night f b1
x Chain Night Not f c1
xs b1 -> x
f c1 -> x
g x -> Either b1 c1
h) = case Chain Night Not f c1
xs of
  Done Not c1
r  -> f x -> Chain1 Night f x
forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (a :: k).
f a -> Chain1 t f a
Done1 (f x -> Chain1 Night f x) -> f x -> Chain1 Night f x
forall a b. (a -> b) -> a -> b
$ (b1 -> x) -> (x -> b1) -> f b1 -> f x
forall a b. (a -> b) -> (b -> a) -> f a -> f b
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap b1 -> x
f ((b1 -> b1) -> (c1 -> b1) -> Either b1 c1 -> b1
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b1 -> b1
forall a. a -> a
id (Void -> b1
forall a. Void -> a
absurd (Void -> b1) -> (c1 -> Void) -> c1 -> b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not c1 -> c1 -> Void
forall a. Not a -> a -> Void
refute Not c1
r) (Either b1 c1 -> b1) -> (x -> Either b1 c1) -> x -> b1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b1 c1
h) f b1
x
  More Night f (Chain Night Not f) c1
ys -> 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 (Night f (Chain1 Night f) x -> Chain1 Night f x)
-> Night f (Chain1 Night f) x -> Chain1 Night f x
forall a b. (a -> b) -> a -> b
$ f b1
-> Chain1 Night f c1
-> (b1 -> x)
-> (c1 -> x)
-> (x -> Either b1 c1)
-> Night f (Chain1 Night f) x
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
IN.Night f b1
x (Night f (Chain Night Not f) c1 -> Chain1 Night f c1
Night f (Chain Night Not f) ~> Chain1 Night f
forall (f :: * -> *).
Invariant f =>
Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_ Night f (Chain Night Not f) c1
ys) b1 -> x
f c1 -> x
g x -> Either b1 c1
h
matchLBINight_ :: Invariant f => Chain IN.Night Not f ~> (Not :+: Chain1 IN.Night f)
matchLBINight_ :: forall (f :: * -> *).
Invariant f =>
Chain Night Not f ~> (Not :+: Chain1 Night f)
matchLBINight_ = \case
  Done Not x
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 Night f (Chain Night Not f) x
xs -> Chain1 Night f x -> (:+:) Not (Chain1 Night f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Chain1 Night f x -> (:+:) Not (Chain1 Night f) x)
-> Chain1 Night f x -> (:+:) Not (Chain1 Night f) x
forall a b. (a -> b) -> a -> b
$ Night f (Chain Night Not f) x -> Chain1 Night f x
Night f (Chain Night Not f) ~> Chain1 Night f
forall (f :: * -> *).
Invariant f =>
Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_ Night f (Chain Night Not f) x
xs
instance Inplus f => MonoidIn IN.Night IN.Not f where
    pureT :: Not ~> f
pureT (Not x -> Void
x) = (x -> Void) -> f x
forall a. (a -> Void) -> f a
forall (f :: * -> *) a. Inplus f => (a -> Void) -> f a
reject x -> Void
x
instance Tensor Night Not where
    type ListBy Night = Dec
    intro1 :: forall (f :: * -> *). f ~> Night f Not
intro1 = f x -> Night f Not x
forall (f :: * -> *). f ~> Night f Not
N.intro2
    intro2 :: forall (g :: * -> *). g ~> Night Not g
intro2 = g x -> Night Not g x
forall (g :: * -> *). g ~> Night Not g
N.intro1
    elim1 :: forall (f :: * -> *). FunctorBy Night f => Night f Not ~> f
elim1 = Night f Not x -> f x
Night f Not ~> f
forall (f :: * -> *). Contravariant f => Night f Not ~> f
N.elim2
    elim2 :: forall (g :: * -> *). FunctorBy Night g => Night Not g ~> g
elim2 = Night Not g x -> g x
Night Not g ~> g
forall (g :: * -> *). Contravariant g => Night Not g ~> g
N.elim1
    appendLB :: forall (f :: * -> *).
Night (ListBy Night f) (ListBy Night f) ~> ListBy Night f
appendLB (Night ListBy Night f b1
x ListBy Night f c1
y x -> Either b1 c1
z) = (x -> Either b1 c1) -> Dec f b1 -> Dec f c1 -> Dec f x
forall a b c. (a -> Either b c) -> Dec f b -> Dec f c -> Dec f a
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either b1 c1
z Dec f b1
ListBy Night f b1
x Dec f c1
ListBy Night f c1
y
    splitNE :: forall (f :: * -> *).
NonEmptyBy Night f ~> Night f (ListBy Night f)
splitNE (Dec1 x -> Either b1 c
f f b1
x Dec f c
xs) = f b1 -> Dec f c -> (x -> Either b1 c) -> Night f (Dec f) x
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1 -> b c1 -> (c -> Either b1 c1) -> Night a b c
Night f b1
x Dec f c
xs x -> Either b1 c
f
    splittingLB :: forall (f :: * -> *).
ListBy Night f <~> (Not :+: Night f (ListBy Night f))
splittingLB = (Dec f ~> (Not :+: Night f (Dec f)))
-> ((Not :+: Night f (Dec f)) ~> Dec f)
-> Dec f <~> (Not :+: Night f (Dec f))
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF Dec f x -> (:+:) Not (Night f (Dec f)) x
Dec f ~> (Not :+: Night f (Dec f))
forall {a :: * -> *} {p}. Dec a p -> (:+:) Not (Night a (Dec a)) p
to_ (:+:) Not (Night f (Dec f)) x -> Dec f x
(Not :+: Night f (Dec f)) ~> Dec f
forall {a :: * -> *} {b}. (:+:) Not (Night a (Dec a)) b -> Dec a b
from_
      where
        to_ :: Dec a p -> (:+:) Not (Night a (Dec a)) p
to_ = \case
          Lose   p -> Void
f      -> Not p -> (:+:) Not (Night a (Dec a)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 ((p -> Void) -> Not p
forall a. (a -> Void) -> Not a
Not p -> Void
f)
          Choose p -> Either b1 c
f a b1
x Dec a c
xs -> Night a (Dec a) p -> (:+:) Not (Night a (Dec a)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (a b1 -> Dec a c -> (p -> Either b1 c) -> Night a (Dec a) p
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1 -> b c1 -> (c -> Either b1 c1) -> Night a b c
Night a b1
x Dec a c
xs p -> Either b1 c
f)
        from_ :: (:+:) Not (Night a (Dec a)) b -> Dec a b
from_ = \case
          L1 (Not b -> Void
f)    -> (b -> Void) -> Dec a b
forall b (a :: * -> *). (b -> Void) -> Dec a b
Lose b -> Void
f
          R1 (Night a b1
x Dec a c1
xs b -> Either b1 c1
f) -> (b -> Either b1 c1) -> a b1 -> Dec a c1 -> Dec a b
forall b b1 c (a :: * -> *).
(b -> Either b1 c) -> a b1 -> Dec a c -> Dec a b
Choose b -> Either b1 c1
f a b1
x Dec a c1
xs
    toListBy :: forall (f :: * -> *). Night f f ~> ListBy Night f
toListBy (Night f b1
x f c1
y x -> Either b1 c1
z) = (x -> Either b1 c1) -> f b1 -> Dec f c1 -> Dec f x
forall b b1 c (a :: * -> *).
(b -> Either b1 c) -> a b1 -> Dec a c -> Dec a b
Choose x -> Either b1 c1
z f b1
x (f c1 -> Dec f c1
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> Dec f
inject f c1
y)
instance Conclude f => MonoidIn Night Not f where
    pureT :: Not ~> f
pureT (Not x -> Void
x) = (x -> Void) -> f x
forall a. (a -> Void) -> f a
forall (f :: * -> *) a. Conclude f => (a -> Void) -> f a
conclude x -> Void
x
instance Tensor (:+:) V1 where
    type ListBy (:+:) = Step
    intro1 :: forall (f :: * -> *). f ~> (f :+: V1)
intro1 = f x -> (:+:) f V1 x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1
    intro2 :: forall (g :: * -> *). g ~> (V1 :+: g)
intro2 = g x -> (:+:) V1 g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
    elim1 :: forall (f :: * -> *). FunctorBy (:+:) f => (f :+: V1) ~> f
elim1 = \case
      L1 f x
x -> f x
x
      R1 V1 x
y -> V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
    elim2 :: forall (g :: * -> *). FunctorBy (:+:) g => (V1 :+: g) ~> g
elim2 = \case
      L1 V1 x
x -> V1 x -> g x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
      R1 g x
y -> g x
y
    appendLB :: forall (f :: * -> *).
(ListBy (:+:) f :+: ListBy (:+:) f) ~> ListBy (:+:) f
appendLB    = Step f x -> Step f x
forall a. a -> a
forall {x}. Step f x -> Step f x
id (forall {x}. Step f x -> Step f x)
-> (forall {x}. Step f x -> Step f x)
-> (Step f :+: Step f) ~> Step f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *).
SemigroupIn t h =>
(f ~> h) -> (g ~> h) -> t f g ~> h
!*! (:+:) f (Step f) x -> Step f x
forall {k} (f :: k -> *) (x :: k). (:+:) f (Step f) x -> Step f x
stepUp ((:+:) f (Step f) x -> Step f x)
-> (Step f x -> (:+:) f (Step f) x) -> Step f x -> Step f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Step f x -> (:+:) f (Step f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
    splitNE :: forall (f :: * -> *). NonEmptyBy (:+:) f ~> (f :+: ListBy (:+:) f)
splitNE     = Step f x -> (:+:) f (Step f) x
NonEmptyBy (:+:) f x -> (:+:) f (ListBy (:+:) f) x
forall {k} (f :: k -> *) (x :: k). Step f x -> (:+:) f (Step f) x
stepDown
    splittingLB :: forall (f :: * -> *).
ListBy (:+:) f <~> (V1 :+: (f :+: ListBy (:+:) f))
splittingLB = p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
-> p (Step f a) (Step f a)
forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
-> p (Step f a) (Step f a)
stepping (p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
 -> p (Step f a) (Step f a))
-> (p ((:+:) V1 (f :+: Step f) a) ((:+:) V1 (f :+: Step f) a)
    -> p ((:+:) f (Step f) a) ((:+:) f (Step f) a))
-> p ((:+:) V1 (f :+: Step f) a) ((:+:) V1 (f :+: Step f) a)
-> p (Step f a) (Step f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ((:+:) V1 (f :+: Step f) a) ((:+:) V1 (f :+: Step f) a)
-> p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:+:) V1 f a) ((:+:) V1 f a) -> p (f a) (f a)
sumLeftIdentity
    toListBy :: forall (f :: * -> *). (f :+: f) ~> ListBy (:+:) f
toListBy  = \case
      L1 f x
x -> Natural -> f x -> Step f x
forall {k} (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step Natural
0 f x
x
      R1 f x
x -> Natural -> f x -> Step f x
forall {k} (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step Natural
1 f x
x
instance MonoidIn (:+:) V1 f where
    pureT :: V1 ~> f
pureT = V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1
instance Tensor Sum V1 where
    type ListBy Sum = Step
    intro1 :: forall (f :: * -> *). f ~> Sum f V1
intro1 = f x -> Sum f V1 x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL
    intro2 :: forall (g :: * -> *). g ~> Sum V1 g
intro2 = g x -> Sum V1 g x
forall {k} (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR
    elim1 :: forall (f :: * -> *). FunctorBy Sum f => Sum f V1 ~> f
elim1 = \case
      InL f x
x -> f x
x
      InR V1 x
y -> V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
    elim2 :: forall (g :: * -> *). FunctorBy Sum g => Sum V1 g ~> g
elim2 = \case
      InL V1 x
x -> V1 x -> g x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
      InR g x
y -> g x
y
    appendLB :: forall (f :: * -> *).
Sum (ListBy Sum f) (ListBy Sum f) ~> ListBy Sum f
appendLB    = Step f x -> Step f x
forall a. a -> a
forall {x}. Step f x -> Step f x
id (forall {x}. Step f x -> Step f x)
-> (forall {x}. Step f x -> Step f x)
-> Sum (Step f) (Step f) ~> Step f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *).
SemigroupIn t h =>
(f ~> h) -> (g ~> h) -> t f g ~> h
!*! (:+:) f (Step f) x -> Step f x
forall {k} (f :: k -> *) (x :: k). (:+:) f (Step f) x -> Step f x
stepUp ((:+:) f (Step f) x -> Step f x)
-> (Step f x -> (:+:) f (Step f) x) -> Step f x -> Step f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Step f x -> (:+:) f (Step f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
    splitNE :: forall (f :: * -> *). NonEmptyBy Sum f ~> Sum f (ListBy Sum f)
splitNE     = ((f :+: Step f) <~> Sum f (Step f))
-> (f :+: Step f) ~> Sum f (Step f)
forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF p (Sum f (Step f) a) (Sum f (Step f) a)
-> p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
forall {k} (f :: k -> *) (g :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p (Sum f g a) (Sum f g a) -> p ((:+:) f g a) ((:+:) f g a)
(f :+: Step f) <~> Sum f (Step f)
sumSum ((:+:) f (Step f) x -> Sum f (Step f) x)
-> (Step f x -> (:+:) f (Step f) x) -> Step f x -> Sum f (Step f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Step f x -> (:+:) f (Step f) x
forall {k} (f :: k -> *) (x :: k). Step f x -> (:+:) f (Step f) x
stepDown
    splittingLB :: forall (f :: * -> *).
ListBy Sum f <~> (V1 :+: Sum f (ListBy Sum f))
splittingLB = p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
-> p (Step f a) (Step f a)
forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
-> p (Step f a) (Step f a)
stepping
                (p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
 -> p (Step f a) (Step f a))
-> (p ((:+:) V1 (Sum f (Step f)) a) ((:+:) V1 (Sum f (Step f)) a)
    -> p ((:+:) f (Step f) a) ((:+:) f (Step f) a))
-> p ((:+:) V1 (Sum f (Step f)) a) ((:+:) V1 (Sum f (Step f)) a)
-> p (Step f a) (Step f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ((:+:) V1 (f :+: Step f) a) ((:+:) V1 (f :+: Step f) a)
-> p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:+:) V1 f a) ((:+:) V1 f a) -> p (f a) (f a)
sumLeftIdentity
                (p ((:+:) V1 (f :+: Step f) a) ((:+:) V1 (f :+: Step f) a)
 -> p ((:+:) f (Step f) a) ((:+:) f (Step f) a))
-> (p ((:+:) V1 (Sum f (Step f)) a) ((:+:) V1 (Sum f (Step f)) a)
    -> p ((:+:) V1 (f :+: Step f) a) ((:+:) V1 (f :+: Step f) a))
-> p ((:+:) V1 (Sum f (Step f)) a) ((:+:) V1 (Sum f (Step f)) a)
-> p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (V1 <~> V1)
-> ((f :+: Step f) <~> Sum f (Step f))
-> (V1 :+: (f :+: Step f)) <~> (V1 :+: Sum f (Step f))
forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (f' :: k -> *) (g :: k -> *) (g' :: k -> *).
HBifunctor t =>
(f <~> f') -> (g <~> g') -> t f g <~> t f' g'
overHBifunctor p (V1 a) (V1 a) -> p (V1 a) (V1 a)
forall a. a -> a
V1 <~> V1
id p (Sum f (Step f) a) (Sum f (Step f) a)
-> p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
forall {k} (f :: k -> *) (g :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p (Sum f g a) (Sum f g a) -> p ((:+:) f g a) ((:+:) f g a)
(f :+: Step f) <~> Sum f (Step f)
sumSum
    toListBy :: forall (f :: * -> *). Sum f f ~> ListBy Sum f
toListBy  = \case
      InL f x
x -> Natural -> f x -> Step f x
forall {k} (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step Natural
0 f x
x
      InR f x
x -> Natural -> f x -> Step f x
forall {k} (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step Natural
1 f x
x
instance MonoidIn Sum V1 f where
    pureT :: V1 ~> f
pureT = V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1
instance Tensor These1 V1 where
    type ListBy These1 = Steps
    intro1 :: forall (f :: * -> *). f ~> These1 f V1
intro1 = f x -> These1 f V1 x
forall (f :: * -> *) (g :: * -> *) a. f a -> These1 f g a
This1
    intro2 :: forall (g :: * -> *). g ~> These1 V1 g
intro2 = g x -> These1 V1 g x
forall (f :: * -> *) (g :: * -> *) a. g a -> These1 f g a
That1
    elim1 :: forall (f :: * -> *). FunctorBy These1 f => These1 f V1 ~> f
elim1  = \case
      This1  f x
x   -> f x
x
      That1    V1 x
y -> V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
      These1 f x
_ V1 x
y -> V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
    elim2 :: forall (g :: * -> *). FunctorBy These1 g => These1 V1 g ~> g
elim2 = \case
      This1  V1 x
x   -> V1 x -> g x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
      That1    g x
y -> g x
y
      These1 V1 x
x g x
_ -> V1 x -> g x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
    appendLB :: forall (f :: * -> *).
These1 (ListBy These1 f) (ListBy These1 f) ~> ListBy These1 f
appendLB    = \case
      This1  ListBy These1 f x
x   -> ListBy These1 f x
x
      That1    ListBy These1 f x
y -> These1 f (Steps f) x -> Steps f x
These1 f (Steps f) x -> ListBy These1 f x
forall (f :: * -> *) x. These1 f (Steps f) x -> Steps f x
stepsUp (These1 f (Steps f) x -> ListBy These1 f x)
-> (ListBy These1 f x -> These1 f (Steps f) x)
-> ListBy These1 f x
-> ListBy These1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Steps f x -> These1 f (Steps f) x
ListBy These1 f x -> These1 f (Steps f) x
forall (f :: * -> *) (g :: * -> *) a. g a -> These1 f g a
That1 (ListBy These1 f x -> ListBy These1 f x)
-> ListBy These1 f x -> ListBy These1 f x
forall a b. (a -> b) -> a -> b
$ ListBy These1 f x
y
      These1 ListBy These1 f x
x ListBy These1 f x
y -> Steps f x
ListBy These1 f x
x Steps f x -> Steps f x -> Steps f x
forall a. Semigroup a => a -> a -> a
<> Steps f x
ListBy These1 f x
y
    splitNE :: forall (f :: * -> *).
NonEmptyBy These1 f ~> These1 f (ListBy These1 f)
splitNE     = Steps f x -> These1 f (Steps f) x
forall (f :: * -> *) x. Steps f x -> These1 f (Steps f) x
stepsDown (Steps f x -> These1 f (Steps f) x)
-> (ComposeT Flagged Steps f x -> Steps f x)
-> ComposeT Flagged Steps f x
-> These1 f (Steps f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Flagged (Steps f) x -> Steps f x
forall {k} (f :: k -> *) (a :: k). Flagged f a -> f a
flaggedVal (Flagged (Steps f) x -> Steps f x)
-> (ComposeT Flagged Steps f x -> Flagged (Steps f) x)
-> ComposeT Flagged Steps f x
-> Steps f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComposeT Flagged Steps f x -> Flagged (Steps f) x
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
       (m :: * -> *) a.
ComposeT f g m a -> f (g m) a
getComposeT
    splittingLB :: forall (f :: * -> *).
ListBy These1 f <~> (V1 :+: These1 f (ListBy These1 f))
splittingLB = p (These1 f (Steps f) a) (These1 f (Steps f) a)
-> p (Steps f a) (Steps f a)
forall (f :: * -> *) (p :: * -> * -> *) a.
Profunctor p =>
p (These1 f (Steps f) a) (These1 f (Steps f) a)
-> p (Steps f a) (Steps f a)
steppings (p (These1 f (Steps f) a) (These1 f (Steps f) a)
 -> p (Steps f a) (Steps f a))
-> (p ((:+:) V1 (These1 f (Steps f)) a)
      ((:+:) V1 (These1 f (Steps f)) a)
    -> p (These1 f (Steps f) a) (These1 f (Steps f) a))
-> p ((:+:) V1 (These1 f (Steps f)) a)
     ((:+:) V1 (These1 f (Steps f)) a)
-> p (Steps f a) (Steps f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ((:+:) V1 (These1 f (Steps f)) a)
  ((:+:) V1 (These1 f (Steps f)) a)
-> p (These1 f (Steps f) a) (These1 f (Steps f) a)
forall {k} (f :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p ((:+:) V1 f a) ((:+:) V1 f a) -> p (f a) (f a)
sumLeftIdentity
    toListBy :: forall (f :: * -> *). These1 f f ~> ListBy These1 f
toListBy  = \case
      This1  f x
x   -> NEMap Natural (f x) -> Steps f x
forall {k} (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps (NEMap Natural (f x) -> Steps f x)
-> NEMap Natural (f x) -> Steps f x
forall a b. (a -> b) -> a -> b
$ Natural -> f x -> NEMap Natural (f x)
forall k a. k -> a -> NEMap k a
NEM.singleton Natural
0 f x
x
      That1    f x
y -> NEMap Natural (f x) -> Steps f x
forall {k} (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps (NEMap Natural (f x) -> Steps f x)
-> NEMap Natural (f x) -> Steps f x
forall a b. (a -> b) -> a -> b
$ Natural -> f x -> NEMap Natural (f x)
forall k a. k -> a -> NEMap k a
NEM.singleton Natural
1 f x
y
      These1 f x
x f x
y -> NEMap Natural (f x) -> Steps f x
forall {k} (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps (NEMap Natural (f x) -> Steps f x)
-> NEMap Natural (f x) -> Steps f x
forall a b. (a -> b) -> a -> b
$ NonEmpty (Natural, f x) -> NEMap Natural (f x)
forall k a. NonEmpty (k, a) -> NEMap k a
NEM.fromDistinctAscList ((Natural
0, f x
x) (Natural, f x) -> [(Natural, f x)] -> NonEmpty (Natural, f x)
forall a. a -> [a] -> NonEmpty a
:| [(Natural
1, f x
y)])
instance Alt f => MonoidIn These1 V1 f where
    pureT :: V1 ~> f
pureT = V1 x -> f x
forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1
instance Tensor Comp Identity where
    type ListBy Comp = Free
    intro1 :: forall (f :: * -> *). f ~> Comp f Identity
intro1 = (f x -> (x -> Identity x) -> Comp f Identity x
forall {k} (f :: * -> *) (g :: k -> *) (a :: k) x.
f x -> (x -> g a) -> Comp f g a
:>>= x -> Identity x
forall a. a -> Identity a
Identity)
    intro2 :: forall (g :: * -> *). g ~> Comp Identity g
intro2 = (() -> Identity ()
forall a. a -> Identity a
Identity () Identity () -> (() -> g x) -> Comp Identity g x
forall {k} (f :: * -> *) (g :: k -> *) (a :: k) x.
f x -> (x -> g a) -> Comp f g a
:>>=) ((() -> g x) -> Comp Identity g x)
-> (g x -> () -> g x) -> g x -> Comp Identity g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> () -> g x
forall a b. a -> b -> a
const
    elim1 :: forall (f :: * -> *). FunctorBy Comp f => Comp f Identity ~> f
elim1 (f x
x :>>= x -> Identity x
y) = Identity x -> x
forall a. Identity a -> a
runIdentity (Identity x -> x) -> (x -> Identity x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Identity x
y (x -> x) -> f x -> f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x
x
    elim2 :: forall (g :: * -> *). FunctorBy Comp g => Comp Identity g ~> g
elim2 (Identity x
x :>>= x -> g x
y) = x -> g x
y (Identity x -> x
forall a. Identity a -> a
runIdentity Identity x
x)
    appendLB :: forall (f :: * -> *).
Comp (ListBy Comp f) (ListBy Comp f) ~> ListBy Comp f
appendLB (ListBy Comp f x
x :>>= x -> ListBy Comp f x
y) = Free f x
ListBy Comp f x
x Free f x -> (x -> Free f x) -> Free f x
forall a b. Free f a -> (a -> Free f b) -> Free f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> Free f x
x -> ListBy Comp f x
y
    splitNE :: forall (f :: * -> *). NonEmptyBy Comp f ~> Comp f (ListBy Comp f)
splitNE             = Free1 f x -> Comp f (Free f) x
NonEmptyBy Comp f x -> Comp f (ListBy Comp f) x
forall (f :: * -> *) x. Free1 f x -> Comp f (Free f) x
free1Comp
    splittingLB :: forall (f :: * -> *).
ListBy Comp f <~> (Identity :+: Comp f (ListBy Comp f))
splittingLB = (Free f ~> (Identity :+: Comp f (Free f)))
-> ((Identity :+: Comp f (Free f)) ~> Free f)
-> Free f <~> (Identity :+: Comp f (Free f))
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF Free f x -> (:+:) Identity (Comp f (Free f)) x
Free f ~> (Identity :+: Comp f (Free f))
forall (f :: * -> *) x.
Free f x -> (:+:) Identity (Comp f (Free f)) x
to_ (:+:) Identity (Comp f (Free f)) x -> Free f x
(Identity :+: Comp f (Free f)) ~> Free f
forall (f :: * -> *) x.
(:+:) Identity (Comp f (Free f)) x -> Free f x
from_
      where
        to_ :: Free f ~> Identity :+: Comp f (Free f)
        to_ :: forall (f :: * -> *) x.
Free f x -> (:+:) Identity (Comp f (Free f)) x
to_ = (x -> (:+:) Identity (Comp f (Free f)) x)
-> (forall {s}.
    f s
    -> (s -> (:+:) Identity (Comp f (Free f)) x)
    -> (:+:) Identity (Comp f (Free f)) x)
-> Free f x
-> (:+:) Identity (Comp f (Free f)) x
forall a r (f :: * -> *).
(a -> r) -> (forall s. f s -> (s -> r) -> r) -> Free f a -> r
foldFree' (Identity x -> (:+:) Identity (Comp f (Free f)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (Identity x -> (:+:) Identity (Comp f (Free f)) x)
-> (x -> Identity x) -> x -> (:+:) Identity (Comp f (Free f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Identity x
forall a. a -> Identity a
Identity) ((forall {s}.
  f s
  -> (s -> (:+:) Identity (Comp f (Free f)) x)
  -> (:+:) Identity (Comp f (Free f)) x)
 -> Free f x -> (:+:) Identity (Comp f (Free f)) x)
-> (forall {s}.
    f s
    -> (s -> (:+:) Identity (Comp f (Free f)) x)
    -> (:+:) Identity (Comp f (Free f)) x)
-> Free f x
-> (:+:) Identity (Comp f (Free f)) x
forall a b. (a -> b) -> a -> b
$ \f s
y s -> (:+:) Identity (Comp f (Free f)) x
n -> Comp f (Free f) x -> (:+:) Identity (Comp f (Free f)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Comp f (Free f) x -> (:+:) Identity (Comp f (Free f)) x)
-> Comp f (Free f) x -> (:+:) Identity (Comp f (Free f)) x
forall a b. (a -> b) -> a -> b
$
            f s
y f s -> (s -> Free f x) -> Comp f (Free f) x
forall {k} (f :: * -> *) (g :: k -> *) (a :: k) x.
f x -> (x -> g a) -> Comp f g a
:>>= ((:+:) Identity (Comp f (Free f)) x -> Free f x
forall (f :: * -> *) x.
(:+:) Identity (Comp f (Free f)) x -> Free f x
from_ ((:+:) Identity (Comp f (Free f)) x -> Free f x)
-> (s -> (:+:) Identity (Comp f (Free f)) x) -> s -> Free f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (:+:) Identity (Comp f (Free f)) x
n)
        from_ :: Identity :+: Comp f (Free f) ~> Free f
        from_ :: forall (f :: * -> *) x.
(:+:) Identity (Comp f (Free f)) x -> Free f x
from_ = Identity x -> Free f x
Identity ~> Free f
forall (f :: * -> *). Applicative f => Identity ~> f
generalize
            (Identity ~> Free f)
-> (Comp f (Free f) ~> Free f)
-> (Identity :+: Comp f (Free f)) ~> Free f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (h :: * -> *)
       (f :: * -> *) (g :: * -> *).
SemigroupIn t h =>
(f ~> h) -> (g ~> h) -> t f g ~> h
!*! (\case f x
x :>>= x -> Free f x
f -> f x -> Free f x
forall (f :: * -> *) x. f x -> Free f x
liftFree f x
x Free f x -> (x -> Free f x) -> Free f x
forall a b. Free f a -> (a -> Free f b) -> Free f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> Free f x
f)
    toListBy :: forall (f :: * -> *). Comp f f ~> ListBy Comp f
toListBy (f x
x :>>= x -> f x
y) = f x -> Free f x
forall (f :: * -> *) x. f x -> Free f x
liftFree f x
x Free f x -> (x -> Free f x) -> Free f x
forall a b. Free f a -> (a -> Free f b) -> Free f b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (f x -> Free f x
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *) x. f x -> Free f x
inject (f x -> Free f x) -> (x -> f x) -> x -> Free f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> f x
y)
instance (Bind f, Monad f) => MonoidIn Comp Identity f where
    pureT :: Identity ~> f
pureT           = Identity x -> f x
Identity ~> f
forall (f :: * -> *). Applicative f => Identity ~> f
generalize
instance Matchable (:*:) Proxy where
    unsplitNE :: forall (f :: * -> *).
FunctorBy (:*:) f =>
(f :*: ListBy (:*:) f) ~> NonEmptyBy (:*:) f
unsplitNE = (:*:) f (ListF f) x -> NonEmptyF f x
(:*:) f (ListBy (:*:) f) x -> NonEmptyBy (:*:) f x
forall {k} (f :: k -> *) (a :: k).
(:*:) f (ListF f) a -> NonEmptyF f a
ProdNonEmpty
    matchLB :: forall (f :: * -> *).
FunctorBy (:*:) f =>
ListBy (:*:) f ~> (Proxy :+: NonEmptyBy (:*:) f)
matchLB   = ListF f x -> (:+:) Proxy (NonEmptyF f) x
ListBy (:*:) f x -> (:+:) Proxy (NonEmptyBy (:*:) f) x
forall {k} (f :: k -> *) (x :: k).
ListF f x -> (:+:) Proxy (NonEmptyF f) x
fromListF
instance Matchable Product Proxy where
    unsplitNE :: forall (f :: * -> *).
FunctorBy Product f =>
Product f (ListBy Product f) ~> NonEmptyBy Product f
unsplitNE = (:*:) f (ListF f) x -> NonEmptyF f x
forall {k} (f :: k -> *) (a :: k).
(:*:) f (ListF f) a -> NonEmptyF f a
ProdNonEmpty ((:*:) f (ListF f) x -> NonEmptyF f x)
-> (Product f (ListF f) x -> (:*:) f (ListF f) x)
-> Product f (ListF f) x
-> NonEmptyF f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((f :*: ListF f) <~> Product f (ListF f))
-> Product f (ListF f) ~> (f :*: ListF f)
forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF p (Product f (ListF f) a) (Product f (ListF f) a)
-> p ((:*:) f (ListF f) a) ((:*:) f (ListF f) a)
forall {k} (f :: k -> *) (g :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p (Product f g a) (Product f g a) -> p ((:*:) f g a) ((:*:) f g a)
(f :*: ListF f) <~> Product f (ListF f)
prodProd
    matchLB :: forall (f :: * -> *).
FunctorBy Product f =>
ListBy Product f ~> (Proxy :+: NonEmptyBy Product f)
matchLB   = ListF f x -> (:+:) Proxy (NonEmptyF f) x
ListBy Product f x -> (:+:) Proxy (NonEmptyBy Product f) x
forall {k} (f :: k -> *) (x :: k).
ListF f x -> (:+:) Proxy (NonEmptyF f) x
fromListF
instance Matchable Day Identity where
    unsplitNE :: forall (f :: * -> *).
FunctorBy Day f =>
Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE = Day f (Ap f) x -> Ap1 f x
Day f (ListBy Day f) x -> NonEmptyBy Day f x
forall (f :: * -> *) a. Day f (Ap f) a -> Ap1 f a
DayAp1
    matchLB :: forall (f :: * -> *).
FunctorBy Day f =>
ListBy Day f ~> (Identity :+: NonEmptyBy Day f)
matchLB   = Ap f x -> (:+:) Identity (Ap1 f) x
ListBy Day f x -> (:+:) Identity (NonEmptyBy Day f) x
forall (f :: * -> *) x. Ap f x -> (:+:) Identity (Ap1 f) x
fromAp
instance Matchable CD.Day Proxy where
    unsplitNE :: forall (f :: * -> *).
FunctorBy Day f =>
Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE (CD.Day f b
x (Div [Coyoneda f c]
xs) x -> (b, c)
f) = NonEmpty (Coyoneda f x) -> Div1 f x
NonEmpty (Coyoneda f x) -> NonEmptyBy Day f x
forall (f :: * -> *) a. NonEmpty (Coyoneda f a) -> Div1 f a
Div1 (NonEmpty (Coyoneda f x) -> NonEmptyBy Day f x)
-> ((:*:) (Coyoneda f) (ListF (Coyoneda f)) x
    -> NonEmpty (Coyoneda f x))
-> (:*:) (Coyoneda f) (ListF (Coyoneda f)) x
-> NonEmptyBy Day f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyF (Coyoneda f) x -> NonEmpty (Coyoneda f x)
forall {k} (f :: k -> *) (a :: k). NonEmptyF f a -> NonEmpty (f a)
runNonEmptyF (NonEmptyF (Coyoneda f) x -> NonEmpty (Coyoneda f x))
-> ((:*:) (Coyoneda f) (ListF (Coyoneda f)) x
    -> NonEmptyF (Coyoneda f) x)
-> (:*:) (Coyoneda f) (ListF (Coyoneda f)) x
-> NonEmpty (Coyoneda f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:*:) (Coyoneda f) (ListF (Coyoneda f)) x
-> NonEmptyF (Coyoneda f) x
(:*:) (Coyoneda f) (ListBy (:*:) (Coyoneda f)) x
-> NonEmptyBy (:*:) (Coyoneda f) x
(Coyoneda f :*: ListBy (:*:) (Coyoneda f))
~> NonEmptyBy (:*:) (Coyoneda f)
forall (f :: * -> *).
FunctorBy (:*:) f =>
(f :*: ListBy (:*:) f) ~> NonEmptyBy (:*:) f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE ((:*:) (Coyoneda f) (ListF (Coyoneda f)) x -> NonEmptyBy Day f x)
-> (:*:) (Coyoneda f) (ListF (Coyoneda f)) x -> NonEmptyBy Day f x
forall a b. (a -> b) -> a -> b
$
      (x -> b) -> f b -> Coyoneda f x
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (x -> (b, c)) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x Coyoneda f x
-> ListF (Coyoneda f) x
-> (:*:) (Coyoneda f) (ListF (Coyoneda f)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (x -> c) -> ListF (Coyoneda f) c -> ListF (Coyoneda f) x
forall a' a.
(a' -> a) -> ListF (Coyoneda f) a -> ListF (Coyoneda f) a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (x -> (b, c)) -> x -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) ([Coyoneda f c] -> ListF (Coyoneda f) c
forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF [Coyoneda f c]
xs)
    matchLB :: forall (f :: * -> *).
FunctorBy Day f =>
ListBy Day f ~> (Proxy :+: NonEmptyBy Day f)
matchLB = (NonEmptyF (Coyoneda f) ~> Div1 f)
-> (Proxy :+: NonEmptyF (Coyoneda f)) ~> (Proxy :+: Div1 f)
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> (f :+: g) ~> (f :+: l)
hright (NonEmpty (Coyoneda f x) -> Div1 f x
forall (f :: * -> *) a. NonEmpty (Coyoneda f a) -> Div1 f a
Div1 (NonEmpty (Coyoneda f x) -> Div1 f x)
-> (NonEmptyF (Coyoneda f) x -> NonEmpty (Coyoneda f x))
-> NonEmptyF (Coyoneda f) x
-> Div1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyF (Coyoneda f) x -> NonEmpty (Coyoneda f x)
forall {k} (f :: k -> *) (a :: k). NonEmptyF f a -> NonEmpty (f a)
runNonEmptyF) ((:+:) Proxy (NonEmptyF (Coyoneda f)) x -> (:+:) Proxy (Div1 f) x)
-> (Div f x -> (:+:) Proxy (NonEmptyF (Coyoneda f)) x)
-> Div f x
-> (:+:) Proxy (Div1 f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
ListBy t f ~> (i :+: NonEmptyBy t f)
matchLB @(:*:) (ListF (Coyoneda f) x -> (:+:) Proxy (NonEmptyF (Coyoneda f)) x)
-> (Div f x -> ListF (Coyoneda f) x)
-> Div f x
-> (:+:) Proxy (NonEmptyF (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] -> ListF (Coyoneda f) x)
-> (Div f x -> [Coyoneda f x]) -> Div f x -> ListF (Coyoneda f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div f x -> [Coyoneda f x]
forall (f :: * -> *) a. Div f a -> [Coyoneda f a]
unDiv
instance Matchable Night Not where
    unsplitNE :: forall (f :: * -> *).
FunctorBy Night f =>
Night f (ListBy Night f) ~> NonEmptyBy Night f
unsplitNE (Night f b1
x ListBy Night f c1
xs x -> Either b1 c1
f) = (x -> Either b1 c1) -> f b1 -> Dec f c1 -> Dec1 f x
forall b b1 c (a :: * -> *).
(b -> Either b1 c) -> a b1 -> Dec a c -> Dec1 a b
Dec1 x -> Either b1 c1
f f b1
x Dec f c1
ListBy Night f c1
xs
    matchLB :: forall (f :: * -> *).
FunctorBy Night f =>
ListBy Night f ~> (Not :+: NonEmptyBy Night f)
matchLB = \case
      Lose   x -> Void
f      -> Not x -> (:+:) Not (Dec1 f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 ((x -> Void) -> Not x
forall a. (a -> Void) -> Not a
Not x -> Void
f)
      Choose x -> Either b1 c
f f b1
x Dec f c
xs -> Dec1 f x -> (:+:) Not (Dec1 f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 ((x -> Either b1 c) -> f b1 -> Dec f c -> Dec1 f x
forall b b1 c (a :: * -> *).
(b -> Either b1 c) -> a b1 -> Dec a c -> Dec1 a b
Dec1 x -> Either b1 c
f f b1
x Dec f c
xs)
instance Matchable (:+:) V1 where
    unsplitNE :: forall (f :: * -> *).
FunctorBy (:+:) f =>
(f :+: ListBy (:+:) f) ~> NonEmptyBy (:+:) f
unsplitNE   = (:+:) f (Step f) x -> Step f x
(:+:) f (ListBy (:+:) f) x -> NonEmptyBy (:+:) f x
forall {k} (f :: k -> *) (x :: k). (:+:) f (Step f) x -> Step f x
stepUp
    matchLB :: forall (f :: * -> *).
FunctorBy (:+:) f =>
ListBy (:+:) f ~> (V1 :+: NonEmptyBy (:+:) f)
matchLB     = Step f x -> (:+:) V1 (Step f) x
ListBy (:+:) f x -> (:+:) V1 (NonEmptyBy (:+:) f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
instance Matchable Sum V1 where
    unsplitNE :: forall (f :: * -> *).
FunctorBy Sum f =>
Sum f (ListBy Sum f) ~> NonEmptyBy Sum f
unsplitNE   = (:+:) f (Step f) x -> Step f x
forall {k} (f :: k -> *) (x :: k). (:+:) f (Step f) x -> Step f x
stepUp ((:+:) f (Step f) x -> Step f x)
-> (Sum f (Step f) x -> (:+:) f (Step f) x)
-> Sum f (Step f) x
-> Step f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((f :+: Step f) <~> Sum f (Step f))
-> Sum f (Step f) ~> (f :+: Step f)
forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF p (Sum f (Step f) a) (Sum f (Step f) a)
-> p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
forall {k} (f :: k -> *) (g :: k -> *) (p :: * -> * -> *) (a :: k).
Profunctor p =>
p (Sum f g a) (Sum f g a) -> p ((:+:) f g a) ((:+:) f g a)
(f :+: Step f) <~> Sum f (Step f)
sumSum
    matchLB :: forall (f :: * -> *).
FunctorBy Sum f =>
ListBy Sum f ~> (V1 :+: NonEmptyBy Sum f)
matchLB     = Step f x -> (:+:) V1 (Step f) x
ListBy Sum f x -> (:+:) V1 (NonEmptyBy Sum f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
newtype WrapF f a = WrapF { forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF :: f a }
  deriving (Int -> WrapF f a -> ShowS
[WrapF f a] -> ShowS
WrapF f a -> String
(Int -> WrapF f a -> ShowS)
-> (WrapF f a -> String)
-> ([WrapF f a] -> ShowS)
-> Show (WrapF f a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> WrapF f a -> ShowS
forall k (f :: k -> *) (a :: k). Show (f a) => [WrapF f a] -> ShowS
forall k (f :: k -> *) (a :: k). Show (f a) => WrapF f a -> String
$cshowsPrec :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> WrapF f a -> ShowS
showsPrec :: Int -> WrapF f a -> ShowS
$cshow :: forall k (f :: k -> *) (a :: k). Show (f a) => WrapF f a -> String
show :: WrapF f a -> String
$cshowList :: forall k (f :: k -> *) (a :: k). Show (f a) => [WrapF f a] -> ShowS
showList :: [WrapF f a] -> ShowS
Show, ReadPrec [WrapF f a]
ReadPrec (WrapF f a)
Int -> ReadS (WrapF f a)
ReadS [WrapF f a]
(Int -> ReadS (WrapF f a))
-> ReadS [WrapF f a]
-> ReadPrec (WrapF f a)
-> ReadPrec [WrapF f a]
-> Read (WrapF f a)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall k (f :: k -> *) (a :: k). Read (f a) => ReadPrec [WrapF f a]
forall k (f :: k -> *) (a :: k). Read (f a) => ReadPrec (WrapF f a)
forall k (f :: k -> *) (a :: k).
Read (f a) =>
Int -> ReadS (WrapF f a)
forall k (f :: k -> *) (a :: k). Read (f a) => ReadS [WrapF f a]
$creadsPrec :: forall k (f :: k -> *) (a :: k).
Read (f a) =>
Int -> ReadS (WrapF f a)
readsPrec :: Int -> ReadS (WrapF f a)
$creadList :: forall k (f :: k -> *) (a :: k). Read (f a) => ReadS [WrapF f a]
readList :: ReadS [WrapF f a]
$creadPrec :: forall k (f :: k -> *) (a :: k). Read (f a) => ReadPrec (WrapF f a)
readPrec :: ReadPrec (WrapF f a)
$creadListPrec :: forall k (f :: k -> *) (a :: k). Read (f a) => ReadPrec [WrapF f a]
readListPrec :: ReadPrec [WrapF f a]
Read, WrapF f a -> WrapF f a -> Bool
(WrapF f a -> WrapF f a -> Bool)
-> (WrapF f a -> WrapF f a -> Bool) -> Eq (WrapF f a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (f :: k -> *) (a :: k).
Eq (f a) =>
WrapF f a -> WrapF f a -> Bool
$c== :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
WrapF f a -> WrapF f a -> Bool
== :: WrapF f a -> WrapF f a -> Bool
$c/= :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
WrapF f a -> WrapF f a -> Bool
/= :: WrapF f a -> WrapF f a -> Bool
Eq, Eq (WrapF f a)
Eq (WrapF f a) =>
(WrapF f a -> WrapF f a -> Ordering)
-> (WrapF f a -> WrapF f a -> Bool)
-> (WrapF f a -> WrapF f a -> Bool)
-> (WrapF f a -> WrapF f a -> Bool)
-> (WrapF f a -> WrapF f a -> Bool)
-> (WrapF f a -> WrapF f a -> WrapF f a)
-> (WrapF f a -> WrapF f a -> WrapF f a)
-> Ord (WrapF f a)
WrapF f a -> WrapF f a -> Bool
WrapF f a -> WrapF f a -> Ordering
WrapF f a -> WrapF f a -> WrapF f a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (f :: k -> *) (a :: k). Ord (f a) => Eq (WrapF f a)
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Bool
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Ordering
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> WrapF f a
$ccompare :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Ordering
compare :: WrapF f a -> WrapF f a -> Ordering
$c< :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Bool
< :: WrapF f a -> WrapF f a -> Bool
$c<= :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Bool
<= :: WrapF f a -> WrapF f a -> Bool
$c> :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Bool
> :: WrapF f a -> WrapF f a -> Bool
$c>= :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Bool
>= :: WrapF f a -> WrapF f a -> Bool
$cmax :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> WrapF f a
max :: WrapF f a -> WrapF f a -> WrapF f a
$cmin :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> WrapF f a
min :: WrapF f a -> WrapF f a -> WrapF f a
Ord, (forall a b. (a -> b) -> WrapF f a -> WrapF f b)
-> (forall a b. a -> WrapF f b -> WrapF f a) -> Functor (WrapF f)
forall a b. a -> WrapF f b -> WrapF f a
forall a b. (a -> b) -> WrapF f a -> WrapF f b
forall (f :: * -> *) a b. Functor f => a -> WrapF f b -> WrapF f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> WrapF f a -> WrapF f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> WrapF f a -> WrapF f b
fmap :: forall a b. (a -> b) -> WrapF f a -> WrapF f b
$c<$ :: forall (f :: * -> *) a b. Functor f => a -> WrapF f b -> WrapF f a
<$ :: forall a b. a -> WrapF f b -> WrapF f a
Functor, (forall m. Monoid m => WrapF f m -> m)
-> (forall m a. Monoid m => (a -> m) -> WrapF f a -> m)
-> (forall m a. Monoid m => (a -> m) -> WrapF f a -> m)
-> (forall a b. (a -> b -> b) -> b -> WrapF f a -> b)
-> (forall a b. (a -> b -> b) -> b -> WrapF f a -> b)
-> (forall b a. (b -> a -> b) -> b -> WrapF f a -> b)
-> (forall b a. (b -> a -> b) -> b -> WrapF f a -> b)
-> (forall a. (a -> a -> a) -> WrapF f a -> a)
-> (forall a. (a -> a -> a) -> WrapF f a -> a)
-> (forall a. WrapF f a -> [a])
-> (forall a. WrapF f a -> Bool)
-> (forall a. WrapF f a -> Int)
-> (forall a. Eq a => a -> WrapF f a -> Bool)
-> (forall a. Ord a => WrapF f a -> a)
-> (forall a. Ord a => WrapF f a -> a)
-> (forall a. Num a => WrapF f a -> a)
-> (forall a. Num a => WrapF f a -> a)
-> Foldable (WrapF f)
forall a. Eq a => a -> WrapF f a -> Bool
forall a. Num a => WrapF f a -> a
forall a. Ord a => WrapF f a -> a
forall m. Monoid m => WrapF f m -> m
forall a. WrapF f a -> Bool
forall a. WrapF f a -> Int
forall a. WrapF f a -> [a]
forall a. (a -> a -> a) -> WrapF f a -> a
forall m a. Monoid m => (a -> m) -> WrapF f a -> m
forall b a. (b -> a -> b) -> b -> WrapF f a -> b
forall a b. (a -> b -> b) -> b -> WrapF f a -> b
forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> WrapF f a -> Bool
forall (f :: * -> *) a. (Foldable f, Num a) => WrapF f a -> a
forall (f :: * -> *) a. (Foldable f, Ord a) => WrapF f a -> a
forall (f :: * -> *) m. (Foldable f, Monoid m) => WrapF f m -> m
forall (f :: * -> *) a. Foldable f => WrapF f a -> Bool
forall (f :: * -> *) a. Foldable f => WrapF f a -> Int
forall (f :: * -> *) a. Foldable f => WrapF f a -> [a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> WrapF f a -> a
forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> WrapF f a -> m
forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> WrapF f a -> b
forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> WrapF f a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => WrapF f m -> m
fold :: forall m. Monoid m => WrapF f m -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> WrapF f a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> WrapF f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> WrapF f a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> WrapF f a -> m
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> WrapF f a -> b
foldr :: forall a b. (a -> b -> b) -> b -> WrapF f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> WrapF f a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> WrapF f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> WrapF f a -> b
foldl :: forall b a. (b -> a -> b) -> b -> WrapF f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> WrapF f a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> WrapF f a -> b
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> WrapF f a -> a
foldr1 :: forall a. (a -> a -> a) -> WrapF f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> WrapF f a -> a
foldl1 :: forall a. (a -> a -> a) -> WrapF f a -> a
$ctoList :: forall (f :: * -> *) a. Foldable f => WrapF f a -> [a]
toList :: forall a. WrapF f a -> [a]
$cnull :: forall (f :: * -> *) a. Foldable f => WrapF f a -> Bool
null :: forall a. WrapF f a -> Bool
$clength :: forall (f :: * -> *) a. Foldable f => WrapF f a -> Int
length :: forall a. WrapF f a -> Int
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> WrapF f a -> Bool
elem :: forall a. Eq a => a -> WrapF f a -> Bool
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => WrapF f a -> a
maximum :: forall a. Ord a => WrapF f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => WrapF f a -> a
minimum :: forall a. Ord a => WrapF f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => WrapF f a -> a
sum :: forall a. Num a => WrapF f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => WrapF f a -> a
product :: forall a. Num a => WrapF f a -> a
Foldable, Functor (WrapF f)
Foldable (WrapF f)
(Functor (WrapF f), Foldable (WrapF f)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> WrapF f a -> f (WrapF f b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    WrapF f (f a) -> f (WrapF f a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> WrapF f a -> m (WrapF f b))
-> (forall (m :: * -> *) a.
    Monad m =>
    WrapF f (m a) -> m (WrapF f a))
-> Traversable (WrapF f)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *). Traversable f => Functor (WrapF f)
forall (f :: * -> *). Traversable f => Foldable (WrapF f)
forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
WrapF f (m a) -> m (WrapF f a)
forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
WrapF f (f a) -> f (WrapF f a)
forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> WrapF f a -> m (WrapF f b)
forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> WrapF f a -> f (WrapF f b)
forall (m :: * -> *) a. Monad m => WrapF f (m a) -> m (WrapF f a)
forall (f :: * -> *) a.
Applicative f =>
WrapF f (f a) -> f (WrapF f a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> WrapF f a -> m (WrapF f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WrapF f a -> f (WrapF f b)
$ctraverse :: forall (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> WrapF f a -> f (WrapF f b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WrapF f a -> f (WrapF f b)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
WrapF f (f a) -> f (WrapF f a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
WrapF f (f a) -> f (WrapF f a)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> WrapF f a -> m (WrapF f b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> WrapF f a -> m (WrapF f b)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
WrapF f (m a) -> m (WrapF f a)
sequence :: forall (m :: * -> *) a. Monad m => WrapF f (m a) -> m (WrapF f a)
Traversable, Typeable, (forall x. WrapF f a -> Rep (WrapF f a) x)
-> (forall x. Rep (WrapF f a) x -> WrapF f a)
-> Generic (WrapF f a)
forall x. Rep (WrapF f a) x -> WrapF f a
forall x. WrapF f a -> Rep (WrapF f a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: k -> *) (a :: k) x. Rep (WrapF f a) x -> WrapF f a
forall k (f :: k -> *) (a :: k) x. WrapF f a -> Rep (WrapF f a) x
$cfrom :: forall k (f :: k -> *) (a :: k) x. WrapF f a -> Rep (WrapF f a) x
from :: forall x. WrapF f a -> Rep (WrapF f a) x
$cto :: forall k (f :: k -> *) (a :: k) x. Rep (WrapF f a) x -> WrapF f a
to :: forall x. Rep (WrapF f a) x -> WrapF f a
Generic, Typeable (WrapF f a)
Typeable (WrapF f a) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> WrapF f a -> c (WrapF f a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (WrapF f a))
-> (WrapF f a -> Constr)
-> (WrapF f a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (WrapF f a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (WrapF f a)))
-> ((forall b. Data b => b -> b) -> WrapF f a -> WrapF f a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> WrapF f a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> WrapF f a -> r)
-> (forall u. (forall d. Data d => d -> u) -> WrapF f a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> WrapF f a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a))
-> Data (WrapF f a)
WrapF f a -> Constr
WrapF f a -> DataType
(forall b. Data b => b -> b) -> WrapF f a -> WrapF f a
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> WrapF f a -> u
forall u. (forall d. Data d => d -> u) -> WrapF f a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
Typeable (WrapF f a)
forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
WrapF f a -> Constr
forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
WrapF f a -> DataType
forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall b. Data b => b -> b) -> WrapF f a -> WrapF f a
forall k (f :: k -> *) (a :: k) u.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
Int -> (forall d. Data d => d -> u) -> WrapF f a -> u
forall k (f :: k -> *) (a :: k) u.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall d. Data d => d -> u) -> WrapF f a -> [u]
forall k (f :: k -> *) (a :: k) r r'.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
forall k (f :: k -> *) (a :: k) r r'.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
forall k (f :: k -> *) (a :: k) (m :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), Monad m) =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
forall k (f :: k -> *) (a :: k) (m :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), MonadPlus m) =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
forall k (f :: k -> *) (a :: k) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WrapF f a)
forall k (f :: k -> *) (a :: k) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WrapF f a -> c (WrapF f a)
forall k (f :: k -> *) (a :: k) (t :: * -> *) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (WrapF f a))
forall k (f :: k -> *) (a :: k) (t :: * -> * -> *) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WrapF f a))
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WrapF f a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WrapF f a -> c (WrapF f a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (WrapF f a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WrapF f a))
$cgfoldl :: forall k (f :: k -> *) (a :: k) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WrapF f a -> c (WrapF f a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> WrapF f a -> c (WrapF f a)
$cgunfold :: forall k (f :: k -> *) (a :: k) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WrapF f a)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (WrapF f a)
$ctoConstr :: forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
WrapF f a -> Constr
toConstr :: WrapF f a -> Constr
$cdataTypeOf :: forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
WrapF f a -> DataType
dataTypeOf :: WrapF f a -> DataType
$cdataCast1 :: forall k (f :: k -> *) (a :: k) (t :: * -> *) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (WrapF f a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (WrapF f a))
$cdataCast2 :: forall k (f :: k -> *) (a :: k) (t :: * -> * -> *) (c :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WrapF f a))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (WrapF f a))
$cgmapT :: forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall b. Data b => b -> b) -> WrapF f a -> WrapF f a
gmapT :: (forall b. Data b => b -> b) -> WrapF f a -> WrapF f a
$cgmapQl :: forall k (f :: k -> *) (a :: k) r r'.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
$cgmapQr :: forall k (f :: k -> *) (a :: k) r r'.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
$cgmapQ :: forall k (f :: k -> *) (a :: k) u.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
(forall d. Data d => d -> u) -> WrapF f a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> WrapF f a -> [u]
$cgmapQi :: forall k (f :: k -> *) (a :: k) u.
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
Int -> (forall d. Data d => d -> u) -> WrapF f a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> WrapF f a -> u
$cgmapM :: forall k (f :: k -> *) (a :: k) (m :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), Monad m) =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
$cgmapMp :: forall k (f :: k -> *) (a :: k) (m :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), MonadPlus m) =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
$cgmapMo :: forall k (f :: k -> *) (a :: k) (m :: * -> *).
(Typeable a, Typeable f, Typeable k, Data (f a), MonadPlus m) =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
Data)
instance Show1 f => Show1 (WrapF f) where
    liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> WrapF f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl Int
d (WrapF f a
x) = (Int -> f a -> ShowS) -> String -> Int -> f a -> ShowS
forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith ((Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
forall (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl) String
"WrapF" Int
d f a
x
instance Eq1 f => Eq1 (WrapF f) where
    liftEq :: forall a b. (a -> b -> Bool) -> WrapF f a -> WrapF f b -> Bool
liftEq a -> b -> Bool
eq (WrapF f a
x) (WrapF f b
y) = (a -> b -> Bool) -> f a -> f b -> Bool
forall a b. (a -> b -> Bool) -> f a -> f b -> Bool
forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
eq f a
x f b
y
instance Ord1 f => Ord1 (WrapF f) where
    liftCompare :: forall a b.
(a -> b -> Ordering) -> WrapF f a -> WrapF f b -> Ordering
liftCompare a -> b -> Ordering
c (WrapF f a
x) (WrapF f b
y) = (a -> b -> Ordering) -> f a -> f b -> Ordering
forall a b. (a -> b -> Ordering) -> f a -> f b -> Ordering
forall (f :: * -> *) a b.
Ord1 f =>
(a -> b -> Ordering) -> f a -> f b -> Ordering
liftCompare a -> b -> Ordering
c f a
x f b
y
instance Tensor t i => Tensor (WrapHBF t) (WrapF i) where
    type ListBy (WrapHBF t) = ListBy t
    intro1 :: forall (f :: * -> *). f ~> WrapHBF t f (WrapF i)
intro1 = t f (WrapF i) x -> WrapHBF t f (WrapF i) x
forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
       (a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF (t f (WrapF i) x -> WrapHBF t f (WrapF i) x)
-> (f x -> t f (WrapF i) x) -> f x -> WrapHBF t f (WrapF i) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i ~> WrapF i) -> t f i ~> t f (WrapF i)
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> t f g ~> t f l
hright i x -> WrapF i x
i ~> WrapF i
forall {k} (f :: k -> *) (a :: k). f a -> WrapF f a
WrapF (t f i x -> t f (WrapF i) x)
-> (f x -> t f i x) -> f x -> t f (WrapF i) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  f x -> t f i x
forall (f :: * -> *). f ~> t f i
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
f ~> t f i
intro1
    intro2 :: forall (g :: * -> *). g ~> WrapHBF t (WrapF i) g
intro2 = t (WrapF i) g x -> WrapHBF t (WrapF i) g x
forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
       (a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF (t (WrapF i) g x -> WrapHBF t (WrapF i) g x)
-> (g x -> t (WrapF i) g x) -> g x -> WrapHBF t (WrapF i) g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i ~> WrapF i) -> t i g ~> t (WrapF i) g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
forall (f :: * -> *) (j :: * -> *) (g :: * -> *).
(f ~> j) -> t f g ~> t j g
hleft i x -> WrapF i x
i ~> WrapF i
forall {k} (f :: k -> *) (a :: k). f a -> WrapF f a
WrapF (t i g x -> t (WrapF i) g x)
-> (g x -> t i g x) -> g x -> t (WrapF i) g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g x -> t i g x
forall (g :: * -> *). g ~> t i g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *).
Tensor t i =>
g ~> t i g
intro2
    elim1 :: forall (f :: * -> *).
FunctorBy (WrapHBF t) f =>
WrapHBF t f (WrapF i) ~> f
elim1 = t f i x -> f x
t f i ~> f
forall (f :: * -> *). FunctorBy t f => t f i ~> f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
(Tensor t i, FunctorBy t f) =>
t f i ~> f
elim1 (t f i x -> f x)
-> (WrapHBF t f (WrapF i) x -> t f i x)
-> WrapHBF t f (WrapF i) x
-> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WrapF i ~> i) -> t f (WrapF i) ~> t f i
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
       (l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
forall (g :: * -> *) (l :: * -> *) (f :: * -> *).
(g ~> l) -> t f g ~> t f l
hright WrapF i x -> i x
WrapF i ~> i
forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF (t f (WrapF i) x -> t f i x)
-> (WrapHBF t f (WrapF i) x -> t f (WrapF i) x)
-> WrapHBF t f (WrapF i) x
-> t f i x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapHBF t f (WrapF i) x -> t f (WrapF i) x
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3 -> *) (f :: k1)
       (g :: k2) (a :: k3).
WrapHBF t f g a -> t f g a
unwrapHBF
    elim2 :: forall (g :: * -> *).
FunctorBy (WrapHBF t) g =>
WrapHBF t (WrapF i) g ~> g
elim2 = t i g x -> g x
t i g ~> g
forall (g :: * -> *). FunctorBy t g => t i g ~> g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (g :: * -> *).
(Tensor t i, FunctorBy t g) =>
t i g ~> g
elim2 (t i g x -> g x)
-> (WrapHBF t (WrapF i) g x -> t i g x)
-> WrapHBF t (WrapF i) g x
-> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WrapF i ~> i) -> t (WrapF i) g ~> t i g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
forall (f :: * -> *) (j :: * -> *) (g :: * -> *).
(f ~> j) -> t f g ~> t j g
hleft WrapF i x -> i x
WrapF i ~> i
forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF (t (WrapF i) g x -> t i g x)
-> (WrapHBF t (WrapF i) g x -> t (WrapF i) g x)
-> WrapHBF t (WrapF i) g x
-> t i g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapHBF t (WrapF i) g x -> t (WrapF i) g x
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3 -> *) (f :: k1)
       (g :: k2) (a :: k3).
WrapHBF t f g a -> t f g a
unwrapHBF
    appendLB :: forall (f :: * -> *).
WrapHBF t (ListBy (WrapHBF t) f) (ListBy (WrapHBF t) f)
~> ListBy (WrapHBF t) f
appendLB = t (ListBy t f) (ListBy t f) x -> ListBy t f x
forall (f :: * -> *). t (ListBy t f) (ListBy t f) ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB (t (ListBy t f) (ListBy t f) x -> ListBy t f x)
-> (WrapHBF t (ListBy t f) (ListBy t f) x
    -> t (ListBy t f) (ListBy t f) x)
-> WrapHBF t (ListBy t f) (ListBy t f) x
-> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapHBF t (ListBy t f) (ListBy t f) x
-> t (ListBy t f) (ListBy t f) x
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3 -> *) (f :: k1)
       (g :: k2) (a :: k3).
WrapHBF t f g a -> t f g a
unwrapHBF
    splitNE :: forall (f :: * -> *).
NonEmptyBy (WrapHBF t) f ~> WrapHBF t f (ListBy (WrapHBF t) f)
splitNE = t f (ListBy t f) x -> WrapHBF t f (ListBy t f) x
forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
       (a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF (t f (ListBy t f) x -> WrapHBF t f (ListBy t f) x)
-> (NonEmptyBy t f x -> t f (ListBy t f) x)
-> NonEmptyBy t f x
-> WrapHBF t f (ListBy t f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyBy t f x -> t f (ListBy t f) x
forall (f :: * -> *). NonEmptyBy t f ~> t f (ListBy t f)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> t f (ListBy t f)
splitNE
    splittingLB :: forall (f :: * -> *).
ListBy (WrapHBF t) f
<~> (WrapF i :+: WrapHBF t f (ListBy (WrapHBF t) f))
splittingLB = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
ListBy t f <~> (i :+: t f (ListBy t f))
splittingLB @t
                (p ((:+:) i (t f (ListBy t f)) a) ((:+:) i (t f (ListBy t f)) a)
 -> p (ListBy t f a) (ListBy t f a))
-> (p ((:+:) (WrapF i) (WrapHBF t f (ListBy t f)) a)
      ((:+:) (WrapF i) (WrapHBF t f (ListBy t f)) a)
    -> p ((:+:) i (t f (ListBy t f)) a) ((:+:) i (t f (ListBy t f)) a))
-> p ((:+:) (WrapF i) (WrapHBF t f (ListBy t f)) a)
     ((:+:) (WrapF i) (WrapHBF t f (ListBy t f)) a)
-> p (ListBy t f a) (ListBy t f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (i <~> WrapF i)
-> (t f (ListBy t f) <~> WrapHBF t f (ListBy t f))
-> (i :+: t f (ListBy t f))
   <~> (WrapF i :+: WrapHBF t f (ListBy t f))
forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (f' :: k -> *) (g :: k -> *) (g' :: k -> *).
HBifunctor t =>
(f <~> f') -> (g <~> g') -> t f g <~> t f' g'
overHBifunctor ((i ~> WrapF i) -> (WrapF i ~> i) -> i <~> WrapF i
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF i x -> WrapF i x
i ~> WrapF i
forall {k} (f :: k -> *) (a :: k). f a -> WrapF f a
WrapF WrapF i x -> i x
WrapF i ~> i
forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF) ((t f (ListBy t f) ~> WrapHBF t f (ListBy t f))
-> (WrapHBF t f (ListBy t f) ~> t f (ListBy t f))
-> t f (ListBy t f) <~> WrapHBF t f (ListBy t f)
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF t f (ListBy t f) x -> WrapHBF t f (ListBy t f) x
t f (ListBy t f) ~> WrapHBF t f (ListBy t f)
forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
       (a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF WrapHBF t f (ListBy t f) x -> t f (ListBy t f) x
WrapHBF t f (ListBy t f) ~> t f (ListBy t f)
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3 -> *) (f :: k1)
       (g :: k2) (a :: k3).
WrapHBF t f g a -> t f g a
unwrapHBF)
    toListBy :: forall (f :: * -> *). WrapHBF t f f ~> ListBy (WrapHBF t) f
toListBy = t f f x -> ListBy t f x
forall (f :: * -> *). t f f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t f f ~> ListBy t f
toListBy (t f f x -> ListBy t f x)
-> (WrapHBF t f f x -> t f f x) -> WrapHBF t f f x -> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapHBF t f f x -> t f f x
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3 -> *) (f :: k1)
       (g :: k2) (a :: k3).
WrapHBF t f g a -> t f g a
unwrapHBF
    fromNE :: forall (f :: * -> *).
NonEmptyBy (WrapHBF t) f ~> ListBy (WrapHBF t) f
fromNE = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> ListBy t f
fromNE @t
newtype WrapLB t f a = WrapLB { forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
WrapLB t f a -> ListBy t f a
unwrapLB :: ListBy t f a }
instance Functor (ListBy t f) => Functor (WrapLB t f) where
    fmap :: forall a b. (a -> b) -> WrapLB t f a -> WrapLB t f b
fmap a -> b
f (WrapLB ListBy t f a
x) = ListBy t f b -> WrapLB t f b
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB ((a -> b) -> ListBy t f a -> ListBy t f b
forall a b. (a -> b) -> ListBy t f a -> ListBy t f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ListBy t f a
x)
instance Contravariant (ListBy t f) => Contravariant (WrapLB t f) where
    contramap :: forall a' a. (a' -> a) -> WrapLB t f a -> WrapLB t f a'
contramap a' -> a
f (WrapLB ListBy t f a
x) = ListBy t f a' -> WrapLB t f a'
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB ((a' -> a) -> ListBy t f a -> ListBy t f a'
forall a' a. (a' -> a) -> ListBy t f a -> ListBy t f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap a' -> a
f ListBy t f a
x)
instance Invariant (ListBy t f) => Invariant (WrapLB t f) where
    invmap :: forall a b. (a -> b) -> (b -> a) -> WrapLB t f a -> WrapLB t f b
invmap a -> b
f b -> a
g (WrapLB ListBy t f a
x) = ListBy t f b -> WrapLB t f b
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB ((a -> b) -> (b -> a) -> ListBy t f a -> ListBy t f b
forall a b. (a -> b) -> (b -> a) -> ListBy t f a -> ListBy t f b
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap a -> b
f b -> a
g ListBy t f a
x)
instance (Tensor t i, FunctorBy t f, FunctorBy t (WrapLB t f)) => SemigroupIn (WrapHBF t) (WrapLB t f) where
    biretract :: WrapHBF t (WrapLB t f) (WrapLB t f) ~> WrapLB t f
biretract = ListBy t f x -> WrapLB t f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB (ListBy t f x -> WrapLB t f x)
-> (WrapHBF t (WrapLB t f) (WrapLB t f) x -> ListBy t f x)
-> WrapHBF t (WrapLB t f) (WrapLB t f) x
-> WrapLB t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (ListBy t f) (ListBy t f) x -> ListBy t f x
forall (f :: * -> *). t (ListBy t f) (ListBy t f) ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB (t (ListBy t f) (ListBy t f) x -> ListBy t f x)
-> (WrapHBF t (WrapLB t f) (WrapLB t f) x
    -> t (ListBy t f) (ListBy t f) x)
-> WrapHBF t (WrapLB t f) (WrapLB t f) x
-> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WrapLB t f ~> ListBy t f)
-> (WrapLB t f ~> ListBy t f)
-> t (WrapLB t f) (WrapLB t f) ~> t (ListBy t f) (ListBy t f)
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
forall (f :: * -> *) (j :: * -> *) (g :: * -> *) (l :: * -> *).
(f ~> j) -> (g ~> l) -> t f g ~> t j l
hbimap WrapLB t f x -> ListBy t f x
WrapLB t f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
WrapLB t f a -> ListBy t f a
unwrapLB WrapLB t f x -> ListBy t f x
WrapLB t f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
WrapLB t f a -> ListBy t f a
unwrapLB (t (WrapLB t f) (WrapLB t f) x -> t (ListBy t f) (ListBy t f) x)
-> (WrapHBF t (WrapLB t f) (WrapLB t f) x
    -> t (WrapLB t f) (WrapLB t f) x)
-> WrapHBF t (WrapLB t f) (WrapLB t f) x
-> t (ListBy t f) (ListBy t f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapHBF t (WrapLB t f) (WrapLB t f) x
-> t (WrapLB t f) (WrapLB t f) x
forall {k1} {k2} {k3} (t :: k1 -> k2 -> k3 -> *) (f :: k1)
       (g :: k2) (a :: k3).
WrapHBF t f g a -> t f g a
unwrapHBF
    binterpret :: forall (g :: * -> *) (h :: * -> *).
(g ~> WrapLB t f)
-> (h ~> WrapLB t f) -> WrapHBF t g h ~> WrapLB t f
binterpret g ~> WrapLB t f
f h ~> WrapLB t f
g = WrapHBF t (WrapLB t f) (WrapLB t f) x -> WrapLB t f x
WrapHBF t (WrapLB t f) (WrapLB t f) ~> WrapLB t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
SemigroupIn t f =>
t f f ~> f
biretract (WrapHBF t (WrapLB t f) (WrapLB t f) x -> WrapLB t f x)
-> (WrapHBF t g h x -> WrapHBF t (WrapLB t f) (WrapLB t f) x)
-> WrapHBF t g h x
-> WrapLB t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (g ~> WrapLB t f)
-> (h ~> WrapLB t f)
-> WrapHBF t g h ~> WrapHBF t (WrapLB t f) (WrapLB t f)
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
forall (f :: * -> *) (j :: * -> *) (g :: * -> *) (l :: * -> *).
(f ~> j) -> (g ~> l) -> WrapHBF t f g ~> WrapHBF t j l
hbimap g x -> WrapLB t f x
g ~> WrapLB t f
f h x -> WrapLB t f x
h ~> WrapLB t f
g
instance (Tensor t i, FunctorBy t f, FunctorBy t (WrapLB t f)) => MonoidIn (WrapHBF t) (WrapF i) (WrapLB t f) where
    pureT :: WrapF i ~> WrapLB t f
pureT = ListBy t f x -> WrapLB t f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB (ListBy t f x -> WrapLB t f x)
-> (WrapF i x -> ListBy t f x) -> WrapF i x -> WrapLB t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
i ~> ListBy t f
nilLB @t (i x -> ListBy t f x)
-> (WrapF i x -> i x) -> WrapF i x -> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WrapF i x -> i x
forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF