{-# 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.Pattern.Category (($), (.), (/)) import Pandora.Pattern.Functor.Covariant (Covariant (comap)) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Functor.Pointable (point) import Pandora.Pattern.Transformer.Liftable (lift) 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.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.Tagged (Tagged (Tag)) import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate)) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached) import Pandora.Paradigm.Primary.Functor.Wye (Wye (Both, Left, Right, End)) import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct)) import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap)) import Pandora.Paradigm.Schemes.TU (type (<:.>)) 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 :: * -> * -> *). Category m => m ~~> m / 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 :: * -> * -> *). Category m => m ~~> m / a <:= Product s forall (t :: * -> *) a. Extractable t => a <:= t 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 :: * -> * -> *). Category m => m ~~> m $ \case { Just a _ -> Boolean True ; Maybe a _ -> Boolean False } instance Substructure Right (Product s) where type Substructural Right (Product s) = Identity substructure :: Lens ((<:.>) (Tagged 'Right) (Product s) a) (Substructural 'Right (Product s) a) substructure (Product s a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract (Product s a <:= Tagged 'Right) -> ((<:.>) (Tagged 'Right) (Product s) a -> Tagged 'Right (Product s a)) -> (<:.>) (Tagged 'Right) (Product s) a -> Product s a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Right) (Product s) a -> Tagged 'Right (Product s a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> s s :*: a x) = (((:*:) (Identity a) :. (->) (Identity a)) := (<:.>) (Tagged 'Right) (Product s) a) -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Identity a) :. (->) (Identity a)) := (<:.>) (Tagged 'Right) (Product s) a) -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a)) -> (((:*:) (Identity a) :. (->) (Identity a)) := (<:.>) (Tagged 'Right) (Product s) a) -> Store (Identity a) ((<:.>) (Tagged 'Right) (Product s) a) forall (m :: * -> * -> *). Category m => m ~~> m $ a -> Identity a forall a. a -> Identity a Identity a x Identity a -> (Identity a -> (<:.>) (Tagged 'Right) (Product s) a) -> ((:*:) (Identity a) :. (->) (Identity a)) := (<:.>) (Tagged 'Right) (Product s) a forall s a. s -> a -> Product s a :*: Product s a -> (<:.>) (Tagged 'Right) (Product s) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Product s a -> (<:.>) (Tagged 'Right) (Product s) a) -> (Identity a -> Product s a) -> Identity a -> (<:.>) (Tagged 'Right) (Product s) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (s s s -> a -> Product s a forall s a. s -> a -> Product s a :*:) (a -> Product s a) -> (Identity a -> a) -> Identity a -> Product s a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Identity a -> a forall (t :: * -> *) a. Extractable t => a <:= t extract instance Covariant t => Substructure Tail (Tap t) where type Substructural Tail (Tap t) = t substructure :: Lens ((<:.>) (Tagged 'Tail) (Tap t) a) (Substructural 'Tail (Tap t) a) substructure (Tap t a <:= Tagged 'Tail forall (t :: * -> *) a. Extractable t => a <:= t extract (Tap t a <:= Tagged 'Tail) -> ((<:.>) (Tagged 'Tail) (Tap t) a -> Tagged 'Tail (Tap t a)) -> (<:.>) (Tagged 'Tail) (Tap t) a -> Tap t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Tail) (Tap t) a -> Tagged 'Tail (Tap t a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Tap a x t a xs) = (((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a) -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a) -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a)) -> (((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a) -> Store (t a) ((<:.>) (Tagged 'Tail) (Tap t) a) forall (m :: * -> * -> *). Category m => m ~~> m $ t a xs t a -> (t a -> (<:.>) (Tagged 'Tail) (Tap t) a) -> ((:*:) (t a) :. (->) (t a)) := (<:.>) (Tagged 'Tail) (Tap t) a forall s a. s -> a -> Product s a :*: Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Tap t a -> (<:.>) (Tagged 'Tail) (Tap t) a) -> (t a -> Tap t a) -> t a -> (<:.>) (Tagged 'Tail) (Tap t) a forall (m :: * -> * -> *) b c a. Category 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 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 -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> 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 morphing ((<:.>) (Tagged ('Into ('Preorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> 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. Category 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 :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> Morphing ('Into ('Preorder (Nonempty List))) (Construction Wye) a forall a (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t into @(Preorder (Nonempty List)) Construction Wye a lst morphing ((<:.>) (Tagged ('Into ('Preorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> 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. Category 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 :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> Morphing ('Into ('Preorder (Nonempty List))) (Construction Wye) a forall a (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t into @(Preorder (Nonempty List)) Construction Wye a rst morphing ((<:.>) (Tagged ('Into ('Preorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> 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. Category 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 :: * -> * -> *). Category m => m ~~> m $ Construction Wye a -> Morphing ('Into ('Preorder (Nonempty List))) (Construction Wye) a forall a (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x Wye (Construction Wye a) End) = a :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x morphing ((<:.>) (Tagged ('Into ('Inorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Left Construction Wye a lst)) = Construction Wye a -> Morphing ('Into ('Inorder (Nonempty List))) (Construction Wye) a forall a (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x morphing ((<:.>) (Tagged ('Into ('Inorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Right Construction Wye a rst)) = a :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x 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 (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t into @(Inorder (Nonempty List)) Construction Wye a rst morphing ((<:.>) (Tagged ('Into ('Inorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> 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 (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x 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 (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x Wye (Construction Wye a) End) = a :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x morphing ((<:.>) (Tagged ('Into ('Postorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Left Construction Wye a lst)) = Construction Wye a -> Morphing ('Into ('Postorder (Nonempty List))) (Construction Wye) a forall a (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x morphing ((<:.>) (Tagged ('Into ('Postorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Construct a x (Right Construction Wye a rst)) = Construction Wye a -> Morphing ('Into ('Postorder (Nonempty List))) (Construction Wye) a forall a (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x morphing ((<:.>) (Tagged ('Into ('Postorder (Construction Maybe)))) (Construction Wye) a -> Construction Wye a forall k (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> 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 (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t 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 :=> Construction Maybe forall (t :: * -> *) a. Pointable t => a :=> t point a x 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 (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t premorph -> Binary a xs) = (Construction Wye a -> Morphing ('Into (o ds)) (Construction Wye) a) -> Maybe (Construction Wye a) -> Maybe (Morphing ('Into (o ds)) (Construction Wye) a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b comap (forall a (f :: a) (t :: * -> *). Morphable ('Into f) t => t ~> Morphing ('Into f) t forall (t :: * -> *). Morphable ('Into (o ds)) t => t ~> Morphing ('Into (o ds)) t into @(o ds)) (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 (t :: * -> *) (u :: * -> *) a b. (Interpreted t, Interpreted u) => (Primary t a -> Primary u b) -> t a -> u b ||= Binary a xs instance Focusable Left (Product s) where type Focusing Left (Product s) a = s focusing :: Tagged 'Left (Product s a) :-. Focusing 'Left (Product s) a focusing (Product s a <:= Tagged 'Left forall (t :: * -> *) a. Extractable t => a <:= t extract -> s s :*: a x) = ((Product s :. (->) s) := Tagged 'Left (Product s a)) -> Store s (Tagged 'Left (Product s a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store (((Product s :. (->) s) := Tagged 'Left (Product s a)) -> Store s (Tagged 'Left (Product s a))) -> ((Product s :. (->) s) := Tagged 'Left (Product s a)) -> Store s (Tagged 'Left (Product s a)) forall (m :: * -> * -> *). Category m => m ~~> m $ s s s -> (s -> Tagged 'Left (Product s a)) -> (Product s :. (->) s) := Tagged 'Left (Product s a) forall s a. s -> a -> Product s a :*: Product s a -> Tagged 'Left (Product s a) forall k (tag :: k) a. a -> Tagged tag a Tag (Product s a -> Tagged 'Left (Product s a)) -> (s -> Product s a) -> s -> Tagged 'Left (Product s a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (s -> a -> Product s a forall s a. s -> a -> Product s a :*: a x) instance Focusable Right (Product s) where type Focusing Right (Product s) a = a focusing :: Tagged 'Right (Product s a) :-. Focusing 'Right (Product s) a focusing (Product s a <:= Tagged 'Right forall (t :: * -> *) a. Extractable t => a <:= t extract -> s s :*: a x) = (((:*:) a :. (->) a) := Tagged 'Right (Product s a)) -> Store a (Tagged 'Right (Product s a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := Tagged 'Right (Product s a)) -> Store a (Tagged 'Right (Product s a))) -> (((:*:) a :. (->) a) := Tagged 'Right (Product s a)) -> Store a (Tagged 'Right (Product s a)) forall (m :: * -> * -> *). Category m => m ~~> m $ a x a -> (a -> Tagged 'Right (Product s a)) -> ((:*:) a :. (->) a) := Tagged 'Right (Product s a) forall s a. s -> a -> Product s a :*: Product s a -> Tagged 'Right (Product s a) forall k (tag :: k) a. a -> Tagged tag a Tag (Product s a -> Tagged 'Right (Product s a)) -> (a -> Product s a) -> a -> Tagged 'Right (Product s a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (s s s -> a -> Product s a forall s a. s -> a -> Product s a :*:) instance Accessible s (s :*: a) where access :: (s :*: a) :-. s access ~(s s :*: a x) = (((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a)) -> (((:*:) s :. (->) s) := (s :*: a)) -> Store s (s :*: a) forall (m :: * -> * -> *). Category m => m ~~> m $ s s s -> (s -> s :*: a) -> ((:*:) s :. (->) s) := (s :*: a) forall s a. s -> a -> Product s a :*: (s -> a -> s :*: a forall s a. s -> a -> Product s a :*: a x) instance Accessible a (s :*: a) where access :: (s :*: a) :-. a access ~(s s :*: a x) = (((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a)) -> (((:*:) a :. (->) a) := (s :*: a)) -> Store a (s :*: a) forall (m :: * -> * -> *). Category m => m ~~> m $ a x a -> (a -> s :*: a) -> ((:*:) a :. (->) a) := (s :*: a) forall s a. s -> a -> Product s a :*: (s s s -> a -> s :*: a forall s a. s -> a -> Product s a :*:) instance {-# OVERLAPS #-} Accessible b a => Accessible b (s :*: a) where access :: (s :*: a) :-. b access = forall src. Accessible a src => src :-. a forall tgt src. Accessible tgt src => src :-. tgt access @a ((s :*: a) :-. a) -> Lens a b -> (s :*: a) :-. b forall src tgt new. Lens src tgt -> Lens tgt new -> Lens src new |> forall src. Accessible b src => src :-. b forall tgt src. Accessible tgt src => src :-. tgt access @b