| Safe Haskell | None |
|---|---|
| Language | GHC2024 |
Proarrow.Core
Description
Synopsis
- type (+->) j k = k -> j -> Type
- type CAT k = k +-> k
- type OB k = k -> Constraint
- type Kind = Type
- class Any (a :: k)
- class Promonad ((~>) :: CAT k) => CategoryOf k where
- type Hom k = (~>) :: CAT k
- class (CategoryOf j, CategoryOf k) => Profunctor (p :: j +-> k) where
- type (:~>) (p :: k -> k1 -> Type) (q :: k -> k1 -> Type) = forall (a :: k) (b :: k1). p a b -> q a b
- (//) :: forall {k1} {k2} p (a :: k2) (b :: k1) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r
- lmap :: forall {j} {k} p (c :: k) (a :: k) (b :: j). Profunctor p => (c ~> a) -> p a b -> p c b
- rmap :: forall {j} {k} p (b :: j) (d :: j) (a :: k). Profunctor p => (b ~> d) -> p a b -> p a d
- dimapDefault :: forall {k} p (c :: k) (a :: k) (b :: k) (d :: k). Promonad p => p c a -> p b d -> p a b -> p c d
- class Profunctor p => Promonad (p :: k +-> k) where
- arr :: forall {k} p (a :: k) (b :: k). Promonad p => (a ~> b) -> p a b
- type Obj (a :: k) = a ~> a
- obj :: forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
- src :: forall {j} {k} (a :: k) (b :: j) p. Profunctor p => p a b -> Obj a
- tgt :: forall {k1} {k2} (a :: k2) (b :: k1) p. Profunctor p => p a b -> Obj b
- type family UN (w :: j -> k) (wa :: k) :: j
- type Is (w :: j -> k) (a :: k) = a ~ w (UN w a)
Type Infrastructure
Basic Type Definitions
type (+->) j k = k -> j -> Type infixr 0 Source Github #
The kind j +-> k of profunctors from category j to category k.
Note that this follows mathematical convention,
swapping the order compared to Haskell's contravariant-first ordering.
type OB k = k -> Constraint Source Github #
Object constraints for kind k.
Universal Constraint
class Any (a :: k) Source Github #
A constraint that's always satisfied, used as a default when no specific object constraints are needed.
Instances
| Any (a :: k) Source Github # | |
Defined in Proarrow.Core | |
Category Infrastructure
CategoryOf Class
class Promonad ((~>) :: CAT k) => CategoryOf k Source Github #
Establishes that k is a category by specifying the morphism type and object constraints.
Associated Types
type (~>) :: CAT k infixr 0 Source Github #
The type of morphisms in the category.
type Ob (a :: k) Source Github #
What constraints objects must satisfy.
Instances
| CategoryOf Nat Source Github # | The (augmented) simplex category is the category of finite ordinals and order preserving maps. | ||||||||
Defined in Proarrow.Category.Instance.Simplex Associated Types
| |||||||||
| CategoryOf Nat Source Github # | The category of qubits, to implement ZX calculus from quantum computing. | ||||||||
Defined in Proarrow.Category.Instance.ZX Associated Types
| |||||||||
| CategoryOf BOOL Source Github # | The category of 2 objects and one arrow between them, a.k.a. the walking arrow. | ||||||||
Defined in Proarrow.Category.Instance.Bool Associated Types
| |||||||||
| CategoryOf KIND Source Github # | The category of categories and profunctors between them. | ||||||||
Defined in Proarrow.Category.Instance.Cat Associated Types
| |||||||||
| CategoryOf CONSTRAINT Source Github # | The category of type class constraints. An arrow from constraint a to constraint b | means that a implies b, i.e. if a holds then b holds. | ||||||||
Defined in Proarrow.Category.Instance.Constraint Associated Types
| |||||||||
| CategoryOf COST Source Github # | Cost category. Categories enriched in the cost category are lawvere metric spaces. | ||||||||
Defined in Proarrow.Category.Instance.Cost Associated Types
| |||||||||
| CategoryOf FINREL Source Github # | |||||||||
Defined in Proarrow.Category.Instance.FinRel | |||||||||
| CategoryOf FINSET Source Github # | |||||||||
Defined in Proarrow.Category.Instance.FinSet | |||||||||
| CategoryOf LINEAR Source Github # | Category of linear functions. | ||||||||
Defined in Proarrow.Category.Instance.Linear | |||||||||
| CategoryOf POINTED Source Github # | The category of types with an added point and point-preserving morphisms. | ||||||||
Defined in Proarrow.Category.Instance.PointedHask | |||||||||
| CategoryOf VOID Source Github # | The category with no objects, the initial category. | ||||||||
Defined in Proarrow.Category.Instance.Zero Associated Types
| |||||||||
| CategoryOf DOT Source Github # | |||||||||
Defined in Proarrow.Tools.Diagrams.Dot | |||||||||
| CategoryOf () Source Github # | The category with one object, the terminal category. | ||||||||
Defined in Proarrow.Category.Instance.Unit Associated Types
| |||||||||
| CategoryOf Symbol Source Github # | |||||||||
Defined in Proarrow.Tools.Diagrams.Dot Associated Types
| |||||||||
| CategoryOf Type Source Github # | The category of Haskell types (a.k.a | ||||||||
Defined in Proarrow.Core Associated Types
| |||||||||
| HasPushouts k => CategoryOf (COSPAN k) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Cospan | |||||||||
| CategoryOf (CODISCRETE k) Source Github # | The codiscrete category has exactly one arrow between every object, every type of kind | ||||||||
Defined in Proarrow.Category.Instance.Discrete Associated Types
| |||||||||
| CategoryOf (DISCRETE k) Source Github # | The discrete category with only identity arrows, every type of kind | ||||||||
Defined in Proarrow.Category.Instance.Discrete | |||||||||
| CategoryOf k => CategoryOf (FAM k) Source Github # | The Fam construction a.k.a. the free coproduct completion of | ||||||||
Defined in Proarrow.Category.Instance.Fam | |||||||||
| CategoryOf (FIN n) Source Github # | The (thin) category of finite ordinals. An arrow from a to b means that a is less than or equal to b. | ||||||||
Defined in Proarrow.Category.Instance.Fin | |||||||||
| TracedMonoidal k => CategoryOf (INT k) Source Github # | The Int construction, a.k.a. the geometry of interaction, the free compact closed category on a traced monoidal category. | ||||||||
Defined in Proarrow.Category.Instance.IntConstruction Associated Types
| |||||||||
| Num a => CategoryOf (MatK a) Source Github # | The category of matrices with entries in a type | ||||||||
Defined in Proarrow.Category.Instance.Mat | |||||||||
| HasPullbacks k => CategoryOf (SPAN k) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Span | |||||||||
| CategoryOf k => CategoryOf (REV k) Source Github # | The reverse of the category of | ||||||||
Defined in Proarrow.Category.Monoidal.Rev | |||||||||
| CategoryOf k => CategoryOf (OPPOSITE k) Source Github # | The opposite category of the category of | ||||||||
Defined in Proarrow.Category.Opposite | |||||||||
| CategoryOf k => CategoryOf (COPROD k) Source Github # | The same category as the category of | ||||||||
Defined in Proarrow.Object.BinaryCoproduct | |||||||||
| CategoryOf k => CategoryOf (PROD k) Source Github # | The same category as the category of | ||||||||
Defined in Proarrow.Object.BinaryProduct | |||||||||
| CategoryOf k => CategoryOf (LIST k) Source Github # | The category of lists of arrows. | ||||||||
Defined in Proarrow.Profunctor.List | |||||||||
| Monoidal k => CategoryOf [k] Source Github # | The strictified monoidal category, making the unitors and associators identities. | ||||||||
Defined in Proarrow.Category.Monoidal.Strictified Associated Types
| |||||||||
| CategoryOf (ADJK a b) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Adj | |||||||||
| CategoryOf (PROFK j k) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Prof | |||||||||
| (Applicative f, CategoryOf k) => CategoryOf (AP f k) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Ap | |||||||||
| (CategoryOf j, CategoryOf k) => CategoryOf (COPRODUCT j k) Source Github # | The coproduct of two categories. | ||||||||
Defined in Proarrow.Category.Instance.Coproduct | |||||||||
| Promonad p => CategoryOf (KLEISLI p) Source Github # | Every promonad makes a category. | ||||||||
Defined in Proarrow.Category.Instance.Kleisli | |||||||||
| CategoryOf (j .-> k) Source Github # | The category of functors and natural transformations. | ||||||||
Defined in Proarrow.Category.Instance.Nat | |||||||||
| CategoryOf k => CategoryOf (SUBCAT ob) Source Github # | The subcategory with objects with instances of the given constraint | ||||||||
Defined in Proarrow.Category.Instance.Sub | |||||||||
| (j ~ '(), k ~ '()) => CategoryOf (Unit j k) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Terminal | |||||||||
| CategoryOf (j +-> k) Source Github # | The category of profunctors and natural transformations between them. | ||||||||
Defined in Proarrow.Category.Instance.Prof | |||||||||
| Monoid m => CategoryOf (MONOIDK m) Source Github # | A monoid as a one object category. | ||||||||
Defined in Proarrow.Monoid | |||||||||
| (CategoryOf k1, CategoryOf k2) => CategoryOf (k1, k2) Source Github # | The product of two categories. | ||||||||
Defined in Proarrow.Category.Instance.Product | |||||||||
| CategoryOf (k1 -> k2 -> k3 -> k4 -> Type) Source Github # | The category of functors with target category k2 -> k3 -> k4 -> Type. | ||||||||
Defined in Proarrow.Category.Instance.Nat | |||||||||
| CategoryOf (k1 -> k2 -> k3 -> Type) Source Github # | The category of functors with target category | ||||||||
Defined in Proarrow.Category.Instance.Nat | |||||||||
| CategoryOf (k1 -> Type) Source Github # | The category of functors with target category Hask. | ||||||||
Defined in Proarrow.Category.Instance.Nat | |||||||||
| (CategoryOf k, Ob i, Ob j) => CategoryOf (PLAINK k i j) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.CategoryAsBi | |||||||||
| CategoryOf k => CategoryOf (MonK k i j) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.MonoidalAsBi | |||||||||
| SelfAction k => CategoryOf (STT' k i j) Source Github # | |||||||||
Defined in Proarrow.Category.Equipment.Stateful | |||||||||
| Profunctor p => CategoryOf (COLLAGE p) Source Github # | The collage of a profunctor. | ||||||||
Defined in Proarrow.Category.Instance.Collage | |||||||||
| Adjunction adj => CategoryOf (DUPLOID adj) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Duploid | |||||||||
| Ok cs p => CategoryOf (FREE cs p) Source Github # | |||||||||
Defined in Proarrow.Category.Instance.Free | |||||||||
| (Bicategory kk, Ob0 kk k) => CategoryOf (ENDO kk k) Source Github # | |||||||||
Defined in Proarrow.Category.Monoidal.Endo | |||||||||
| (CategoryOf j, CategoryOf k) => CategoryOf (OPTIC j k c) Source Github # | |||||||||
Defined in Proarrow.Optic | |||||||||
| CategoryOf (DiscreteK ob j k) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Bidiscrete Associated Types
| |||||||||
| CategoryOf (kk j k2) => CategoryOf (COK kk j k2) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Co | |||||||||
| CategoryOf (kk k2 j) => CategoryOf (OPK kk j k2) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Op | |||||||||
| (CategoryOf (kk j k2), Bicategory kk) => CategoryOf (Path kk j k2) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Strictified Associated Types
| |||||||||
| CategoryOf (kk i j) => CategoryOf (HK kk i j) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Hom | |||||||||
| CategoryOf (kk i j) => CategoryOf (SUBCAT tag kk i j) Source Github # | The subcategory with objects with instances of the given constraint `IsOb tag`. | ||||||||
Defined in Proarrow.Category.Bicategory.Sub | |||||||||
| (CategoryOf (jj (Fst ik) (Fst jl)), CategoryOf (kk (Snd ik) (Snd jl))) => CategoryOf (PRODK jj kk ik jl) Source Github # | |||||||||
Defined in Proarrow.Category.Bicategory.Product | |||||||||
type Hom k = (~>) :: CAT k Source Github #
A type synonym for (~>) :: CAT k, the type of morphisms in the category of kind k.
Profunctors
Profunctor Class
class (CategoryOf j, CategoryOf k) => Profunctor (p :: j +-> k) where Source Github #
The core profunctor abstraction. A profunctor is contravariant in its first argument and covariant in its second argument.
Laws:
Minimal complete definition
Methods
dimap :: forall (c :: k) (a :: k) (b :: j) (d :: j). (c ~> a) -> (b ~> d) -> p a b -> p c d Source Github #
Map contravariantly over the first argument and covariantly over the second.
(\\) :: forall (a :: k) (b :: j) r. ((Ob a, Ob b) => r) -> p a b -> r infixl 1 Source Github #
Constraint elimination, extracts object constraints from a profunctor heteromorphism.
Instances
Natural Transformations
type (:~>) (p :: k -> k1 -> Type) (q :: k -> k1 -> Type) = forall (a :: k) (b :: k1). p a b -> q a b infixr 0 Source Github #
Natural transformation between profunctors.
Profunctor Utilities
(//) :: forall {k1} {k2} p (a :: k2) (b :: k1) r. Profunctor p => p a b -> ((Ob a, Ob b) => r) -> r infixr 0 Source Github #
Flipped version of (\\).
lmap :: forall {j} {k} p (c :: k) (a :: k) (b :: j). Profunctor p => (c ~> a) -> p a b -> p c b Source Github #
Left mapping (contravariant mapping over first argument).
rmap :: forall {j} {k} p (b :: j) (d :: j) (a :: k). Profunctor p => (b ~> d) -> p a b -> p a d Source Github #
Right mapping (covariant mapping over second argument).
Default Implementation
dimapDefault :: forall {k} p (c :: k) (a :: k) (b :: k) (d :: k). Promonad p => p c a -> p b d -> p a b -> p c d Source Github #
Default implementation of dimap for promonads using composition.
Promonads
Promonad Class
class Profunctor p => Promonad (p :: k +-> k) where Source Github #
A promonad is a category-like profunctor with identity morphisms and composition.
This is also known as a category structure, or an identity-on-objects functor.
Laws:
Methods
id :: forall (a :: k). Ob a => p a a Source Github #
Identity morphisms.
(.) :: forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p a c infixr 9 Source Github #
Composition (note the parameter order matches function composition).
Instances
Promonad Utilities
arr :: forall {k} p (a :: k) (b :: k). Promonad p => (a ~> b) -> p a b Source Github #
Lifts morphisms from the base category into the promonad.
Object Identities
obj :: forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a Source Github #
The identity morphism for a given object.
Compared to id this makes the kind argument implicit,
allowing to write obj @a instead of id @k @a.
src :: forall {j} {k} (a :: k) (b :: j) p. Profunctor p => p a b -> Obj a Source Github #
Extract source identity morphism from a profunctor heteromorphism.
tgt :: forall {k1} {k2} (a :: k2) (b :: k1) p. Profunctor p => p a b -> Obj b Source Github #
Extract target identity morphism from a profunctor heteromorphism.
Type Family Utilities
Kind Unwrapping
type family UN (w :: j -> k) (wa :: k) :: j Source Github #
A helper type family to unwrap a wrapped kind. This is needed because the field selector functions of newtypes have to be lower case and therefore cannot be used at the type level.
Instances
| type UN 'FR ('FR n :: FINREL) Source Github # | |
Defined in Proarrow.Category.Instance.FinRel | |
| type UN 'FS ('FS n :: FINSET) Source Github # | |
Defined in Proarrow.Category.Instance.FinSet | |
| type UN 'K ('K k :: KIND) Source Github # | |
Defined in Proarrow.Category.Instance.Cat | |
| type UN 'CNSTRNT ('CNSTRNT a :: CONSTRAINT) Source Github # | |
Defined in Proarrow.Category.Instance.Constraint | |
| type UN 'L ('L a :: LINEAR) Source Github # | |
Defined in Proarrow.Category.Instance.Linear | |
| type UN 'P ('P a :: POINTED) Source Github # | |
Defined in Proarrow.Category.Instance.PointedHask | |
| type UN ('M :: Nat -> MatK a) ('M n :: MatK a) Source Github # | |
| type UN ('CS :: j -> COSPAN j) ('CS k :: COSPAN j) Source Github # | |
| type UN ('CD :: j -> CODISCRETE j) ('CD a :: CODISCRETE j) Source Github # | |
Defined in Proarrow.Category.Instance.Discrete | |
| type UN ('D :: j -> DISCRETE j) ('D a :: DISCRETE j) Source Github # | |
| type UN ('SP :: j -> SPAN j) ('SP k :: SPAN j) Source Github # | |
| type UN ('R :: j -> REV j) ('R a :: REV j) Source Github # | |
| type UN ('OP :: j -> OPPOSITE j) ('OP k :: OPPOSITE j) Source Github # | |
| type UN ('COPR :: j -> COPROD j) ('COPR k :: COPROD j) Source Github # | |
| type UN ('PR :: j -> PROD j) ('PR k :: PROD j) Source Github # | |
| type UN ('F :: j -> FK j) ('F a :: FK j) Source Github # | |
| type UN ('A :: j -> AP f j) ('A k :: AP f j) Source Github # | |
| type UN ('KL :: j -> KLEISLI p) ('KL k :: KLEISLI p) Source Github # | |
| type UN ('SUB :: j -> SUBCAT ob) ('SUB k :: SUBCAT ob) Source Github # | |
| type UN ('EMB :: j -> FREE cs p) ('EMB a :: FREE cs p) Source Github # | |
| type UN ('MK :: j1 -> MonK j1 i j2) ('MK k :: MonK j1 i j2) Source Github # | |
| type UN 'D ('D ss :: DOT) Source Github # | |
Defined in Proarrow.Tools.Diagrams.Dot | |
| type UN ('L :: [k] -> LIST k) ('L as :: LIST k) Source Github # | |
| type UN ('DEP_ :: (x +-> k) -> FAM k) ('DEP_ dx :: FAM k) Source Github # | |
| type UN ('PK :: (j +-> k) -> PROFK j k) ('PK p :: PROFK j k) Source Github # | |
| type UN ('NT :: (j -> k) -> j .-> k) ('NT f :: j .-> k) Source Github # | |
| type UN ('ST :: (k +-> k) -> STT' k i j) ('ST p :: STT' k i j) Source Github # | |
| type UN ('E :: kk k k -> ENDO kk k) ('E p :: ENDO kk k) Source Github # | |
| type UN ('CO :: kk j k2 -> COK kk j k2) ('CO k3 :: COK kk j k2) Source Github # | |
| type UN ('OP :: kk k2 j -> OPK kk j k2) ('OP k3 :: OPK kk j k2) Source Github # | |
| type UN ('HomK :: kk i j -> HK kk i j) ('HomK k3 :: HK kk i j) Source Github # | |
| type UN ('SUB :: kk i j -> SUBCAT tag kk i j) ('SUB p :: SUBCAT tag kk i j) Source Github # | |
| type UN ('AK :: Path ABK i j -> ADJK i j) ('AK ps :: ADJK i j) Source Github # | |