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.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.HFunctor
import Data.HFunctor.Internal
import Data.HFunctor.Interpret
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import GHC.Generics
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.Map.NonEmpty as NEM
class (Associative t, Inject (ListBy t)) => Tensor t i | t -> i where
type ListBy t :: (Type -> Type) -> Type -> Type
intro1 :: f ~> t f i
intro2 :: g ~> t i g
elim1 :: FunctorBy t f => t f i ~> f
elim2 :: FunctorBy t g => t i g ~> g
appendLB :: t (ListBy t f) (ListBy t f) ~> ListBy t f
splitNE :: NonEmptyBy t f ~> t f (ListBy t f)
splittingLB :: ListBy t f <~> i :+: t f (ListBy t f)
toListBy :: t f f ~> ListBy t f
toListBy = (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)
-> (t f f x -> (:+:) i (t f (ListBy t f)) x)
-> t f f x
-> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t f (ListBy t f) x -> (:+:) i (t f (ListBy t f)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
(t f (ListBy t f) x -> (:+:) i (t f (ListBy t f)) x)
-> (t f f x -> t f (ListBy t f) x)
-> t f f x
-> (:+:) i (t f (ListBy t f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f ~> ListBy t f) -> t f f ~> t f (ListBy t 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 (f :: * -> *). Inject (ListBy t) => f ~> ListBy t f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject @(ListBy t))
fromNE :: NonEmptyBy t f ~> ListBy t f
fromNE = (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)
-> (NonEmptyBy t f x -> (:+:) i (t f (ListBy t f)) x)
-> NonEmptyBy t f x
-> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t f (ListBy t f) x -> (:+:) i (t f (ListBy t f)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (t f (ListBy t f) x -> (:+:) i (t f (ListBy t f)) x)
-> (NonEmptyBy t f x -> t f (ListBy t f) x)
-> NonEmptyBy t f x
-> (:+:) i (t f (ListBy t f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (i :: * -> *) (f :: * -> *).
Tensor t i =>
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
{-# MINIMAL intro1, intro2, elim1, elim2, appendLB, splitNE, splittingLB #-}
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
nilLB :: forall t i f. Tensor t i => i ~> ListBy t f
nilLB :: i ~> ListBy t f
nilLB = (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
consLB :: Tensor t i => t f (ListBy t f) ~> ListBy t f
consLB :: t f (ListBy t f) ~> ListBy t f
consLB = (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 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 ((:+:) i (t f (ListBy t f)) x -> ListBy t f x)
-> (t f (ListBy t f) x -> (:+:) i (t f (ListBy t f)) x)
-> t f (ListBy t f) x
-> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t f (ListBy t f) x -> (:+:) i (t f (ListBy t f)) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1
unconsLB :: Tensor t i => ListBy t f ~> i :+: t f (ListBy t f)
unconsLB :: ListBy t f ~> (i :+: t f (ListBy t f))
unconsLB = (ListBy t f <~> (i :+: t f (ListBy t f)))
-> ListBy t f ~> (i :+: t f (ListBy t f))
forall k (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF 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
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 (Div1 f x xs) = f b -> Div f c -> (x -> (b, c)) -> Day f (Div f) x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x Div f c
xs x -> (b, c)
f
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 ~> (Proxy :+: Day f (Div f)))
-> ((Proxy :+: Day f (Div f)) ~> Div f)
-> Div f <~> (Proxy :+: Day f (Div f))
forall k (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF Div f ~> (Proxy :+: Day f (Div f))
forall (a :: * -> *) p. Div a p -> (:+:) Proxy (Day a (Div a)) p
to_ (Proxy :+: Day f (Div f)) ~> Div f
forall (f :: * -> *) a. (:+:) Proxy (Day f (Div f)) a -> Div f a
from_
where
to_ :: Div a p -> (:+:) Proxy (Day a (Div a)) p
to_ = \case
Conquer -> Proxy p -> (:+:) Proxy (Day a (Div a)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Proxy p
forall k (t :: k). Proxy t
Proxy
Divide f :: p -> (b, c)
f x :: a b
x xs :: Div a c
xs -> Day a (Div a) p -> (:+:) Proxy (Day a (Div a)) p
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (a b -> Div a c -> (p -> (b, c)) -> Day a (Div a) p
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day a b
x Div a c
xs p -> (b, c)
f)
from_ :: (:+:) Proxy (Day f (Div f)) a -> Div f a
from_ = \case
L1 Proxy -> Div f a
forall (f :: * -> *) a. Div f a
Conquer
R1 (CD.Day x :: f b
x xs :: Div f c
xs f :: a -> (b, c)
f) -> (a -> (b, c)) -> f b -> Div f c -> Div f a
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide a -> (b, c)
f f b
x Div f c
xs
toListBy :: Day f f x -> ListBy Day f x
toListBy (CD.Day x :: f b
x y :: f c
y z :: x -> (b, c)
z) = (x -> (b, c)) -> f b -> Div f c -> Div f x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide x -> (b, c)
z f b
x (f c -> Div f c
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject 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 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 xs :: ListBy Day f c
xs f :: x -> (b, c)
f) = (x -> (b, c)) -> f b -> Div f c -> Div1 f x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div1 f a
Div1 x -> (b, c)
f f b
x Div f c
ListBy Day f c
xs
matchLB :: ListBy Day f ~> (Proxy :+: NonEmptyBy Day f)
matchLB = \case
Conquer -> Proxy x -> (:+:) Proxy (Div1 f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Proxy x
forall k (t :: k). Proxy t
Proxy
Divide f x xs -> Div1 f x -> (:+:) Proxy (Div1 f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 ((x -> (b, c)) -> f b -> Div f c -> Div1 f x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div1 f a
Div1 x -> (b, c)
f f b
x Div f c
xs)
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