Safe Haskell	None
Language	GHC2024

Proarrow.Category.Monoidal.Strictified

Contents

Orphan instances

Description

The strictification of a monoidal category: objects are lists of objects of k, tensoring is list concatenation, and a morphism as ~> bs is a Fold as ~> Fold bs in k (the Strictified arrow). Unitors and associators become identities, which makes composing long tensor expressions, string diagrams in particular, much more convenient.

Synopsis

(==) :: forall k (a :: k) (b :: k) (c :: k). CategoryOf k => (a ~> b) -> (b ~> c) -> a ~> c
type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...
data SList (as :: [a]) where
- SNil :: forall {a}. SList ('[] :: [a])
- SSing :: forall {a} (a1 :: a). Ob a1 => SList '[a1]
- SCons :: forall {a} (a1 :: a) (as1 :: [a]) (bs :: [a]) (b :: a). (Ob a1, Ob as1, Ob bs, as1 ~ (b ': bs)) => SList (a1 ': as1)
class (CategoryOf k, Obs as, Strictly as) => IsList (as :: [k]) where
- listCase :: (as ~ ('[] :: [k]) => r) -> (forall (a :: k). (Ob a, as ~ '[a]) => r) -> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]). (Ob b, Ob bs, Ob cs, as ~ (b ': bs), bs ~ (c ': cs)) => r) -> r
- sList :: SList as
- withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList (as ++ bs) => r) -> r
- swap1 :: forall (b :: k). (Ob b, SymMonoidal k) => (as ++ '[b]) ~> (b ': as)
- swap1Inv :: forall (b :: k). (Ob b, SymMonoidal k) => (b ': as) ~> (as ++ '[b])
- swap' :: forall (bs :: [k]). (IsList bs, SymMonoidal k) => (as ++ bs) ~> (bs ++ as)
type family Fold (as :: [k]) :: k where ...
fold :: forall {k} (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as)
withObFold :: forall {k} (as :: [k]) r. (Monoidal k, Ob as) => (Ob (Fold as) => r) -> r
type family Obs (as :: [k]) where ...
withObs :: forall {k} (as :: [k]) r. (Monoidal k, Ob as) => (Obs as => r) -> r
concatFold :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs, Monoidal k) => (Fold as ** Fold bs) ~> Fold (as ++ bs)
splitFold :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs, Monoidal k) => Fold (as ++ bs) ~> (Fold as ** Fold bs)
foldAppendCase :: forall {k} (as :: [k]) (bs :: [k]) r. (Ob as, Ob bs, Monoidal k) => (Fold (as ++ bs) ~ (Fold as ** Fold bs) => r) -> r -> r
splitThen :: forall {k} (as :: [k]) (bs :: [k]) (x :: k). (Ob as, Ob bs, Monoidal k) => ((Fold as ** Fold bs) ~> x) -> Fold (as ++ bs) ~> x
thenConcat :: forall {k} (as :: [k]) (bs :: [k]) (x :: k). (Ob as, Ob bs, Monoidal k) => (x ~> (Fold as ** Fold bs)) -> x ~> Fold (as ++ bs)
data Strictified (as :: [k]) (bs :: [k]) where
- Str :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs) => {..} -> Strictified as bs
singleton :: forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> '[a] ~> '[b]
obj1 :: forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a]
concatMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => as ~> '[Fold as]
splitMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => '[Fold as] ~> as
swap2 :: forall {k} (a :: k) (b :: k). (SymMonoidal k, Ob a, Ob b) => '[a, b] ~> '[b, a]

Documentation

(==) :: forall k (a :: k) (b :: k) (c :: k). CategoryOf k => (a ~> b) -> (b ~> c) -> a ~> c infixl 7 Source Github #

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ... Source Github #

Equations

('[] :: [k]) ++ (bs :: [k]) = bs
(a ': as :: [k]) ++ (bs :: [k]) = a ': (as ++ bs)

data SList (as :: [a]) where Source Github #

Constructors

SNil :: forall {a}. SList ('[] :: [a])
SSing :: forall {a} (a1 :: a). Ob a1 => SList '[a1]
SCons :: forall {a} (a1 :: a) (as1 :: [a]) (bs :: [a]) (b :: a). (Ob a1, Ob as1, Ob bs, as1 ~ (b ': bs)) => SList (a1 ': as1)

class (CategoryOf k, Obs as, Strictly as) => IsList (as :: [k]) where Source Github #

Methods

listCase :: (as ~ ('[] :: [k]) => r) -> (forall (a :: k). (Ob a, as ~ '[a]) => r) -> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]). (Ob b, Ob bs, Ob cs, as ~ (b ': bs), bs ~ (c ': cs)) => r) -> r Source Github #

sList :: SList as Source Github #

withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList (as ++ bs) => r) -> r Source Github #

swap1 :: forall (b :: k). (Ob b, SymMonoidal k) => (as ++ '[b]) ~> (b ': as) Source Github #

swap1Inv :: forall (b :: k). (Ob b, SymMonoidal k) => (b ': as) ~> (as ++ '[b]) Source Github #

swap' :: forall (bs :: [k]). (IsList bs, SymMonoidal k) => (as ++ bs) ~> (bs ++ as) Source Github #

Instances

Instances details

CategoryOf k => IsList ('[] :: [k]) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Strictified Methods listCase :: (('[] :: [k]) ~ ('[] :: [k]) => r) -> (forall (a :: k). (Ob a, ('[] :: [k]) ~ '[a]) => r) -> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]). (Ob b, Ob bs, Ob cs, ('[] :: [k]) ~ (b ': bs), bs ~ (c ': cs)) => r) -> r Source Github # sList :: SList ('[] :: [k]) Source Github # withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList (('[] :: [k]) ++ bs) => r) -> r Source Github # swap1 :: forall (b :: k). (Ob b, SymMonoidal k) => (('[] :: [k]) ++ '[b]) ~> '[b] Source Github # swap1Inv :: forall (b :: k). (Ob b, SymMonoidal k) => '[b] ~> (('[] :: [k]) ++ '[b]) Source Github # swap' :: forall (bs :: [k]). (IsList bs, SymMonoidal k) => (('[] :: [k]) ++ bs) ~> (bs ++ ('[] :: [k])) Source Github #
(Ob a, CategoryOf k) => IsList ('[a] :: [k]) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Strictified Methods listCase :: ('[a] ~ ('[] :: [k]) => r) -> (forall (a0 :: k). (Ob a0, '[a] ~ '[a0]) => r) -> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]). (Ob b, Ob bs, Ob cs, '[a] ~ (b ': bs), bs ~ (c ': cs)) => r) -> r Source Github # sList :: SList '[a] Source Github # withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList ('[a] ++ bs) => r) -> r Source Github # swap1 :: forall (b :: k). (Ob b, SymMonoidal k) => ('[a] ++ '[b]) ~> '[b, a] Source Github # swap1Inv :: forall (b :: k). (Ob b, SymMonoidal k) => '[b, a] ~> ('[a] ++ '[b]) Source Github # swap' :: forall (bs :: [k]). (IsList bs, SymMonoidal k) => ('[a] ++ bs) ~> (bs ++ '[a]) Source Github #
(Ob a1, IsList (a2 ': as), IsList as) => IsList (a1 ': (a2 ': as) :: [k]) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Strictified Methods listCase :: ((a1 ': (a2 ': as)) ~ ('[] :: [k]) => r) -> (forall (a :: k). (Ob a, (a1 ': (a2 ': as)) ~ '[a]) => r) -> (forall (b :: k) (bs :: [k]) (c :: k) (cs :: [k]). (Ob b, Ob bs, Ob cs, (a1 ': (a2 ': as)) ~ (b ': bs), bs ~ (c ': cs)) => r) -> r Source Github # sList :: SList (a1 ': (a2 ': as)) Source Github # withIsList2 :: forall (bs :: [k]) r. IsList bs => (IsList ((a1 ': (a2 ': as)) ++ bs) => r) -> r Source Github # swap1 :: forall (b :: k). (Ob b, SymMonoidal k) => ((a1 ': (a2 ': as)) ++ '[b]) ~> (b ': (a1 ': (a2 ': as))) Source Github # swap1Inv :: forall (b :: k). (Ob b, SymMonoidal k) => (b ': (a1 ': (a2 ': as))) ~> ((a1 ': (a2 ': as)) ++ '[b]) Source Github # swap' :: forall (bs :: [k]). (IsList bs, SymMonoidal k) => ((a1 ': (a2 ': as)) ++ bs) ~> (bs ++ (a1 ': (a2 ': as))) Source Github #

type family Fold (as :: [k]) :: k where ... Source Github #

Equations

Fold ('[] :: [k]) = Unit :: k
Fold ('[a] :: [k]) = a
Fold (a ': as :: [k]) = a ** Fold as

fold :: forall {k} (as :: [k]). (Monoidal k, Ob as) => Obj (Fold as) Source Github #

withObFold :: forall {k} (as :: [k]) r. (Monoidal k, Ob as) => (Ob (Fold as) => r) -> r Source Github #

type family Obs (as :: [k]) where ... Source Github #

Equations

Obs ('[] :: [k]) = ()
Obs (a ': as :: [k]) = (Ob a, Obs as)

withObs :: forall {k} (as :: [k]) r. (Monoidal k, Ob as) => (Obs as => r) -> r Source Github #

concatFold :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs, Monoidal k) => (Fold as ** Fold bs) ~> Fold (as ++ bs) Source Github #

splitFold :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs, Monoidal k) => Fold (as ++ bs) ~> (Fold as ** Fold bs) Source Github #

foldAppendCase :: forall {k} (as :: [k]) (bs :: [k]) r. (Ob as, Ob bs, Monoidal k) => (Fold (as ++ bs) ~ (Fold as ** Fold bs) => r) -> r -> r Source Github #

Whether Fold (as ++ bs) already is Fold as ** Fold bs: when as is one object and bs is not empty.

splitThen :: forall {k} (as :: [k]) (bs :: [k]) (x :: k). (Ob as, Ob bs, Monoidal k) => ((Fold as ** Fold bs) ~> x) -> Fold (as ++ bs) ~> x Source Github #

Precompose splitFold, unless it is the identity.

thenConcat :: forall {k} (as :: [k]) (bs :: [k]) (x :: k). (Ob as, Ob bs, Monoidal k) => (x ~> (Fold as ** Fold bs)) -> x ~> Fold (as ++ bs) Source Github #

Postcompose concatFold, unless it is the identity.

data Strictified (as :: [k]) (bs :: [k]) where Source Github #

Constructors

Str
Fields :: forall {k} (as :: [k]) (bs :: [k]). (Ob as, Ob bs) => { unStr :: Fold as ~> Fold bs } -> Strictified as bs

Instances

Instances details

Monoidal k => Promonad (Strictified :: [k] -> [k] -> Type) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Strictified Methods id :: forall (a :: [k]). Ob a => Strictified a a Source Github # (.) :: forall (b :: [k]) (c :: [k]) (a :: [k]). Strictified b c -> Strictified a b -> Strictified a c Source Github #
Monoidal k => MonoidalProfunctor (Strictified :: [k] -> [k] -> Type) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Strictified Methods one :: Strictified (Unit :: [k]) (Unit :: [k]) Source Github # () :: forall (x1 :: [k]) (x2 :: [k]) (y1 :: [k]) (y2 :: [k]). Strictified x1 x2 -> Strictified y1 y2 -> Strictified (x1 y1) (x2 ** y2) Source Github #
Monoidal k => Profunctor (Strictified :: [k] -> [k] -> Type) Source Github #
Instance details Defined in Proarrow.Category.Monoidal.Strictified Methods dimap :: forall (c :: [k]) (a :: [k]) (b :: [k]) (d :: [k]). (c ~> a) -> (b ~> d) -> Strictified a b -> Strictified c d Source Github # lmap :: forall (c :: [k]) (a :: [k]) (b :: [k]). (c ~> a) -> Strictified a b -> Strictified c b Source Github # rmap :: forall (b :: [k]) (d :: [k]) (a :: [k]). (b ~> d) -> Strictified a b -> Strictified a d Source Github # (\\) :: forall (a :: [k]) (b :: [k]) r. ((Ob a, Ob b) => r) -> Strictified a b -> r Source Github #

singleton :: forall k (a :: k) (b :: k). CategoryOf k => (a ~> b) -> '[a] ~> '[b] Source Github #

obj1 :: forall {k} (a :: k). (Monoidal k, Ob a) => Obj '[a] Source Github #

concatMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => as ~> '[Fold as] Source Github #

splitMany :: forall {k} (as :: [k]). (Ob as, Monoidal k) => '[Fold as] ~> as Source Github #

swap2 :: forall {k} (a :: k) (b :: k). (SymMonoidal k, Ob a, Ob b) => '[a, b] ~> '[b, a] Source Github #

Orphan instances

Monoidal k => Monoidal [k] Source Github #

List concatenation as monoidal tensor.

Instance details

Associated Types

type Unit
Instance details Defined in Proarrow.Category.Monoidal.Strictified type Unit = '[] :: [k]

Methods

withOb2 :: forall (a :: [k]) (b :: [k]) r. (Ob a, Ob b) => (Ob (a ** b) => r) -> r Source Github #

leftUnitor :: forall (a :: [k]). Ob a => ((Unit :: [k]) ** a) ~> a Source Github #

leftUnitorInv :: forall (a :: [k]). Ob a => a ~> ((Unit :: [k]) ** a) Source Github #

rightUnitor :: forall (a :: [k]). Ob a => (a ** (Unit :: [k])) ~> a Source Github #

rightUnitorInv :: forall (a :: [k]). Ob a => a ~> (a ** (Unit :: [k])) Source Github #

associator :: forall (a :: [k]) (b :: [k]) (c :: [k]). (Ob a, Ob b, Ob c) => ((a ** b) ** c) ~> (a ** (b ** c)) Source Github #

associatorInv :: forall (a :: [k]) (b :: [k]) (c :: [k]). (Ob a, Ob b, Ob c) => (a ** (b ** c)) ~> ((a ** b) ** c) Source Github #

SymMonoidal k => SymMonoidal [k] Source Github #

Instance details

Methods

swap :: forall (a :: [k]) (b :: [k]). (Ob a, Ob b) => (a ** b) ~> (b ** a) Source Github #

Monoidal k => CategoryOf [k] Source Github #

The strictified monoidal category, making the unitors and associators identities.

Instance details

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Monoidal.Strictified type (~>) = Strictified :: [k] -> [k] -> Type