{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Structure.Some.List where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern ((.|..))
import Pandora.Pattern.Category ((.), (/), ($), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Applicative (Applicative ((<*>)))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Avoidable (empty)
import Pandora.Pattern.Functor.Traversable (Traversable ((->>)))
import Pandora.Pattern.Functor.Extendable (Extendable ((=>>)))
import Pandora.Pattern.Functor.Bivariant ((<->))
import Pandora.Pattern.Functor.Adjoint ((|-))
import Pandora.Pattern.Functor ()
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False), (?))
import Pandora.Paradigm.Primary.Object.Numerator (Numerator (Numerator))
import Pandora.Paradigm.Primary.Object.Denumerator (Denumerator (One))
import Pandora.Paradigm.Primary.Functor.Function ((%), (&))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached, twosome)
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+))
import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap))
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Inventory.State (State, fold, modify)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Inventory.Optics (view)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (||=))
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Zipper (Zipper)
import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Head), focus)
import Pandora.Paradigm.Structure.Ability.Measurable (Measurable (Measural, measurement), Scale (Length), measure)
import Pandora.Paradigm.Structure.Ability.Monotonic (Monotonic (reduce, resolve))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate, Into, Push, Pop, Delete, Find, Element)
	, Occurrence (All, First), premorph, rotate, item, filter, find, into)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure), Segment (Tail), sub, subview)
import Pandora.Paradigm.Structure.Interface.Stack (Stack)

-- | Linear data structure that serves as a collection of elements
type List = Maybe <:.> Construction Maybe

instance Setoid a => Setoid (List a) where
	TU (Maybe :. Construction Maybe) := a
ls == :: List a -> List a -> Boolean
== TU (Maybe :. Construction Maybe) := a
rs = (Maybe :. Construction Maybe) := a
ls ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a) -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (Maybe :. Construction Maybe) := a
rs

instance Semigroup (List a) where
	TU Maybe (Construction Maybe a)
Nothing + :: List a -> List a -> List a
+ TU Maybe (Construction Maybe a)
ys = Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
ys
	TU (Just (Construct a
x Maybe (Construction Maybe a)
xs)) + TU Maybe (Construction Maybe a)
ys = Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. 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)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run
		(List a -> List a) -> List a -> List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU @Covariant @Covariant Maybe (Construction Maybe a)
xs List a -> List a -> List a
forall a. Semigroup a => a -> a -> a
+ Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU @Covariant @Covariant Maybe (Construction Maybe a)
ys

instance Monoid (List a) where
	zero :: List a
zero = List a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Morphable Push List where
	type Morphing Push List = Identity <:.:> List := (->)
	morphing :: (<:.>) (Tagged 'Push) List a -> Morphing 'Push List a
morphing ((<:.>) (Tagged 'Push) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> List a
xs) = (Identity a -> List a)
-> T_U Covariant Covariant (->) Identity List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Identity a -> List a)
 -> T_U Covariant Covariant (->) Identity List a)
-> (Identity a -> List a)
-> T_U Covariant Covariant (->) Identity List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \(Identity a
x) -> Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. 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)
-> (List a -> (Maybe :. Construction Maybe) := a)
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. List a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ List a
xs

instance Morphable Pop List where
	type Morphing Pop List = List
	morphing :: (<:.>) (Tagged 'Pop) List a -> Morphing 'Pop List a
morphing ((<:.>) (Tagged 'Pop) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> List a
xs) = (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing (Primary List a -> Primary List a) -> List a -> List a
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= List a
xs

instance Morphable (Find Element) List where
	type Morphing (Find Element) List = Predicate <:.:> Maybe := (->)
	morphing :: (<:.>) (Tagged ('Find 'Element)) List a
-> Morphing ('Find 'Element) List a
morphing ((<:.>) (Tagged ('Find 'Element)) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> TU Maybe (Construction Maybe a)
Nothing) = (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> Maybe a)
 -> T_U Covariant Covariant (->) Predicate Maybe a)
-> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \Predicate a
_ -> Maybe a
forall a. Maybe a
Nothing
	morphing ((<:.>) (Tagged ('Find 'Element)) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> TU (Just (Construct a
x Maybe (Construction Maybe a)
xs))) = (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> Maybe a)
 -> T_U Covariant Covariant (->) Predicate Maybe a)
-> (Predicate a -> Maybe a)
-> T_U Covariant Covariant (->) Predicate Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \Predicate a
p ->
		Predicate a -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> Maybe a -> Maybe a -> Maybe a
forall a. Boolean -> a -> a -> a
? a -> Maybe a
forall a. a -> Maybe a
Just a
x (Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (forall a2.
(Morphable ('Find 'Element) List,
 Morphing ('Find 'Element) List
 ~ ((Predicate <:.:> Maybe) := (->))) =>
Predicate a2 -> List a2 -> Maybe a2
forall a1 (f :: a1) (t :: * -> *) (u :: * -> *) a2.
(Morphable ('Find f) t,
 Morphing ('Find f) t ~ ((Predicate <:.:> u) := (->))) =>
Predicate a2 -> t a2 -> u a2
find @Element @List @Maybe (Predicate a -> List a -> Maybe a)
-> Predicate a -> List a -> Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
/ Predicate a
p (List a -> Maybe a) -> List a -> Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
/ Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs)

instance Morphable (Delete First) List where
	type Morphing (Delete First) List = Predicate <:.:> List := (->)
	morphing :: (<:.>) (Tagged ('Delete 'First)) List a
-> Morphing ('Delete 'First) List a
morphing ((<:.>) (Tagged ('Delete 'First)) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> TU Maybe (Construction Maybe a)
Nothing) = (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \Predicate a
_ -> Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
forall a. Maybe a
Nothing
	morphing ((<:.>) (Tagged ('Delete 'First)) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> TU (Just (Construct a
x Maybe (Construction Maybe a)
xs))) = (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \Predicate a
p ->
		Predicate a -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> List a -> List a -> List a
forall a. Boolean -> a -> a -> a
? Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. 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)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (List a -> List a) -> List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Predicate a -> List a -> List a
forall a1 (f :: a1) (t :: * -> *) a2.
(Morphable ('Delete f) t,
 Morphing ('Delete f) t ~ ((Predicate <:.:> t) := (->))) =>
Predicate a2 -> t a2 -> t a2
filter @First @List Predicate a
p (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs

instance Morphable (Delete All) List where
	type Morphing (Delete All) List = Predicate <:.:> List := (->)
	morphing :: (<:.>) (Tagged ('Delete 'All)) List a
-> Morphing ('Delete 'All) List a
morphing ((<:.>) (Tagged ('Delete 'All)) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> TU Maybe (Construction Maybe a)
Nothing) = (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \Predicate a
_ -> Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
forall a. Maybe a
Nothing
	morphing ((<:.>) (Tagged ('Delete 'All)) List a -> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> TU (Just (Construct a
x Maybe (Construction Maybe a)
xs))) = (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Predicate a -> List a)
 -> T_U Covariant Covariant (->) Predicate List a)
-> (Predicate a -> List a)
-> T_U Covariant Covariant (->) Predicate List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \Predicate a
p ->
		Predicate a -> a -> Boolean
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Predicate a
p a
x Boolean -> List a -> List a -> List a
forall a. Boolean -> a -> a -> a
? Predicate a -> List a -> List a
forall a1 (f :: a1) (t :: * -> *) a2.
(Morphable ('Delete f) t,
 Morphing ('Delete f) t ~ ((Predicate <:.:> t) := (->))) =>
Predicate a2 -> t a2 -> t a2
filter @All @List Predicate a
p (Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs) (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a -> List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> List a)
-> (List a -> Construction Maybe a) -> List a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. 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)
-> (List a -> Maybe (Construction Maybe a))
-> List a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (List a -> List a) -> List a -> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Predicate a -> List a -> List a
forall a1 (f :: a1) (t :: * -> *) a2.
(Morphable ('Delete f) t,
 Morphing ('Delete f) t ~ ((Predicate <:.:> t) := (->))) =>
Predicate a2 -> t a2 -> t a2
filter @All @List Predicate a
p (List a -> List a) -> List a -> List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Maybe (Construction Maybe a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU Maybe (Construction Maybe a)
xs

instance Stack List where

instance Focusable Head List where
	type Focusing Head List a = Maybe a
	focusing :: Tagged 'Head (List a) :-. Focusing 'Head List a
focusing (List a <:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> List a
stack) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a))
-> Store (Maybe a) (Tagged 'Head (List a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a))
 -> Store (Maybe a) (Tagged 'Head (List a)))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a))
-> Store (Maybe a) (Tagged 'Head (List a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract (a <:= Construction Maybe)
-> Maybe (Construction Maybe a) -> Maybe a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> List a -> Primary List a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run List a
stack Maybe a
-> (Maybe a -> Tagged 'Head (List a))
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Head (List a)
forall s a. s -> a -> Product s a
:*: \case
		Just a
x -> List a
stack List a -> (List a -> List a) -> List a
forall a b. a -> (a -> b) -> b
& forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
forall (t :: * -> *).
Substructure 'Tail t =>
t ~> Substructural 'Tail t
subview @Tail List a -> (List a -> List a) -> List a
forall a b. a -> (a -> b) -> b
& a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x List a
-> (List a -> Tagged 'Head (List a)) -> Tagged 'Head (List a)
forall a b. a -> (a -> b) -> b
& List a -> Tagged 'Head (List a)
forall k (tag :: k) a. a -> Tagged tag a
Tag
		Maybe a
Nothing -> List a
stack List a -> (List a -> List a) -> List a
forall a b. a -> (a -> b) -> b
& forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
forall (t :: * -> *).
Substructure 'Tail t =>
t ~> Substructural 'Tail t
subview @Tail List a
-> (List a -> Tagged 'Head (List a)) -> Tagged 'Head (List a)
forall a b. a -> (a -> b) -> b
& List a -> Tagged 'Head (List a)
forall k (tag :: k) a. a -> Tagged tag a
Tag

instance Measurable Length List where
	type Measural Length List a = Numerator
	measurement :: Tagged 'Length (List a) -> Measural 'Length List a
measurement (List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (Tagged 'Length (List a) -> List a)
-> Tagged 'Length (List a)
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (List a) -> List a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Maybe (Construction Maybe a)
Nothing) = Measural 'Length List a
forall a. Monoid a => a
zero
	measurement (List a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (List a -> Maybe (Construction Maybe a))
-> (Tagged 'Length (List a) -> List a)
-> Tagged 'Length (List a)
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (List a) -> List a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Maybe a
xs) = Denumerator -> Numerator
Numerator (Denumerator -> Numerator) -> Denumerator -> Numerator
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a -> Measural 'Length (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Length Construction Maybe a
xs

instance Nullable List where
	null :: (Predicate :. List) := a
null = (List a -> Boolean) -> (Predicate :. List) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((List a -> Boolean) -> (Predicate :. List) := a)
-> (List a -> Boolean) -> (Predicate :. List) := a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \case { TU Maybe (Construction Maybe a)
Nothing -> Boolean
True ; List a
_ -> Boolean
False }

instance Substructure Tail List where
	type Substructural Tail List = List
	substructure :: Lens ((<:.>) (Tagged 'Tail) List a) (Substructural 'Tail List a)
substructure (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
 -> Maybe (Construction Maybe a))
-> ((<:.>) (Tagged 'Tail) List a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) List a
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
<:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Maybe) a
 <:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) List a
    -> Tagged
         'Tail (TU Covariant Covariant Maybe (Construction Maybe) a))
-> (<:.>) (Tagged 'Tail) List a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) List a
-> Tagged
     'Tail (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Just Construction Maybe a
ns) = TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Tail) List a)
-> (Construction Maybe a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> Construction Maybe a
-> (<:.>) (Tagged 'Tail) List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a -> (<:.>) (Tagged 'Tail) List a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (Construction Maybe a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) List a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens
  (Construction Maybe a) (Substructural 'Tail (Construction Maybe) a)
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
sub @Tail Construction Maybe a
ns
	substructure (TU Covariant Covariant Maybe (Construction Maybe) a
-> Maybe (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
 -> Maybe (Construction Maybe a))
-> ((<:.>) (Tagged 'Tail) List a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (<:.>) (Tagged 'Tail) List a
-> Maybe (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
<:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction Maybe) a
 <:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) List a
    -> Tagged
         'Tail (TU Covariant Covariant Maybe (Construction Maybe) a))
-> (<:.>) (Tagged 'Tail) List a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) List a
-> Tagged
     'Tail (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Maybe (Construction Maybe a)
Nothing) = (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
 := (<:.>) (Tagged 'Tail) List a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) List a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
  := (<:.>) (Tagged 'Tail) List a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Tail) List a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
    := (<:.>) (Tagged 'Tail) List a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) List a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (<:.>) (Tagged 'Tail) List a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
   := (<:.>) (Tagged 'Tail) List a
forall s a. s -> a -> Product s a
:*: TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (<:.>) (Tagged 'Tail) List a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) a. Category m => m a a
identity

-- | Transform any traversable structure into a stack
linearize :: forall t a . Traversable t => t a -> List a
linearize :: t a -> List a
linearize = ((Maybe :. Construction Maybe) := a) -> List a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe :. Construction Maybe) := a) -> List a)
-> (t a -> (Maybe :. Construction Maybe) := a) -> t a -> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction Maybe) := a)
<:= Product ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) a. Extractable t => a <:= t
extract (((Maybe :. Construction Maybe) := a)
 <:= Product ((Maybe :. Construction Maybe) := a))
-> (t a
    -> Product
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> t a
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State ((Maybe :. Nonempty List) := a)) =>
State ((Maybe :. Nonempty List) := a) a
-> Primary (State ((Maybe :. Nonempty List) := a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State (Maybe :. Nonempty List := a)) (State
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> ((Maybe :. Construction Maybe) := a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> ((Maybe :. Construction Maybe) := a)
-> State
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall a b c. (a -> b -> c) -> b -> a -> c
% (Maybe :. Construction Maybe) := a
forall a. Maybe a
Nothing (State
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> (t a
    -> State
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> t a
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a
 -> ((Maybe :. Construction Maybe) := a)
 -> (Maybe :. Construction Maybe) := a)
-> t a
-> State
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (t :: * -> *) s (u :: * -> *) a.
(Traversable t, Memorable s u) =>
(a -> s -> s) -> t a -> u s
fold (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (((->) a :. (->) ((Maybe :. Construction Maybe) := a))
    := Construction Maybe a)
-> a
-> ((Maybe :. Construction Maybe) := a)
-> (Maybe :. Construction Maybe) := a
forall (v :: * -> * -> *) a c d b.
(Category v, Covariant (v a)) =>
v c d -> ((v a :. v b) := c) -> (v a :. v b) := d
.|.. ((->) a :. (->) ((Maybe :. Construction Maybe) := a))
:= Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct)

type instance Nonempty List = Construction Maybe

instance {-# OVERLAPS #-} Semigroup (Construction Maybe a) where
	Construct a
x Maybe (Construction Maybe a)
Nothing + :: Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
+ Construction Maybe a
ys = 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)
-> Maybe (Construction Maybe a) -> Construction Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a -> Maybe (Construction Maybe a)
forall a. a -> Maybe a
Just Construction Maybe a
ys
	Construct a
x (Just Construction Maybe a
xs) + Construction Maybe a
ys = 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 Maybe a
xs Construction Maybe a
-> Construction Maybe a -> Construction Maybe a
forall a. Semigroup a => a -> a -> a
+ Construction Maybe a
ys

instance Morphable (Into List) (Construction Maybe) where
	type Morphing (Into List) (Construction Maybe) = List
	morphing :: (<:.>) (Tagged ('Into List)) (Construction Maybe) a
-> Morphing ('Into List) (Construction Maybe) a
morphing = Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> ((<:.>) (Tagged ('Into List)) (Construction Maybe) a
    -> Construction Maybe a)
-> (<:.>) (Tagged ('Into List)) (Construction Maybe) a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Into List)) (Construction Maybe) a
-> Construction Maybe a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph

instance Focusable Head (Construction Maybe) where
	type Focusing Head (Construction Maybe) a = a
	focusing :: Tagged 'Head (Construction Maybe a)
:-. Focusing 'Head (Construction Maybe) a
focusing (Construction Maybe a <:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Construction Maybe a
stack) = (((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
 -> Store a (Tagged 'Head (Construction Maybe a)))
-> (((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a))
-> Store a (Tagged 'Head (Construction Maybe a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
stack a
-> (a -> Tagged 'Head (Construction Maybe a))
-> ((:*:) a :. (->) a) := Tagged 'Head (Construction Maybe a)
forall s a. s -> a -> Product s a
:*: Construction Maybe a -> Tagged 'Head (Construction Maybe a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Construction Maybe a -> Tagged 'Head (Construction Maybe a))
-> (a -> Construction Maybe a)
-> a
-> Tagged 'Head (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a)
-> ((Maybe :. Construction Maybe) := a)
-> a
-> Construction Maybe a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
stack

instance Morphable Push (Construction Maybe) where
	type Morphing Push (Construction Maybe) = Identity <:.:> Construction Maybe := (->)
	morphing :: (<:.>) (Tagged 'Push) (Construction Maybe) a
-> Morphing 'Push (Construction Maybe) a
morphing ((<:.>) (Tagged 'Push) (Construction Maybe) a
-> Construction Maybe a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construction Maybe a
xs) = (Identity a -> Construction Maybe a)
-> T_U Covariant Covariant (->) Identity (Construction Maybe) a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((Identity a -> Construction Maybe a)
 -> T_U Covariant Covariant (->) Identity (Construction Maybe) a)
-> (Identity a -> Construction Maybe a)
-> T_U Covariant Covariant (->) Identity (Construction Maybe) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ \(Identity a
x) -> 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)
-> ((Maybe :. Construction Maybe) := a) -> Construction Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall a. a -> Maybe a
Just Construction Maybe a
xs

instance Measurable Length (Construction Maybe) where
	type Measural Length (Construction Maybe) a = Denumerator
	measurement :: Tagged 'Length (Construction Maybe a)
-> Measural 'Length (Construction Maybe) a
measurement (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (Tagged 'Length (Construction Maybe a) -> Construction Maybe a)
-> Tagged 'Length (Construction Maybe a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> (Maybe :. Construction Maybe) := a
Nothing) = Denumerator
Measural 'Length (Construction Maybe) a
One
	measurement (Construction Maybe a -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe a -> (Maybe :. Construction Maybe) := a)
-> (Tagged 'Length (Construction Maybe a) -> Construction Maybe a)
-> Tagged 'Length (Construction Maybe a)
-> (Maybe :. Construction Maybe) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Length (Construction Maybe a) -> Construction Maybe a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction Maybe a
xs) = Denumerator
One Denumerator -> Denumerator -> Denumerator
forall a. Semigroup a => a -> a -> a
+ Construction Maybe a -> Measural 'Length (Construction Maybe) a
forall k (f :: k) (t :: * -> *) a.
Measurable f t =>
t a -> Measural f t a
measure @Length Construction Maybe a
xs

instance Monotonic a (Construction Maybe a) where
	reduce :: (a -> r -> r) -> r -> Construction Maybe a -> r
reduce a -> r -> r
f r
r ~(Construct a
x (Maybe :. Construction Maybe) := a
xs) = a -> r -> r
f a
x (r -> r) -> r -> r
forall (m :: * -> * -> *). Category m => m ~~> m
$ (a -> r -> r) -> r -> ((Maybe :. Construction Maybe) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (Maybe :. Construction Maybe) := a
xs

instance Substructure Tail (Construction Maybe) where
	type Substructural Tail (Construction Maybe) = List
	substructure :: Lens
  ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
  (Substructural 'Tail (Construction Maybe) a)
substructure (Construction Maybe a <:= Tagged 'Tail
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction Maybe a <:= Tagged 'Tail)
-> ((<:.>) (Tagged 'Tail) (Construction Maybe) a
    -> Tagged 'Tail (Construction Maybe a))
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Tail) (Construction Maybe) a
-> Tagged 'Tail (Construction Maybe a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (Maybe :. Construction Maybe) := a
xs) =
		(((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
  :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
 := (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
   :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
  := (<:.>) (Tagged 'Tail) (Construction Maybe) a)
 -> Store
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      ((<:.>) (Tagged 'Tail) (Construction Maybe) a))
-> (((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
     :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
    := (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> Store
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     ((<:.>) (Tagged 'Tail) (Construction Maybe) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ ((Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (Maybe :. Construction Maybe) := a
xs TU Covariant Covariant Maybe (Construction Maybe) a
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> ((:*:) (TU Covariant Covariant Maybe (Construction Maybe) a)
    :. (->) (TU Covariant Covariant Maybe (Construction Maybe) a))
   := (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall s a. s -> a -> Product s a
:*: Construction Maybe a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> (<:.>) (Tagged 'Tail) (Construction Maybe) a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> Construction Maybe a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (<:.>) (Tagged 'Tail) (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. 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)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (Maybe :. Construction Maybe) := a)
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run

type instance Zipper List = Tap (List <:.:> List := (:*:))

instance {-# OVERLAPS #-} Traversable (Tap (List <:.:> List := (:*:))) where
	Tap a
x (T_U (List a
future :*: List a
past)) ->> :: Tap ((List <:.:> List) := (:*:)) a
-> (a -> u b) -> (u :. Tap ((List <:.:> List) := (:*:))) := b
->> a -> u b
f = (\Reverse List b
past' b
x' TU Covariant Covariant Maybe (Construction Maybe) b
future' -> b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
x' ((:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Maybe) b
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (TU Covariant Covariant Maybe (Construction Maybe) b
 -> TU Covariant Covariant Maybe (Construction Maybe) b
 -> (:=) (List <:.:> List) (:*:) b)
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *). Category m => m ~~> m
/ TU Covariant Covariant Maybe (Construction Maybe) b
future' (TU Covariant Covariant Maybe (Construction Maybe) b
 -> (:=) (List <:.:> List) (:*:) b)
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *). Category m => m ~~> m
/ Reverse List b -> Primary (Reverse List) b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Reverse List b
past')
		(Reverse List b
 -> b
 -> TU Covariant Covariant Maybe (Construction Maybe) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> u (Reverse List b)
-> u (b
      -> TU Covariant Covariant Maybe (Construction Maybe) b
      -> Tap ((List <:.:> List) := (:*:)) b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> List a -> Reverse List a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse List a
past Reverse List a -> (a -> u b) -> u (Reverse List b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f u (b
   -> TU Covariant Covariant Maybe (Construction Maybe) b
   -> Tap ((List <:.:> List) := (:*:)) b)
-> u b
-> u (TU Covariant Covariant Maybe (Construction Maybe) b
      -> Tap ((List <:.:> List) := (:*:)) b)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> a -> u b
f a
x u (TU Covariant Covariant Maybe (Construction Maybe) b
   -> Tap ((List <:.:> List) := (:*:)) b)
-> u (TU Covariant Covariant Maybe (Construction Maybe) b)
-> (u :. Tap ((List <:.:> List) := (:*:))) := b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> List a
future List a
-> (a -> u b)
-> u (TU Covariant Covariant Maybe (Construction Maybe) b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f

instance {-# OVERLAPS #-} Extendable (Tap (List <:.:> List := (:*:))) where
	Tap ((List <:.:> List) := (:*:)) a
z =>> :: Tap ((List <:.:> List) := (:*:)) a
-> (Tap ((List <:.:> List) := (:*:)) a -> b)
-> Tap ((List <:.:> List) := (:*:)) b
=>> Tap ((List <:.:> List) := (:*:)) a -> b
f = let move :: (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
move Tap ((List <:.:> List) := (:*:)) a
-> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
rtt = ((Maybe :. Construction Maybe)
 := Tap ((List <:.:> List) := (:*:)) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe :. Construction Maybe)
  := Tap ((List <:.:> List) := (:*:)) a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (Tap ((List <:.:> List) := (:*:)) a))
-> (Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
    -> (Maybe :. Construction Maybe)
       := Tap ((List <:.:> List) := (:*:)) a)
-> Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
-> (Maybe :. Construction Maybe)
   := Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct (Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Construction Maybe)
      (Tap ((List <:.:> List) := (:*:)) a))
-> Construction Maybe (Tap ((List <:.:> List) := (:*:)) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
-> Maybe (Tap ((List <:.:> List) := (:*:)) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
 -> Maybe (Tap ((List <:.:> List) := (:*:)) a))
-> (Tap ((List <:.:> List) := (:*:)) a
    -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> Tap ((List <:.:> List) := (:*:)) a
-> Maybe (Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tap ((List <:.:> List) := (:*:)) a
-> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a
rtt (Tap ((List <:.:> List) := (:*:)) a
 -> Maybe (Tap ((List <:.:> List) := (:*:)) a))
-> Tap ((List <:.:> List) := (:*:)) a :=> Construction Maybe
forall (t :: * -> *) a.
Covariant t =>
(a :=> t) -> a :=> Construction t
.-+ Tap ((List <:.:> List) := (:*:)) a
z in
		b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (b
 -> (:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> b
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *). Category m => m ~~> m
/ Tap ((List <:.:> List) := (:*:)) a -> b
f Tap ((List <:.:> List) := (:*:)) a
z ((:=) (List <:.:> List) (:*:) b
 -> Tap ((List <:.:> List) := (:*:)) b)
-> (:=) (List <:.:> List) (:*:) b
-> Tap ((List <:.:> List) := (:*:)) b
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant Maybe (Construction Maybe) b
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (TU Covariant Covariant Maybe (Construction Maybe) b
 -> TU Covariant Covariant Maybe (Construction Maybe) b
 -> (:=) (List <:.:> List) (:*:) b)
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *). Category m => m ~~> m
/ Tap ((List <:.:> List) := (:*:)) a -> b
f (Tap ((List <:.:> List) := (:*:)) a -> b)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
-> TU Covariant Covariant Maybe (Construction Maybe) b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
move (forall a (f :: a) (t :: * -> *).
Morphable ('Rotate f) t =>
t ~> Morphing ('Rotate f) t
forall (t :: * -> *).
Morphable ('Rotate 'Left) t =>
t ~> Morphing ('Rotate 'Left) t
rotate @Left) (TU Covariant Covariant Maybe (Construction Maybe) b
 -> (:=) (List <:.:> List) (:*:) b)
-> TU Covariant Covariant Maybe (Construction Maybe) b
-> (:=) (List <:.:> List) (:*:) b
forall (m :: * -> * -> *). Category m => m ~~> m
/ Tap ((List <:.:> List) := (:*:)) a -> b
f (Tap ((List <:.:> List) := (:*:)) a -> b)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
-> TU Covariant Covariant Maybe (Construction Maybe) b
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> (Tap ((List <:.:> List) := (:*:)) a
 -> (<:.>) Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Tap ((List <:.:> List) := (:*:)) a)
move (forall a (f :: a) (t :: * -> *).
Morphable ('Rotate f) t =>
t ~> Morphing ('Rotate f) t
forall (t :: * -> *).
Morphable ('Rotate 'Right) t =>
t ~> Morphing ('Rotate 'Right) t
rotate @Right)

instance Focusable Head (Tap (List <:.:> List := (:*:))) where
	type Focusing Head (Tap (List <:.:> List := (:*:))) a = a
	focusing :: Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a)
:-. Focusing 'Head (Tap ((List <:.:> List) := (:*:))) a
focusing (Tap ((List <:.:> List) := (:*:)) a <:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Tap ((List <:.:> List) := (:*:)) a
zipper) = (((:*:) a :. (->) a)
 := Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a))
-> Store a (Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a)
  := Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a))
 -> Store a (Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a)))
-> (((:*:) a :. (->) a)
    := Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a))
-> Store a (Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a <:= Tap ((List <:.:> List) := (:*:))
forall (t :: * -> *) a. Extractable t => a <:= t
extract Tap ((List <:.:> List) := (:*:)) a
zipper a
-> (a -> Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a))
-> ((:*:) a :. (->) a)
   := Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a)
forall s a. s -> a -> Product s a
:*: Tap ((List <:.:> List) := (:*:)) a
-> Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Tap ((List <:.:> List) := (:*:)) a
 -> Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a))
-> (a -> Tap ((List <:.:> List) := (:*:)) a)
-> a
-> Tagged 'Head (Tap ((List <:.:> List) := (:*:)) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> (:=) (List <:.:> List) (:*:) a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> (:=) (List <:.:> List) (:*:) a
-> a
-> Tap ((List <:.:> List) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% Tap ((List <:.:> List) := (:*:)) a
-> (:=) (List <:.:> List) (:*:) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower Tap ((List <:.:> List) := (:*:)) a
zipper

instance Morphable (Rotate Left) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Rotate Left) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper List
	morphing :: (<:.>)
  (Tagged ('Rotate 'Left)) (Tap ((List <:.:> List) := (:*:))) a
-> Morphing ('Rotate 'Left) (Tap ((List <:.:> List) := (:*:))) a
morphing ((<:.>)
  (Tagged ('Rotate 'Left)) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (List a
future :*: List a
past))) = ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU
		(((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
 -> TU
      Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> T_U Covariant Covariant (:*:) List List a
-> a
-> Tap ((List <:.:> List) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (List a -> Substructural 'Tail List a
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
subview @Tail List a
future) (a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x List a
past) (a -> Tap ((List <:.:> List) := (:*:)) a)
-> Maybe a -> (Maybe :. Tap ((List <:.:> List) := (:*:))) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens (List a) (Maybe a) -> List a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: * -> k) (t :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head) List a
future

instance Morphable (Rotate Right) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Rotate Right) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper List
	morphing :: (<:.>)
  (Tagged ('Rotate 'Right)) (Tap ((List <:.:> List) := (:*:))) a
-> Morphing ('Rotate 'Right) (Tap ((List <:.:> List) := (:*:))) a
morphing ((<:.>)
  (Tagged ('Rotate 'Right)) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (List a
future :*: List a
past))) = ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU
		(((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
 -> TU
      Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a)
-> ((Maybe :. Tap ((List <:.:> List) := (:*:))) := a)
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> T_U Covariant Covariant (:*:) List List a
-> a
-> Tap ((List <:.:> List) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x List a
future) (List a -> Substructural 'Tail List a
forall k (f :: k) (t :: * -> *).
Substructure f t =>
t ~> Substructural f t
subview @Tail List a
past) (a -> Tap ((List <:.:> List) := (:*:)) a)
-> Maybe a -> (Maybe :. Tap ((List <:.:> List) := (:*:))) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Lens (List a) (Maybe a) -> List a -> Maybe a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: * -> k) (t :: * -> *) a.
Focusable f t =>
t a :-. Focusing f t a
forall (t :: * -> *) a.
Focusable 'Head t =>
t a :-. Focusing 'Head t a
focus @Head) List a
past

instance Morphable (Into (Tap (List <:.:> List := (:*:)))) List where
	type Morphing (Into (Tap (List <:.:> List := (:*:)))) List = Maybe <:.> Zipper List
	morphing :: (<:.>) (Tagged ('Into (Tap ((List <:.:> List) := (:*:))))) List a
-> Morphing ('Into (Tap ((List <:.:> List) := (:*:)))) List a
morphing ((<:.>) (Tagged ('Into (Tap ((List <:.:> List) := (:*:))))) List a
-> List a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> List a
list) = (forall a (f :: a) (t :: * -> *).
Morphable ('Into f) t =>
t ~> Morphing ('Into f) t
forall (t :: * -> *).
Morphable ('Into (Zipper List)) t =>
t ~> Morphing ('Into (Zipper List)) t
into @(Zipper List) (Construction Maybe a -> Tap ((List <:.:> List) := (:*:)) a)
-> Maybe (Construction Maybe a)
-> Maybe (Tap ((List <:.:> List) := (:*:)) a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>) (Primary List a
 -> Primary
      (TU Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))))
      a)
-> List a
-> TU
     Covariant Covariant Maybe (Tap ((List <:.:> List) := (:*:))) a
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= List a
list

instance Morphable (Into List) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Into List) (Tap (List <:.:> List := (:*:))) = List
	morphing :: (<:.>) (Tagged ('Into List)) (Tap ((List <:.:> List) := (:*:))) a
-> Morphing ('Into List) (Tap ((List <:.:> List) := (:*:))) a
morphing ((<:.>) (Tagged ('Into List)) (Tap ((List <:.:> List) := (:*:))) a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (List a
future :*: List a
past))) = (List a
 :*: TU Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall a b. (a :*: b) -> a
attached ((List a
  :*: TU Covariant Covariant Maybe (Construction Maybe) (List a))
 -> List a)
-> (State
      (List a)
      (TU Covariant Covariant Maybe (Construction Maybe) (List a))
    -> List a
       :*: TU Covariant Covariant Maybe (Construction Maybe) (List a))
-> State
     (List a)
     (TU Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State (List a)) =>
State (List a) a -> Primary (State (List a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _)
		(State
   (List a)
   (TU Covariant Covariant Maybe (Construction Maybe) (List a))
 -> ((->) (List a) :. (:*:) (List a))
    := TU Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
-> State
     (List a)
     (TU Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
   :*: TU Covariant Covariant Maybe (Construction Maybe) (List a)
forall a b c. (a -> b -> c) -> b -> a -> c
% a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x List a
future (State
   (List a)
   (TU Covariant Covariant Maybe (Construction Maybe) (List a))
 -> List a)
-> State
     (List a)
     (TU Covariant Covariant Maybe (Construction Maybe) (List a))
-> List a
forall (m :: * -> * -> *). Category m => m ~~> m
$ List a
past List a
-> (a -> State (List a) (List a))
-> State
     (List a)
     (TU Covariant Covariant Maybe (Construction Maybe) (List a))
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> (List a -> List a) -> State (List a) (List a)
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify ((List a -> List a) -> State (List a) (List a))
-> (a :=:=> List) -> a -> State (List a) (List a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
(Morphable 'Push List,
 Morphing 'Push List ~ ((Identity <:.:> List) := (->))) =>
a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push @List

type instance Zipper (Construction Maybe) = Tap (Construction Maybe <:.:> Construction Maybe := (:*:))

instance {-# OVERLAPS #-} Traversable (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past)) ->> :: Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (a -> u b)
-> (u
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := b
->> a -> u b
f = (\Reverse (Construction Maybe) b
past' b
x' Construction Maybe b
future' -> b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap b
x' ((:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe b
-> Construction Maybe b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Maybe b
 -> Construction Maybe b
 -> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b)
-> Construction Maybe b
-> Construction Maybe b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
forall (m :: * -> * -> *). Category m => m ~~> m
/ Construction Maybe b
future' (Construction Maybe b
 -> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b)
-> Construction Maybe b
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) b
forall (m :: * -> * -> *). Category m => m ~~> m
/ Reverse (Construction Maybe) b
-> Primary (Reverse (Construction Maybe)) b
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run Reverse (Construction Maybe) b
past')
		(Reverse (Construction Maybe) b
 -> b
 -> Construction Maybe b
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> u (Reverse (Construction Maybe) b)
-> u (b
      -> Construction Maybe b
      -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Reverse (Construction Maybe) a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse Construction Maybe a
past Reverse (Construction Maybe) a
-> (a -> u b) -> u (Reverse (Construction Maybe) b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f u (b
   -> Construction Maybe b
   -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> u b
-> u (Construction Maybe b
      -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> a -> u b
f a
x u (Construction Maybe b
   -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) b)
-> u (Construction Maybe b)
-> (u
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := b
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> Construction Maybe a
future Construction Maybe a -> (a -> u b) -> u (Construction Maybe b)
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> a -> u b
f

instance Focusable Head (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Focusing Head (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) a = a
	focusing :: Tagged
  'Head
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
:-. Focusing
      'Head
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a
focusing (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
<:= Tagged 'Head
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper) = (((:*:) a :. (->) a)
 := Tagged
      'Head
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a))
-> Store
     a
     (Tagged
        'Head
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a)
  := Tagged
       'Head
       (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a))
 -> Store
      a
      (Tagged
         'Head
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)))
-> (((:*:) a :. (->) a)
    := Tagged
         'Head
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a))
-> Store
     a
     (Tagged
        'Head
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a <:= Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:))
forall (t :: * -> *) a. Extractable t => a <:= t
extract Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper a
-> (a
    -> Tagged
         'Head
         (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a))
-> ((:*:) a :. (->) a)
   := Tagged
        'Head
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
forall s a. s -> a -> Product s a
:*: Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> Tagged
     'Head
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
 -> Tagged
      'Head
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a))
-> (a
    -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> a
-> Tagged
     'Head
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
-> a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall a b c. (a -> b -> c) -> b -> a -> c
% Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper

instance Morphable (Rotate Left) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Rotate Left) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
	morphing :: (<:.>)
  (Tagged ('Rotate 'Left))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Rotate 'Left)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Rotate 'Left))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = ((Maybe
  :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
 := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe
   :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  := a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> ((Maybe
     :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
future) (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Construction Maybe a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Construction Maybe a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (Construction Maybe a
 -> Construction Maybe a
 -> T_U
      Covariant
      Covariant
      (:*:)
      (Construction Maybe)
      (Construction Maybe)
      a)
-> Construction Maybe a
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall a b c. (a -> b -> c) -> b -> a -> c
% a :=:=> Construction Maybe
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x Construction Maybe a
past (Construction Maybe a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Maybe (Construction Maybe a)
-> (Maybe
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
future

instance Morphable (Rotate Right) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Rotate Right) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
	morphing :: (<:.>)
  (Tagged ('Rotate 'Right))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Rotate 'Right)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Rotate 'Right))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = ((Maybe
  :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
 := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe
   :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  := a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> ((Maybe
     :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
past) (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Construction Maybe a
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Construction Maybe a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe a
-> Construction Maybe a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (a :=:=> Construction Maybe
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x Construction Maybe a
future) (Construction Maybe a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Maybe (Construction Maybe a)
-> (Maybe
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> Construction Maybe a -> Maybe (Construction Maybe a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Maybe a
past

instance Morphable (Into (Tap (List <:.:> List := (:*:)))) (Construction Maybe) where
	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Construction Maybe) = Zipper List
	morphing :: (<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Construction Maybe)
  a
-> Morphing
     ('Into (Tap ((List <:.:> List) := (:*:)))) (Construction Maybe) a
morphing ((<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Construction Maybe)
  a
-> Construction Maybe a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Construction Maybe a
ne) = a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> a
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *). Category m => m ~~> m
/ a <:= Construction Maybe
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Maybe a
ne (T_U Covariant Covariant (:*:) List List a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> T_U Covariant Covariant (:*:) List List a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (<:.:>) t u (:*:) a
twosome (List a -> List a -> T_U Covariant Covariant (:*:) List List a)
-> List a -> List a -> T_U Covariant Covariant (:*:) List List a
forall (m :: * -> * -> *). Category m => m ~~> m
/ Lens (Construction Maybe a) (List a)
-> Construction Maybe a -> List a
forall src tgt. Lens src tgt -> src -> tgt
view (forall k (f :: k) (t :: * -> *).
Substructure f t =>
t :~. Substructural f t
forall (t :: * -> *).
Substructure 'Tail t =>
t :~. Substructural 'Tail t
sub @Tail) Construction Maybe a
ne (List a -> T_U Covariant Covariant (:*:) List List a)
-> List a -> T_U Covariant Covariant (:*:) List List a
forall (m :: * -> * -> *). Category m => m ~~> m
/ List a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Morphable (Into (Tap (List <:.:> List := (:*:)))) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Into (Tap (List <:.:> List := (:*:)))) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Zipper List
	morphing :: (<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Into (Tap ((List <:.:> List) := (:*:))))
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Into (Tap ((List <:.:> List) := (:*:)))))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper) = a
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a
 -> (:=) (List <:.:> List) (:*:) a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> a
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *). Category m => m ~~> m
/ a <:= Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:))
forall (t :: * -> *) a. Extractable t => a <:= t
extract Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper ((:=) (List <:.:> List) (:*:) a
 -> Tap ((List <:.:> List) := (:*:)) a)
-> (:=) (List <:.:> List) (:*:) a
-> Tap ((List <:.:> List) := (:*:)) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ (Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Maybe a
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (Construction Maybe a
    -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> Product (Construction Maybe a) (Construction Maybe a)
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (v :: * -> * -> *) a b c d.
Bivariant v =>
(a -> b) -> (c -> d) -> v a c -> v b d
<-> Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift) (Primary ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
 -> Primary ((List <:.:> List) := (:*:)) a)
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
-> (:=) (List <:.:> List) (:*:) a
forall (t :: * -> *) (u :: * -> *) a b.
(Interpreted t, Interpreted u) =>
(Primary t a -> Primary u b) -> t a -> u b
||= Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
-> (:=) (Construction Maybe <:.:> Construction Maybe) (:*:) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
zipper

instance Morphable (Into (Tap (Construction Maybe <:.:> Construction Maybe := (:*:)))) (Tap (List <:.:> List := (:*:))) where
	type Morphing (Into (Tap (Construction Maybe <:.:> Construction Maybe := (:*:)))) (Tap (List <:.:> List := (:*:))) = Maybe <:.> Zipper (Construction Maybe)
	morphing :: (<:.>)
  (Tagged
     ('Into
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))))
  (Tap ((List <:.:> List) := (:*:)))
  a
-> Morphing
     ('Into
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:))))
     (Tap ((List <:.:> List) := (:*:)))
     a
morphing ((<:.>)
  (Tagged
     ('Into
        (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))))
  (Tap ((List <:.:> List) := (:*:)))
  a
-> Tap ((List <:.:> List) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap ((List <:.:> List) := (:*:)) a
zipper) = let spread :: t s -> t a -> t (Product s a)
spread t s
x t a
y = s -> a -> Product s a
forall s a. s -> a -> Product s a
(:*:) (s -> a -> Product s a) -> t s -> t (a -> Product s a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> t s
x t (a -> Product s a) -> t a -> t (Product s a)
forall (t :: * -> *) a b. Applicative t => t (a -> b) -> t a -> t b
<*> t a
y in ((Maybe
  :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
 := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
       (a :: k).
((t :. u) := a) -> TU ct cu t u a
TU (((Maybe
   :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  := a)
 -> TU
      Covariant
      Covariant
      Maybe
      (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
      a)
-> ((Maybe
     :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
    := a)
-> TU
     Covariant
     Covariant
     Maybe
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
forall (m :: * -> * -> *). Category m => m ~~> m
$ a
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (t :: * -> *) a. a -> t a -> Tap t a
Tap (a <:= Tap ((List <:.:> List) := (:*:))
forall (t :: * -> *) a. Extractable t => a <:= t
extract Tap ((List <:.:> List) := (:*:)) a
zipper) (T_U
   Covariant
   Covariant
   (:*:)
   (Construction Maybe)
   (Construction Maybe)
   a
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> (Product (Construction Maybe a) (Construction Maybe a)
    -> T_U
         Covariant
         Covariant
         (:*:)
         (Construction Maybe)
         (Construction Maybe)
         a)
-> Product (Construction Maybe a) (Construction Maybe a)
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Product (Construction Maybe a) (Construction Maybe a)
-> T_U
     Covariant
     Covariant
     (:*:)
     (Construction Maybe)
     (Construction Maybe)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U (Product (Construction Maybe a) (Construction Maybe a)
 -> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a)
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
-> (Maybe
    :. Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
   := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$> ((Product
  ((Maybe :. Construction Maybe) := a)
  ((Maybe :. Construction Maybe) := a)
-> (((Maybe :. Construction Maybe) := a)
    -> ((Maybe :. Construction Maybe) := a)
    -> Maybe (Product (Construction Maybe a) (Construction Maybe a)))
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (t :: * -> *) (u :: * -> *) a b.
Adjoint t u =>
t a -> (a -> u b) -> b
|- ((Maybe :. Construction Maybe) := a)
-> ((Maybe :. Construction Maybe) := a)
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (t :: * -> *) s a.
Applicative t =>
t s -> t a -> t (Product s a)
spread) (Product
   ((Maybe :. Construction Maybe) := a)
   ((Maybe :. Construction Maybe) := a)
 -> Maybe (Product (Construction Maybe a) (Construction Maybe a)))
-> (T_U Covariant Covariant (:*:) List List a
    -> Product
         ((Maybe :. Construction Maybe) := a)
         ((Maybe :. Construction Maybe) := a))
-> T_U Covariant Covariant (:*:) List List a
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction Maybe) a
 -> (Maybe :. Construction Maybe) := a)
-> (TU Covariant Covariant Maybe (Construction Maybe) a
    -> (Maybe :. Construction Maybe) := a)
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (v :: * -> * -> *) a b c d.
Bivariant v =>
(a -> b) -> (c -> d) -> v a c -> v b d
<-> TU Covariant Covariant Maybe (Construction Maybe) a
-> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run) (Product
   (TU Covariant Covariant Maybe (Construction Maybe) a)
   (TU Covariant Covariant Maybe (Construction Maybe) a)
 -> Product
      ((Maybe :. Construction Maybe) := a)
      ((Maybe :. Construction Maybe) := a))
-> (T_U Covariant Covariant (:*:) List List a
    -> Product
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         (TU Covariant Covariant Maybe (Construction Maybe) a))
-> T_U Covariant Covariant (:*:) List List a
-> Product
     ((Maybe :. Construction Maybe) := a)
     ((Maybe :. Construction Maybe) := a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant (:*:) List List a
-> Product
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (T_U Covariant Covariant (:*:) List List a
 -> Maybe (Product (Construction Maybe a) (Construction Maybe a)))
-> T_U Covariant Covariant (:*:) List List a
-> Maybe (Product (Construction Maybe a) (Construction Maybe a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ Tap ((List <:.:> List) := (:*:)) a
-> T_U Covariant Covariant (:*:) List List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant u) =>
t u ~> u
lower Tap ((List <:.:> List) := (:*:)) a
zipper)

instance Morphable (Into (Construction Maybe)) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Into (Construction Maybe)) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = Construction Maybe
	morphing :: (<:.>)
  (Tagged ('Into (Construction Maybe)))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Into (Construction Maybe))
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Into (Construction Maybe)))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = (Construction Maybe a
 :*: Construction Maybe (Construction Maybe a))
-> Construction Maybe a
forall a b. (a :*: b) -> a
attached ((Construction Maybe a
  :*: Construction Maybe (Construction Maybe a))
 -> Construction Maybe a)
-> (State
      (Construction Maybe a) (Construction Maybe (Construction Maybe a))
    -> Construction Maybe a
       :*: Construction Maybe (Construction Maybe a))
-> State
     (Construction Maybe a) (Construction Maybe (Construction Maybe a))
-> Construction Maybe a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted (State (Construction Maybe a)) =>
State (Construction Maybe a) a
-> Primary (State (Construction Maybe a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _)
		(State
   (Construction Maybe a) (Construction Maybe (Construction Maybe a))
 -> ((->) (Construction Maybe a) :. (:*:) (Construction Maybe a))
    := Construction Maybe (Construction Maybe a))
-> Construction Maybe a
-> State
     (Construction Maybe a) (Construction Maybe (Construction Maybe a))
-> Construction Maybe a
   :*: Construction Maybe (Construction Maybe a)
forall a b c. (a -> b -> c) -> b -> a -> c
% a :=:=> Construction Maybe
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x Construction Maybe a
future (State
   (Construction Maybe a) (Construction Maybe (Construction Maybe a))
 -> Construction Maybe a)
-> State
     (Construction Maybe a) (Construction Maybe (Construction Maybe a))
-> Construction Maybe a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a
past Construction Maybe a
-> (a -> State (Construction Maybe a) (Construction Maybe a))
-> State
     (Construction Maybe a) (Construction Maybe (Construction Maybe a))
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> (Construction Maybe a -> Construction Maybe a)
-> State (Construction Maybe a) (Construction Maybe a)
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify ((Construction Maybe a -> Construction Maybe a)
 -> State (Construction Maybe a) (Construction Maybe a))
-> (a :=:=> Construction Maybe)
-> a
-> State (Construction Maybe a) (Construction Maybe a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
(Morphable 'Push (Nonempty List),
 Morphing 'Push (Nonempty List)
 ~ ((Identity <:.:> Nonempty List) := (->))) =>
a :=:=> Nonempty List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push @(Nonempty List)

instance Morphable (Into List) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) where
	type Morphing (Into List) (Tap (Construction Maybe <:.:> Construction Maybe := (:*:))) = List
	morphing :: (<:.>)
  (Tagged ('Into List))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Morphing
     ('Into List)
     (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
     a
morphing ((<:.>)
  (Tagged ('Into List))
  (Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)))
  a
-> Tap ((Construction Maybe <:.:> Construction Maybe) := (:*:)) a
forall k (f :: k) (t :: * -> *).
Morphable f t =>
(Tagged f <:.> t) ~> t
premorph -> Tap a
x (T_U (Construction Maybe a
future :*: Construction Maybe a
past))) = (TU Covariant Covariant Maybe (Construction Maybe) a
 :*: Construction
       Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall a b. (a :*: b) -> a
attached ((TU Covariant Covariant Maybe (Construction Maybe) a
  :*: Construction
        Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> (State
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      (Construction
         Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
    -> TU Covariant Covariant Maybe (Construction Maybe) a
       :*: Construction
             Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> State
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (Construction
        Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
Interpreted
  (State (TU Covariant Covariant Maybe (Construction Maybe) a)) =>
State (TU Covariant Covariant Maybe (Construction Maybe) a) a
-> Primary
     (State (TU Covariant Covariant Maybe (Construction Maybe) a)) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run @(State _)
		(State
   (TU Covariant Covariant Maybe (Construction Maybe) a)
   (Construction
      Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
 -> ((->) (TU Covariant Covariant Maybe (Construction Maybe) a)
     :. (:*:) (TU Covariant Covariant Maybe (Construction Maybe) a))
    := Construction
         Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
-> State
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (Construction
        Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
   :*: Construction
         Maybe (TU Covariant Covariant Maybe (Construction Maybe) a)
forall a b c. (a -> b -> c) -> b -> a -> c
% a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push a
x (Construction Maybe a
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift Construction Maybe a
future) (State
   (TU Covariant Covariant Maybe (Construction Maybe) a)
   (Construction
      Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> State
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (Construction
        Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
-> TU Covariant Covariant Maybe (Construction Maybe) a
forall (m :: * -> * -> *). Category m => m ~~> m
$ Construction Maybe a
past Construction Maybe a
-> (a
    -> State
         (TU Covariant Covariant Maybe (Construction Maybe) a)
         (TU Covariant Covariant Maybe (Construction Maybe) a))
-> State
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (Construction
        Maybe (TU Covariant Covariant Maybe (Construction Maybe) a))
forall (t :: * -> *) (u :: * -> *) a b.
(Traversable t, Pointable u, Applicative u) =>
t a -> (a -> u b) -> (u :. t) := b
->> (TU Covariant Covariant Maybe (Construction Maybe) a
 -> TU Covariant Covariant Maybe (Construction Maybe) a)
-> State
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
modify ((TU Covariant Covariant Maybe (Construction Maybe) a
  -> TU Covariant Covariant Maybe (Construction Maybe) a)
 -> State
      (TU Covariant Covariant Maybe (Construction Maybe) a)
      (TU Covariant Covariant Maybe (Construction Maybe) a))
-> (a :=:=> List)
-> a
-> State
     (TU Covariant Covariant Maybe (Construction Maybe) a)
     (TU Covariant Covariant Maybe (Construction Maybe) a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. forall a.
(Morphable 'Push List,
 Morphing 'Push List ~ ((Identity <:.:> List) := (->))) =>
a :=:=> List
forall k (f :: k) (t :: * -> *) a.
(Morphable f t, Morphing f t ~ ((Identity <:.:> t) := (->))) =>
a :=:=> t
item @Push @List

instance Monotonic a (Maybe <:.> Construction Maybe := a) where
	reduce :: (a -> r -> r) -> r -> (List := a) -> r
reduce a -> r -> r
f r
r = (a -> r -> r) -> r -> ((Maybe :. Construction Maybe) := a) -> r
forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r
reduce a -> r -> r
f r
r (((Maybe :. Construction Maybe) := a) -> r)
-> ((List := a) -> (Maybe :. Construction Maybe) := a)
-> (List := a)
-> r
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (List := a) -> (Maybe :. Construction Maybe) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run