module Data.HBifunctor.Tensor.Internal (
Tensor(..)
, unconsLB
, nilLB
, consLB
, appendChain
, unroll
, reroll
, rerollNE
, splitChain1
) where
import Control.Natural
import Control.Natural.IsoF
import Data.HBifunctor
import Data.HBifunctor.Associative
import Data.HFunctor
import Data.HFunctor.Chain.Internal
import Data.Kind
import GHC.Generics
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 #-}
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
appendChain
:: forall t i f. Tensor t i
=> t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain :: t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain = ListBy t f x -> Chain t i f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
ListBy t f ~> Chain t i f
unroll
(ListBy t f x -> Chain t i f x)
-> (t (Chain t i f) (Chain t i f) x -> ListBy t f x)
-> t (Chain t i f) (Chain t i f) x
-> Chain t i 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)
-> (t (Chain t i f) (Chain t i f) x
-> t (ListBy t f) (ListBy t f) x)
-> t (Chain t i f) (Chain t i f) x
-> ListBy t f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Chain t i f ~> ListBy t f)
-> (Chain t i f ~> ListBy t f)
-> t (Chain t i f) (Chain t i 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 Chain t i f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
Chain t i f ~> ListBy t f
reroll Chain t i f ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
Chain t i f ~> ListBy t f
reroll
unroll
:: Tensor t i
=> ListBy t f ~> Chain t i f
unroll :: ListBy t f ~> Chain t i f
unroll = (ListBy t f ~> (i :+: t f (ListBy t f)))
-> ListBy t f ~> Chain t i f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *)
(g :: * -> *) (i :: * -> *).
HBifunctor t =>
(g ~> (i :+: t f g)) -> g ~> Chain t i f
unfoldChain 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
reroll
:: forall t i f. Tensor t i
=> Chain t i f ~> ListBy t f
reroll :: Chain t i f ~> ListBy t f
reroll = (i ~> ListBy t f)
-> (t f (ListBy t f) ~> ListBy t f) -> Chain t i f ~> ListBy t f
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
(f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain (forall (i :: * -> *) (f :: * -> *). Tensor t i => i ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
i ~> ListBy t f
nilLB @t) t f (ListBy t f) ~> ListBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t f (ListBy t f) ~> ListBy t f
consLB
rerollNE :: Associative t => Chain1 t f ~> NonEmptyBy t f
rerollNE :: Chain1 t f ~> NonEmptyBy t f
rerollNE = (f ~> NonEmptyBy t f)
-> (t f (NonEmptyBy t f) ~> NonEmptyBy t f)
-> Chain1 t f ~> NonEmptyBy t f
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> NonEmptyBy t f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject t f (NonEmptyBy t f) ~> NonEmptyBy t f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
Associative t =>
t f (NonEmptyBy t f) ~> NonEmptyBy t f
consNE
splitChain1
:: forall t i f. Tensor t i
=> Chain1 t f ~> t f (Chain t i f)
splitChain1 :: Chain1 t f ~> t f (Chain t i f)
splitChain1 = (ListBy t f ~> Chain t i f)
-> t f (ListBy t f) ~> t f (Chain t i 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 :: * -> *).
Tensor t i =>
ListBy t f ~> Chain t i f
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
ListBy t f ~> Chain t i f
unroll @t) (t f (ListBy t f) x -> t f (Chain t i f) x)
-> (Chain1 t f x -> t f (ListBy t f) x)
-> Chain1 t f x
-> t f (Chain t i 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 (NonEmptyBy t f x -> t f (ListBy t f) x)
-> (Chain1 t f x -> NonEmptyBy t f x)
-> Chain1 t f x
-> t f (ListBy t f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Chain1 t f x -> NonEmptyBy t f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
Associative t =>
Chain1 t f ~> NonEmptyBy t f
rerollNE