{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure (module Exports) where
import Pandora.Paradigm.Structure.Ability as Exports
import Pandora.Paradigm.Structure.Interface as Exports
import Pandora.Paradigm.Structure.Modification as Exports
import Pandora.Paradigm.Structure.Some as Exports
import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((#), identity)
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=), (!))
import Pandora.Paradigm.Inventory.Optics ()
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), attached, twosome)
import Pandora.Paradigm.Primary.Algebraic.Sum ((:+:) (Option, Adoption))
import Pandora.Paradigm.Primary.Algebraic.Exponential (type (-->), (%))
import Pandora.Paradigm.Primary.Algebraic (extract)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Both, Left, Right, End))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Schemes.TU (type (<:.>))
import Pandora.Paradigm.Schemes.T_U ( type (<:.:>))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
instance Monotonic s a => Monotonic s (s :*: a) where
reduce :: (s -> r -> r) -> r -> (s :*: a) -> r
reduce s -> r -> r
f r
r s :*: a
x = (s -> r -> r) -> r -> a -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce s -> r -> r
f (r -> a -> r) -> r -> a -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# s -> r -> r
f ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x) r
r (a -> r) -> a -> r
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (s :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract s :*: a
x
instance Nullable Maybe where
null :: (Predicate :. Maybe) := a
null = (Maybe a -> Boolean) -> (Predicate :. Maybe) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Maybe a -> Boolean) -> (Predicate :. Maybe) := a)
-> (Maybe a -> Boolean) -> (Predicate :. Maybe) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case { Just a
_ -> Boolean
True ; Maybe a
_ -> Boolean
False }
instance (Covariant (->) (->) t) => Substructure Tail (Tap t) where
type Available Tail (Tap t) = Identity
type Substance Tail (Tap t) = t
substructure :: Lens
(Available 'Tail (Tap t))
((<:.>) (Tagged 'Tail) (Tap t) a)
(Substance 'Tail (Tap t) a)
substructure = ((<:.>) (Tagged 'Tail) (Tap t) a
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> P_Q_T
(->) Store Identity ((<:.>) (Tagged 'Tail) (Tap t) a) (t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Tail) (Tap t) a
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> P_Q_T
(->) Store Identity ((<:.>) (Tagged 'Tail) (Tap t) a) (t a))
-> ((<:.>) (Tagged 'Tail) (Tap t) a
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> P_Q_T
(->) Store Identity ((<:.>) (Tagged 'Tail) (Tap t) a) (t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Tail) (Tap t) a
tap -> case Tagged 'Tail (Tap t a) -> Tap t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Tagged 'Tail (Tap t a) -> Tap t a)
-> Tagged 'Tail (Tap t a) -> Tap t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Tail) (Tap t) a -> Tagged 'Tail (Tap t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (<:.>) (Tagged 'Tail) (Tap t) a
tap of
Tap a
x t a
xs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Tail) (Tap t) a)
-> Store (Identity (t a)) ((<:.>) (Tagged 'Tail) (Tap t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Identity (t a)
forall a. a -> Identity a
Identity t a
xs Identity (t a)
-> (Identity (t a) -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Tail) (Tap t) a
forall s a. s -> a -> s :*: a
:*: Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a)
-> (Identity (t a) -> Tap t a)
-> Identity (t a)
-> (<:.>) (Tagged 'Tail) (Tap t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> t a -> Tap t a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap a
x (t a -> Tap t a)
-> (Identity (t a) -> t a) -> Identity (t a) -> Tap t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance Morphable (Into (Preorder (Construction Maybe))) (Construction Wye) where
type Morphing (Into (Preorder (Construction Maybe))) (Construction Wye) = Construction Maybe
morphing :: (<::>)
(Tagged ('Into ('Preorder (Construction Maybe))))
(Construction Wye)
a
-> Morphing
('Into ('Preorder (Construction Maybe))) (Construction Wye) a
morphing (<::>)
(Tagged ('Into ('Preorder (Construction Maybe))))
(Construction Wye)
a
nonempty_binary = case (<::>)
(Tagged ('Into ('Preorder (Construction Maybe))))
(Construction Wye)
a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
(Tagged ('Into ('Preorder (Construction Maybe))))
(Construction Wye)
a
nonempty_binary of
Construct a
x Wye (Construction Wye a)
End -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
Construct a
x (Left Construction Wye a
lst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a
-> Morphing
('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
lst
Construct a
x (Right Construction Wye a
rst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a
-> Morphing
('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
rst
Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> Construction Maybe a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> Construction Maybe a)
-> Construction Maybe a -> Construction Maybe a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Construction Wye a
-> Morphing
('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing
('Into ('Preorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Preorder (Nonempty List)) Construction Wye a
rst
instance Morphable (Into (Inorder (Construction Maybe))) (Construction Wye) where
type Morphing (Into (Inorder (Construction Maybe))) (Construction Wye) = Construction Maybe
morphing :: (<::>)
(Tagged ('Into ('Inorder (Construction Maybe))))
(Construction Wye)
a
-> Morphing
('Into ('Inorder (Construction Maybe))) (Construction Wye) a
morphing (<::>)
(Tagged ('Into ('Inorder (Construction Maybe))))
(Construction Wye)
a
nonempty_binary = case (<::>)
(Tagged ('Into ('Inorder (Construction Maybe))))
(Construction Wye)
a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
(Tagged ('Into ('Inorder (Construction Maybe))))
(Construction Wye)
a
nonempty_binary of
Construct a
x Wye (Construction Wye a)
End -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
Construct a
x (Left Construction Wye a
lst) -> Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
Construct a
x (Right Construction Wye a
rst) -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
rst
Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Inorder (Nonempty List)) Construction Wye a
rst
instance Morphable (Into (Postorder (Construction Maybe))) (Construction Wye) where
type Morphing (Into (Postorder (Construction Maybe))) (Construction Wye) = Construction Maybe
morphing :: (<::>)
(Tagged ('Into ('Postorder (Construction Maybe))))
(Construction Wye)
a
-> Morphing
('Into ('Postorder (Construction Maybe))) (Construction Wye) a
morphing (<::>)
(Tagged ('Into ('Postorder (Construction Maybe))))
(Construction Wye)
a
nonempty_binary = case (<::>)
(Tagged ('Into ('Postorder (Construction Maybe))))
(Construction Wye)
a
-> Construction Wye a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
(Tagged ('Into ('Postorder (Construction Maybe))))
(Construction Wye)
a
nonempty_binary of
Construct a
x Wye (Construction Wye a)
End -> a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
Construct a
x (Left Construction Wye a
lst) -> Construction Wye a
-> Morphing
('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
Construct a
x (Right Construction Wye a
rst) -> Construction Wye a
-> Morphing
('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
rst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
Construct a
x (Both Construction Wye a
lst Construction Wye a
rst) -> Construction Wye a
-> Morphing
('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
lst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Wye a
-> Morphing
('Into ('Postorder (Nonempty List))) (Construction Wye) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
into @(Postorder (Nonempty List)) Construction Wye a
rst Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing
instance Morphable (Into (o ds)) (Construction Wye) => Morphable (Into (o ds)) Binary where
type Morphing (Into (o ds)) Binary = Maybe <:.> Morphing (Into (o ds)) (Construction Wye)
morphing :: (<::>) (Tagged ('Into (o ds))) Binary a
-> Morphing ('Into (o ds)) Binary a
morphing ((<::>) (Tagged ('Into (o ds))) Binary a -> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
xs) = (forall a (mod :: a) (struct :: * -> *).
Morphable ('Into mod) struct =>
struct ~> Morphing ('Into mod) struct
forall (struct :: * -> *).
Morphable ('Into (o ds)) struct =>
struct ~> Morphing ('Into (o ds)) struct
into @(o ds) (Construction Wye a
-> Morphing ('Into (o ds)) (Construction Wye) a)
-> Maybe (Construction Wye a)
-> Maybe (Morphing ('Into (o ds)) (Construction Wye) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary Binary a
-> Primary
(TU
Covariant
Covariant
Maybe
(Morphing ('Into (o ds)) (Construction Wye)))
a)
-> Binary a
-> TU
Covariant
Covariant
Maybe
(Morphing ('Into (o ds)) (Construction Wye))
a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
m (Primary t a) (Primary u b) -> m (t a) (u b)
||= Binary a
xs
instance Substructure Left (Flip (:*:) a) where
type Available Left (Flip (:*:) a) = Identity
type Substance Left (Flip (:*:) a) = Identity
substructure :: Lens
(Available 'Left (Flip (:*:) a))
((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
(Substance 'Left (Flip (:*:) a) a)
substructure = ((<:.>) (Tagged 'Left) (Flip (:*:) a) a
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
(Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) (Flip (:*:) a) a
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
(Identity a))
-> ((<:.>) (Tagged 'Left) (Flip (:*:) a) a
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
(Identity a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) (Flip (:*:) a) a
product -> case Flip (:*:) a a -> a :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Flip (:*:) a a -> a :*: a) -> Flip (:*:) a a -> a :*: a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) (Flip (:*:) a) a -> Flip (:*:) a a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) (Flip (:*:) a) a
product of
a
s :*: a
x -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Left) (Flip (:*:) a) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity a
s) Identity (Identity a)
-> (Identity (Identity a)
-> (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall s a. s -> a -> s :*: a
:*: Flip (:*:) a a -> (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Flip (:*:) a a -> (<:.>) (Tagged 'Left) (Flip (:*:) a) a)
-> (Identity (Identity a) -> Flip (:*:) a a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Left) (Flip (:*:) a) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a :*: a) -> Flip (:*:) a a
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((a :*: a) -> Flip (:*:) a a)
-> (Identity (Identity a) -> a :*: a)
-> Identity (Identity a)
-> Flip (:*:) a a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> a -> a :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (a -> a :*: a)
-> (Identity (Identity a) -> a) -> Identity (Identity a) -> a :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance Substructure Right ((:*:) s) where
type Available Right ((:*:) s) = Identity
type Substance Right ((:*:) s) = Identity
substructure :: Lens
(Available 'Right ((:*:) s))
((<:.>) (Tagged 'Right) ((:*:) s) a)
(Substance 'Right ((:*:) s) a)
substructure = ((<:.>) (Tagged 'Right) ((:*:) s) a
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Right) ((:*:) s) a)
(Identity a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) ((:*:) s) a
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Right) ((:*:) s) a)
(Identity a))
-> ((<:.>) (Tagged 'Right) ((:*:) s) a
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Right) ((:*:) s) a)
(Identity a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) ((:*:) s) a
product -> case (<:.>) (Tagged 'Right) ((:*:) s) a -> s :*: a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) ((:*:) s) a
product of
s
s :*: a
x -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Right) ((:*:) s) a)
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Right) ((:*:) s) a)
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Right) ((:*:) s) a)
-> Store
(Identity (Identity a)) ((<:.>) (Tagged 'Right) ((:*:) s) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity a
x) Identity (Identity a)
-> (Identity (Identity a) -> (<:.>) (Tagged 'Right) ((:*:) s) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
:= (<:.>) (Tagged 'Right) ((:*:) s) a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> (<:.>) (Tagged 'Right) ((:*:) s) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((s :*: a) -> (<:.>) (Tagged 'Right) ((:*:) s) a)
-> (Identity (Identity a) -> s :*: a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Right) ((:*:) s) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*:) (a -> s :*: a)
-> (Identity (Identity a) -> a) -> Identity (Identity a) -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance Accessible s (s :*: a) where
access :: Lens Identity (s :*: a) s
access = ((s :*: a) -> Store (Identity s) (s :*: a))
-> Lens Identity (s :*: a) s
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((s :*: a) -> Store (Identity s) (s :*: a))
-> Lens Identity (s :*: a) s)
-> ((s :*: a) -> Store (Identity s) (s :*: a))
-> Lens Identity (s :*: a) s
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(s
s :*: a
x) -> (((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a))
-> Store (Identity s) (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a))
-> Store (Identity s) (s :*: a))
-> (((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a))
-> Store (Identity s) (s :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! s -> Identity s
forall a. a -> Identity a
Identity s
s Identity s
-> (Identity s -> s :*: a)
-> ((:*:) (Identity s) :. (->) (Identity s)) := (s :*: a)
forall s a. s -> a -> s :*: a
:*: (s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x) (s -> s :*: a) -> (Identity s -> s) -> Identity s -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity s -> s
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance Accessible a (s :*: a) where
access :: Lens Identity (s :*: a) a
access = ((s :*: a) -> Store (Identity a) (s :*: a))
-> Lens Identity (s :*: a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((s :*: a) -> Store (Identity a) (s :*: a))
-> Lens Identity (s :*: a) a)
-> ((s :*: a) -> Store (Identity a) (s :*: a))
-> Lens Identity (s :*: a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(s
s :*: a
x) -> (((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a))
-> Store (Identity a) (s :*: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a))
-> Store (Identity a) (s :*: a))
-> (((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a))
-> Store (Identity a) (s :*: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a -> s :*: a)
-> ((:*:) (Identity a) :. (->) (Identity a)) := (s :*: a)
forall s a. s -> a -> s :*: a
:*: (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*:) (a -> s :*: a) -> (Identity a -> a) -> Identity a -> s :*: a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance {-# OVERLAPS #-} Accessible b a => Accessible b (s :*: a) where
access :: Lens Identity (s :*: a) b
access = forall source. Accessible b source => Lens Identity source b
forall target source.
Accessible target source =>
Lens Identity source target
access @b Lens Identity a b
-> P_Q_T (->) Store Identity (s :*: a) a
-> Lens Identity (s :*: a) b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall source. Accessible a source => Lens Identity source a
forall target source.
Accessible target source =>
Lens Identity source target
access @a
instance Accessible a (Identity a) where
access :: Lens Identity (Identity a) a
access = (Identity a -> Store (Identity a) (Identity a))
-> Lens Identity (Identity a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Identity a -> Store (Identity a) (Identity a))
-> Lens Identity (Identity a) a)
-> (Identity a -> Store (Identity a) (Identity a))
-> Lens Identity (Identity a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(Identity a
x) -> (((:*:) (Identity a) :. (->) (Identity a)) := Identity a)
-> Store (Identity a) (Identity a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity a) :. (->) (Identity a)) := Identity a)
-> Store (Identity a) (Identity a))
-> (((:*:) (Identity a) :. (->) (Identity a)) := Identity a)
-> Store (Identity a) (Identity a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Identity a
forall a. a -> Identity a
Identity a
x Identity a
-> (Identity a -> Identity a)
-> ((:*:) (Identity a) :. (->) (Identity a)) := Identity a
forall s a. s -> a -> s :*: a
:*: Identity a -> Identity a
forall (m :: * -> * -> *) a. Category m => m a a
identity
instance Possible a (Maybe a) where
perhaps :: Lens Maybe (Maybe a) a
perhaps = (Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a)
-> (Maybe a -> Store (Maybe a) (Maybe a)) -> Lens Maybe (Maybe a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \Maybe a
x -> (((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
-> Store (Maybe a) (Maybe a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
-> Store (Maybe a) (Maybe a))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a)
-> Store (Maybe a) (Maybe a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe a
x Maybe a
-> (Maybe a -> Maybe a)
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Maybe a
forall s a. s -> a -> s :*: a
:*: Maybe a -> Maybe a
forall (m :: * -> * -> *) a. Category m => m a a
identity
instance Possible a (o :+: a) where
perhaps :: Lens Maybe (o :+: a) a
perhaps = ((o :+: a) -> Store (Maybe a) (o :+: a)) -> Lens Maybe (o :+: a) a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((o :+: a) -> Store (Maybe a) (o :+: a))
-> Lens Maybe (o :+: a) a)
-> ((o :+: a) -> Store (Maybe a) (o :+: a))
-> Lens Maybe (o :+: a) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case
Option o
s -> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe a
forall a. Maybe a
Nothing Maybe a
-> (Maybe a -> o :+: a)
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a)
forall s a. s -> a -> s :*: a
:*: (a -> o :+: a) -> (o :+: a) -> Maybe a -> o :+: a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @a @(Maybe a) a -> o :+: a
forall o a. a -> o :+: a
Adoption (o -> o :+: a
forall o a. o -> o :+: a
Option o
s)
Adoption a
x -> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a))
-> Store (Maybe a) (o :+: a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> Maybe a
forall a. a -> Maybe a
Just a
x Maybe a
-> (Maybe a -> o :+: a)
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := (o :+: a)
forall s a. s -> a -> s :*: a
:*: (a -> o :+: a) -> (o :+: a) -> Maybe a -> o :+: a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @a @(Maybe a) a -> o :+: a
forall o a. a -> o :+: a
Adoption (a -> o :+: a
forall o a. a -> o :+: a
Adoption a
x)
instance Accessible target source => Possible target (Maybe source) where
perhaps :: Lens Maybe (Maybe source) target
perhaps = let lst :: Lens Identity source target
lst = Accessible target source => Lens Identity source target
forall target source.
Accessible target source =>
Lens Identity source target
access @target @source in (Maybe source -> Store (Maybe target) (Maybe source))
-> Lens Maybe (Maybe source) target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Maybe source -> Store (Maybe target) (Maybe source))
-> Lens Maybe (Maybe source) target)
-> (Maybe source -> Store (Maybe target) (Maybe source))
-> Lens Maybe (Maybe source) target
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \case
Just source
source -> let (Identity target
target :*: Identity target -> source
its) = Store (Identity target) source
-> Identity target :*: (Identity target -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Lens Identity source target
lst Lens Identity source target
-> source -> Store (Identity target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! source
source) in
(((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source))
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! target -> Maybe target
forall a. a -> Maybe a
Just target
target Maybe target
-> (Maybe target -> Maybe source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source
forall s a. s -> a -> s :*: a
:*: (Identity target -> source
its (Identity target -> source)
-> (target -> Identity target) -> target -> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. target -> Identity target
forall a. a -> Identity a
Identity (target -> source) -> Maybe target -> Maybe source
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)
Maybe source
Nothing -> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source))
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source)
-> Store (Maybe target) (Maybe source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Maybe target
forall a. Maybe a
Nothing Maybe target
-> (Maybe target -> Maybe source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := Maybe source
forall s a. s -> a -> s :*: a
:*: \Maybe target
_ -> Maybe source
forall a. Maybe a
Nothing
instance Accessible (Maybe target) source => Possible target source where
perhaps :: Lens Maybe source target
perhaps = let lst :: Lens Identity source (Maybe target)
lst = Accessible (Maybe target) source =>
Lens Identity source (Maybe target)
forall target source.
Accessible target source =>
Lens Identity source target
access @(Maybe target) @source in (source -> Store (Maybe target) source) -> Lens Maybe source target
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((source -> Store (Maybe target) source)
-> Lens Maybe source target)
-> (source -> Store (Maybe target) source)
-> Lens Maybe source target
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \source
source ->
let Identity (Maybe target)
target :*: Identity (Maybe target) -> source
imts = Store (Identity (Maybe target)) source
-> Identity (Maybe target) :*: (Identity (Maybe target) -> source)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Lens Identity source (Maybe target)
lst Lens Identity source (Maybe target)
-> source -> Store (Identity (Maybe target)) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! source
source) in
(((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source)
-> (((:*:) (Maybe target) :. (->) (Maybe target)) := source)
-> Store (Maybe target) source
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! Identity (Maybe target) -> Maybe target
forall (t :: * -> *) a. Extractable t => t a -> a
extract Identity (Maybe target)
target Maybe target
-> (Maybe target -> source)
-> ((:*:) (Maybe target) :. (->) (Maybe target)) := source
forall s a. s -> a -> s :*: a
:*: Identity (Maybe target) -> source
imts (Identity (Maybe target) -> source)
-> (Maybe target -> Identity (Maybe target))
-> Maybe target
-> source
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Maybe target -> Identity (Maybe target)
forall a. a -> Identity a
Identity
instance (Covariant (->) (->) t) => Substructure Left (t <:.:> t := (:*:)) where
type Available Left (t <:.:> t := (:*:)) = Identity
type Substance Left (t <:.:> t := (:*:)) = t
substructure :: Lens
(Available 'Left ((t <:.:> t) := (:*:)))
((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
(Substance 'Left ((t <:.:> t) := (:*:)) a)
substructure = ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
(t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
(t a))
-> ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
(t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
x -> case (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (t <:.:> t) (:*:) a -> t a :*: t a)
-> (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
-> (:=) (t <:.:> t) (:*:) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
x of
t a
ls :*: t a
rs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Identity (t a)
forall a. a -> Identity a
Identity t a
ls Identity (t a)
-> (Identity (t a)
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall s a. s -> a -> s :*: a
:*: (:=) (t <:.:> t) (:*:) a
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (t <:.:> t) (:*:) a
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a)
-> (Identity (t a) -> (:=) (t <:.:> t) (:*:) a)
-> Identity (t a)
-> (<:.>) (Tagged 'Left) ((t <:.:> t) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> t a -> (:=) (t <:.:> t) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (t a -> t a -> (:=) (t <:.:> t) (:*:) a)
-> t a -> t a -> (:=) (t <:.:> t) (:*:) a
forall a b c. (a -> b -> c) -> b -> a -> c
% t a
rs) (t a -> (:=) (t <:.:> t) (:*:) a)
-> (Identity (t a) -> t a)
-> Identity (t a)
-> (:=) (t <:.:> t) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
instance (Covariant (->) (->) t) => Substructure Right (t <:.:> t := (:*:)) where
type Available Right (t <:.:> t := (:*:)) = Identity
type Substance Right (t <:.:> t := (:*:)) = t
substructure :: Lens
(Available 'Right ((t <:.:> t) := (:*:)))
((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
(Substance 'Right ((t <:.:> t) := (:*:)) a)
substructure = ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
(t a)
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
(t a))
-> ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> P_Q_T
(->)
Store
Identity
((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
(t a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! \(<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
x -> case (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run ((:=) (t <:.:> t) (:*:) a -> t a :*: t a)
-> (:=) (t <:.:> t) (:*:) a -> t a :*: t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
-> (:=) (t <:.:> t) (:*:) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
x of
t a
ls :*: t a
rs -> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a))
-> (((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> Store
(Identity (t a)) ((<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! t a -> Identity (t a)
forall a. a -> Identity a
Identity t a
rs Identity (t a)
-> (Identity (t a)
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> ((:*:) (Identity (t a)) :. (->) (Identity (t a)))
:= (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall s a. s -> a -> s :*: a
:*: (:=) (t <:.:> t) (:*:) a
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((:=) (t <:.:> t) (:*:) a
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a)
-> (Identity (t a) -> (:=) (t <:.:> t) (:*:) a)
-> Identity (t a)
-> (<:.>) (Tagged 'Right) ((t <:.:> t) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (t a -> t a -> (:=) (t <:.:> t) (:*:) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome t a
ls) (t a -> (:=) (t <:.:> t) (:*:) a)
-> (Identity (t a) -> t a)
-> Identity (t a)
-> (:=) (t <:.:> t) (:*:) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (t a) -> t a
forall (t :: * -> *) a. Extractable t => t a -> a
extract