{-# 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.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 :: 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 ~> t f i
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
f ~> t f i
intro1 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 :: 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 ~> t i g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
Tensor t i =>
g ~> t i g
intro2 t i g ~> g
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
(Tensor t i, FunctorBy t g) =>
t i g ~> g
elim2
sumLeftIdentity :: f <~> V1 :+: f
sumLeftIdentity :: 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 ~> (V1 :+: f)
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (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 ~> f
forall a. a -> a
id)
sumRightIdentity :: f <~> f :+: V1
sumRightIdentity :: 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 ~> (f :+: V1)
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (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 ~> f
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1)
prodLeftIdentity :: f <~> Proxy :*: f
prodLeftIdentity :: 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 _ :*: y -> f x
y)
prodRightIdentity :: g <~> g :*: Proxy
prodRightIdentity :: 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 x :*: _ -> g x
x)
prodOutL :: f :*: g ~> f
prodOutL :: (:*:) f g x -> f x
prodOutL (x :: f x
x :*: _) = f x
x
prodOutR :: f :*: g ~> g
prodOutR :: (:*:) f g x -> g x
prodOutR (_ :*: y :: 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
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 (i :: * -> *) (f :: * -> *).
Tensor t i =>
ListBy t f <~> (i :+: t f (ListBy t f))
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 :: ListBy t f ~> f
retractLB = (forall (i :: * -> *) (f :: * -> *). MonoidIn t i f => i ~> f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
MonoidIn t i f =>
i ~> f
pureT @t (forall x. i x -> f x)
-> (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 (f :: * -> *). SemigroupIn t f => t f f ~> f
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
hright (forall (i :: * -> *) (f :: * -> *).
MonoidIn t i f =>
ListBy t f ~> f
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 (i :: * -> *) (f :: * -> *).
Tensor t i =>
ListBy t f ~> (i :+: t f (ListBy t f))
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 :: (g ~> f) -> ListBy t g ~> f
interpretLB f :: g ~> f
f = forall (i :: * -> *) (f :: * -> *).
MonoidIn t i f =>
ListBy t 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 k (t :: (k -> *) -> k -> *) (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 :: 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
hright (forall (i :: * -> *) (f :: * -> *). MonoidIn t i f => i ~> f
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 (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 :: 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
hleft (forall (i :: * -> *) (f :: * -> *). MonoidIn t i f => i ~> f
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 (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
Tensor t i =>
g ~> t i g
intro2
outL
:: (Tensor t Proxy, FunctorBy t f)
=> t f g ~> f
outL :: t f g ~> f
outL = t f Proxy x -> f x
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
hright g ~> Proxy
forall k (f :: k -> *). f ~> Proxy
absorb
outR
:: (Tensor t Proxy, FunctorBy t g)
=> t f g ~> g
outR :: t f g ~> g
outR = t Proxy g x -> g x
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
hleft f ~> Proxy
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 :: 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 ~> 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) ~> 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 :: 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 (i :: * -> *) (f :: * -> *).
(Matchable t i, FunctorBy t f) =>
ListBy t f ~> (i :+: NonEmptyBy t f)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Matchable t i, FunctorBy t f) =>
ListBy t f ~> (i :+: NonEmptyBy t f)
matchLB @t) (forall (i :: * -> *) (f :: * -> *). Tensor t i => i ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
i ~> ListBy t f
nilLB @t (forall x. i x -> ListBy t f x)
-> (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 (i :: * -> *) (f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> ListBy t f
fromNE @t)
instance Tensor (:*:) Proxy where
type ListBy (:*:) = ListF
intro1 :: f x -> (:*:) f Proxy x
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 :: g x -> (:*:) Proxy g x
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 :: (f :*: Proxy) ~> f
elim1 (x :: f x
x :*: ~Proxy x
Proxy) = f x
x
elim2 :: (Proxy :*: g) ~> g
elim2 (~Proxy x
Proxy :*: y :: g x
y ) = g x
y
appendLB :: (:*:) (ListBy (:*:) f) (ListBy (:*:) f) x -> ListBy (:*:) f x
appendLB (ListF xs :*: ListF 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 :: NonEmptyBy (:*:) f x -> (:*:) f (ListBy (:*:) f) x
splitNE = NonEmptyBy (:*:) f x -> (:*:) f (ListBy (:*:) f) x
forall k (f :: k -> *) (a :: k).
NonEmptyF f a -> (:*:) f (ListF f) a
nonEmptyProd
splittingLB :: p ((:+:) Proxy (f :*: ListBy (:*:) f) a)
((:+:) Proxy (f :*: ListBy (:*:) f) a)
-> p (ListBy (:*:) f a) (ListBy (:*:) f a)
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 ~> (Proxy :+: (f :*: ListF f))
forall k (f :: k -> *) (p :: k).
ListF f p -> (:+:) Proxy (f :*: ListF f) p
to_ (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 (x :: f p
x:xs :: [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 (x :: f a
x :*: ListF xs :: [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 :: (:*:) f f x -> ListBy (:*:) f x
toListBy (x :: f x
x :*: y :: 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 x -> f x
pureT _ = f x
forall (f :: * -> *) a. Plus f => f a
zero
instance Tensor Product Proxy where
type ListBy Product = ListF
intro1 :: f x -> Product f Proxy x
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 :: g x -> Product Proxy g x
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 :: Product f Proxy ~> f
elim1 (Pair x :: f x
x ~Proxy x
Proxy) = f x
x
elim2 :: Product Proxy g ~> g
elim2 (Pair ~Proxy x
Proxy y :: g x
y) = g x
y
appendLB :: Product (ListBy Product f) (ListBy Product f) x
-> ListBy Product f x
appendLB (ListF xs `Pair` ListF 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 :: NonEmptyBy Product f x -> Product f (ListBy Product f) x
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 forall k (f :: k -> *) (g :: k -> *). (f :*: g) <~> Product f g
(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 :: p ((:+:) Proxy (Product f (ListBy Product f)) a)
((:+:) Proxy (Product f (ListBy Product f)) a)
-> p (ListBy Product f a) (ListBy Product f a)
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 ~> (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)) ~> 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 (x :: f p
x:xs :: [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 (x :: f a
x `Pair` ListF xs :: [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 :: Product f f x -> ListBy Product f x
toListBy (Pair x :: f x
x y :: 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 x -> f x
pureT _ = f x
forall (f :: * -> *) a. Plus f => f a
zero
instance Tensor Day Identity where
type ListBy Day = Ap
intro1 :: f x -> Day f Identity x
intro1 = f x -> Day f Identity x
forall (f :: * -> *). f ~> Day f Identity
D.intro2
intro2 :: g x -> Day Identity g x
intro2 = g x -> Day Identity g x
forall (g :: * -> *). g ~> Day Identity g
D.intro1
elim1 :: 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 :: 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 :: Day (ListBy Day f) (ListBy Day f) x -> ListBy Day f x
appendLB (Day x :: ListBy Day f b
x y :: ListBy Day f c
y z :: 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ap f c
ListBy Day f c
y
splitNE :: NonEmptyBy Day f x -> Day f (ListBy Day f) x
splitNE = NonEmptyBy Day f x -> Day f (ListBy Day f) x
forall (f :: * -> *) a. Ap1 f a -> Day f (Ap f) a
ap1Day
splittingLB :: p ((:+:) Identity (Day f (ListBy Day f)) a)
((:+:) Identity (Day f (ListBy Day f)) a)
-> p (ListBy Day f a) (ListBy Day f a)
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 ~> (Identity :+: Day f (Ap f))
forall (f :: * -> *) p. Ap f p -> (:+:) Identity (Day f (Ap f)) p
to_ (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 x :: 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 x :: f a1
x xs :: 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 x :: a
x) -> a -> Ap f a
forall a (f :: * -> *). a -> Ap f a
Pure a
x
R1 (Day x :: f b
x xs :: Ap f c
xs f :: 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 :: Day f f x -> ListBy Day f x
toListBy (Day x :: f b
x y :: f c
y z :: 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 x -> f x
pureT = Identity x -> f x
forall (f :: * -> *). Applicative f => Identity ~> f
generalize
instance Tensor CD.Day Proxy where
type ListBy CD.Day = Div
intro1 :: f x -> Day f Proxy x
intro1 = f x -> Day f Proxy x
forall (f :: * -> *). f ~> Day f Proxy
CD.intro2
intro2 :: g x -> Day Proxy g x
intro2 = g x -> Day Proxy g x
forall (g :: * -> *). g ~> Day Proxy g
CD.intro1
elim1 :: 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 :: 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 :: Day (ListBy Day f) (ListBy Day f) x -> ListBy Day f x
appendLB (CD.Day x :: ListBy Day f b
x y :: ListBy Day f c
y z :: x -> (b, c)
z) = (x -> (b, c)) -> Div f b -> Div f c -> Div f x
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 :: NonEmptyBy Day f x -> Day f (ListBy Day f) x
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 (i :: * -> *) (f :: * -> *).
Tensor (:*:) i =>
NonEmptyBy (:*:) f ~> (f :*: ListBy (:*:) f)
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 f :: p -> b
f x :: f b
x :*: ListF 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) (\y :: p
y -> (p -> b
f p
y, p
y))
splittingLB :: p ((:+:) Proxy (Day f (ListBy Day f)) a)
((:+:) Proxy (Day f (ListBy Day f)) a)
-> p (ListBy Day f a) (ListBy Day f a)
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 (i :: * -> *) (f :: * -> *).
Tensor (:*:) i =>
ListBy (:*:) f <~> (i :+: (f :*: ListBy (:*:) f))
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
hright (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
hright 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 f :: p -> b
f x :: f b
x :*: ListF 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) (\y :: p
y -> (p -> b
f p
y, p
y))
from_ :: Day f (Div f) a -> (:*:) (Coyoneda f) (ListF (Coyoneda f)) a
from_ (CD.Day x :: f b
x (Div xs) f :: 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 (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> 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 :: Day f f x -> ListBy Day f x
toListBy (CD.Day x :: f b
x y :: f c
y f :: x -> (b, c)
f) = [Coyoneda f x] -> Div f x
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div ([Coyoneda f x] -> Div f x)
-> ((:*:) (Coyoneda f) (Coyoneda f) x -> [Coyoneda f x])
-> (:*:) (Coyoneda f) (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 (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
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 x -> f x
pureT _ = f x
forall (f :: * -> *) a. Divisible f => f a
conquer
instance Tensor ID.Day Identity where
type ListBy ID.Day = DivAp
intro1 :: f x -> Day f Identity x
intro1 = f x -> Day f Identity x
forall (f :: * -> *). f ~> Day f Identity
ID.intro2
intro2 :: g x -> Day Identity g x
intro2 = g x -> Day Identity g x
forall (g :: * -> *). g ~> Day Identity g
ID.intro1
elim1 :: 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 :: 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 :: Day (ListBy Day f) (ListBy Day f) x -> ListBy Day f x
appendLB (ID.Day (DivAp xs) (DivAp ys) f :: b -> c -> x
f g :: x -> (b, c)
g) = Chain Day Identity f x -> ListBy Day f x
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f x -> ListBy Day f x)
-> Chain Day Identity f x -> ListBy Day f x
forall a b. (a -> b) -> a -> b
$ case Chain Day Identity f b
xs of
Done (Identity x :: b
x) -> (c -> x)
-> (x -> c) -> Chain Day Identity f c -> Chain Day Identity f x
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 z :: f b
z zs :: Chain Day Identity f c
zs h :: b -> c -> b
h j :: b -> (b, c)
j) -> Day f (Chain Day Identity f) x -> Chain Day Identity f x
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
t f (Chain t i f) a -> Chain t i f a
More (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 (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))
(\q :: b
q (r :: c
r, s :: c
s) -> b -> c -> x
f (b -> c -> b
h b
q c
r) c
s)
(((b, c), c) -> (b, (c, 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 (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 :: NonEmptyBy Day f x -> Day f (ListBy Day f) x
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
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
Chain1 t f ~> t f (Chain t i f)
splitChain1
splittingLB :: p ((:+:) Identity (Day f (ListBy Day f)) a)
((:+:) Identity (Day f (ListBy Day f)) a)
-> p (ListBy Day f a) (ListBy Day f a)
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
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).
Chain t i f <~> (i :+: t f (Chain t i f))
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
coercedF
toListBy :: Day f f x -> ListBy Day f x
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 k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
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
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
inject)
instance Matchable ID.Day Identity where
unsplitNE :: 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
forall (f :: * -> *).
Invariant f =>
Day f (Chain Day Identity f) ~> Chain1 Day f
unsplitNEIDay_
matchLB :: 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
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_ :: Day f (Chain Day Identity f) ~> Chain1 Day f
unsplitNEIDay_ (ID.Day x :: f b
x xs :: Chain Day Identity f c
xs g :: b -> c -> x
g f :: x -> (b, c)
f) = case Chain Day Identity f c
xs of
Done (Identity r :: 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 (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 ys :: 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
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_ :: Chain Day Identity f ~> (Identity :+: Chain1 Day f)
matchLBIDay_ = \case
Done x :: 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 xs :: 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
forall (f :: * -> *).
Invariant f =>
Day f (Chain Day Identity f) ~> Chain1 Day f
unsplitNEIDay_ Day f (Chain Day Identity f) x
xs
instance Tensor IN.Night IN.Not where
type ListBy IN.Night = DecAlt
intro1 :: f x -> Night f Not x
intro1 = f x -> Night f Not x
forall (f :: * -> *). f ~> Night f Not
IN.intro2
intro2 :: g x -> Night Not g x
intro2 = g x -> Night Not g x
forall (g :: * -> *). g ~> Night Not g
IN.intro1
elim1 :: Night f Not ~> f
elim1 = Night f Not x -> f x
forall (f :: * -> *). Invariant f => Night f Not ~> f
IN.elim2
elim2 :: Night Not g ~> g
elim2 = Night Not g x -> g x
forall (g :: * -> *). Invariant g => Night Not g ~> g
IN.elim1
appendLB :: Night (ListBy Night f) (ListBy Night f) x -> ListBy Night f x
appendLB (IN.Night (DecAlt xs) (DecAlt ys) f :: x -> Either b c
f g :: b -> x
g h :: c -> x
h) = Chain Night Not f x -> ListBy Night f x
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt (Chain Night Not f x -> ListBy Night f x)
-> Chain Night Not f x -> ListBy Night f x
forall a b. (a -> b) -> a -> b
$ case Chain Night Not f b
xs of
Done r :: Not b
r -> (c -> x) -> (x -> c) -> Chain Night Not f c -> Chain Night Not f x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap c -> x
h ((b -> c) -> (c -> c) -> Either b c -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> c
forall a. Void -> a
absurd (Void -> c) -> (b -> Void) -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not b -> b -> Void
forall a. Not a -> a -> Void
refute Not b
r) c -> c
forall a. a -> a
id (Either b c -> c) -> (x -> Either b c) -> x -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
f) Chain Night Not f c
ys
More (IN.Night z :: f b
z zs :: Chain Night Not f c
zs j :: b -> Either b c
j k :: b -> b
k l :: c -> b
l) -> Night f (Chain Night Not f) x -> Chain Night Not f x
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) 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 b
-> Chain Night Not f (Either c c)
-> (x -> Either b (Either c c))
-> (b -> x)
-> (Either c c -> x)
-> Night f (Chain Night Not f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
IN.Night
f b
z
(DecAlt f (Either c c) -> Chain Night Not f (Either c c)
forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt (DecAlt f (Either c c) -> Chain Night Not f (Either c c))
-> DecAlt f (Either c c) -> Chain Night Not f (Either c c)
forall a b. (a -> b) -> a -> b
$ Night (ListBy Night f) (ListBy Night f) (Either c c)
-> ListBy Night f (Either c c)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (ListBy t f) (ListBy t f) ~> ListBy t f
appendLB (DecAlt f c
-> DecAlt f c
-> (Either c c -> Either c c)
-> (c -> Either c c)
-> (c -> Either c c)
-> Night (DecAlt f) (DecAlt f) (Either c c)
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
IN.Night (Chain Night Not f c -> DecAlt f c
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c
zs) (Chain Night Not f c -> DecAlt f c
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c
ys) Either c c -> Either c c
forall a. a -> a
id c -> Either c c
forall a b. a -> Either a b
Left c -> Either c c
forall a b. b -> Either a b
Right))
(Either (Either b c) c -> Either b (Either c c)
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc (Either (Either b c) c -> Either b (Either c c))
-> (x -> Either (Either b c) c) -> x -> Either b (Either c c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Either b c) -> Either b c -> Either (Either b c) c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> Either b c
j (Either b c -> Either (Either b c) c)
-> (x -> Either b c) -> x -> Either (Either b c) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
f)
(b -> x
g (b -> x) -> (b -> b) -> b -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b
k)
((c -> x) -> (c -> x) -> Either c c -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> x
g (b -> x) -> (c -> b) -> c -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> b
l) c -> x
h)
splitNE :: NonEmptyBy Night f x -> Night f (ListBy Night f) x
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
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
Chain1 t f ~> t f (Chain t i f)
splitChain1
splittingLB :: p ((:+:) Not (Night f (ListBy Night f)) a)
((:+:) Not (Night f (ListBy Night f)) a)
-> p (ListBy Night f a) (ListBy Night f a)
splittingLB = p (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
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).
Chain t i f <~> (i :+: t f (Chain t i f))
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
coercedF
toListBy :: Night f f x -> ListBy Night f x
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 k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) 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
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
inject)
instance Matchable IN.Night Not where
unsplitNE :: 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
forall (f :: * -> *).
Invariant f =>
Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_
matchLB :: 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
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_ :: Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_ (IN.Night x :: f b
x xs :: Chain Night Not f c
xs f :: x -> Either b c
f g :: b -> x
g h :: c -> x
h) = case Chain Night Not f c
xs of
Done r :: Not c
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
$ (b -> x) -> (x -> b) -> f b -> f x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap b -> x
g ((b -> b) -> (c -> b) -> Either b c -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
id (Void -> b
forall a. Void -> a
absurd (Void -> b) -> (c -> Void) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not c -> c -> Void
forall a. Not a -> a -> Void
refute Not c
r) (Either b c -> b) -> (x -> Either b c) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
f) f b
x
More ys :: Night f (Chain Night Not f) c
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 b
-> Chain1 Night f c
-> (x -> Either b c)
-> (b -> x)
-> (c -> x)
-> Night f (Chain1 Night f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
IN.Night f b
x (Night f (Chain Night Not f) c -> Chain1 Night f c
forall (f :: * -> *).
Invariant f =>
Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_ Night f (Chain Night Not f) c
ys) x -> Either b c
f b -> x
g c -> x
h
matchLBINight_ :: Invariant f => Chain IN.Night Not f ~> (Not :+: Chain1 IN.Night f)
matchLBINight_ :: Chain Night Not f ~> (Not :+: Chain1 Night f)
matchLBINight_ = \case
Done x :: 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 xs :: 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
forall (f :: * -> *).
Invariant f =>
Night f (Chain Night Not f) ~> Chain1 Night f
unsplitNEINight_ Night f (Chain Night Not f) x
xs
instance Tensor Night Not where
type ListBy Night = Dec
intro1 :: f x -> Night f Not x
intro1 = f x -> Night f Not x
forall (f :: * -> *). f ~> Night f Not
N.intro2
intro2 :: g x -> Night Not g x
intro2 = g x -> Night Not g x
forall (g :: * -> *). g ~> Night Not g
N.intro1
elim1 :: Night f Not ~> f
elim1 = Night f Not x -> f x
forall (f :: * -> *). Contravariant f => Night f Not ~> f
N.elim2
elim2 :: Night Not g ~> g
elim2 = Night Not g x -> g x
forall (g :: * -> *). Contravariant g => Night Not g ~> g
N.elim1
appendLB :: Night (ListBy Night f) (ListBy Night f) x -> ListBy Night f x
appendLB (Night x :: ListBy Night f b
x y :: ListBy Night f c
y z :: x -> Either b c
z) = (x -> Either b c) -> Dec f b -> Dec f c -> Dec f x
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either b c
z Dec f b
ListBy Night f b
x Dec f c
ListBy Night f c
y
splitNE :: NonEmptyBy Night f x -> Night f (ListBy Night f) x
splitNE (Dec1 f x xs) = f b -> Dec f c -> (x -> Either b c) -> Night f (Dec f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f b
x Dec f c
xs x -> Either b c
f
splittingLB :: p ((:+:) Not (Night f (ListBy Night f)) a)
((:+:) Not (Night f (ListBy Night f)) a)
-> p (ListBy Night f a) (ListBy Night f a)
splittingLB = (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 ~> (Not :+: Night f (Dec f))
forall (a :: * -> *) p. Dec a p -> (:+:) Not (Night a (Dec a)) p
to_ (Not :+: Night f (Dec f)) ~> Dec f
forall (f :: * -> *) p. (:+:) Not (Night f (Dec f)) p -> Dec f p
from_
where
to_ :: Dec a p -> (:+:) Not (Night a (Dec a)) p
to_ = \case
Lose f :: 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 f :: p -> Either b c
f x :: a b
x xs :: 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 b -> Dec a c -> (p -> Either b c) -> Night a (Dec a) p
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night a b
x Dec a c
xs p -> Either b c
f)
from_ :: (:+:) Not (Night f (Dec f)) p -> Dec f p
from_ = \case
L1 (Not f :: p -> Void
f) -> (p -> Void) -> Dec f p
forall a (f :: * -> *). (a -> Void) -> Dec f a
Lose p -> Void
f
R1 (Night x :: f b
x xs :: Dec f c
xs f :: p -> Either b c
f) -> (p -> Either b c) -> f b -> Dec f c -> Dec f p
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec f a
Choose p -> Either b c
f f b
x Dec f c
xs
toListBy :: Night f f x -> ListBy Night f x
toListBy (Night x :: f b
x y :: f c
y z :: x -> Either b c
z) = (x -> Either b c) -> f b -> Dec f c -> Dec f x
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec f a
Choose x -> Either b c
z f b
x (f c -> Dec f c
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject f c
y)
instance Conclude f => MonoidIn Night Not f where
pureT :: Not x -> f x
pureT (Not x :: x -> Void
x) = (x -> Void) -> f x
forall (f :: * -> *) a. Conclude f => (a -> Void) -> f a
conclude x -> Void
x
instance Tensor (:+:) V1 where
type ListBy (:+:) = Step
intro1 :: f x -> (:+:) f V1 x
intro1 = f x -> (:+:) f V1 x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1
intro2 :: g x -> (:+:) V1 g x
intro2 = g x -> (:+:) V1 g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
elim1 :: (f :+: V1) ~> f
elim1 = \case
L1 x :: f x
x -> f x
x
R1 y :: V1 x
y -> V1 x -> f x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
elim2 :: (V1 :+: g) ~> g
elim2 = \case
L1 x :: V1 x
x -> V1 x -> g x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
R1 y :: g x
y -> g x
y
appendLB :: (:+:) (ListBy (:+:) f) (ListBy (:+:) f) x -> ListBy (:+:) f x
appendLB = 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 -> *). (f :+: Step f) ~> Step f
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 :: NonEmptyBy (:+:) f x -> (:+:) f (ListBy (:+:) f) x
splitNE = NonEmptyBy (:+:) f x -> (:+:) f (ListBy (:+:) f) x
forall k (f :: k -> *). Step f ~> (f :+: Step f)
stepDown
splittingLB :: p ((:+:) V1 (f :+: ListBy (:+:) f) a)
((:+:) V1 (f :+: ListBy (:+:) f) a)
-> p (ListBy (:+:) f a) (ListBy (:+:) f a)
splittingLB = p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
-> p (Step f a) (Step f a)
forall k (f :: k -> *). Step f <~> (f :+: Step f)
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 -> *). f <~> (V1 :+: f)
sumLeftIdentity
toListBy :: (:+:) f f x -> ListBy (:+:) f x
toListBy = \case
L1 x :: f x
x -> Natural -> f x -> Step f x
forall k (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step 0 f x
x
R1 x :: f x
x -> Natural -> f x -> Step f x
forall k (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step 1 f x
x
instance MonoidIn (:+:) V1 f where
pureT :: V1 x -> f x
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 :: f x -> Sum f V1 x
intro1 = f x -> Sum f V1 x
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL
intro2 :: g x -> Sum V1 g x
intro2 = g x -> Sum V1 g x
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR
elim1 :: Sum f V1 ~> f
elim1 = \case
InL x :: f x
x -> f x
x
InR y :: V1 x
y -> V1 x -> f x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
elim2 :: Sum V1 g ~> g
elim2 = \case
InL x :: V1 x
x -> V1 x -> g x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
InR y :: g x
y -> g x
y
appendLB :: Sum (ListBy Sum f) (ListBy Sum f) x -> ListBy Sum f x
appendLB = 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 -> *). (f :+: Step f) ~> Step f
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 :: NonEmptyBy Sum f x -> Sum f (ListBy Sum f) x
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 forall k (f :: k -> *) (g :: k -> *). (f :+: g) <~> Sum f g
(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 -> *). Step f ~> (f :+: Step f)
stepDown
splittingLB :: p ((:+:) V1 (Sum f (ListBy Sum f)) a)
((:+:) V1 (Sum f (ListBy Sum f)) a)
-> p (ListBy Sum f a) (ListBy Sum f a)
splittingLB = p ((:+:) f (Step f) a) ((:+:) f (Step f) a)
-> p (Step f a) (Step f a)
forall k (f :: k -> *). Step f <~> (f :+: Step f)
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 -> *). f <~> (V1 :+: f)
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 forall a. a -> a
V1 <~> V1
id forall k (f :: k -> *) (g :: k -> *). (f :+: g) <~> Sum f g
(f :+: Step f) <~> Sum f (Step f)
sumSum
toListBy :: Sum f f x -> ListBy Sum f x
toListBy = \case
InL x :: f x
x -> Natural -> f x -> Step f x
forall k (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step 0 f x
x
InR x :: f x
x -> Natural -> f x -> Step f x
forall k (f :: k -> *) (a :: k). Natural -> f a -> Step f a
Step 1 f x
x
instance MonoidIn Sum V1 f where
pureT :: V1 x -> f x
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 :: f x -> These1 f V1 x
intro1 = f x -> These1 f V1 x
forall (f :: * -> *) (g :: * -> *) a. f a -> These1 f g a
This1
intro2 :: g x -> These1 V1 g x
intro2 = g x -> These1 V1 g x
forall (f :: * -> *) (g :: * -> *) a. g a -> These1 f g a
That1
elim1 :: These1 f V1 ~> f
elim1 = \case
This1 x :: f x
x -> f x
x
That1 y :: V1 x
y -> V1 x -> f x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
These1 _ y :: V1 x
y -> V1 x -> f x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
y
elim2 :: These1 V1 g ~> g
elim2 = \case
This1 x :: V1 x
x -> V1 x -> g x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
That1 y :: g x
y -> g x
y
These1 x :: V1 x
x _ -> V1 x -> g x
forall k (a :: k) (f :: k -> *). V1 a -> f a
absurd1 V1 x
x
appendLB :: These1 (ListBy These1 f) (ListBy These1 f) x -> ListBy These1 f x
appendLB = \case
This1 x :: ListBy These1 f x
x -> ListBy These1 f x
x
That1 y :: ListBy These1 f x
y -> These1 f (Steps f) x -> Steps f x
forall (f :: * -> *). These1 f (Steps f) ~> Steps f
stepsUp (These1 f (Steps f) x -> Steps f x)
-> (Steps f x -> These1 f (Steps f) x) -> Steps f x -> Steps f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Steps f x -> These1 f (Steps f) x
forall (f :: * -> *) (g :: * -> *) a. g a -> These1 f g a
That1 (Steps f x -> ListBy These1 f x) -> Steps f x -> ListBy These1 f x
forall a b. (a -> b) -> a -> b
$ Steps f x
ListBy These1 f x
y
These1 x :: ListBy These1 f x
x y :: 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 :: NonEmptyBy These1 f x -> These1 f (ListBy These1 f) x
splitNE = Steps f x -> These1 f (Steps f) x
forall (f :: * -> *). Steps f ~> These1 f (Steps f)
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 :: p ((:+:) V1 (These1 f (ListBy These1 f)) a)
((:+:) V1 (These1 f (ListBy These1 f)) a)
-> p (ListBy These1 f a) (ListBy These1 f a)
splittingLB = p (These1 f (Steps f) a) (These1 f (Steps f) a)
-> p (Steps f a) (Steps f a)
forall (f :: * -> *). Steps f <~> These1 f (Steps f)
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 -> *). f <~> (V1 :+: f)
sumLeftIdentity
toListBy :: These1 f f x -> ListBy These1 f x
toListBy = \case
This1 x :: f x
x -> NEMap Natural (f x) -> ListBy These1 f x
forall k (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps (NEMap Natural (f x) -> ListBy These1 f x)
-> NEMap Natural (f x) -> ListBy These1 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 0 f x
x
That1 y :: f x
y -> NEMap Natural (f x) -> ListBy These1 f x
forall k (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps (NEMap Natural (f x) -> ListBy These1 f x)
-> NEMap Natural (f x) -> ListBy These1 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 1 f x
y
These1 x :: f x
x y :: f x
y -> NEMap Natural (f x) -> ListBy These1 f x
forall k (f :: k -> *) (a :: k). NEMap Natural (f a) -> Steps f a
Steps (NEMap Natural (f x) -> ListBy These1 f x)
-> NEMap Natural (f x) -> ListBy These1 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 ((0, f x
x) (Natural, f x) -> [(Natural, f x)] -> NonEmpty (Natural, f x)
forall a. a -> [a] -> NonEmpty a
:| [(1, f x
y)])
instance Alt f => MonoidIn These1 V1 f where
pureT :: V1 x -> f x
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 :: f x -> Comp f Identity x
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 :: g x -> Comp Identity g x
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 :: Comp f Identity ~> f
elim1 (x :: f x
x :>>= y :: 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 :: Comp Identity g ~> g
elim2 (x :: Identity x
x :>>= y :: x -> g x
y) = x -> g x
y (Identity x -> x
forall a. Identity a -> a
runIdentity Identity x
x)
appendLB :: Comp (ListBy Comp f) (ListBy Comp f) x -> ListBy Comp f x
appendLB (x :: ListBy Comp f x
x :>>= y :: 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> Free f x
x -> ListBy Comp f x
y
splitNE :: NonEmptyBy Comp f x -> Comp f (ListBy Comp f) x
splitNE = NonEmptyBy Comp f x -> Comp f (ListBy Comp f) x
forall (f :: * -> *). Free1 f ~> Comp f (Free f)
free1Comp
splittingLB :: p ((:+:) Identity (Comp f (ListBy Comp f)) a)
((:+:) Identity (Comp f (ListBy Comp f)) a)
-> p (ListBy Comp f a) (ListBy Comp f a)
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 ~> (Identity :+: Comp f (Free f))
forall (f :: * -> *). Free f ~> (Identity :+: Comp f (Free f))
to_ (Identity :+: Comp f (Free f)) ~> Free f
forall (f :: * -> *). (Identity :+: Comp f (Free f)) ~> Free f
from_
where
to_ :: Free f ~> Identity :+: Comp f (Free f)
to_ :: 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
$ \y :: f s
y n :: 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 :: * -> *). (Identity :+: Comp f (Free f)) ~> Free f
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_ :: (:+:) Identity (Comp f (Free f)) x -> Free f x
from_ = forall x. Identity x -> Free f x
forall (f :: * -> *). Applicative f => Identity ~> f
generalize
(forall x. Identity x -> Free f x)
-> (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 x :>>= f -> f x -> Free f x
forall (f :: * -> *). f ~> Free f
liftFree f x
x Free f x -> (x -> Free f x) -> Free f x
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= x -> Free f x
f)
toListBy :: Comp f f x -> ListBy Comp f x
toListBy (x :: f x
x :>>= y :: x -> f x
y) = f x -> Free f x
forall (f :: * -> *). f ~> Free f
liftFree f x
x Free f x -> (x -> Free f x) -> Free f x
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
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 x -> f x
pureT = Identity x -> f x
forall (f :: * -> *). Applicative f => Identity ~> f
generalize
instance Matchable (:*:) Proxy where
unsplitNE :: (f :*: ListBy (:*:) f) ~> NonEmptyBy (:*:) f
unsplitNE = (:*:) f (ListBy (:*:) f) x -> NonEmptyBy (:*:) f x
forall k (f :: k -> *) (a :: k).
(:*:) f (ListF f) a -> NonEmptyF f a
ProdNonEmpty
matchLB :: ListBy (:*:) f ~> (Proxy :+: NonEmptyBy (:*:) f)
matchLB = ListBy (:*:) f x -> (:+:) Proxy (NonEmptyBy (:*:) f) x
forall k (f :: k -> *). ListF f ~> (Proxy :+: NonEmptyF f)
fromListF
instance Matchable Product Proxy where
unsplitNE :: 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 forall k (f :: k -> *) (g :: k -> *). (f :*: g) <~> Product f g
(f :*: ListF f) <~> Product f (ListF f)
prodProd
matchLB :: ListBy Product f ~> (Proxy :+: NonEmptyBy Product f)
matchLB = ListBy Product f x -> (:+:) Proxy (NonEmptyBy Product f) x
forall k (f :: k -> *). ListF f ~> (Proxy :+: NonEmptyF f)
fromListF
instance Matchable Day Identity where
unsplitNE :: Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE = Day f (ListBy Day f) x -> NonEmptyBy Day f x
forall (f :: * -> *) a. Day f (Ap f) a -> Ap1 f a
DayAp1
matchLB :: ListBy Day f ~> (Identity :+: NonEmptyBy Day f)
matchLB = ListBy Day f x -> (:+:) Identity (NonEmptyBy Day f) x
forall (f :: * -> *). Ap f ~> (Identity :+: Ap1 f)
fromAp
instance Matchable CD.Day Proxy where
unsplitNE :: Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE (CD.Day x :: f b
x (Div xs) f :: x -> (b, c)
f) = 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)
-> ((:*:) (Coyoneda f) (ListF (Coyoneda f)) x
-> NonEmpty (Coyoneda f x))
-> (:*:) (Coyoneda f) (ListF (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 (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
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 (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> 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 :: 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
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 (i :: * -> *) (f :: * -> *).
(Matchable (:*:) i, FunctorBy (:*:) f) =>
ListBy (:*:) f ~> (i :+: NonEmptyBy (:*:) f)
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 :: Night f (ListBy Night f) ~> NonEmptyBy Night f
unsplitNE (Night x :: f b
x xs :: ListBy Night f c
xs f :: x -> Either b c
f) = (x -> Either b c) -> f b -> Dec f c -> Dec1 f x
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec1 f a
Dec1 x -> Either b c
f f b
x Dec f c
ListBy Night f c
xs
matchLB :: ListBy Night f ~> (Not :+: NonEmptyBy Night f)
matchLB = \case
Lose 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 f x xs -> Dec1 f x -> (:+:) Not (Dec1 f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 ((x -> Either b c) -> f b -> Dec f c -> Dec1 f x
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec1 f a
Dec1 x -> Either b c
f f b
x Dec f c
xs)
instance Matchable (:+:) V1 where
unsplitNE :: (f :+: ListBy (:+:) f) ~> NonEmptyBy (:+:) f
unsplitNE = (:+:) f (ListBy (:+:) f) x -> NonEmptyBy (:+:) f x
forall k (f :: k -> *). (f :+: Step f) ~> Step f
stepUp
matchLB :: ListBy (:+:) f ~> (V1 :+: NonEmptyBy (:+:) f)
matchLB = 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 :: Sum f (ListBy Sum f) ~> NonEmptyBy Sum f
unsplitNE = (:+:) f (Step f) x -> Step f x
forall k (f :: k -> *). (f :+: Step f) ~> Step f
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 forall k (f :: k -> *) (g :: k -> *). (f :+: g) <~> Sum f g
(f :+: Step f) <~> Sum f (Step f)
sumSum
matchLB :: ListBy Sum f ~> (V1 :+: NonEmptyBy Sum f)
matchLB = 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 { 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
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)
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]
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
(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
/= :: 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, 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
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
$cp1Ord :: forall k (f :: k -> *) (a :: k). Ord (f a) => Eq (WrapF f a)
Ord, a -> WrapF f b -> WrapF f a
(a -> b) -> WrapF f a -> WrapF f b
(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
<$ :: a -> WrapF f b -> WrapF f a
$c<$ :: forall (f :: * -> *) a b. Functor f => a -> WrapF f b -> WrapF f a
fmap :: (a -> b) -> WrapF f a -> WrapF f b
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> WrapF f a -> WrapF f b
Functor, a -> WrapF f a -> Bool
WrapF f m -> m
WrapF f a -> [a]
WrapF f a -> Bool
WrapF f a -> Int
WrapF f a -> a
WrapF f a -> a
WrapF f a -> a
WrapF f a -> a
(a -> m) -> WrapF f a -> m
(a -> m) -> WrapF f a -> m
(a -> b -> b) -> b -> WrapF f a -> b
(a -> b -> b) -> b -> WrapF f a -> b
(b -> a -> b) -> b -> WrapF f a -> b
(b -> a -> b) -> b -> WrapF f a -> b
(a -> a -> a) -> WrapF f a -> a
(a -> a -> a) -> WrapF f a -> a
(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
product :: WrapF f a -> a
$cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => WrapF f a -> a
sum :: WrapF f a -> a
$csum :: forall (f :: * -> *) a. (Foldable f, Num a) => WrapF f a -> a
minimum :: WrapF f a -> a
$cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => WrapF f a -> a
maximum :: WrapF f a -> a
$cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => WrapF f a -> a
elem :: a -> WrapF f a -> Bool
$celem :: forall (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> WrapF f a -> Bool
length :: WrapF f a -> Int
$clength :: forall (f :: * -> *) a. Foldable f => WrapF f a -> Int
null :: WrapF f a -> Bool
$cnull :: forall (f :: * -> *) a. Foldable f => WrapF f a -> Bool
toList :: WrapF f a -> [a]
$ctoList :: forall (f :: * -> *) a. Foldable f => WrapF f a -> [a]
foldl1 :: (a -> a -> a) -> WrapF f a -> a
$cfoldl1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> WrapF f a -> a
foldr1 :: (a -> a -> a) -> WrapF f a -> a
$cfoldr1 :: forall (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> WrapF f a -> a
foldl' :: (b -> a -> b) -> b -> WrapF f a -> b
$cfoldl' :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> WrapF f a -> b
foldl :: (b -> a -> b) -> b -> WrapF f a -> b
$cfoldl :: forall (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> WrapF f a -> b
foldr' :: (a -> b -> b) -> b -> WrapF f a -> b
$cfoldr' :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> WrapF f a -> b
foldr :: (a -> b -> b) -> b -> WrapF f a -> b
$cfoldr :: forall (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> WrapF f a -> b
foldMap' :: (a -> m) -> WrapF f a -> m
$cfoldMap' :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> WrapF f a -> m
foldMap :: (a -> m) -> WrapF f a -> m
$cfoldMap :: forall (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> WrapF f a -> m
fold :: WrapF f m -> m
$cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => WrapF f m -> m
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)
(a -> f b) -> WrapF f a -> f (WrapF f b)
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)
sequence :: 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 :: (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 :: 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 :: (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)
$cp2Traversable :: forall (f :: * -> *). Traversable f => Foldable (WrapF f)
$cp1Traversable :: forall (f :: * -> *). Traversable f => Functor (WrapF f)
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
$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, Typeable (WrapF f a)
DataType
Constr
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 -> DataType
WrapF f a -> Constr
(forall b. Data b => b -> b) -> WrapF f a -> WrapF 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 b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (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 -> 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 (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))
$cWrapF :: Constr
$tWrapF :: DataType
gmapMo :: (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 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 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 :: 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 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 :: (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 :: (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 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 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 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 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)
$cp1Data :: forall k (f :: k -> *) (a :: k).
(Typeable a, Typeable f, Typeable k, Data (f a)) =>
Typeable (WrapF f a)
Data)
instance Show1 f => Show1 (WrapF f) where
liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> WrapF f a -> ShowS
liftShowsPrec sp :: Int -> a -> ShowS
sp sl :: [a] -> ShowS
sl d :: Int
d (WrapF x :: 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 (f :: * -> *) a.
Show1 f =>
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
sl) "WrapF" Int
d f a
x
instance Eq1 f => Eq1 (WrapF f) where
liftEq :: (a -> b -> Bool) -> WrapF f a -> WrapF f b -> Bool
liftEq eq :: a -> b -> Bool
eq (WrapF x :: f a
x) (WrapF y :: f b
y) = (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 :: (a -> b -> Ordering) -> WrapF f a -> WrapF f b -> Ordering
liftCompare c :: a -> b -> Ordering
c (WrapF x :: f a
x) (WrapF y :: f b
y) = (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 :: f x -> WrapHBF t f (WrapF i) x
intro1 = t f (WrapF i) x -> WrapHBF t f (WrapF i) x
forall k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
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
hright 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 (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
f ~> t f i
intro1
intro2 :: g x -> WrapHBF t (WrapF i) g x
intro2 = t (WrapF i) g x -> WrapHBF t (WrapF i) g x
forall k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
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
hleft 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 (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(g :: * -> *).
Tensor t i =>
g ~> t i g
intro2
elim1 :: WrapHBF t f (WrapF i) ~> f
elim1 = t f i x -> f x
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
hright 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 k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
WrapHBF t f g a -> t f g a
unwrapHBF
elim2 :: WrapHBF t (WrapF i) g ~> g
elim2 = t i g x -> g x
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
hleft 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 k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
WrapHBF t f g a -> t f g a
unwrapHBF
appendLB :: WrapHBF t (ListBy (WrapHBF t) f) (ListBy (WrapHBF t) f) x
-> ListBy (WrapHBF t) f x
appendLB = t (ListBy t f) (ListBy t f) x -> ListBy t f x
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 k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
WrapHBF t f g a -> t f g a
unwrapHBF
splitNE :: NonEmptyBy (WrapHBF t) f x -> WrapHBF t f (ListBy (WrapHBF t) f) x
splitNE = t f (ListBy t f) x -> WrapHBF t f (ListBy t f) x
forall k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
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 (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> t f (ListBy t f)
splitNE
splittingLB :: p ((:+:) (WrapF i) (WrapHBF t f (ListBy (WrapHBF t) f)) a)
((:+:) (WrapF i) (WrapHBF t f (ListBy (WrapHBF t) f)) a)
-> p (ListBy (WrapHBF t) f a) (ListBy (WrapHBF t) f a)
splittingLB = forall (i :: * -> *) (f :: * -> *).
Tensor t i =>
ListBy t f <~> (i :+: t f (ListBy t f))
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 ~> WrapF i
forall k (f :: k -> *) (a :: k). f a -> WrapF f a
WrapF 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) ~> WrapHBF t f (ListBy t f)
forall k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
t f g a -> WrapHBF t f g a
WrapHBF WrapHBF t f (ListBy t f) ~> t f (ListBy t f)
forall k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
WrapHBF t f g a -> t f g a
unwrapHBF)
toListBy :: WrapHBF t f f x -> ListBy (WrapHBF t) f x
toListBy = t f f x -> ListBy t f x
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 k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
WrapHBF t f g a -> t f g a
unwrapHBF
fromNE :: NonEmptyBy (WrapHBF t) f x -> ListBy (WrapHBF t) f x
fromNE = forall (i :: * -> *) (f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
NonEmptyBy t f ~> ListBy t f
fromNE @t
newtype WrapLB t f a = WrapLB { WrapLB t f a -> ListBy t f a
unwrapLB :: ListBy t f a }
instance Functor (ListBy t f) => Functor (WrapLB t f) where
fmap :: (a -> b) -> WrapLB t f a -> WrapLB t f b
fmap f :: a -> b
f (WrapLB x :: 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 (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 :: (a -> b) -> WrapLB t f b -> WrapLB t f a
contramap f :: a -> b
f (WrapLB x :: ListBy t f b
x) = ListBy t f a -> WrapLB t f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
ListBy t f a -> WrapLB t f a
WrapLB ((a -> b) -> ListBy t f b -> ListBy t f a
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap a -> b
f ListBy t f b
x)
instance Invariant (ListBy t f) => Invariant (WrapLB t f) where
invmap :: (a -> b) -> (b -> a) -> WrapLB t f a -> WrapLB t f b
invmap f :: a -> b
f g :: b -> a
g (WrapLB x :: 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 (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) x -> WrapLB t f x
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 (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
hbimap WrapLB t f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *) a.
WrapLB t f a -> ListBy t f a
unwrapLB 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 k k k (t :: k -> k -> k -> *) (f :: k) (g :: k) (a :: k).
WrapHBF t f g a -> t f g a
unwrapHBF
binterpret :: (g ~> WrapLB t f)
-> (h ~> WrapLB t f) -> WrapHBF t g h ~> WrapLB t f
binterpret f :: g ~> WrapLB t f
f g :: h ~> WrapLB t f
g = WrapHBF t (WrapLB t f) (WrapLB t f) x -> WrapLB t f x
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
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 x -> WrapLB t f x
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 (i :: * -> *) (f :: * -> *). Tensor t i => i ~> ListBy t f
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