{-# 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 = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
f ~> t f i
intro1 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 = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
Tensor t i =>
g ~> t i g
intro2 forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
(Tensor t i, FunctorBy t g) =>
t i g ~> g
elim2
sumLeftIdentity :: f <~> V1 :+: f
sumLeftIdentity :: forall {k} (f :: k -> *). f <~> (V1 :+: f)
sumLeftIdentity = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 forall {k} (f :: k -> *) (h :: k -> *) (g :: k -> *).
(f ~> h) -> (g ~> h) -> (f :+: g) ~> h
!+! forall a. a -> a
id)
sumRightIdentity :: f <~> f :+: V1
sumRightIdentity :: forall {k} (f :: k -> *). f <~> (f :+: V1)
sumRightIdentity = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall a. a -> a
id forall {k} (f :: k -> *) (h :: k -> *) (g :: k -> *).
(f ~> h) -> (g ~> h) -> (f :+: g) ~> h
!+! forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1)
prodLeftIdentity :: f <~> Proxy :*: f
prodLeftIdentity :: forall {k} (f :: k -> *). f <~> (Proxy :*: f)
prodLeftIdentity = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (forall {k} (t :: k). Proxy t
Proxy 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 -> *). g <~> (g :*: Proxy)
prodRightIdentity = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: 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 -> *). (f :*: g) ~> f
prodOutL (f x
x :*: g x
_) = f x
x
prodOutR :: f :*: g ~> g
prodOutR :: forall {k} (f :: k -> *) (g :: k -> *). (f :*: g) ~> g
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 = forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Interpret t f =>
t f ~> f
retract forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
MonoidIn t i f =>
ListBy t f ~> f
retractLB @t))
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k1} (t :: (k -> *) -> k1 -> *) (f :: k -> *)
(g :: k -> *).
HFunctor t =>
(f ~> g) -> t f ~> t g
hmap 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 = forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
MonoidIn t i f =>
i ~> f
pureT @t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
hleft (forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
MonoidIn t i f =>
i ~> f
pureT @t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Tensor t i, FunctorBy t f) =>
t f i ~> f
elim1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright forall {k} (f :: k -> *). f ~> Proxy
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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
(Tensor t i, FunctorBy t g) =>
t i g ~> g
elim2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
hleft forall {k} (f :: k -> *). f ~> Proxy
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 = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> t f (ListBy t f)
splitNE 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 = 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 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 = (forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall {k} (t :: k). Proxy t
Proxy)
intro2 :: forall (g :: * -> *). g ~> (Proxy :*: g)
intro2 = (forall {k} (t :: k). Proxy t
Proxy 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) = forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([f x]
xs forall a. [a] -> [a] -> [a]
++ [f x]
ys)
splitNE :: forall (f :: * -> *). NonEmptyBy (:*:) f ~> (f :*: ListBy (:*:) f)
splitNE = forall {k} (f :: k -> *) (a :: k).
NonEmptyF f a -> (:*:) f (ListF f) a
nonEmptyProd
splittingLB :: forall (f :: * -> *).
ListBy (:*:) f <~> (Proxy :+: (f :*: ListBy (:*:) f))
splittingLB = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall {k} {f :: k -> *} {p :: k}.
ListF f p -> (:+:) Proxy (f :*: ListF f) p
to_ 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 [] -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall {k} (t :: k). Proxy t
Proxy
ListF (f p
x:[f p]
xs) -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (f p
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g 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 -> forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF []
R1 (f a
x :*: ListF [f a]
xs) -> forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF (f a
xforall a. a -> [a] -> [a]
:[f a]
xs)
toListBy :: forall (f :: * -> *). (f :*: f) ~> ListBy (:*:) f
toListBy (f x
x :*: f x
y) = 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
_ = 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 = (forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
`Pair` forall {k} (t :: k). Proxy t
Proxy)
intro2 :: forall (g :: * -> *). g ~> Product Proxy g
intro2 = (forall {k} (t :: k). Proxy t
Proxy 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) = forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([f x]
xs forall a. [a] -> [a] -> [a]
++ [f x]
ys)
splitNE :: forall (f :: * -> *).
NonEmptyBy Product f ~> Product f (ListBy Product f)
splitNE = forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF forall {k} (f :: k -> *) (g :: k -> *). (f :*: g) <~> Product f g
prodProd forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall {k} {f :: k -> *} {p :: k}.
ListF f p -> (:+:) Proxy (Product f (ListF f)) p
to_ 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 [] -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall {k} (t :: k). Proxy t
Proxy
ListF (f p
x:[f p]
xs) -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (f p
x forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
`Pair` 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 -> forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF []
R1 (f a
x `Pair` ListF [f a]
xs) -> forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF (f a
xforall a. a -> [a] -> [a]
:[f a]
xs)
toListBy :: forall (f :: * -> *). Product f f ~> ListBy Product f
toListBy (Pair f x
x f x
y) = 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
_ = 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 = forall (f :: * -> *). f ~> Day f Identity
D.intro2
intro2 :: forall (g :: * -> *). g ~> Day Identity g
intro2 = forall (g :: * -> *). g ~> Day Identity g
D.intro1
elim1 :: forall (f :: * -> *). FunctorBy Day f => Day f Identity ~> f
elim1 = forall (f :: * -> *) a. Functor f => Day f Identity a -> f a
D.elim2
elim2 :: forall (g :: * -> *). FunctorBy Day g => Day Identity g ~> g
elim2 = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ListBy Day f b
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ListBy Day f c
y
splitNE :: forall (f :: * -> *). NonEmptyBy Day f ~> Day f (ListBy Day f)
splitNE = 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 = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall {f :: * -> *} {p}. Ap f p -> (:+:) Identity (Day f (Ap f)) p
to_ 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 -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall a. a -> Identity a
Identity p
x)
Ap f a1
x Ap f (a1 -> p)
xs -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (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 forall a b. a -> (a -> b) -> b
(&))
from_ :: (:+:) Identity (Day f (Ap f)) a -> Ap f a
from_ = \case
L1 (Identity a
x) -> forall a (f :: * -> *). a -> Ap f a
Pure a
x
R1 (Day f b
x Ap f c
xs b -> c -> a
f) -> forall (f :: * -> *) a1 a. f a1 -> Ap f (a1 -> a) -> Ap f a
Ap f b
x (forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> a
f 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) = forall (f :: * -> *) a1 a. f a1 -> Ap f (a1 -> a) -> Ap f a
Ap f b
x (forall (f :: * -> *) a1 a. f a1 -> Ap f (a1 -> a) -> Ap f a
Ap f c
y (forall a (f :: * -> *). a -> Ap f a
Pure (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 = 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 = forall (f :: * -> *). f ~> Day f Proxy
CD.intro2
intro2 :: forall (g :: * -> *). g ~> Day Proxy g
intro2 = forall (g :: * -> *). g ~> Day Proxy g
CD.intro1
elim1 :: forall (f :: * -> *). FunctorBy Day f => Day f Proxy ~> f
elim1 = 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 = 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) = forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide x -> (b, c)
z ListBy Day f b
x ListBy Day f c
y
splitNE :: forall (f :: * -> *). NonEmptyBy Day f ~> Day f (ListBy Day f)
splitNE = forall {f :: * -> *} {f :: * -> *} {p}.
(:*:) (Coyoneda f) (ListF (Coyoneda f)) p -> Day f (Div f) p
go 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 @(:*:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). NonEmpty (f a) -> NonEmptyF f a
NonEmptyF forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x (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 = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Div f a -> [Coyoneda f a]
unDiv) (forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). ListF f a -> [f a]
runListF) 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 @(:*:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF (forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright forall {f :: * -> *} {f :: * -> *} {p}.
(:*:) (Coyoneda f) (ListF (Coyoneda f)) p -> Day f (Div f) p
to_) (forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright 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) = forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x (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) = forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
f) f b
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
f) (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) = forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). ListF f a -> [f a]
runListF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t f f ~> ListBy t f
toListBy forall a b. (a -> b) -> a -> b
$
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda (forall a b. (a, b) -> b
snd 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
_ = 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 = forall (f :: * -> *). f ~> Day f Identity
ID.intro2
intro2 :: forall (g :: * -> *). g ~> Day Identity g
intro2 = forall (g :: * -> *). g ~> Day Identity g
ID.intro1
elim1 :: forall (f :: * -> *). FunctorBy Day f => Day f Identity ~> f
elim1 = forall (f :: * -> *) a. Invariant f => Day f Identity a -> f a
ID.elim2
elim2 :: forall (g :: * -> *). FunctorBy Day g => Day Identity g ~> g
elim2 = 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) = forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp forall a b. (a -> b) -> a -> b
$ case Chain Day Identity f b
xs of
Done (Identity b
x) -> forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> x
f b
x) (forall a b. (a, b) -> b
snd 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) -> 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 forall a b. (a -> b) -> a -> b
$ 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
(forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB (forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
ID.Day (forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp Chain Day Identity f c
zs) (forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp Chain Day Identity f c
ys) (,) 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)
(forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> (b, c)
j 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 = coerce :: forall a b. Coercible a b => a -> b
coerce 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 = forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
coercedF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} (t :: k1 -> (k2 -> *) -> k2 -> *) (i :: k2 -> *)
(f :: k1).
Chain t i f <~> (i :+: t f (Chain t i f))
splittingChain forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
coercedF
toListBy :: forall (f :: * -> *). Day f f ~> ListBy Day f
toListBy = forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright (forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject)
instance Matchable ID.Day Identity where
unsplitNE :: forall (f :: * -> *).
FunctorBy Day f =>
Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE = coerce :: forall a b. Coercible a b => a -> b
coerce 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 = coerce :: forall a b. Coercible a b => a -> b
coerce 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) -> forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> x
`g` c
r) (forall a b. (a, b) -> a
fst 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 -> forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 forall a b. (a -> b) -> a -> b
$ 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 (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 -> 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 -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ 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) = 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 = forall (f :: * -> *). f ~> Night f Not
IN.intro2
intro2 :: forall (g :: * -> *). g ~> Night Not g
intro2 = forall (g :: * -> *). g ~> Night Not g
IN.intro1
elim1 :: forall (f :: * -> *). FunctorBy Night f => Night f Not ~> f
elim1 = forall (f :: * -> *). Invariant f => Night f Not ~> f
IN.elim2
elim2 :: forall (g :: * -> *). FunctorBy Night g => Night Not g ~> g
elim2 = 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) = forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt forall a b. (a -> b) -> a -> b
$ case Chain Night Not f b1
xs of
Done Not b1
r -> forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap c1 -> x
g (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a. Void -> a
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Not a -> a -> Void
refute Not b1
r) forall a. a -> a
id 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) -> 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 forall a b. (a -> b) -> a -> b
$ 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
(forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB (forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
IN.Night (forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c1
zs) (forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c1
ys) forall a b. a -> Either a b
Left forall a b. b -> Either a b
Right forall a. a -> a
id))
(b1 -> x
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. b1 -> b1
j)
(forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b1 -> x
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. c1 -> b1
k) c1 -> x
g)
(forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b1 -> Either b1 c1
l 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 = coerce :: forall a b. Coercible a b => a -> b
coerce 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 = forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
coercedF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} (t :: k1 -> (k2 -> *) -> k2 -> *) (i :: k2 -> *)
(f :: k1).
Chain t i f <~> (i :+: t f (Chain t i f))
splittingChain forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
coercedF
toListBy :: forall (f :: * -> *). Night f f ~> ListBy Night f
toListBy = forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright (forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject)
instance Matchable IN.Night Not where
unsplitNE :: forall (f :: * -> *).
FunctorBy Night f =>
Night f (ListBy Night f) ~> NonEmptyBy Night f
unsplitNE = coerce :: forall a b. Coercible a b => a -> b
coerce 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 = coerce :: forall a b. Coercible a b => a -> b
coerce 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 -> forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap b1 -> x
f (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id (forall a. Void -> a
absurd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Not a -> a -> Void
refute Not c1
r) 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 -> forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 forall a b. (a -> b) -> a -> b
$ 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 (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 -> 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 -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ 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) = 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 = forall (f :: * -> *). f ~> Night f Not
N.intro2
intro2 :: forall (g :: * -> *). g ~> Night Not g
intro2 = forall (g :: * -> *). g ~> Night Not g
N.intro1
elim1 :: forall (f :: * -> *). FunctorBy Night f => Night f Not ~> f
elim1 = forall (f :: * -> *). Contravariant f => Night f Not ~> f
N.elim2
elim2 :: forall (g :: * -> *). FunctorBy Night g => Night Not g ~> g
elim2 = 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) = forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either b1 c1
z ListBy Night f b1
x 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) = 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 = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall {a :: * -> *} {p}. Dec a p -> (:+:) Not (Night a (Dec a)) p
to_ 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 -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall a. (a -> Void) -> Not a
Not p -> Void
f)
Choose p -> Either b1 c
f a b1
x Dec a c
xs -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (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) -> 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) -> 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) = 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 (forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject f c1
y)
instance Conclude f => MonoidIn Night Not f where
pureT :: Not ~> f
pureT (Not x -> Void
x) = 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 = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1
intro2 :: forall (g :: * -> *). g ~> (V1 :+: g)
intro2 = 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 -> 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 -> 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 = forall a. a -> a
id forall (t :: (* -> *) -> (* -> *) -> * -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *).
SemigroupIn t h =>
(f ~> h) -> (g ~> h) -> t f g ~> h
!*! forall {k} (f :: k -> *). (f :+: Step f) ~> Step f
stepUp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
splitNE :: forall (f :: * -> *). NonEmptyBy (:+:) f ~> (f :+: ListBy (:+:) f)
splitNE = forall {k} (f :: k -> *). Step f ~> (f :+: Step f)
stepDown
splittingLB :: forall (f :: * -> *).
ListBy (:+:) f <~> (V1 :+: (f :+: ListBy (:+:) f))
splittingLB = forall {k} (f :: k -> *). Step f <~> (f :+: Step f)
stepping forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *). f <~> (V1 :+: f)
sumLeftIdentity
toListBy :: forall (f :: * -> *). (f :+: f) ~> ListBy (:+:) f
toListBy = \case
L1 f x
x -> forall {k} (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step Natural
0 f x
x
R1 f x
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 = 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 = forall {k} (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL
intro2 :: forall (g :: * -> *). g ~> Sum V1 g
intro2 = 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 -> 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 -> 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 = forall a. a -> a
id forall (t :: (* -> *) -> (* -> *) -> * -> *) (h :: * -> *)
(f :: * -> *) (g :: * -> *).
SemigroupIn t h =>
(f ~> h) -> (g ~> h) -> t f g ~> h
!*! forall {k} (f :: k -> *). (f :+: Step f) ~> Step f
stepUp forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF forall {k} (f :: k -> *) (g :: k -> *). (f :+: g) <~> Sum f g
sumSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *). Step f ~> (f :+: Step f)
stepDown
splittingLB :: forall (f :: * -> *).
ListBy Sum f <~> (V1 :+: Sum f (ListBy Sum f))
splittingLB = forall {k} (f :: k -> *). Step f <~> (f :+: Step f)
stepping
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *). f <~> (V1 :+: f)
sumLeftIdentity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. a -> a
id forall {k} (f :: k -> *) (g :: k -> *). (f :+: g) <~> Sum f g
sumSum
toListBy :: forall (f :: * -> *). Sum f f ~> ListBy Sum f
toListBy = \case
InL f x
x -> forall {k} (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step Natural
0 f x
x
InR f x
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 = 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 = forall (f :: * -> *) (g :: * -> *) a. f a -> These1 f g a
This1
intro2 :: forall (g :: * -> *). g ~> These1 V1 g
intro2 = 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 -> forall {k} (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
These1 f x
_ V1 x
y -> 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 -> 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
_ -> 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 -> forall (f :: * -> *). These1 f (Steps f) ~> Steps f
stepsUp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) (g :: * -> *) a. g a -> These1 f g a
That1 forall a b. (a -> b) -> a -> b
$ ListBy These1 f x
y
These1 ListBy These1 f x
x ListBy These1 f x
y -> ListBy These1 f x
x forall a. Semigroup a => a -> a -> a
<> ListBy These1 f x
y
splitNE :: forall (f :: * -> *).
NonEmptyBy These1 f ~> These1 f (ListBy These1 f)
splitNE = forall (f :: * -> *). Steps f ~> These1 f (Steps f)
stepsDown forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Flagged f a -> f a
flaggedVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (f :: * -> *). Steps f <~> These1 f (Steps f)
steppings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *). f <~> (V1 :+: f)
sumLeftIdentity
toListBy :: forall (f :: * -> *). These1 f f ~> ListBy These1 f
toListBy = \case
This1 f x
x -> forall {k} (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> NEMap k a
NEM.singleton Natural
0 f x
x
That1 f x
y -> forall {k} (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> NEMap k a
NEM.singleton Natural
1 f x
y
These1 f x
x f x
y -> forall {k} (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps forall a b. (a -> b) -> a -> b
$ forall k a. NonEmpty (k, a) -> NEMap k a
NEM.fromDistinctAscList ((Natural
0, f x
x) forall a. a -> [a] -> NonEmpty a
:| [(Natural
1, f x
y)])
instance Alt f => MonoidIn These1 V1 f where
pureT :: V1 ~> f
pureT = 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 = (forall {k} (f :: * -> *) (g :: k -> *) (a :: k) x.
f x -> (x -> g a) -> Comp f g a
:>>= forall a. a -> Identity a
Identity)
intro2 :: forall (g :: * -> *). g ~> Comp Identity g
intro2 = (forall a. a -> Identity a
Identity () forall {k} (f :: * -> *) (g :: k -> *) (a :: k) x.
f x -> (x -> g a) -> Comp f g a
:>>=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Identity x
y 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 (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) = ListBy Comp f x
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> ListBy Comp f x
y
splitNE :: forall (f :: * -> *). NonEmptyBy Comp f ~> Comp f (ListBy Comp f)
splitNE = forall (f :: * -> *). Free1 f ~> Comp f (Free f)
free1Comp
splittingLB :: forall (f :: * -> *).
ListBy Comp f <~> (Identity :+: Comp f (ListBy Comp f))
splittingLB = forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall (f :: * -> *). Free f ~> (Identity :+: Comp f (Free f))
to_ forall (f :: * -> *). (Identity :+: Comp f (Free f)) ~> Free f
from_
where
to_ :: Free f ~> Identity :+: Comp f (Free f)
to_ :: forall (f :: * -> *). Free f ~> (Identity :+: Comp f (Free f))
to_ = forall a r (f :: * -> *).
(a -> r) -> (forall s. f s -> (s -> r) -> r) -> Free f a -> r
foldFree' (forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity) forall a b. (a -> b) -> a -> b
$ \f s
y s -> (:+:) Identity (Comp f (Free f)) x
n -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$
f s
y forall {k} (f :: * -> *) (g :: k -> *) (a :: k) x.
f x -> (x -> g a) -> Comp f g a
:>>= (forall (f :: * -> *). (Identity :+: Comp f (Free f)) ~> Free f
from_ 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 :: * -> *). (Identity :+: Comp f (Free f)) ~> Free f
from_ = forall (f :: * -> *). Applicative f => Identity ~> f
generalize
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 -> forall (f :: * -> *). f ~> Free f
liftFree f x
x 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) = forall (f :: * -> *). f ~> Free f
liftFree f x
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject 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 = forall (f :: * -> *). Applicative f => Identity ~> f
generalize
instance Matchable (:*:) Proxy where
unsplitNE :: forall (f :: * -> *).
FunctorBy (:*:) f =>
(f :*: ListBy (:*:) f) ~> NonEmptyBy (:*:) f
unsplitNE = 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 = forall {k} (f :: k -> *). ListF f ~> (Proxy :+: NonEmptyF f)
fromListF
instance Matchable Product Proxy where
unsplitNE :: forall (f :: * -> *).
FunctorBy Product f =>
Product f (ListBy Product f) ~> NonEmptyBy Product f
unsplitNE = forall {k} (f :: k -> *) (a :: k).
(:*:) f (ListF f) a -> NonEmptyF f a
ProdNonEmpty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF forall {k} (f :: k -> *) (g :: k -> *). (f :*: g) <~> Product f g
prodProd
matchLB :: forall (f :: * -> *).
FunctorBy Product f =>
ListBy Product f ~> (Proxy :+: NonEmptyBy Product f)
matchLB = forall {k} (f :: k -> *). ListF f ~> (Proxy :+: NonEmptyF f)
fromListF
instance Matchable Day Identity where
unsplitNE :: forall (f :: * -> *).
FunctorBy Day f =>
Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE = 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 = forall (f :: * -> *). Ap f ~> (Identity :+: Ap1 f)
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) = forall (f :: * -> *) a. NonEmpty (Coyoneda f a) -> Div1 f a
Div1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). NonEmptyF f a -> NonEmpty (f a)
runNonEmptyF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE forall a b. (a -> b) -> a -> b
$
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
CCY.Coyoneda (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) (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 = forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright (forall (f :: * -> *) a. NonEmpty (Coyoneda f a) -> Div1 f a
Div1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). NonEmptyF f a -> NonEmpty (f a)
runNonEmptyF) 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 @(:*:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = 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 ListBy Night f c1
xs
matchLB :: forall (f :: * -> *).
FunctorBy Night f =>
ListBy Night f ~> (Not :+: NonEmptyBy Night f)
matchLB = \case
Lose x -> Void
f -> forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (forall a. (a -> Void) -> Not a
Not x -> Void
f)
Choose x -> Either b1 c
f f b1
x Dec f c
xs -> forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (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 = forall {k} (f :: k -> *). (f :+: Step f) ~> Step f
stepUp
matchLB :: forall (f :: * -> *).
FunctorBy (:+:) f =>
ListBy (:+:) f ~> (V1 :+: NonEmptyBy (:+:) f)
matchLB = 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 = forall {k} (f :: k -> *). (f :+: Step f) ~> Step f
stepUp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF forall {k} (f :: k -> *) (g :: k -> *). (f :+: g) <~> Sum f g
sumSum
matchLB :: forall (f :: * -> *).
FunctorBy Sum f =>
ListBy Sum f ~> (V1 :+: NonEmptyBy Sum f)
matchLB = 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
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
showList :: [WrapF f a] -> ShowS
$cshowList :: forall k (f :: k -> *) (a :: k). Show (f a) => [WrapF f a] -> ShowS
show :: WrapF f a -> String
$cshow :: forall k (f :: k -> *) (a :: k). Show (f a) => WrapF f a -> String
showsPrec :: Int -> WrapF f a -> ShowS
$cshowsPrec :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> WrapF f a -> ShowS
Show, ReadPrec [WrapF f a]
ReadPrec (WrapF f a)
ReadS [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]
readListPrec :: ReadPrec [WrapF f a]
$creadListPrec :: forall k (f :: k -> *) (a :: k). Read (f a) => ReadPrec [WrapF f a]
readPrec :: ReadPrec (WrapF f a)
$creadPrec :: forall k (f :: k -> *) (a :: k). Read (f a) => ReadPrec (WrapF f a)
readList :: ReadS [WrapF f a]
$creadList :: forall k (f :: k -> *) (a :: k). Read (f a) => ReadS [WrapF f a]
readsPrec :: Int -> ReadS (WrapF f a)
$creadsPrec :: forall k (f :: k -> *) (a :: k).
Read (f a) =>
Int -> ReadS (WrapF f a)
Read, WrapF f a -> WrapF f a -> Bool
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
/= :: 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
Eq, 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
min :: 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
max :: WrapF f a -> WrapF f a -> WrapF f a
$cmax :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> WrapF f a
>= :: 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
$c< :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Bool
compare :: WrapF f a -> WrapF f a -> Ordering
$ccompare :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
WrapF f a -> WrapF f a -> Ordering
Ord, 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
<$ :: forall a b. a -> WrapF f b -> WrapF f a
$c<$ :: forall (f :: * -> *) a b. Functor f => a -> WrapF f b -> WrapF f a
fmap :: forall a b. (a -> b) -> WrapF f a -> WrapF f b
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> WrapF f a -> WrapF f b
Functor, 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
product :: forall a. Num a => WrapF f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => WrapF f a -> a
sum :: forall a. Num a => WrapF f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => WrapF f a -> a
minimum :: forall a. Ord a => WrapF f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => WrapF f a -> a
maximum :: forall a. Ord a => WrapF f a -> a
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => WrapF f a -> a
elem :: forall a. Eq a => a -> WrapF f a -> Bool
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> WrapF f a -> Bool
length :: forall a. WrapF f a -> Int
$clength :: forall (f :: * -> *) a. Foldable f => WrapF f a -> Int
null :: forall a. WrapF f a -> Bool
$cnull :: forall (f :: * -> *) a. Foldable f => WrapF f a -> Bool
toList :: forall a. WrapF f a -> [a]
$ctoList :: forall (f :: * -> *) a. Foldable f => WrapF f a -> [a]
foldl1 :: forall a. (a -> a -> a) -> WrapF f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> WrapF f a -> a
foldr1 :: forall a. (a -> a -> a) -> WrapF f a -> a
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> WrapF f a -> a
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
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> 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
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> WrapF f a -> b
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
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> WrapF f a -> m
fold :: forall m. Monoid m => WrapF f m -> m
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => WrapF f m -> m
Foldable, 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 (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> WrapF f a -> f (WrapF f b)
sequence :: forall (m :: * -> *) a. Monad m => WrapF f (m a) -> m (WrapF f a)
$csequence :: forall (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
WrapF f (m a) -> m (WrapF f a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> WrapF f a -> m (WrapF f b)
$cmapM :: forall (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> WrapF f a -> m (WrapF f b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
WrapF f (f a) -> f (WrapF f a)
$csequenceA :: forall (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
WrapF f (f a) -> f (WrapF f a)
traverse :: 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)
Traversable, Typeable, 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
$cto :: forall k (f :: k -> *) (a :: k) x. Rep (WrapF f a) x -> WrapF f a
$cfrom :: forall k (f :: k -> *) (a :: k) x. WrapF f a -> Rep (WrapF f a) x
Generic, WrapF f a -> DataType
WrapF f a -> Constr
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 {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 -> DataType
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)) =>
(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 (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)
gmapMo :: 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)
gmapMp :: forall (m :: * -> *).
MonadPlus 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)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> WrapF f a -> m (WrapF f a)
$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)
gmapQi :: forall u. Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> WrapF f a -> [u]
$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]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> WrapF f a -> r
$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
gmapT :: (forall b. Data b => b -> b) -> WrapF f a -> 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
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> 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))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (WrapF f a))
$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))
dataTypeOf :: WrapF f a -> DataType
$cdataTypeOf :: forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
WrapF f a -> DataType
toConstr :: WrapF f a -> Constr
$ctoConstr :: forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
WrapF f a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> 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)
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)
$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)
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) = forall a. (Int -> a -> ShowS) -> String -> Int -> a -> ShowS
showsUnaryWith (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) = 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) = 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 = forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
(a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright forall {k} (f :: k -> *) (a :: k). f a -> WrapF f a
WrapF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
f ~> t f i
intro1
intro2 :: forall (g :: * -> *). g ~> WrapHBF t (WrapF i) g
intro2 = forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
(a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
hleft forall {k} (f :: k -> *) (a :: k). f a -> WrapF f a
WrapF forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Tensor t i, FunctorBy t f) =>
t f i ~> f
elim1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (g :: k -> *)
(l :: k -> *) (f :: k -> *).
HBifunctor t =>
(g ~> l) -> t f g ~> t f l
hright forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
(Tensor t i, FunctorBy t g) =>
t i g ~> g
elim2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(j :: k -> *) (g :: k -> *).
HBifunctor t =>
(f ~> j) -> t f g ~> t j g
hleft forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
(a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF 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
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
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall {k} (f :: k -> *) (a :: k). f a -> WrapF f a
WrapF forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF) (forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF forall {k} {k1} {k2} (t :: k -> k1 -> k2 -> *) (f :: k) (g :: k1)
(a :: k2).
t f g a -> WrapHBF t f g a
WrapHBF 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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t f f ~> ListBy t f
toListBy forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB (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) = forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB (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) = forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB (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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(j :: k -> *) (g :: k -> *) (l :: k -> *).
HBifunctor t =>
(f ~> j) -> (g ~> l) -> t f g ~> t j l
hbimap forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
WrapLB t f a -> ListBy t f a
unwrapLB forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
WrapLB t f a -> ListBy t f a
unwrapLB forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
SemigroupIn t f =>
t f f ~> f
biretract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(j :: k -> *) (g :: k -> *) (l :: k -> *).
HBifunctor t =>
(f ~> j) -> (g ~> l) -> t f g ~> t j l
hbimap g ~> WrapLB t f
f 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 = forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
i ~> ListBy t f
nilLB @t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). WrapF f a -> f a
unwrapF