proarrow
Safe HaskellNone
LanguageGHC2024

Proarrow.Squares

Synopsis

Documentation

type SQ' (kk :: CAT c) (h :: c) (i :: c) (j :: c) (k :: c) = (kk k i, SUBCAT Tight kk j k) +-> (kk j h, SUBCAT Tight kk h i) Source Comments #

The kind of a square '(q, f) '(p, g).

h--f--i
|  v  |
p--@--q
|  v  |
j--g--k

type SQ (kk :: CAT c) = forall {h :: c} {i :: c} {j :: c} {k :: c}. SQ' kk h i j k Source Comments #

data Sq' (pf :: (kk j h, SUBCAT Tight kk h i)) (qg :: (kk k i, SUBCAT Tight kk j k)) where Source Comments #

Constructors

Sq :: forall {c} {kk1 :: CAT c} {h :: c} {i :: c} {j :: c} {k :: c} (p :: Path kk1 j h) (q :: Path kk1 k i) (f :: Path kk1 h i) (g :: Path kk1 j k). (Ob p, Ob q, IsTight f, IsTight g) => (O f p ~> O q g) -> Sq' '(p, 'SUB f :: SUBCAT Tight (Path kk1) h i) '(q, 'SUB g :: SUBCAT Tight (Path kk1) j k) 

Instances

Instances details
(Bicategory kk, Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k) => Profunctor (Sq' :: (kk j h, SUBCAT Tight kk h i) -> (kk k i, SUBCAT Tight kk j k) -> Type) Source Comments # 
Instance details

Defined in Proarrow.Squares

Methods

dimap :: forall (c0 :: (kk j h, SUBCAT Tight kk h i)) (a :: (kk j h, SUBCAT Tight kk h i)) (b :: (kk k i, SUBCAT Tight kk j k)) (d :: (kk k i, SUBCAT Tight kk j k)). (c0 ~> a) -> (b ~> d) -> Sq' a b -> Sq' c0 d Source Comments #

(\\) :: forall (a :: (kk j h, SUBCAT Tight kk h i)) (b :: (kk k i, SUBCAT Tight kk j k)) r. ((Ob a, Ob b) => r) -> Sq' a b -> r Source Comments #

type Sq (p :: kk j h) (q :: kk k i) (f :: kk h i) (g :: kk j k) = Sq' '(p, 'SUB f :: SUBCAT Tight kk h i) '(q, 'SUB g :: SUBCAT Tight kk j k) Source Comments #

object :: forall {k1} (kk :: CAT k1) (k2 :: k1). (Equipment kk, Ob0 kk k2) => Sq ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) Source Comments #

The empty square for an object.

K-----K
|     |
|     |
|     |
K-----K

hArr :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (p :: kk j k2) (q :: kk j k2). Equipment kk => (p ~> q) -> Sq (p '::: ('Nil :: Path kk k2 k2)) (q '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk j j) Source Comments #

Make a square from a horizontal proarrow

K-----K
|     |
p--@--q
|     |
J-----J

hId :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (p :: kk j k2). (Equipment kk, Ob p) => Sq (p '::: ('Nil :: Path kk k2 k2)) (p '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk j j) Source Comments #

A horizontal identity square.

J-----J
|     |
p-----p
|     |
K-----K

vArr :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2) (g :: kk j k2). (Equipment kk, IsTight f, IsTight g) => (f ~> g) -> Sq ('Nil :: Path kk j j) ('Nil :: Path kk k2 k2) (f '::: ('Nil :: Path kk k2 k2)) (g '::: ('Nil :: Path kk k2 k2)) Source Comments #

Make a square from a vertical arrow

J--f--K
|  v  |
|  @  |
|  v  |
J--g--K

vId :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2). (Equipment kk, IsTight f) => Sq ('Nil :: Path kk j j) ('Nil :: Path kk k2 k2) (f '::: ('Nil :: Path kk k2 k2)) (f '::: ('Nil :: Path kk k2 k2)) Source Comments #

A vertical identity square.

J--f--K
|  v  |
|  |  |
|  v  |
J--f--K

(|||) :: forall {k} {b :: k} {c1 :: k} {c2 :: k} {kk :: CAT k} {h :: k} {l :: k} {m :: k} (ps :: Path kk m l) (qs :: Path kk b h) (rs :: Path kk c1 c2) (ds :: Path kk l h) (es :: Path kk m b) (fs :: Path kk h c2) (gs :: Path kk b c1). Equipment kk => Sq ps qs ds es -> Sq qs rs fs gs -> Sq ps rs (ds +++ fs) (es +++ gs) infixl 6 Source Comments #

Horizontal composition

L--d--H     H--f--I     L-d+f-I
|  v  |     |  v  |     |  v  |
p--@--q ||| q--@--r  =  p--@--r
|  v  |     |  v  |     |  v  |
M--e--J     J--g--K     M-e+g-K

(===) :: forall {k1} {k2 :: k1} {b :: k1} {kk :: CAT k1} {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path kk l j) (qs :: Path kk k2 b) (rs :: Path kk j h) (ss :: Path kk b i) (es :: Path kk h i) (fs :: Path kk j b) (gs :: Path kk l k2). Equipment kk => Sq rs ss es fs -> Sq ps qs fs gs -> Sq (ps +++ rs) (qs +++ ss) es gs infixl 5 Source Comments #

Vertical composition

 H--e--I
 |  v  |
 r--@--s
 |  v  |
 J--f--K
   ===
 J--f--K
 |  v  |
 p--@--q
 |  v  |
 L--g--M

   v v

 H--e--I
 |  v  |
p+r-@-q+s
 |  v  |
 J--g--K

toRight :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2). (Equipment kk, IsTight f) => Sq ('Nil :: Path kk j j) (f '::: ('Nil :: Path kk k2 k2)) (f '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk j j) Source Comments #

Bend a vertical arrow in the companion direction.

J--f--K
|  v  |
|  \->f
|     |
J-----J

toLeft :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2) (f' :: kk k2 j). (Equipment kk, TightPair f f') => Sq (f' '::: ('Nil :: Path kk j j)) ('Nil :: Path kk k2 k2) (f '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) Source Comments #

Bend a vertical arrow in the conjoint direction.

J--f--K
|  v  |
f<-/  |
|     |
K-----K

fromLeft :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2). (Equipment kk, IsTight f) => Sq (f '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) (f '::: ('Nil :: Path kk k2 k2)) Source Comments #

Bend a companion proarrow back to a vertical arrow.

K-----K
|     |
f>-\  |
|  v  |
J--f--K

fromRight :: forall {k1} {kk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: kk j k2) (f' :: kk k2 j). (Equipment kk, TightPair f f') => Sq ('Nil :: Path kk j j) (f' '::: ('Nil :: Path kk j j)) ('Nil :: Path kk j j) (f '::: ('Nil :: Path kk k2 k2)) Source Comments #

Bend a conjoint proarrow back to a vertical arrow.

J-----J
|     |
|  /-<f
|  v  |
J--f--K

vUnitor :: forall {k1} (kk :: CAT k1) (k2 :: k1). (Equipment kk, Ob0 kk k2) => Sq ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) ((I :: kk k2 k2) '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) Source Comments #

vUnitorInv :: forall {k1} (kk :: CAT k1) (k2 :: k1). (Equipment kk, Ob0 kk k2) => Sq ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) ('Nil :: Path kk k2 k2) ((I :: kk k2 k2) '::: ('Nil :: Path kk k2 k2)) Source Comments #

vCombine :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Equipment kk, IsTight p, IsTight q) => Sq ('Nil :: Path kk i i) ('Nil :: Path kk k2 k2) (p '::: (q '::: ('Nil :: Path kk k2 k2))) (O q p '::: ('Nil :: Path kk k2 k2)) Source Comments #

vSplit :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (p :: kk i j) (q :: kk j k2). (Equipment kk, IsTight p, IsTight q) => Sq ('Nil :: Path kk i i) ('Nil :: Path kk k2 k2) (O q p '::: ('Nil :: Path kk k2 k2)) (p '::: (q '::: ('Nil :: Path kk k2 k2))) Source Comments #

vCombineAll :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path kk j k2). (Equipment kk, IsTight ps) => Sq ('Nil :: Path kk j j) ('Nil :: Path kk k2 k2) ps (Fold ps '::: ('Nil :: Path kk k2 k2)) Source Comments #

Combine a whole bunch of vertical arrows into one composed arrow.

vSplitAll :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path kk j k2). (Equipment kk, IsTight ps) => Sq ('Nil :: Path kk j j) ('Nil :: Path kk k2 k2) (Fold ps '::: ('Nil :: Path kk k2 k2)) ps Source Comments #

Split one composed arrow into a whole bunch of vertical arrows.

J--f--K
|  v  |
| /@\ |
| vvv |
J-p..-K

hCombineAll :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path kk j k2). (Equipment kk, Ob ps) => Sq ps (Fold ps '::: ('Nil :: Path kk k2 k2)) ('Nil :: Path kk k2 k2) ('Nil :: Path kk j j) Source Comments #

Combine a whole bunch of horizontal proarrows into one composed proarrow.

K-----K
p--\  |
:--@--F
:--/  |
J-----J

hSplitAll :: forall {k1} {kk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path kk j k2). (Equipment kk, Ob ps) => Sq (Fold ps '::: ('Nil :: Path kk k2 k2)) ps ('Nil :: Path kk k2 k2) ('Nil :: Path kk j j) Source Comments #

Split one composed proarrow into a whole bunch of horizontal proarrows.

K-----K
|  /--p
F--@--:
|  \--:
J-----J

type Optic (a :: kk z j) (b :: kk k1 z) (s :: kk x j) (t :: kk k1 x) = (IsTight a, IsCotight b, IsTight s, IsCotight t) => Sq (t '::: (s '::: ('Nil :: Path kk j j))) (b '::: (a '::: ('Nil :: Path kk j j))) ('Nil :: Path kk j j) ('Nil :: Path kk k1 k1) Source Comments #

Optics in proarrow equipments.

J-------J
s>--@-->a
|   @   |
t<--@--<b
K-------K

type ProfOptic (a :: z +-> j) (b :: k +-> z) (s :: x +-> j) (t :: k +-> x) = Optic ('PK a) ('PK b) ('PK s) ('PK t) Source Comments #

mkProfOptic :: forall {x} {j} {k} {z} (s :: x +-> j) (t :: k +-> x) (a :: z +-> j) (b :: k +-> z). ((s :.: t) :~> (a :.: b)) -> ProfOptic a b s t Source Comments #

type HaskOptic (a :: z -> j) (b :: z -> k) (s :: x -> j) (t :: x -> k) = ProfOptic (Star a) (Costar b) (Star s) (Costar t) Source Comments #

mkHaskOptic :: forall {z} {j} {k} {x} (a :: z -> j) (b :: z -> k) (s :: x -> j) (t :: x -> k). (Functor a, Functor b, Functor s, Functor t) => (forall (x1 :: x) r. Ob x1 => (forall (y :: z). Ob y => (s x1 ~> a y) -> (b y ~> t x1) -> r) -> r) -> HaskOptic a b s t Source Comments #

type Lens s t a b = HaskOptic ((,) a) ((,) b) ((,) s) ((,) t) Source Comments #

mkLens :: (s -> a) -> (s -> b -> t) -> Lens s t a b Source Comments #

type Prism s t a b = HaskOptic (Either a) (Either b) (Either s) (Either t) Source Comments #

mkPrism :: (s -> Either a t) -> (b -> t) -> Prism s t a b Source Comments #

data FlipApp (a :: k) (f :: k -> Type) Source Comments #

Constructors

FlipApp 

Fields

Instances

Instances details
Ob a => Functor (FlipApp a :: (k -> Type) -> Type) Source Comments # 
Instance details

Defined in Proarrow.Squares

Methods

map :: forall (a0 :: k -> Type) (b :: k -> Type). (a0 ~> b) -> FlipApp a a0 ~> FlipApp a b Source Comments #

type Traversal (s :: k) (t :: k) (a :: k1) (b :: k1) = HaskOptic (FlipApp a) (FlipApp b) (FlipApp s) (FlipApp t) Source Comments #

mkTraversal :: (Traversable f, Functor f) => Traversal (f a) (f b) a b Source Comments #