Copyright | (c) Edward Kmett 2008-2014 and Sjoerd Visscher 2014 |
---|---|
License | BSD3 |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
- Natural transformations
- Functors
- Functor composition
- Colim -| Const -| Lim
- Natural Isomorphisms
- Adjunctions
- Automatic Lifting
- Constraints
- Lens Esoterica
- Monoidal Categories
- Closed Categories
- Terminal and Initial Objects
- Copowers and Cartesian Categories
- Distributive bicartesian categories
- CCC's
- Monoidal Functors
- Monads
- Monoids
- Strength
- Identity functors
- Kan extensions
- Categories
- Candidates for Removal:
- Internals
This package explores category theory via a couple of non-standard tricks.
First, we use lens-style isomorphism-families to talk about most operations.
Second, we heavily abuse parametricity as a proxy for naturality.
This means that the category Nat that gets used throughout is a
particularly well-behaved. An inhabitant of Nat :: (i -> j) -> (i -> j) -> *
is required to be polymorphic in its argument.
Parametricity is a very strong notion of naturality. Notably, we
don't have to care if i or j are co -or- contravariant. (forall a. f a ~> g a)
respects _both_ -- at least so long as the functors
involved aren't GADTs.
Third, we use kind-indexing to pick the category. This means it is harder to talk about Kleisli categories, etc. but in exchange most of the category selection _just works_. A central working hypothesis of this code is that this is sufficient to talk about interesting categories, and it certainly results in less verbose code than more explicit encodings which clutter up every type class talking about the choice of category.
Here, much of the time the selection is implicit.
- type family Hom :: i -> i -> k
- type (~>) = (Hom :: i -> i -> *)
- type (^) a b = Internal Hom b a
- type Dom f = (Hom :: i -> i -> *)
- type Cod f = (Hom :: j -> j -> *)
- type Cod2 f = (Hom :: k -> k -> *)
- type Arr a = (Hom :: i -> i -> *)
- type Enriched k = (Hom :: i -> i -> j)
- type Internal k = (Hom :: i -> i -> i)
- type External k = (Hom :: i -> i -> *)
- type Natural k = (Hom :: (i -> j) -> (i -> j) -> *)
- newtype Nat f g = Nat {}
- nat2 :: (forall a b. f a b ~> g a b) -> f ~> g
- nat3 :: (forall a b c. f a b c ~> g a b c) -> f ~> g
- nat4 :: (forall a b c d. f a b c d ~> g a b c d) -> f ~> g
- runNat2 :: Nat (k1 -> k) k2 f g -> Hom k * (f a1 a) (g a1 a)
- runNat3 :: Nat (k2 -> k1 -> k) k3 f g -> Hom k * (f a2 a1 a) (g a2 a1 a)
- runNat4 :: Nat (k3 -> k2 -> k1 -> k) k4 f g -> Hom k * (f a3 a2 a1 a) (g a3 a2 a1 a)
- class Functor f where
- first :: Functor f => (a ~> b) -> f a c ~> f b c
- class Contravariant f where
- lmap :: Contravariant f => (a ~> b) -> f b c ~> f a c
- class (hom ~ Hom) => Composed hom | k -> hom where
- type · = Compose
- composed :: (Functor k1 k2 (p (Any k)), Contravariant (k1 -> k2) k p, Composed k1 (Hom k1 *), Composed k (Hom k *), Category k2 (Hom k2 *)) => (~>) k2 (p (f (g a)) (f1 (g1 a1))) (p (Compose k k3 k4 f g a) (Compose k1 k5 k6 f1 g1 a1))
- associateCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Functor k8 k3 f1, Functor k5 k1 f, Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k8 (Hom k8 *), Composed k5 (Hom k5 *), Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Category k3 (Hom k3 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p (Compose k1 k5 k2 f (Compose k5 k6 k2 g g1)) (Compose k3 k8 k4 f1 (Compose k8 k7 k4 g3 g2))) (p (Compose k1 k6 k2 (Compose k1 k5 k6 f g) g1) (Compose k3 k7 k4 (Compose k3 k8 k7 f1 g3) g2))
- whiskerComposeL :: (Functor k * (Hom k * (Any k)), Contravariant (k -> *) k (Hom k *), Composed k (Hom k *)) => Nat k k2 f g1 -> Nat k k1 (Compose k k2 k1 f g) (Compose k k2 k1 g1 g)
- whiskerComposeR :: (Functor x k f, Functor k * (Hom k * (Any k)), Contravariant (k -> *) k (Hom k *), Composed k (Hom k *)) => Nat x k1 g g1 -> Nat k k1 (Compose k x k1 f g) (Compose k x k1 f g1)
- lambdaCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Identity k3 (Id k3), Identity k1 (Id k1), Category k3 (Hom k3 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p b c) (p (Compose k1 k1 k2 (Id k1) b) (Compose k3 k3 k4 (Id k3) c))
- rhoCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Functor k4 k3 c, Functor k2 k1 b, Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Identity k4 (Id k4), Identity k2 (Id k2), Category k4 (Hom k4 *), Category k3 (Hom k3 *), Category k2 (Hom k2 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p b c) (p (Compose k1 k2 k2 b (Id k2)) (Compose k3 k4 k4 c (Id k4)))
- class LimC (f `·` p) => Post f p
- fmap1 :: forall p a b c. Post Functor p => (a ~> b) -> p c a ~> p c b
- contramap1 :: forall p a b c. Post Contravariant p => (a ~> b) -> p c b ~> p c a
- fmap2 :: forall p a b c d. Post (Post Functor) p => (a ~> b) -> p c d a ~> p c d b
- class (Functor p, Post Functor p) => Bifunctor p
- bimap :: (Bifunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p a c ~> p b d
- class (Contravariant p, Post Functor p) => Profunctor p
- dimap :: (Profunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p b c ~> p a d
- class (Contravariant p, Functor p) => Phantom p
- class (k ~ (~>)) => Cocomplete k where
- class (Const ~ k) => Constant k | j i -> k where
- class (hom ~ Hom) => Complete hom | j -> hom where
- type Iso s t a b = forall p. Profunctor p => p a b -> p s t
- type Iso' s a = Iso s s a a
- class (Functor f, Functor u) => f -| u | f -> u, u -> f where
- unitAdj :: (f -| u, Category (Dom u)) => a ~> u (f a)
- counitAdj :: (f -| u, Category (Dom f)) => f (u b) ~> b
- zipR :: (f -| u, Cartesian (Dom u), Cartesian (Cod u)) => Iso (u a * u b) (u a' * u b') (u (a * b)) (u (a' * b'))
- absurdL :: (f -| u, Initial z) => Iso z z (f z) (f z)
- cozipL :: (f -| u, Cocartesian (Cod u), Cocartesian (Cod f)) => Iso (f (a + b)) (f (a' + b')) (f a + f b) (f a' + f b')
- class Curried p e | p -> e, e -> p where
- curried :: (Curried p e, Curryable p a) => Iso (p a b ~> c) (p a' b' ~> c') (a ~> e b c) (a' ~> e b' c')
- ccc :: (Category (Cod2 p), Symmetric p, Curried p e, Curryable p a) => Iso (p i a ~> b) (p i' a' ~> b') (a ~> e i b) (a' ~> e i' b')
- class Cocurried f u | f -> u, u -> f where
- type Cocurryable u :: k -> Constraint
- cocurry :: (f a b ~> c) -> b ~> u c a
- uncocurry :: Cocurryable u c => (b ~> u c a) -> f a b ~> c
- cocurried :: (Cocurried f u, Cocurryable u c') => Iso (f a b ~> c) (f a' b' ~> c') (b ~> u c a) (b' ~> u c' a')
- class (hom ~ Hom) => Lifted hom where
- newtype a :- b :: Constraint -> Constraint -> * = Sub (a -> Dict b)
- data Dict $a :: Constraint -> * where
- (\\) :: a => (b -> r) -> (:-) a b -> r
- class (p, q) => p & q
- class p |- q where
- _Sub :: Iso (p :- q) (p' :- q') (Dict p -> Dict q) (Dict p' -> Dict q')
- _Implies :: Iso (p :- q) (p' :- q') (Dict (p |- q)) (Dict (p' |- q'))
- class Class b h | h -> b where
- class b :=> h | h -> b where
- newtype Get r a b = Get {}
- _Get :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k2 * a r) (Hom k4 * a1 r1)) (p (Get k1 k2 r a b) (Get k3 k4 r1 a1 b1))
- get :: (Category c, c ~ (~>)) => (Get a a a -> Get a s s) -> c s a
- newtype Beget r a b = Beget {}
- _Beget :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k2 * r b) (Hom k4 * r1 b1)) (p (Beget k1 k2 r a b) (Beget k3 k4 r1 a1 b1))
- beget :: (Category c, c ~ (~>)) => (Beget b b b -> Beget b t t) -> c b t
- (#) :: (Beget b b b -> Beget b t t) -> b -> t
- newtype Un p a b s t = Un {}
- _Un :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k1 * (p1 t s) (p1 b a)) (Hom k2 * (p2 t1 s1) (p2 b1 a1))) (p (Un i k1 p1 a b s t) (Un i1 k2 p2 a1 b1 s1 t1))
- un :: (Un p a b a b -> Un p a b s t) -> p t s -> p b a
- data Via a b s t where
- via :: forall a b r p c t u. Category p => (Via a b a b -> Via r (p c c) u t) -> (t -> u) -> r
- mapping :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s) (f' t) (f a) (f' b)
- lmapping :: (Contravariant f, Contravariant f', Category (Dom f)) => (Via s t s t -> Via s t a b) -> Iso (f s x) (f' t y) (f a x) (f' b y)
- swapping :: (Profunctor f, Profunctor f', Category (Dom f), Category (Cod2 f), Category (Cod2 f')) => (Via a b a b -> Via a b s t) -> Iso (f a s) (f' b t) (f s a) (f' t b)
- mapping1 :: (Post Functor f, Post Functor f', Category (Dom1 f)) => (Via a b a b -> Via a b s t) -> Iso (f i s) (f' j t) (f i a) (f' j b)
- firstly :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s x) (f' t y) (f a x) (f' b y)
- post :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (i ~> s) (j ~> t) (i ~> a) (j ~> b)
- pre :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (a ~> i) (b ~> j) (s ~> i) (t ~> j)
- newtype Self a b = Self {}
- _Self :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k1 * a b) (Hom k2 * a1 b1)) (p (Self k1 a b) (Self k2 a1 b1))
- class (Functor p, Profunctor (Cod2 p), Category (Cod2 p)) => Semitensor p where
- type Tensorable p :: x -> Constraint
- second :: Tensorable p c => (a ~> b) -> p c a ~> p c b
- associate :: (Tensorable p a, Tensorable p b, Tensorable p c, Tensorable p a', Tensorable p b', Tensorable p c') => Iso (p (p a b) c) (p (p a' b') c') (p a (p b c)) (p a' (p b' c'))
- type family I p :: x
- class Semitensor p => Tensor p where
- lambda :: (Tensorable p a, Tensorable p a') => Iso (p (I p) a) (p (I p) a') a a'
- rho :: (Tensorable p a, Tensorable p a') => Iso (p a (I p)) (p a' (I p)) a a'
- class Bifunctor p => Symmetric p where
- class (Profunctor (Internal k), Category k, k ~ Hom) => Closed k where
- class (One ~ t) => Terminal t | i -> t where
- class (Zero ~ t) => Initial t | i -> t where
- type family Copower :: i -> j -> j
- type * = (Copower :: i -> i -> i)
- class (h ~ (~>), Symmetric (* :: i -> i -> i), Semitensor (* :: i -> i -> i)) => Precartesian h | i -> h where
- class (h ~ (~>), Tensor (* :: i -> i -> i), Terminal (I (* :: i -> i -> i)), Precartesian h) => Cartesian h | i -> h
- class (h ~ (~>), Symmetric ((+) :: i -> i -> i), Semitensor ((+) :: i -> i -> i)) => Precocartesian h | i -> h where
- class (h ~ (~>), Tensor ((+) :: i -> i -> i), Initial (I ((+) :: i -> i -> i)), Precocartesian h) => Cocartesian h | i -> h
- class (Cartesian k, Cocartesian k) => Distributive k | i -> k where
- class (Cartesian k, Closed k, Curried * (Internal k), I (Internal k) ~ I *, Curryable * (I (Internal k))) => CCC k | x -> k
- class (Precartesian ((~>) :: x -> x -> *), Precartesian ((~>) :: y -> y -> *), Functor f) => Semimonoidal f where
- ap :: (Semimonoidal f, CCC (Dom f), CCC (Cod f), Curryable * (f (b ^ a))) => f (b ^ a) ~> (f b ^ f a)
- ap2Applicative :: Applicative f => (f a * f b) -> f (a * b)
- class (Cartesian ((~>) :: x -> x -> *), Cartesian ((~>) :: y -> y -> *), Semimonoidal f) => Monoidal f where
- return :: (Monoidal f, Strength f, CCC (Dom f), Tensorable * a) => a ~> f a
- class (Precocartesian ((~>) :: x -> x -> *), Precocartesian ((~>) :: y -> y -> *), Functor f) => Cosemimonoidal f where
- class (Cocartesian ((~>) :: x -> x -> *), Cocartesian ((~>) :: y -> y -> *), Cosemimonoidal f) => Comonoidal f where
- class Semimonoidal (m :: x -> x) => Semimonad m where
- class (Monoidal m, Semimonad m) => Monad m
- class (Functor f, Category (Dom f)) => Cosemimonad f where
- class Cosemimonad f => Comonad f where
- class Precartesian (Arr m) => Semigroup m where
- multM :: (Semimonoidal u, Semigroup m) => (u m * u m) ~> u m
- class (Semigroup m, Cartesian (Arr m)) => Monoid m where
- oneM :: (Monoidal u, Monoid m) => One ~> u m
- mappend :: (Semigroup m, CCC (Arr m), Curryable * m) => m ~> (m ^ m)
- class Precocartesian (Arr m) => Cosemigroup m where
- zeroOp :: (Comonoidal f, Comonoid m) => f m ~> Zero
- class (Cosemigroup m, Cocartesian (Arr m)) => Comonoid m where
- comultOp :: (Cosemimonoidal f, Cosemigroup m) => f m ~> (f m + f m)
- class Functor f => Strength f where
- class Functor f => Costrength f where
- costrength :: f (a + b) ~> (a + f b)
- class (f -| f, Id ~ f) => Identity f | i -> f where
- class (c ~ Hom) => HasRan c | k -> c where
- type Ran :: (i -> j) -> (i -> k) -> j -> k
- ranCurried :: Dict (Curried Compose (Ran :: (i -> j) -> (i -> k) -> j -> k))
- ranProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Ran :: (i -> j) -> (i -> k) -> j -> k))
- ranFunctor :: Dict (Functor (Ran f g :: j -> k))
- iotaRan :: forall f g id. (Category (Cod f), Category (Dom f), Functor g, Identity id) => Iso (Ran id f) (Ran id g) f g
- jotRan :: forall f. Id ~> Ran f f
- class (c ~ Hom) => HasLan c | k -> c where
- type Lan :: (i -> j) -> (i -> k) -> j -> k
- lanCocurried :: Dict (Cocurried (Lan :: (i -> j) -> (i -> k) -> j -> k) Compose)
- lanProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Lan :: (i -> j) -> (i -> k) -> j -> k))
- lanFunctor :: Dict (Functor (Lan f g :: j -> k))
- epsilonLan :: forall f g id. (Category (Cod f), Category (Dom f), Functor f, Identity id) => Iso (Lan id f) (Lan id g) f g
- data Prod :: (i, j) -> (i, j) -> * where
- runProd :: forall a b c d. (Category ((~>) :: i -> i -> *), Category ((~>) :: j -> j -> *)) => Prod `(a, c)` `(b, d)` -> (a ~> b, c ~> d)
- runFst :: forall a b c d. Category ((~>) :: i -> i -> *) => Prod `(a, c)` `(b, d)` -> a ~> b
- runSnd :: forall a b c d. Category ((~>) :: j -> j -> *) => Prod `(a, c)` `(b, d)` -> c ~> d
- diagProdAdj :: forall a b c a' b' c'. Cartesian ((~>) :: i -> i -> *) => Iso (`(a, a)` ~> `(b, c)`) (`(a', a')` ~> `(b', c')`) (a ~> (b * c)) (a' ~> (b' * c'))
- sumDiagAdj :: forall a b c a' b' c'. Cocartesian ((~>) :: i -> i -> *) => Iso ((b + c) ~> a) ((b' + c') ~> a') (`(b, c)` ~> `(a, a)`) (`(b', c')` ~> `(a', a')`)
- data Unit a b = Unit
- newtype Empty a b = Empty (Empty a b)
- data No a
- class (Profunctor p, p ~ (~>)) => Semicategory p
- newtype Compose1 f g a = Compose {
- getCompose :: f (g a)
- newtype Compose2 f g a b = Compose2 {
- getCompose2 :: f (g a) b
- class f (g a) => ComposeC f g a
- newtype Lim1 f = Lim {
- getLim :: forall x. f x
- newtype Lim2 f y = Lim2 {
- getLim2 :: forall x. f x y
- newtype Lim3 f y z = Lim3 {
- getLim3 :: forall x. f x y z
- class LimC p where
- newtype Const1 b a = Const {
- getConst :: b
- newtype Const2 f a c = Const2 {
- getConst2 :: f c
- class b => ConstC b a
- data Colim1 f where
- data Colim2 f x where
- newtype Id0 a = Id {
- runId :: a
- newtype Id1 f a = Id1 {
- runId1 :: f a
- class c => IdC c
- newtype Lift1 p f g a = Lift {
- lower :: p (f a) (g a)
- newtype Lift2 p f g a b = Lift2 {
- lower2 :: p (f a) (g a) b
- class r (p a) (q a) => LiftC r p q a
- class r (f a) (g a) b => LiftC2 r f g a b
- data Copower1 x f a = Copower x (f a)
- data Copower2 x f a b = Copower2 x (f a b)
- data Copower2_1 x f a b = Copower2_1 (x a) (f a b)
- data Ran1 f g a = forall z . Functor z => Ran (Compose z f ~> g) (z a)
- newtype Lan1 f g a = Lan {}
- newtype Lan2 f g a b = Lan2 {}
- data Constraint :: BOX
- undefined :: a
- ($) :: (a -> b) -> a -> b
- data Either a b :: * -> * -> *
- data Maybe a :: * -> *
- newtype Tagged s b :: k -> * -> * = Tagged {
- unTagged :: b
- data Proxy t :: k -> * = Proxy
- class Category cat where
- data Void :: *
- absurd :: Void -> a
Documentation
type family Hom :: i -> i -> k infixr 0 Source
All of our categories will be denoted by the kinds of their arguments.
This is allows for enriched Homs
Natural transformations
newtype Nat f g infixr 0 Source
Semimonoidal * (i -> Constraint) (Nat Constraint i f) | |
Semimonoidal * (i -> *) (Nat * i f) | |
(Monoidal (k1 -> k) * (Nat k k1 f), Monoid (k1 -> k) m) => Monoid * (Nat k k f m) | |
(Semimonoidal * (k1 -> k) (Nat k k1 f), Semigroup (k1 -> k) m) => Semigroup * (Nat k k f m) | |
Powered (i -> *) * (Nat * i) | |
Corepresentable (i -> *) * (i -> *) (Nat * i) | |
Representable (i -> *) * (i -> *) (Nat * i) | |
Monoidal (i -> Constraint) * (Nat Constraint i f) | |
Monoidal (i -> *) * (Nat * i f) | |
Category j ((~>) j) => Functor (i -> j) * (Nat j i f) | |
Category j ((~>) j) => Category (i -> j) (Nat j i) | |
HasLan (i -> *) (Nat * i) | |
Cocomplete (i -> *) (Nat * i) | |
Distributive (i -> j -> *) (Nat (j -> *) i) | |
Distributive (i -> *) (Nat * i) | |
Precocartesian (i -> j -> *) (Nat (j -> *) i) | |
Precocartesian (i -> *) (Nat * i) | |
Precartesian (i -> j -> Constraint) (Nat (j -> Constraint) i) | |
Precartesian (i -> Constraint) (Nat Constraint i) | |
Precartesian (i -> j -> *) (Nat (j -> *) i) | |
Precartesian (i -> *) (Nat * i) | |
Closed (i -> Constraint) (Nat Constraint i) | |
Closed (i -> *) (Nat * i) | |
Lifted (i -> *) (Nat * i) | |
Lifted (i -> Constraint) (Nat Constraint i) | |
Complete (i -> *) (Nat * i) | |
Composed (k -> *) (Nat * k) | |
Coended (i -> *) (Nat * i) | |
Ended (i -> *) (Nat * i) | |
Groupoid j ((~>) j) => Groupoid (i -> j) (Nat j i) | |
Strong (i -> Constraint) (Nat Constraint i) | |
Strong (i -> *) (Nat * i) | |
Choice (i -> j -> *) (Nat (j -> *) i) | |
Choice (i -> *) (Nat * i) | |
Curried (k -> *) (k -> *) * (Copower1 k) (Nat * k) | |
Curried (k -> k -> *) (k -> k -> *) * (Copower2 k k) (Nat (k -> *) k) | |
Contravariant (j -> *) j ((~>) j) => Contravariant ((i -> j) -> *) (i -> j) (Nat j i) | |
Curried (k -> k -> *) (k -> k -> *) (k -> *) (Copower2_1 k k) (Lift1 (k -> *) (k -> *) k (Nat * k)) | |
type Corep (i -> *) * (i -> *) (Nat * i) = Id (i -> *) | |
type Rep (i -> *) * (i -> *) (Nat * i) = Id (i -> *) |
Functors
Functor * * [] | |
Functor * * Maybe | |
Functor * * Id0 | |
Functor Constraint * Dict | |
Functor Constraint Constraint IdC | |
Functor Void * No | |
Functor * * ((->) e) | |
Functor * * (Either e) | |
Functor * * ((,) a) | |
Functor * * (Store0 s) | |
Functor * * (EnvC p) | |
Functor * * ((|=) e) | |
Functor Constraint * ((:-) f) | |
Functor Constraint Constraint ((|-) p) | |
Functor Constraint Constraint ((&) p) | |
Functor () * (Unit a) | |
Functor k * (Proxy k) | |
Functor Void * (Empty a) | |
Functor * * (Tagged k e) | |
Functor k * f => Functor k * (Id1 k f) | |
Category k (Arr k a) => Functor k * (Self k a) | |
Functor k Constraint (ConstC k b) | |
Functor k * (Const1 k b) | |
Functor k * f => Functor k * (Copower1 k x f) | |
Functor k * f => Functor k * (Power1 k v f) | |
Functor k * (Lan1 k k f g) | |
Functor k * (Ran1 k k f g) | |
(Functor k1 Constraint f, Functor k k1 g) => Functor k Constraint (ComposeC k k f g) | |
(Functor k1 * f, Functor k k1 g) => Functor k * (Compose1 k k f g) | |
Category i ((~>) i) => Functor i * (Beget k i r a) | |
Functor k * (Get k k r a) | |
Post x (x -> *) (Functor x *) ((~>) x) => Functor x * (Via x a b s) | |
Functor k * f => Functor k * (Const2 k k f a) | |
(Functor k k1 f, Category k1 (Cod k1 k f)) => Functor k * (Down k k f a) | |
Category k (Cod k k1 f) => Functor k * (Up k k f a) | |
Post k1 (k -> *) (Functor k *) f => Functor k * (Copower2_1 k k x f a) | |
Post k1 (k -> *) (Functor k *) f => Functor k * (Copower2 k k x f a) | |
(Category j ((~>) j), Contravariant (i -> j) i p) => Functor i * (Un i j p a b s) | |
(Functor k1 (k2 -> *) p, Post k1 (k2 -> *) (Functor k2 *) p, Functor k k1 f, Functor k k2 g) => Functor k * (Lift1 k k k p f g) | |
Post k2 (k -> *) (Functor k *) q => Functor k * (ProfR k k k p q a) | |
Post k1 (k -> *) (Functor k *) p => Functor k * (Prof k k k p q a) | |
Functor * (* -> *) Either | |
Functor * (* -> *) (,) | |
Functor Constraint (* -> *) EnvC | |
Functor Constraint (Constraint -> Constraint) (&) | |
Functor () (() -> *) Unit | |
Functor Void (Void -> *) Empty | |
Functor * ((k -> *) -> k -> *) (Copower1 k) | |
Functor * (k -> *) (Const1 k) | |
Functor * (k -> k -> *) (Coat0 k) | |
Functor * (k -> k -> *) (At0 k) | |
Functor Constraint (k -> Constraint) (ConstC k) | |
Functor Constraint (k -> k -> Constraint) (CoatC k) | |
Functor Constraint (k -> k -> Constraint) (AtC k) | |
Post x (x -> *) (Functor x *) ((~>) x) => Functor x (x -> x -> x -> *) (Via x) | |
Functor k (* -> *) (Tagged k) | |
Functor * ((k -> k -> *) -> k -> k -> *) (Copower2 k k) | |
Category i ((~>) i) => Functor i (i -> k -> *) (Get k i) | |
Functor x (x -> *) ((~>) x) => Functor x (x -> x -> *) (Via x a) | |
Functor * (k -> *) g => Functor * (k -> *) (ComposeConst1 k f g) | |
Functor k (k -> *) (Beget k k r) | |
Functor x (x -> *) ((~>) x) => Functor x (x -> *) (Via x a b) | |
Functor k (k -> *) (Const2 k k f) | |
(Functor k * x, Functor k (k1 -> *) f) => Functor k (k -> *) (Copower2_1 k k x f) | |
Functor k (k1 -> *) f => Functor k (k -> *) (Copower2 k k x f) | |
Functor k (k -> *) (Lan2 k k k f g) | |
(Functor k1 (k2 -> *) f, Functor k k1 g) => Functor k (k -> *) (Compose2 k k k f g) | |
(Category j ((~>) j), Post i (i -> j) (Contravariant j i) p) => Functor i (i -> *) (Un i j p a b) | |
Post k1 (k -> *) (Contravariant * k) p => Functor k (k -> *) (ProfR k k k p q) | |
Functor k (k1 -> *) q => Functor k (k -> *) (Prof k k k p q) | |
Functor (k -> *) * (Colim1 k) | |
Functor (k -> *) * (Lim1 k) | |
Functor (k -> Constraint) Constraint (LimC k) | |
Functor (k -> k -> *) * (Coend1 k) | |
Functor (k -> k -> Constraint) Constraint (EndC k) | |
Functor (k -> k -> *) * (End1 k) | |
Category j ((~>) j) => Functor (i -> j) * (Nat j i f) | |
(Functor i * ((~>) i a), Functor j * ((~>) j b), (~) ((,) i j) ab ((,) i j a b)) => Functor ((,) i j) * (Prod i j ab) | |
Functor (* -> k -> *) ((* -> k -> *) -> * -> k -> *) (ComposeConst1 k) | |
Functor (k -> *) (k -> *) (Id1 k) | |
Functor (* -> k -> *) (* -> k -> *) (ComposeConst1 k f) | |
Functor (k -> k -> *) (k -> *) (Colim2 k k) | |
Functor (k -> *) ((k -> k -> *) -> k -> k -> *) (Copower2_1 k k) | |
Functor (k -> *) (k -> *) (Copower1 k x) | |
Functor (k -> Constraint) ((k -> k) -> k -> Constraint) (ComposeC k k) | |
Functor (k -> *) ((k -> k) -> k -> *) (Compose1 k k) | |
Functor (k -> k -> *) (k -> *) (Lim2 k k) | |
Functor (k -> *) (k -> k -> *) (Const2 k k) | |
Functor (k -> k -> k -> *) (k -> *) (Coend2 k k) | |
Functor (k -> k -> k -> *) (k -> *) (End2 k k) | |
Category i (Hom i *) => Functor (j -> i) (i -> j -> *) (Down i j) | |
Functor (k -> *) (k -> *) (Store1 k s) | |
Functor (k -> *) (k -> *) (Power1 k v) | |
Category j (Hom j *) => Functor (i -> *) (j -> *) (Lan1 j i f) | |
Category j (Hom j *) => Functor (i -> *) (j -> *) (Ran1 j i f) | |
Functor (k -> k -> *) (k -> k -> *) (Copower2_1 k k x) | |
Functor (k -> k -> *) (k -> k -> *) (Copower2 k k x) | |
Functor k Constraint f => Functor (k -> k) (k -> Constraint) (ComposeC k k f) | |
Functor k * f => Functor (k -> k) (k -> *) (Compose1 k k f) | |
Functor (k -> k -> *) ((k -> k) -> k -> k -> *) (Compose2 k k k) | |
Functor (k -> k -> *) ((k -> k) -> (k -> k) -> k -> *) (Lift1 k k k) | |
Functor (k -> k -> *) ((k -> k -> *) -> k -> k -> *) (Prof k k k) | |
Category j (Hom j *) => Functor (i -> k -> *) (j -> k -> *) (Lan2 j i k f) | |
Functor k (k1 -> *) f => Functor (k -> k) (k -> k -> *) (Compose2 k k k f) | |
Functor (k -> k -> k -> *) ((k -> k) -> (k -> k) -> k -> k -> *) (Lift2 k k k k) | |
Functor (k -> k -> k -> Constraint) ((k -> k) -> (k -> k) -> k -> k -> Constraint) (LiftC2 k k k k) | |
Functor k (k1 -> Constraint) p => Functor (k -> k) ((k -> k) -> k -> Constraint) (LiftC k k k p) | |
Functor k (k1 -> *) p => Functor (k -> k) ((k -> k) -> k -> *) (Lift1 k k k p) | |
Functor (k -> k -> *) (k -> k -> *) (ProfR k k k p) | |
Functor (k -> k -> *) (k -> k -> *) (Prof k k k p) | |
Functor k (k1 -> k2 -> *) p => Functor (k -> k) ((k -> k) -> k -> k -> *) (Lift2 k k k k p) | |
Functor k (k1 -> k2 -> Constraint) p => Functor (k -> k) ((k -> k) -> k -> k -> Constraint) (LiftC2 k k k k p) | |
Post k (k1 -> Constraint) (Functor k1 Constraint) p => Functor (k -> k) (k -> Constraint) (LiftC k k k p e) | |
Post k (k1 -> *) (Functor k1 *) p => Functor (k -> k) (k -> *) (Lift1 k k k p f) | |
Post k (k1 -> k2 -> *) (Functor k1 (k2 -> *)) p => Functor (k -> k) (k -> k -> *) (Lift2 k k k k p f) | |
Post k (k1 -> k2 -> Constraint) (Functor k1 (k2 -> Constraint)) p => Functor (k -> k) (k -> k -> Constraint) (LiftC2 k k k k p f) |
class Contravariant f where Source
Contravariant * () (Unit a) | |
Contravariant * k (Proxy k) | |
Contravariant * Void (Empty a) | |
Contravariant * k f => Contravariant * k (Id1 k f) | |
Contravariant * k (Const1 k b) | |
Contravariant * k f => Contravariant * k (Copower1 k x f) | |
Contravariant * k (Get k k r a) | |
Post x (x -> *) (Contravariant * x) ((~>) x) => Contravariant * x (Via x a b s) | |
Post k1 (k -> *) (Contravariant * k) f => Contravariant * k (Copower2_1 k k x f a) | |
Post k1 (k -> *) (Contravariant * k) f => Contravariant * k (Copower2 k k x f a) | |
(Category j ((~>) j), Functor i (i -> j) p) => Contravariant * i (Un i j p a b s) | |
Post k2 (k -> *) (Contravariant * k) q => Contravariant * k (ProfR k k k p q a) | |
Post k1 (k -> *) (Contravariant * k) p => Contravariant * k (Prof k k k p q a) | |
Contravariant (* -> *) * (->) | |
Contravariant (* -> *) Constraint (|=) | |
Contravariant (Constraint -> *) Constraint (:-) | |
Contravariant (Constraint -> Constraint) Constraint (|-) | |
Contravariant (() -> *) () Unit | |
Contravariant (Void -> *) Void Empty | |
Contravariant ((k -> *) -> k -> *) * (Power1 k) | |
Contravariant (* -> *) k (Tagged k) | |
Category x ((~>) x) => Contravariant (x -> *) x (Self x) | |
Post x (x -> *) (Contravariant * x) ((~>) x) => Contravariant (x -> x -> x -> *) x (Via x) | |
Category i ((~>) i) => Contravariant (k -> i -> *) i (Beget k i) | |
Contravariant (x -> *) x ((~>) x) => Contravariant (x -> x -> *) x (Via x a) | |
Contravariant (k -> *) k (Beget k k r) | |
Category k (Arr k r) => Contravariant (k -> *) k (Get k k r) | |
Contravariant (k -> *) k (Const2 k k k) | |
Contravariant (x -> *) x ((~>) x) => Contravariant (x -> *) x (Via x a b) | |
Category k (Cod k k1 f) => Contravariant (k -> *) k (Down k k f) | |
(Functor k k1 f, Category k1 (Cod k1 k f)) => Contravariant (k -> *) k (Up k k f) | |
(Contravariant * k x, Contravariant (k1 -> *) k f) => Contravariant (k -> *) k (Copower2_1 k k x f) | |
Contravariant (k1 -> *) k f => Contravariant (k -> *) k (Copower2 k k x f) | |
(Category j ((~>) j), Post i (i -> j) (Functor i j) p) => Contravariant (i -> *) i (Un i j p a b) | |
Post k1 (k -> *) (Functor k *) p => Contravariant (k -> *) k (ProfR k k k p q) | |
Contravariant (k1 -> *) k q => Contravariant (k -> *) k (Prof k k k p q) | |
Contravariant ((k -> *) -> k -> *) (k -> k) (Lan1 k k) | |
Contravariant ((k -> *) -> k -> *) (k -> k) (Ran1 k k) | |
Contravariant (j -> *) j ((~>) j) => Contravariant ((i -> j) -> *) (i -> j) (Nat j i) | |
(Contravariant (i -> *) i ((~>) i), Contravariant (j -> *) j ((~>) j)) => Contravariant ((,) i j -> *) ((,) i j) (Prod i j) | |
Category j (Hom j *) => Contravariant (i -> j -> *) (i -> j) (Up j i) | |
Contravariant ((k -> k -> *) -> k -> k -> *) (k -> k) (Lan2 k k k) | |
Contravariant ((k -> k -> *) -> k -> k -> *) (k -> k -> *) (ProfR k k k) | |
Contravariant Constraint k f => Contravariant (k -> Constraint) (k -> k) (ComposeC k k f) | |
Contravariant * k f => Contravariant (k -> *) (k -> k) (Compose1 k k f) | |
Contravariant (k1 -> Constraint) k p => Contravariant ((k -> k) -> k -> Constraint) (k -> k) (LiftC k k k p) | |
Contravariant (k1 -> *) k p => Contravariant ((k -> k) -> k -> *) (k -> k) (Lift1 k k k p) | |
Contravariant (k1 -> *) k f => Contravariant (k -> k -> *) (k -> k) (Compose2 k k k f) | |
Contravariant (k1 -> k2 -> *) k p => Contravariant ((k -> k) -> k -> k -> *) (k -> k) (Lift2 k k k k p) | |
Contravariant (k1 -> k2 -> Constraint) k p => Contravariant ((k -> k) -> k -> k -> Constraint) (k -> k) (LiftC2 k k k k p) | |
Post k (k1 -> Constraint) (Contravariant Constraint k1) p => Contravariant (k -> Constraint) (k -> k) (LiftC k k k p e) | |
Post k (k1 -> *) (Contravariant * k1) p => Contravariant (k -> *) (k -> k) (Lift1 k k k p f) | |
Post k (k1 -> k2 -> *) (Contravariant (k2 -> *) k1) p => Contravariant (k -> k -> *) (k -> k) (Lift2 k k k k p f) | |
Post k (k1 -> k2 -> Constraint) (Contravariant (k2 -> Constraint) k1) p => Contravariant (k -> k -> Constraint) (k -> k) (LiftC2 k k k k p f) |
lmap :: Contravariant f => (a ~> b) -> f b c ~> f a c Source
Functor composition
composed :: (Functor k1 k2 (p (Any k)), Contravariant (k1 -> k2) k p, Composed k1 (Hom k1 *), Composed k (Hom k *), Category k2 (Hom k2 *)) => (~>) k2 (p (f (g a)) (f1 (g1 a1))) (p (Compose k k3 k4 f g a) (Compose k1 k5 k6 f1 g1 a1)) Source
associateCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Functor k8 k3 f1, Functor k5 k1 f, Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k8 (Hom k8 *), Composed k5 (Hom k5 *), Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Category k3 (Hom k3 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p (Compose k1 k5 k2 f (Compose k5 k6 k2 g g1)) (Compose k3 k8 k4 f1 (Compose k8 k7 k4 g3 g2))) (p (Compose k1 k6 k2 (Compose k1 k5 k6 f g) g1) (Compose k3 k7 k4 (Compose k3 k8 k7 f1 g3) g2)) Source
whiskerComposeL :: (Functor k * (Hom k * (Any k)), Contravariant (k -> *) k (Hom k *), Composed k (Hom k *)) => Nat k k2 f g1 -> Nat k k1 (Compose k k2 k1 f g) (Compose k k2 k1 g1 g) Source
whiskerComposeR :: (Functor x k f, Functor k * (Hom k * (Any k)), Contravariant (k -> *) k (Hom k *), Composed k (Hom k *)) => Nat x k1 g g1 -> Nat k k1 (Compose k x k1 f g) (Compose k x k1 f g1) Source
lambdaCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Identity k3 (Id k3), Identity k1 (Id k1), Category k3 (Hom k3 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p b c) (p (Compose k1 k1 k2 (Id k1) b) (Compose k3 k3 k4 (Id k3) c)) Source
rhoCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Functor k4 k3 c, Functor k2 k1 b, Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Identity k4 (Id k4), Identity k2 (Id k2), Category k4 (Hom k4 *), Category k3 (Hom k3 *), Category k2 (Hom k2 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p b c) (p (Compose k1 k2 k2 b (Id k2)) (Compose k3 k4 k4 c (Id k4))) Source
In the limit
Derived notions
contramap1 :: forall p a b c. Post Contravariant p => (a ~> b) -> p c b ~> p c a Source
class (Contravariant p, Post Functor p) => Profunctor p Source
(Contravariant (k1 -> k2) k p, Post k (k1 -> k2) (Functor k1 k2) p) => Profunctor k k k p |
class (Contravariant p, Functor p) => Phantom p Source
(Contravariant k1 k p, Functor k k1 p) => Phantom k k p |
Colim -| Const -| Lim
class (k ~ (~>)) => Cocomplete k where Source
Cocomplete * (->) | |
Cocomplete (i -> *) (Nat * i) |
Natural Isomorphisms
type Iso s t a b = forall p. Profunctor p => p a b -> p s t Source
Adjunctions
class (Functor f, Functor u) => f -| u | f -> u, u -> f where infixr 0 Source
f -| u
indicates f is left adjoint to u
(-|) * * Id0 Id0 | |
(-|) Constraint Constraint IdC IdC | |
(-|) * * ((,) e) ((->) e) | |
(-|) * * (EnvC e) ((|=) e) | |
(-|) Constraint Constraint ((&) p) ((|-) p) | |
((-|) k * f g, (-|) * k f' g', Category * (Dom * k f), Category k (Cod k * f)) => (-|) * * (Compose1 k * f' f) (Compose1 k * g g') | |
((-|) k Constraint f g, (-|) * k f' g', Category Constraint (Dom Constraint k f), Category k (Cod k Constraint f)) => (-|) * Constraint (Compose1 k Constraint f' f) (ComposeC k * g g') | |
(-|) * (k -> *) (Colim1 k) (Const1 k) | |
((-|) k (k1 -> *) f g, (-|) * k f' g', Category (k1 -> *) (Dom (k1 -> *) k f), Category k (Cod k (k1 -> *) f)) => (-|) * (k -> *) (Compose1 k (k -> *) f' f) (Compose2 k k * g g') | |
(-|) (k -> Constraint) Constraint (ConstC k) (LimC k) | |
(-|) (k -> *) * (Const1 k) (Lim1 k) | |
(-|) (k -> *) (k -> *) (Id1 k) (Id1 k) | |
(-|) (k -> *) (k -> k -> *) (Colim2 k k) (Const2 k k) | |
(-|) (k -> k -> *) (k -> *) (Const2 k k) (Lim2 k k) |
zipR :: (f -| u, Cartesian (Dom u), Cartesian (Cod u)) => Iso (u a * u b) (u a' * u b') (u (a * b)) (u (a' * b')) Source
cozipL :: (f -| u, Cocartesian (Cod u), Cocartesian (Cod f)) => Iso (f (a + b)) (f (a' + b')) (f a + f b) (f a' + f b') Source
Currying
class Curried p e | p -> e, e -> p where Source
type Curryable p :: k -> Constraint Source
curry :: Curryable p a => (p a b ~> c) -> a ~> e b c Source
uncurry :: (a ~> e b c) -> p a b ~> c Source
Curried * * * (,) (->) | |
Curried Constraint Constraint Constraint (&) (|-) | |
Curried (k -> *) (k -> *) * (Copower1 k) (Nat * k) | |
Curried (k -> k -> *) (k -> k -> *) * (Copower2 k k) (Nat (k -> *) k) | |
Curried (k -> *) (k -> k) (k -> *) (Compose1 k k) (Ran1 k k) | |
Curried (k -> k -> *) (k -> k -> *) (k -> *) (Copower2_1 k k) (Lift1 (k -> *) (k -> *) k (Nat * k)) | |
Curried (k -> k -> *) (k -> k -> *) (k -> k -> *) (Prof k k k) (ProfR k k k) | |
Curried Constraint k1 Constraint p q => Curried (k -> Constraint) (k -> k) (k -> Constraint) (LiftC Constraint k k p) (LiftC k Constraint k q) | |
Curried * k1 * p q => Curried (k -> *) (k -> k) (k -> *) (Lift1 * k k p) (Lift1 k * k q) | |
Curried (k -> Constraint) k2 (k3 -> Constraint) p q => Curried (k -> k -> Constraint) (k -> k) (k -> k -> Constraint) (LiftC2 (k -> Constraint) k k k p) (LiftC2 k (k -> Constraint) k k q) | |
Curried (k -> *) k2 (k3 -> *) p q => Curried (k -> k -> *) (k -> k) (k -> k -> *) (Lift2 (k -> *) k k k p) (Lift2 k (k -> *) k k q) |
curried :: (Curried p e, Curryable p a) => Iso (p a b ~> c) (p a' b' ~> c') (a ~> e b c) (a' ~> e b' c') Source
ccc :: (Category (Cod2 p), Symmetric p, Curried p e, Curryable p a) => Iso (p i a ~> b) (p i' a' ~> b') (a ~> e i b) (a' ~> e i' b') Source
Cocurrying
class Cocurried f u | f -> u, u -> f where Source
type Cocurryable u :: k -> Constraint Source
cocurried :: (Cocurried f u, Cocurryable u c') => Iso (f a b ~> c) (f a' b' ~> c') (b ~> u c a) (b' ~> u c' a') Source
Automatic Lifting
class (hom ~ Hom) => Lifted hom where Source
Nothing
_Lift :: forall q r f h g e a b. Iso (Lift q f g a) (Lift r h e b) (q (f a) (g a)) (r (h b) (e b)) Source
Lifted * (->) | |
Lifted Constraint (:-) | |
Lifted (i -> *) (Nat * i) | |
Lifted (i -> Constraint) (Nat Constraint i) |
Constraints
newtype a :- b :: Constraint -> Constraint -> *
Category Constraint (:-) | |
Precocartesian Constraint (:-) | |
Precartesian Constraint (:-) | |
Closed Constraint (:-) | |
Lifted Constraint (:-) | |
Complete Constraint (:-) | |
Composed Constraint (:-) | |
Ended Constraint (:-) | |
Strong Constraint (:-) | |
HasAt Constraint (:-) | |
Subst Constraint * (:-) | |
Corepresentable Constraint * Constraint (:-) | |
Representable Constraint * Constraint (:-) | |
Monoidal Constraint * ((:-) f) | |
Semimonoidal * Constraint ((:-) f) | |
Functor Constraint * ((:-) f) | |
() :=> (Eq ((:-) a b)) | |
() :=> (Ord ((:-) a b)) | |
() :=> (Show ((:-) a b)) | |
Monoid Constraint m => Monoid * ((:-) f m) | |
Semigroup * ((:-) f m) | |
Eq ((:-) a b) | |
Ord ((:-) a b) | |
Show ((:-) a b) | |
Contravariant (Constraint -> *) Constraint (:-) | |
type Corep Constraint * Constraint (:-) = Id Constraint | |
type Rep Constraint * Constraint (:-) = Id Constraint |
data Dict $a :: Constraint -> * where
Monoidal Constraint * Dict | |
Semimonoidal * Constraint Dict | |
Functor Constraint * Dict | |
a :=> (Read (Dict a)) | |
a :=> (Monoid (Dict a)) | |
a :=> (Enum (Dict a)) | |
a :=> (Bounded (Dict a)) | |
() :=> (Eq (Dict a)) | |
() :=> (Ord (Dict a)) | |
() :=> (Show (Dict a)) | |
Monoid Constraint m => Monoid * (Dict m) | |
Semigroup * (Dict m) | |
a => Bounded (Dict a) | |
a => Enum (Dict a) | |
Eq (Dict a) | |
Ord (Dict a) | |
a => Read (Dict a) | |
Show (Dict a) | |
a => Monoid (Dict a) |
class (p, q) => p & q infixr 2 Source
Tensor Constraint (&) | |
Semitensor Constraint (&) | |
(p, q) => p & q | |
Symmetric Constraint Constraint (&) | |
Curried Constraint Constraint Constraint (&) (|-) | |
Functor Constraint Constraint ((&) p) | |
Foldable Constraint Constraint ((&) e) | |
(-|) Constraint Constraint ((&) p) ((|-) p) | |
Functor Constraint (Constraint -> Constraint) (&) | |
Class ((&) a ((~) k i j)) (AtC k a i j) | |
((&) a ((~) k i j)) :=> (AtC k a i j) | |
type I Constraint (&) = () | |
type Tensorable Constraint (&) = Const Constraint Constraint () | |
type Curryable Constraint Constraint Constraint (&) = Const Constraint Constraint () |
class p |- q where infixr 9 Source
Subst Constraint Constraint (|-) | |
Powered Constraint Constraint (|-) | |
Corepresentable Constraint Constraint Constraint (|-) | |
Curried Constraint Constraint Constraint (&) (|-) | |
Monoidal Constraint Constraint ((|-) f) | |
Semimonoidal Constraint Constraint ((|-) f) | |
Functor Constraint Constraint ((|-) p) | |
(-|) Constraint Constraint ((&) p) ((|-) p) | |
Monoid Constraint m => Monoid Constraint ((|-) f m) | |
Contravariant (Constraint -> Constraint) Constraint (|-) | |
Class ((|-) ((~) k i j) a) (CoatC k a i j) | |
((|-) ((~) k i j) a) :=> (CoatC k a i j) | |
type I Constraint (|-) = () | |
type Corep Constraint Constraint Constraint (|-) = IdC |
class Class b h | h -> b where
Class () () | |
Class () (Bounded a) | |
Class () (Enum a) | |
Class () (Eq a) | |
Class () (Monad f) | |
Class () (Functor f) | |
Class () (Num a) | |
Class () (Read a) | |
Class () (Show a) | |
Class () (Monoid a) | |
Class () (Class b a) | |
Class () ((:=>) b a) | |
Class b a => () :=> (Class b a) | |
Class (Eq a) (Ord a) | |
Class (Fractional a) (Floating a) | |
Class (Monad f) (MonadPlus f) | |
Class (Functor f) (Applicative f) | |
Class (Num a) (Fractional a) | |
Class (Applicative f) (Alternative f) | |
Class (f (g a)) (ComposeC k k f g a) | |
Class (Num a, Ord a) (Real a) | |
Class (Real a, Fractional a) (RealFrac a) | |
Class (Real a, Enum a) (Integral a) | |
Class (RealFrac a, Floating a) (RealFloat a) | |
Class ((|-) ((~) k i j) a) (CoatC k a i j) | |
Class ((&) a ((~) k i j)) (AtC k a i j) |
class b :=> h | h -> b where
Lens Esoterica
The Yoneda embedding
Get is the Yoneda embedding C -> [ C^op, Set]
How? We can view it as a functor from C -> [ C^op X 1, Set ] with the latter embedded in Prof.
Where does the 1 come from? We use the existence of Contravariance and Covariance in all arguments to make a
category where every object is the same as long as the kind chosen has either an initial or a terminal object.
But get is polymorphic in the choice of kind for the b
parameter, making it possible to choose it to be anything
you want.
_Get :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k2 * a r) (Hom k4 * a1 r1)) (p (Get k1 k2 r a b) (Get k3 k4 r1 a1 b1)) Source
Beget is the contravariant Yoneda embedding. C^op -> [C, Set]
we can view it as a functor from C^op -> [ 1^op X C, Set ] with the latter embedded in Prof.
_Beget :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k2 * r b) (Hom k4 * r1 b1)) (p (Beget k1 k2 r a b) (Beget k3 k4 r1 a1 b1)) Source
Inverting natural isomorphisms
(Category j ((~>) j), Functor i (i -> j) p) => Contravariant * i (Un i j p a b s) | |
(Category j ((~>) j), Contravariant (i -> j) i p) => Functor i * (Un i j p a b s) | |
(Category j ((~>) j), Post i (i -> j) (Contravariant j i) p) => Functor i (i -> *) (Un i j p a b) | |
(Category j ((~>) j), Post i (i -> j) (Functor i j) p) => Contravariant (i -> *) i (Un i j p a b) |
_Un :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k1 * (p1 t s) (p1 b a)) (Hom k2 * (p2 t1 s1) (p2 b1 a1))) (p (Un i k1 p1 a b s t) (Un i1 k2 p2 a1 b1 s1 t1)) Source
Post x (x -> *) (Contravariant * x) ((~>) x) => Contravariant * x (Via x a b s) | |
Post x (x -> *) (Functor x *) ((~>) x) => Functor x * (Via x a b s) | |
Post x (x -> *) (Functor x *) ((~>) x) => Functor x (x -> x -> x -> *) (Via x) | |
Functor x (x -> *) ((~>) x) => Functor x (x -> x -> *) (Via x a) | |
Functor x (x -> *) ((~>) x) => Functor x (x -> *) (Via x a b) | |
Post x (x -> *) (Contravariant * x) ((~>) x) => Contravariant (x -> x -> x -> *) x (Via x) | |
Contravariant (x -> *) x ((~>) x) => Contravariant (x -> x -> *) x (Via x a) | |
Contravariant (x -> *) x ((~>) x) => Contravariant (x -> *) x (Via x a b) |
via :: forall a b r p c t u. Category p => (Via a b a b -> Via r (p c c) u t) -> (t -> u) -> r Source
get = via _Get beget = via _Beget un = via _Un
mapping :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s) (f' t) (f a) (f' b) Source
lmapping :: (Contravariant f, Contravariant f', Category (Dom f)) => (Via s t s t -> Via s t a b) -> Iso (f s x) (f' t y) (f a x) (f' b y) Source
swapping :: (Profunctor f, Profunctor f', Category (Dom f), Category (Cod2 f), Category (Cod2 f')) => (Via a b a b -> Via a b s t) -> Iso (f a s) (f' b t) (f s a) (f' t b) Source
mapping1 :: (Post Functor f, Post Functor f', Category (Dom1 f)) => (Via a b a b -> Via a b s t) -> Iso (f i s) (f' j t) (f i a) (f' j b) Source
firstly :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s x) (f' t y) (f a x) (f' b y) Source
post :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (i ~> s) (j ~> t) (i ~> a) (j ~> b) Source
pre :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (a ~> i) (b ~> j) (s ~> i) (t ~> j) Source
Hom as a Profunctor
Cartesian x (Arr x a) => Monoidal x * (Self x a) | |
Precartesian x (Arr x a) => Semimonoidal * x (Self x a) | |
Category k (Arr k a) => Functor k * (Self k a) | |
Precartesian i ((~>) i) => Strong i (Self i) | |
Precocartesian i ((~>) i) => Choice i (Self i) | |
(Cartesian k (Arr k a), Monoid k b) => Monoid * (Self k a b) | |
(Precartesian k (Arr k a), Semigroup k b) => Semigroup * (Self k a b) | |
Category x ((~>) x) => Contravariant (x -> *) x (Self x) |
_Self :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k1 * a b) (Hom k2 * a1 b1)) (p (Self k1 a b) (Self k2 a1 b1)) Source
Monoidal Categories
class (Functor p, Profunctor (Cod2 p), Category (Cod2 p)) => Semitensor p where Source
type Tensorable p :: x -> Constraint Source
second :: Tensorable p c => (a ~> b) -> p c a ~> p c b Source
associate :: (Tensorable p a, Tensorable p b, Tensorable p c, Tensorable p a', Tensorable p b', Tensorable p c') => Iso (p (p a b) c) (p (p a' b') c') (p a (p b c)) (p a' (p b' c')) Source
Semitensor * Either | |
Semitensor * (,) | |
Semitensor Constraint (&) | |
Semitensor (* -> k -> *) (ComposeConst1 k) | |
Semitensor (* -> *) (Compose1 * *) | |
Semitensor (Constraint -> Constraint) (ComposeC Constraint Constraint) | |
Semitensor ((k -> *) -> k -> *) (Compose2 (k -> *) k (k -> *)) | |
Category i ((~>) i) => Semitensor (i -> i -> *) (Prof i i i) | |
Semitensor Constraint p => Semitensor (k -> Constraint) (LiftC Constraint Constraint k p) | |
Semitensor * p => Semitensor (k -> *) (Lift1 * * k p) | |
Semitensor (k -> Constraint) p => Semitensor (k -> k -> Constraint) (LiftC2 (k -> Constraint) (k -> Constraint) k k p) | |
Semitensor (i -> *) p => Semitensor (k -> i -> *) (Lift2 (i -> *) (i -> *) i k p) |
type I * (->) = () | |
type I * Either = Void | |
type I * (,) = () | |
type I Constraint (|-) = () | |
type I Constraint (&) = () | |
type I (* -> k -> *) (ComposeConst1 k) = Const1 k | |
type I (* -> *) (Compose1 * *) = Id * | |
type I (Constraint -> Constraint) (ComposeC Constraint Constraint) = Id Constraint | |
type I ((k -> *) -> k -> *) (Compose2 (k -> *) k (k -> *)) = Id (k -> *) | |
type I (k -> k -> *) (ProfR k k k) = (~>) k | |
type I (k -> k -> *) (Prof k k k) = (~>) k | |
type I (k -> Constraint) (LiftC Constraint Constraint k p) = ConstC k (I Constraint p) | |
type I (k -> *) (Lift1 * * k p) = Const1 k (I * p) | |
type I (k -> k1 -> Constraint) (LiftC2 (k1 -> Constraint) (k1 -> Constraint) k1 k p) | |
type I (k -> k1 -> *) (Lift2 (k1 -> *) (k1 -> *) k1 k p) = Const2 k1 k (I (k1 -> *) p) |
class Semitensor p => Tensor p where Source
lambda :: (Tensorable p a, Tensorable p a') => Iso (p (I p) a) (p (I p) a') a a' Source
rho :: (Tensorable p a, Tensorable p a') => Iso (p a (I p)) (p a' (I p)) a a' Source
Tensor * Either | |
Tensor * (,) | |
Tensor Constraint (&) | |
Tensor (* -> k -> *) (ComposeConst1 k) | |
Tensor (* -> *) (Compose1 * *) | |
Tensor (Constraint -> Constraint) (ComposeC Constraint Constraint) | |
Tensor ((k -> *) -> k -> *) (Compose2 (k -> *) k (k -> *)) | |
Category i ((~>) i) => Tensor (i -> i -> *) (Prof i i i) | |
Tensor Constraint p => Tensor (k -> Constraint) (LiftC Constraint Constraint k p) | |
Tensor * p => Tensor (k -> *) (Lift1 * * k p) | |
Tensor (k -> Constraint) p => Tensor (k -> k -> Constraint) (LiftC2 (k -> Constraint) (k -> Constraint) k k p) | |
Tensor (k -> *) p => Tensor (k -> k -> *) (Lift2 (k -> *) (k -> *) k k p) |
class Bifunctor p => Symmetric p where Source
Symmetric * * Either | |
Symmetric * * (,) | |
Symmetric Constraint Constraint (&) | |
Symmetric () * Unit | |
Symmetric Void * Empty | |
Symmetric k Constraint p => Symmetric (k -> k) (k -> Constraint) (LiftC k k k p) | |
Symmetric k * p => Symmetric (k -> k) (k -> *) (Lift1 k k k p) | |
Symmetric k (k1 -> Constraint) p => Symmetric (k -> k) (k -> k -> Constraint) (LiftC2 k k k k p) | |
Symmetric k (k1 -> *) p => Symmetric (k -> k) (k -> k -> *) (Lift2 k k k k p) |
Closed Categories
class (Profunctor (Internal k), Category k, k ~ Hom) => Closed k where Source
Nothing
Closed * (->) | |
Closed Constraint (:-) | |
Closed (i -> Constraint) (Nat Constraint i) | |
Closed (i -> *) (Nat * i) |
Terminal and Initial Objects
Copowers and Cartesian Categories
type family Copower :: i -> j -> j Source
This is factored out of Precartesian so that we can also use it for copowers/tensors
type Copower * * = (,) | |
type Copower Constraint Constraint = (&) | |
type Copower * (k -> k1 -> *) = Copower2 k k1 | |
type Copower * (k -> *) = Copower1 k | |
type Copower (k -> *) (k -> k1 -> *) = Copower2_1 k k1 | |
type Copower (k1 -> k -> Constraint) (k1 -> k -> Constraint) = LiftC2 (k -> Constraint) (k -> Constraint) k k1 (* (k -> Constraint)) | |
type Copower (k -> Constraint) (k -> Constraint) = LiftC Constraint Constraint k (&) | |
type Copower (k1 -> k -> *) (k1 -> k -> *) = Lift2 (k -> *) (k -> *) k k1 (* (k -> *)) | |
type Copower (k -> *) (k -> *) = Lift * * * k (,) |
class (h ~ (~>), Symmetric (* :: i -> i -> i), Semitensor (* :: i -> i -> i)) => Precartesian h | i -> h where Source
fst :: forall a b. (a * b) ~> a Source
snd :: forall a b. (a * b) ~> b Source
(&&&) :: forall a b c. (a ~> b) -> (a ~> c) -> a ~> (b * c) Source
Precartesian * (->) | |
Precartesian Constraint (:-) | |
Precartesian (i -> j -> Constraint) (Nat (j -> Constraint) i) | |
Precartesian (i -> Constraint) (Nat Constraint i) | |
Precartesian (i -> j -> *) (Nat (j -> *) i) | |
Precartesian (i -> *) (Nat * i) |
class (h ~ (~>), Tensor (* :: i -> i -> i), Terminal (I (* :: i -> i -> i)), Precartesian h) => Cartesian h | i -> h Source
class (h ~ (~>), Symmetric ((+) :: i -> i -> i), Semitensor ((+) :: i -> i -> i)) => Precocartesian h | i -> h where Source
inl :: forall a b. a ~> (a + b) Source
inr :: forall a b. b ~> (a + b) Source
(|||) :: forall a b c. (a ~> c) -> (b ~> c) -> (a + b) ~> c Source
Precocartesian * (->) | |
Precocartesian Constraint (:-) | |
Precocartesian (i -> j -> *) (Nat (j -> *) i) | |
Precocartesian (i -> *) (Nat * i) |
class (h ~ (~>), Tensor ((+) :: i -> i -> i), Initial (I ((+) :: i -> i -> i)), Precocartesian h) => Cocartesian h | i -> h Source
((~) (i -> i -> *) h ((~>) i), Tensor i ((+) i), Initial i (I i ((+) i)), Precocartesian i h) => Cocartesian i h |
Distributive bicartesian categories
class (Cartesian k, Cocartesian k) => Distributive k | i -> k where Source
distribute :: forall a b c a' b' c'. Iso ((a * b) + (a * c)) ((a' * b') + (a' * c')) (a * (b + c)) (a' * (b' + c')) Source
Distributive * (->) | |
Distributive (i -> j -> *) (Nat (j -> *) i) | |
Distributive (i -> *) (Nat * i) |
CCC's
class (Cartesian k, Closed k, Curried * (Internal k), I (Internal k) ~ I *, Curryable * (I (Internal k))) => CCC k | x -> k Source
Monoidal Functors
class (Precartesian ((~>) :: x -> x -> *), Precartesian ((~>) :: y -> y -> *), Functor f) => Semimonoidal f where Source
ap :: (Semimonoidal f, CCC (Dom f), CCC (Cod f), Curryable * (f (b ^ a))) => f (b ^ a) ~> (f b ^ f a) Source
ap2Applicative :: Applicative f => (f a * f b) -> f (a * b) Source
class (Cartesian ((~>) :: x -> x -> *), Cartesian ((~>) :: y -> y -> *), Semimonoidal f) => Monoidal f where Source
class (Precocartesian ((~>) :: x -> x -> *), Precocartesian ((~>) :: y -> y -> *), Functor f) => Cosemimonoidal f where Source
Cosemimonoidal * * Id0 | |
Cosemimonoidal * * ((,) e) | |
Cosemimonoidal * * (EnvC p) | |
Cosemimonoidal * * (Tagged k s) | |
Cosemimonoidal k * f => Cosemimonoidal k * (Id1 k f) | |
(Cosemigroup Constraint b, Precocartesian i ((~>) i)) => Cosemimonoidal i Constraint (ConstC i b) | |
(Cosemigroup * b, Precocartesian i ((~>) i)) => Cosemimonoidal i * (Const1 i b) | |
(Cosemimonoidal k1 Constraint f, Cosemimonoidal k k1 g) => Cosemimonoidal k Constraint (ComposeC k k f g) | |
(Cosemimonoidal k1 * f, Cosemimonoidal k k1 g) => Cosemimonoidal k * (Compose1 k k f g) | |
Cosemimonoidal * (k -> k -> *) (At0 k) | |
(Cosemigroup (j -> *) b, Precocartesian i ((~>) i)) => Cosemimonoidal i (j -> *) (Const2 j i b) | |
(Cosemimonoidal k1 (k2 -> *) f, Cosemimonoidal k k1 g) => Cosemimonoidal k (k -> *) (Compose2 k k k f g) | |
Cosemimonoidal (k -> *) * (Colim1 k) | |
Cosemimonoidal (k -> *) (k -> *) (Id1 k) | |
Cosemimonoidal (k -> *) (k -> *) (Lift1 * * k (,) e) |
class (Cocartesian ((~>) :: x -> x -> *), Cocartesian ((~>) :: y -> y -> *), Cosemimonoidal f) => Comonoidal f where Source
Comonoidal * * Id0 | |
Comonoidal * * ((,) e) | |
Comonoidal * * (EnvC p) | |
Comonoidal * * (Tagged k s) | |
Comonoidal k * f => Comonoidal k * (Id1 k f) | |
(Comonoid Constraint b, Cocartesian i ((~>) i)) => Comonoidal i Constraint (ConstC i b) | |
(Comonoid * b, Cocartesian i ((~>) i)) => Comonoidal i * (Const1 i b) | |
(Comonoidal k1 Constraint f, Comonoidal k k1 g) => Comonoidal k Constraint (ComposeC k k f g) | |
(Comonoidal k1 * f, Comonoidal k k1 g) => Comonoidal k * (Compose1 k k f g) | |
Comonoidal * (k -> k -> *) (At0 k) | |
(Comonoid (j -> *) b, Cocartesian i ((~>) i)) => Comonoidal i (j -> *) (Const2 j i b) | |
(Comonoidal k1 (k2 -> *) f, Comonoidal k k1 g) => Comonoidal k (k -> *) (Compose2 k k k f g) | |
Comonoidal (k -> *) * (Colim1 k) | |
Comonoidal (k -> *) (k -> *) (Id1 k) | |
Comonoidal (k -> *) (k -> *) (Lift1 * * k (,) e) |
Monads
class Semimonoidal (m :: x -> x) => Semimonad m where Source
class (Functor f, Category (Dom f)) => Cosemimonad f where Source
Cosemimonad * (Store0 s) | |
Cosemimonad * (EnvC p) | |
Cosemimonad * ((|=) e) | |
Cosemimonad (k -> *) (Id1 k) | |
Cosemimonad (k -> *) (Store1 k s) |
class Cosemimonad f => Comonad f where Source
Monoids
class Precartesian (Arr m) => Semigroup m where Source
Semigroup * Void | |
Semigroup Constraint p | |
Semigroup * (Dict m) | |
Semigroup * ((:-) f m) | |
Semigroup (k -> *) m => Semigroup * (Lim1 k m) | |
Semigroup * p => Semigroup * ((|=) e p) | |
Semigroup * m => Semigroup * (Tagged k s m) | |
(Precartesian k (Arr k a), Semigroup k b) => Semigroup * (Self k a b) | |
Semigroup * b => Semigroup * (Const1 k b a) | |
(Semimonoidal * (k1 -> k) (Nat k k1 f), Semigroup (k1 -> k) m) => Semigroup * (Nat k k f m) | |
(Semimonoidal * k f, Semigroup k m) => Semigroup * (Power1 k v f m) | |
(Semimonoidal * k f, Semimonoidal k k1 g, Semigroup k1 m) => Semigroup * (Compose1 k k f g m) | |
(Semimonoidal k k1 f, Semigroup k1 b) => Semigroup * (Down k k f a b) | |
(Precartesian k (Cod k k1 f), Semigroup k b) => Semigroup * (Up k k f a b) | |
Semigroup (k -> *) (Const1 k Void) | |
Semigroup (k -> *) (Const1 k ()) | |
Semigroup (k -> *) m => Semigroup (k -> *) (Id1 k m) | |
Semigroup Constraint m => Semigroup (k -> k -> Constraint) (CoatC k m) | |
Semigroup * m => Semigroup (k -> k -> *) (Coat0 k m) | |
Semigroup (k -> *) m => Semigroup (k -> *) (Power1 k v m) | |
Semigroup (k -> *) b => Semigroup (k -> *) (Const2 k k b a) | |
(Semimonoidal (k1 -> *) k f, Semimonoidal k k2 g, Semigroup k2 m) => Semigroup (k -> *) (Compose2 k k k f g m) |
class (Semigroup m, Cartesian (Arr m)) => Monoid m where Source
Monoid Constraint () | |
Monoid Constraint m => Monoid * (Dict m) | |
Monoid Constraint m => Monoid * ((:-) f m) | |
Monoid (k -> *) m => Monoid * (Lim1 k m) | |
Monoid * p => Monoid * ((|=) e p) | |
Monoid Constraint m => Monoid Constraint ((|-) f m) | |
Monoid (k -> Constraint) m => Monoid Constraint (LimC k m) | |
Monoid * m => Monoid * (Tagged k s m) | |
(Cartesian k (Arr k a), Monoid k b) => Monoid * (Self k a b) | |
Monoid * b => Monoid * (Const1 k b a) | |
Monoid Constraint b => Monoid Constraint (ConstC k b a) | |
(Monoidal (k1 -> k) * (Nat k k1 f), Monoid (k1 -> k) m) => Monoid * (Nat k k f m) | |
(Monoidal k * f, Monoid k m) => Monoid * (Power1 k v f m) | |
(Monoidal k * f, Monoidal k1 k g, Monoid k1 m) => Monoid * (Compose1 k k f g m) | |
(Monoidal k1 k f, Monoid k1 b) => Monoid * (Down k k f a b) | |
(Cartesian k (Cod k k1 f), Monoid k b) => Monoid * (Up k k f a b) | |
(Monoidal k Constraint f, Monoidal k1 k g, Monoid k1 m) => Monoid Constraint (ComposeC k k f g m) | |
Monoid (k -> *) (Const1 k ()) | |
Monoid (k -> *) m => Monoid (k -> *) (Id1 k m) | |
Monoid Constraint m => Monoid (k -> k -> Constraint) (CoatC k m) | |
Monoid * m => Monoid (k -> k -> *) (Coat0 k m) | |
Monoid (k -> *) m => Monoid (k -> *) (Power1 k v m) | |
Monoid (k -> *) b => Monoid (k -> *) (Const2 k k b a) | |
(Monoidal k (k1 -> *) f, Monoidal k2 k g, Monoid k2 m) => Monoid (k -> *) (Compose2 k k k f g m) |
class Precocartesian (Arr m) => Cosemigroup m where Source
class (Cosemigroup m, Cocartesian (Arr m)) => Comonoid m where Source
Comonoid * Void | |
Comonoid * m => Comonoid * (Id0 m) | |
Comonoid * m => Comonoid * (e, m) | |
Comonoid (k -> *) m => Comonoid * (Colim1 k m) | |
Comonoid * m => Comonoid * (Tagged k s m) | |
(Comonoidal k * f, Comonoid k m) => Comonoid * (Id1 k f m) | |
Comonoid * b => Comonoid * (Const1 k b a) | |
Comonoid Constraint b => Comonoid Constraint (ConstC k b a) | |
(Comonoidal k * f, Comonoidal k1 k g, Comonoid k1 m) => Comonoid * (Compose1 k k f g m) | |
(Comonoidal k Constraint f, Comonoidal k1 k g, Comonoid k1 m) => Comonoid Constraint (ComposeC k k f g m) | |
Comonoid (k -> *) (Const1 k Void) | |
Comonoid (k -> *) m => Comonoid (k -> *) (Id1 k m) | |
Comonoid * m => Comonoid (k -> k -> *) (At0 k m) | |
Comonoid (k -> *) b => Comonoid (k -> *) (Const2 k k b a) | |
(Comonoidal k (k1 -> *) f, Comonoidal k2 k g, Comonoid k2 m) => Comonoid (k -> *) (Compose2 k k k f g m) | |
Comonoid (k -> *) m => Comonoid (k -> *) (Lift1 * * k (,) e m) |
comultOp :: (Cosemimonoidal f, Cosemigroup m) => f m ~> (f m + f m) Source
Strength
class Functor f => Costrength f where Source
costrength :: f (a + b) ~> (a + f b) Source
(Functor * * f, Traversable f) => Costrength * f |
Identity functors
Kan extensions
class (c ~ Hom) => HasRan c | k -> c where Source
ranCurried :: Dict (Curried Compose (Ran :: (i -> j) -> (i -> k) -> j -> k)) Source
ranProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Ran :: (i -> j) -> (i -> k) -> j -> k)) Source
ranFunctor :: Dict (Functor (Ran f g :: j -> k)) Source
iotaRan :: forall f g id. (Category (Cod f), Category (Dom f), Functor g, Identity id) => Iso (Ran id f) (Ran id g) f g Source
jotRan :: forall f. Id ~> Ran f f Source
return for Codensity
HasRan * (->) |
class (c ~ Hom) => HasLan c | k -> c where Source
lanCocurried :: Dict (Cocurried (Lan :: (i -> j) -> (i -> k) -> j -> k) Compose) Source
lanProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Lan :: (i -> j) -> (i -> k) -> j -> k)) Source
lanFunctor :: Dict (Functor (Lan f g :: j -> k)) Source
epsilonLan :: forall f g id. (Category (Cod f), Category (Dom f), Functor f, Identity id) => Iso (Lan id f) (Lan id g) f g Source
Categories
Products
data Prod :: (i, j) -> (i, j) -> * where Source
(Functor i * ((~>) i a), Functor j * ((~>) j b), (~) ((,) i j) ab ((,) i j a b)) => Functor ((,) i j) * (Prod i j ab) | |
(Category i ((~>) i), Category j ((~>) j)) => Category ((,) i j) (Prod i j) | |
(Groupoid i ((~>) i), Groupoid j ((~>) j)) => Groupoid ((,) i j) (Prod i j) | |
(Contravariant (i -> *) i ((~>) i), Contravariant (j -> *) j ((~>) j)) => Contravariant ((,) i j -> *) ((,) i j) (Prod i j) |
runProd :: forall a b c d. (Category ((~>) :: i -> i -> *), Category ((~>) :: j -> j -> *)) => Prod `(a, c)` `(b, d)` -> (a ~> b, c ~> d) Source
diagProdAdj :: forall a b c a' b' c'. Cartesian ((~>) :: i -> i -> *) => Iso (`(a, a)` ~> `(b, c)`) (`(a', a')` ~> `(b', c')`) (a ~> (b * c)) (a' ~> (b' * c')) Source
sumDiagAdj :: forall a b c a' b' c'. Cocartesian ((~>) :: i -> i -> *) => Iso ((b + c) ~> a) ((b' + c') ~> a') (`(b, c)` ~> `(a, a)`) (`(b', c')` ~> `(a', a')`) Source
Unit
Empty
Candidates for Removal:
class (Profunctor p, p ~ (~>)) => Semicategory p Source
(Profunctor k k * p, (~) (k -> k -> *) p ((~>) k)) => Semicategory k p |
Internals
Categories
Composition
Compose | |
|
(Comonoidal k1 * f, Comonoidal k k1 g) => Comonoidal k * (Compose1 k k f g) | |
(Cosemimonoidal k1 * f, Cosemimonoidal k k1 g) => Cosemimonoidal k * (Compose1 k k f g) | |
(Monoidal k1 * f, Monoidal k k1 g) => Monoidal k * (Compose1 k k f g) | |
(Semimonoidal * k1 f, Semimonoidal k1 k g) => Semimonoidal * k (Compose1 k k f g) | |
(Functor k1 * f, Functor k k1 g) => Functor k * (Compose1 k k f g) | |
((-|) k * f g, (-|) * k f' g', Category * (Dom * k f), Category k (Cod k * f)) => (-|) * * (Compose1 k * f' f) (Compose1 k * g g') | |
((-|) k Constraint f g, (-|) * k f' g', Category Constraint (Dom Constraint k f), Category k (Cod k Constraint f)) => (-|) * Constraint (Compose1 k Constraint f' f) (ComposeC k * g g') | |
((-|) k (k1 -> *) f g, (-|) * k f' g', Category (k1 -> *) (Dom (k1 -> *) k f), Category k (Cod k (k1 -> *) f)) => (-|) * (k -> *) (Compose1 k (k -> *) f' f) (Compose2 k k * g g') | |
(Comonoidal k * f, Comonoidal k1 k g, Comonoid k1 m) => Comonoid * (Compose1 k k f g m) | |
(Cosemimonoidal k * f, Cosemimonoidal k1 k g, Cosemigroup k1 m) => Cosemigroup * (Compose1 k k f g m) | |
(Monoidal k * f, Monoidal k1 k g, Monoid k1 m) => Monoid * (Compose1 k k f g m) | |
(Semimonoidal * k f, Semimonoidal k k1 g, Semigroup k1 m) => Semigroup * (Compose1 k k f g m) | |
Tensor (* -> *) (Compose1 * *) | |
Semitensor (* -> *) (Compose1 * *) | |
Functor (k -> *) ((k -> k) -> k -> *) (Compose1 k k) | |
Cocurried (k -> k) (k -> *) (k -> *) (Lan1 k k) (Compose1 k k) | |
Curried (k -> *) (k -> k) (k -> *) (Compose1 k k) (Ran1 k k) | |
Contravariant * k f => Contravariant (k -> *) (k -> k) (Compose1 k k f) | |
Functor k * f => Functor (k -> k) (k -> *) (Compose1 k k f) | |
type I (* -> *) (Compose1 * *) = Id * | |
type Tensorable (* -> *) (Compose1 * *) = Functor * * | |
type Cocurryable (k1 -> k) (k1 -> *) (k -> *) (Compose1 k k1) = Functor k * | |
type Curryable (k1 -> *) (k1 -> k) (k -> *) (Compose1 k k1) = Functor k * |
newtype Compose2 f g a b Source
Compose2 | |
|
((-|) k (k1 -> *) f g, (-|) * k f' g', Category (k1 -> *) (Dom (k1 -> *) k f), Category k (Cod k (k1 -> *) f)) => (-|) * (k -> *) (Compose1 k (k -> *) f' f) (Compose2 k k * g g') | |
(Comonoidal k1 (k2 -> *) f, Comonoidal k k1 g) => Comonoidal k (k -> *) (Compose2 k k k f g) | |
(Cosemimonoidal k1 (k2 -> *) f, Cosemimonoidal k k1 g) => Cosemimonoidal k (k -> *) (Compose2 k k k f g) | |
(Monoidal k1 (k2 -> *) f, Monoidal k k1 g) => Monoidal k (k -> *) (Compose2 k k k f g) | |
(Functor k1 (k2 -> *) f, Functor k k1 g) => Functor k (k -> *) (Compose2 k k k f g) | |
(Semimonoidal (k2 -> *) k1 f, Semimonoidal k1 k g) => Semimonoidal (k -> *) k (Compose2 k k k f g) | |
Cocurried (k -> k) (k -> k -> *) (k -> k -> *) (Lan2 k k k) (Compose2 k k k) | |
Functor (k -> k -> *) ((k -> k) -> k -> k -> *) (Compose2 k k k) | |
Contravariant (k1 -> *) k f => Contravariant (k -> k -> *) (k -> k) (Compose2 k k k f) | |
Functor k (k1 -> *) f => Functor (k -> k) (k -> k -> *) (Compose2 k k k f) | |
Tensor ((k -> *) -> k -> *) (Compose2 (k -> *) k (k -> *)) | |
Semitensor ((k -> *) -> k -> *) (Compose2 (k -> *) k (k -> *)) | |
(Comonoidal k (k1 -> *) f, Comonoidal k2 k g, Comonoid k2 m) => Comonoid (k -> *) (Compose2 k k k f g m) | |
(Cosemimonoidal k (k1 -> *) f, Cosemimonoidal k2 k g, Cosemigroup k2 m) => Cosemigroup (k -> *) (Compose2 k k k f g m) | |
(Monoidal k (k1 -> *) f, Monoidal k2 k g, Monoid k2 m) => Monoid (k -> *) (Compose2 k k k f g m) | |
(Semimonoidal (k1 -> *) k f, Semimonoidal k k2 g, Semigroup k2 m) => Semigroup (k -> *) (Compose2 k k k f g m) | |
type Cocurryable (k2 -> k) (k2 -> k1 -> *) (k -> k1 -> *) (Compose2 k k1 k2) = Functor k (k1 -> *) | |
type I ((k -> *) -> k -> *) (Compose2 (k -> *) k (k -> *)) = Id (k -> *) | |
type Tensorable ((k -> *) -> k -> *) (Compose2 (k -> *) k (k -> *)) = Functor (k -> *) (k -> *) |
class f (g a) => ComposeC f g a Source
We can compose constraints
Limits
LimC :: (i -> Constraint) -> Constraint
takes limits in the category of constraints
type instance Lim = LimC
p (Any i) => LimC i p | |
Monoid (k -> Constraint) m => Monoid Constraint (LimC k m) | |
Semimonoidal Constraint (k -> Constraint) (LimC k) | |
(~|) (k -> Constraint) Constraint Constraint (ConstC k) (LimC k) | |
Monoidal (k -> Constraint) Constraint (LimC k) | |
Functor (k -> Constraint) Constraint (LimC k) | |
(-|) (k -> Constraint) Constraint (ConstC k) (LimC k) |
Functor k * f => Functor k * (Const2 k k f a) | |
Constant k (k -> *) (Const2 k k) | |
(Comonoid (j -> *) b, Cocartesian i ((~>) i)) => Comonoidal i (j -> *) (Const2 j i b) | |
(Cosemigroup (j -> *) b, Precocartesian i ((~>) i)) => Cosemimonoidal i (j -> *) (Const2 j i b) | |
(Monoid (j -> *) b, Cartesian i ((~>) i)) => Monoidal i (j -> *) (Const2 j i b) | |
Functor k (k -> *) (Const2 k k f) | |
(Semigroup (j -> *) b, Precartesian i ((~>) i)) => Semimonoidal (j -> *) i (Const2 j i b) | |
Contravariant (k -> *) k (Const2 k k k) | |
Functor (k -> *) (k -> k -> *) (Const2 k k) | |
RelMonad (k -> *) (k -> k -> *) (Const2 k k) | |
(-|) (k -> *) (k -> k -> *) (Colim2 k k) (Const2 k k) | |
(-|) (k -> k -> *) (k -> *) (Const2 k k) (Lim2 k k) | |
(~|) (k -> k -> *) (k -> *) (k -> *) (Const2 k k) (Lim2 k k) | |
Initial (k -> *) i => Initial (k -> k -> *) (Const2 k k i) | |
Terminal (k -> *) t => Terminal (k -> k -> *) (Const2 k k t) | |
Comonoid (k -> *) b => Comonoid (k -> *) (Const2 k k b a) | |
Cosemigroup (k -> *) b => Cosemigroup (k -> *) (Const2 k k b a) | |
Monoid (k -> *) b => Monoid (k -> *) (Const2 k k b a) | |
Semigroup (k -> *) b => Semigroup (k -> *) (Const2 k k b a) |
b => ConstC k b a | |
Constant k Constraint (ConstC k) | |
(Comonoid Constraint b, Cocartesian i ((~>) i)) => Comonoidal i Constraint (ConstC i b) | |
(Cosemigroup Constraint b, Precocartesian i ((~>) i)) => Cosemimonoidal i Constraint (ConstC i b) | |
(Monoid Constraint b, Cartesian i ((~>) i)) => Monoidal i Constraint (ConstC i b) | |
(Semigroup Constraint b, Precartesian i ((~>) i)) => Semimonoidal Constraint i (ConstC i b) | |
Functor k Constraint (ConstC k b) | |
Functor Constraint (k -> Constraint) (ConstC k) | |
RelMonad Constraint (k -> Constraint) (ConstC k) | |
Comonoid Constraint b => Comonoid Constraint (ConstC k b a) | |
Cosemigroup Constraint b => Cosemigroup Constraint (ConstC k b a) | |
Monoid Constraint b => Monoid Constraint (ConstC k b a) | |
(~|) (k -> Constraint) Constraint Constraint (ConstC k) (LimC k) | |
(-|) (k -> Constraint) Constraint (ConstC k) (LimC k) | |
Initial Constraint i => Initial (k -> Constraint) (ConstC k i) | |
Terminal (k -> Constraint) (ConstC k ()) |
Comonoid (k -> *) m => Comonoid * (Colim1 k m) | |
Cosemigroup (k -> *) m => Cosemigroup * (Colim1 k m) | |
(-|) * (k -> *) (Colim1 k) (Const1 k) | |
(~|) * (i -> *) (i -> *) (Colim1 i) (Const1 i) | |
Comonoidal (k -> *) * (Colim1 k) | |
Cosemimonoidal (k -> *) * (Colim1 k) | |
Functor (k -> *) * (Colim1 k) |
Identities
Identity * Id0 | |
Comonoidal * * Id0 | |
Cosemimonoidal * * Id0 | |
Functor * * Id0 | |
RelComposed * * Id0 | |
(-|) * * Id0 Id0 | |
(~|) * * * Id0 Id0 | |
Comonoid * m => Comonoid * (Id0 m) | |
Cosemigroup * m => Cosemigroup * (Id0 m) |
Comonoidal k * f => Comonoidal k * (Id1 k f) | |
Cosemimonoidal k * f => Cosemimonoidal k * (Id1 k f) | |
Monoidal k * f => Monoidal k * (Id1 k f) | |
Semimonoidal * k f => Semimonoidal * k (Id1 k f) | |
Contravariant * k f => Contravariant * k (Id1 k f) | |
Functor k * f => Functor k * (Id1 k f) | |
(Comonoidal k * f, Comonoid k m) => Comonoid * (Id1 k f m) | |
(Cosemimonoidal k * f, Cosemigroup k m) => Cosemigroup * (Id1 k f m) | |
Comonad (k -> *) (Id1 k) | |
Cosemimonad (k -> *) (Id1 k) | |
Identity (k -> *) (Id1 k) | |
Monad (k -> *) (Id1 k) | |
Semimonad (k -> *) (Id1 k) | |
Comonoid (k -> *) m => Comonoid (k -> *) (Id1 k m) | |
Cosemigroup (k -> *) m => Cosemigroup (k -> *) (Id1 k m) | |
Monoid (k -> *) m => Monoid (k -> *) (Id1 k m) | |
Semigroup (k -> *) m => Semigroup (k -> *) (Id1 k m) | |
Comonoidal (k -> *) (k -> *) (Id1 k) | |
Cosemimonoidal (k -> *) (k -> *) (Id1 k) | |
Monoidal (k -> *) (k -> *) (Id1 k) | |
Semimonoidal (k -> *) (k -> *) (Id1 k) | |
Functor (k -> *) (k -> *) (Id1 k) | |
RelComposed (k -> *) (k -> *) (Id1 k) | |
RelMonad (k -> *) (k -> *) (Id1 k) | |
(-|) (k -> *) (k -> *) (Id1 k) (Id1 k) | |
(~|) (k -> *) (k -> *) (k -> *) (Id1 k) (Id1 k) |
Lifts
(Functor k1 (k2 -> *) p, Post k1 (k2 -> *) (Functor k2 *) p, Functor k k1 f, Functor k k2 g) => Functor k * (Lift1 k k k p f g) | |
Curried (k -> k -> *) (k -> k -> *) (k -> *) (Copower2_1 k k) (Lift1 (k -> *) (k -> *) k (Nat * k)) | |
Curried * k1 * p q => Curried (k -> *) (k -> k) (k -> *) (Lift1 * k k p) (Lift1 k * k q) | |
Functor (k -> k -> *) ((k -> k) -> (k -> k) -> k -> *) (Lift1 k k k) | |
Symmetric k * p => Symmetric (k -> k) (k -> *) (Lift1 k k k p) | |
Contravariant (k1 -> *) k p => Contravariant ((k -> k) -> k -> *) (k -> k) (Lift1 k k k p) | |
Functor k (k1 -> *) p => Functor (k -> k) ((k -> k) -> k -> *) (Lift1 k k k p) | |
Powered (k -> *) (k -> *) (Lift1 * * k (->)) | |
Comonoidal (k -> *) (k -> *) (Lift1 * * k (,) e) | |
Cosemimonoidal (k -> *) (k -> *) (Lift1 * * k (,) e) | |
Post k (k1 -> *) (Contravariant * k1) p => Contravariant (k -> *) (k -> k) (Lift1 k k k p f) | |
Post k (k1 -> *) (Functor k1 *) p => Functor (k -> k) (k -> *) (Lift1 k k k p f) | |
Powered (k -> k -> *) (k -> k -> *) (Lift2 (k -> *) (k -> *) k k (Lift1 * * k (->))) | |
Foldable (k -> *) (k -> *) (Lift1 * * k Either e) | |
Foldable (k -> *) (k -> *) (Lift1 * * k (,) e) | |
Foldable (k -> k -> *) (k -> k -> *) (Lift2 (k -> *) (k -> *) k k (Lift1 * * k Either) e) | |
Foldable (k -> k -> *) (k -> k -> *) (Lift2 (k -> *) (k -> *) k k (Lift1 * * k (,)) e) | |
Tensor * p => Tensor (k -> *) (Lift1 * * k p) | |
Semitensor * p => Semitensor (k -> *) (Lift1 * * k p) | |
Comonoid (k -> *) m => Comonoid (k -> *) (Lift1 * * k (,) e m) | |
Cosemigroup (k -> *) m => Cosemigroup (k -> *) (Lift1 * * k (,) e m) | |
type Curryable (k1 -> *) (k1 -> k) (k1 -> *) (Lift1 * k k1 p) = Post k1 * (Curryable * k * p) | |
type I (k -> *) (Lift1 * * k p) = Const1 k (I * p) | |
type Tensorable (k -> *) (Lift1 * * k p) = Post k * (Tensorable * p) |
newtype Lift2 p f g a b Source
Curried (k -> *) k2 (k3 -> *) p q => Curried (k -> k -> *) (k -> k) (k -> k -> *) (Lift2 (k -> *) k k k p) (Lift2 k (k -> *) k k q) | |
Functor (k -> k -> k -> *) ((k -> k) -> (k -> k) -> k -> k -> *) (Lift2 k k k k) | |
Symmetric k (k1 -> *) p => Symmetric (k -> k) (k -> k -> *) (Lift2 k k k k p) | |
Contravariant (k1 -> k2 -> *) k p => Contravariant ((k -> k) -> k -> k -> *) (k -> k) (Lift2 k k k k p) | |
Functor k (k1 -> k2 -> *) p => Functor (k -> k) ((k -> k) -> k -> k -> *) (Lift2 k k k k p) | |
Powered (k -> k -> *) (k -> k -> *) (Lift2 (k -> *) (k -> *) k k (Lift1 * * k (->))) | |
Post k (k1 -> k2 -> *) (Contravariant (k2 -> *) k1) p => Contravariant (k -> k -> *) (k -> k) (Lift2 k k k k p f) | |
Post k (k1 -> k2 -> *) (Functor k1 (k2 -> *)) p => Functor (k -> k) (k -> k -> *) (Lift2 k k k k p f) | |
Foldable (k -> k -> *) (k -> k -> *) (Lift2 (k -> *) (k -> *) k k (Lift1 * * k Either) e) | |
Foldable (k -> k -> *) (k -> k -> *) (Lift2 (k -> *) (k -> *) k k (Lift1 * * k (,)) e) | |
Tensor (k -> *) p => Tensor (k -> k -> *) (Lift2 (k -> *) (k -> *) k k p) | |
Semitensor (i -> *) p => Semitensor (k -> i -> *) (Lift2 (i -> *) (i -> *) i k p) | |
type Curryable (k3 -> k -> *) (k3 -> k1) (k3 -> k2 -> *) (Lift2 (k2 -> *) k1 k k3 p) = Post k3 (k2 -> *) (Curryable (k -> *) k1 (k2 -> *) p) | |
type I (k -> k1 -> *) (Lift2 (k1 -> *) (k1 -> *) k1 k p) = Const2 k1 k (I (k1 -> *) p) | |
type Tensorable (k -> i -> *) (Lift2 (i -> *) (i -> *) i k p) = Post k (i -> *) (Tensorable (i -> *) p) |
class r (p a) (q a) => LiftC r p q a Source
class r (f a) (g a) b => LiftC2 r f g a b Source
r (f a) (g a) b => LiftC2 k k k k r f g a b | |
Curried (k -> Constraint) k2 (k3 -> Constraint) p q => Curried (k -> k -> Constraint) (k -> k) (k -> k -> Constraint) (LiftC2 (k -> Constraint) k k k p) (LiftC2 k (k -> Constraint) k k q) | |
Functor (k -> k -> k -> Constraint) ((k -> k) -> (k -> k) -> k -> k -> Constraint) (LiftC2 k k k k) | |
Symmetric k (k1 -> Constraint) p => Symmetric (k -> k) (k -> k -> Constraint) (LiftC2 k k k k p) | |
Contravariant (k1 -> k2 -> Constraint) k p => Contravariant ((k -> k) -> k -> k -> Constraint) (k -> k) (LiftC2 k k k k p) | |
Functor k (k1 -> k2 -> Constraint) p => Functor (k -> k) ((k -> k) -> k -> k -> Constraint) (LiftC2 k k k k p) | |
Post k (k1 -> k2 -> Constraint) (Contravariant (k2 -> Constraint) k1) p => Contravariant (k -> k -> Constraint) (k -> k) (LiftC2 k k k k p f) | |
Post k (k1 -> k2 -> Constraint) (Functor k1 (k2 -> Constraint)) p => Functor (k -> k) (k -> k -> Constraint) (LiftC2 k k k k p f) | |
Tensor (k -> Constraint) p => Tensor (k -> k -> Constraint) (LiftC2 (k -> Constraint) (k -> Constraint) k k p) | |
Semitensor (k -> Constraint) p => Semitensor (k -> k -> Constraint) (LiftC2 (k -> Constraint) (k -> Constraint) k k p) | |
type Curryable (k3 -> k -> Constraint) (k3 -> k1) (k3 -> k2 -> Constraint) (LiftC2 (k2 -> Constraint) k1 k k3 p) = Post k3 (k2 -> Constraint) (Curryable (k -> Constraint) k1 (k2 -> Constraint) p) | |
type I (k -> k1 -> Constraint) (LiftC2 (k1 -> Constraint) (k1 -> Constraint) k1 k p) | |
type Tensorable (k1 -> k -> Constraint) (LiftC2 (k -> Constraint) (k -> Constraint) k k1 p) = Post k1 (k -> Constraint) (Tensorable (k -> Constraint) p) |
Copowers
Copower x (f a) |
Contravariant * k f => Contravariant * k (Copower1 k x f) | |
Functor k * f => Functor k * (Copower1 k x f) | |
Functor * ((k -> *) -> k -> *) (Copower1 k) | |
Curried (k -> *) (k -> *) * (Copower1 k) (Nat * k) | |
Functor (k -> *) (k -> *) (Copower1 k x) | |
type Curryable (k -> *) (k -> *) * (Copower1 k) = Const * Constraint () |
Copower2 x (f a b) |
Post k1 (k -> *) (Contravariant * k) f => Contravariant * k (Copower2 k k x f a) | |
Post k1 (k -> *) (Functor k *) f => Functor k * (Copower2 k k x f a) | |
Functor * ((k -> k -> *) -> k -> k -> *) (Copower2 k k) | |
Functor k (k1 -> *) f => Functor k (k -> *) (Copower2 k k x f) | |
Contravariant (k1 -> *) k f => Contravariant (k -> *) k (Copower2 k k x f) | |
Curried (k -> k -> *) (k -> k -> *) * (Copower2 k k) (Nat (k -> *) k) | |
Functor (k -> k -> *) (k -> k -> *) (Copower2 k k x) | |
type Curryable (k -> k1 -> *) (k -> k1 -> *) * (Copower2 k k1) = Const * Constraint () |
data Copower2_1 x f a b Source
Copower2_1 (x a) (f a b) |
Post k1 (k -> *) (Contravariant * k) f => Contravariant * k (Copower2_1 k k x f a) | |
Post k1 (k -> *) (Functor k *) f => Functor k * (Copower2_1 k k x f a) | |
(Functor k * x, Functor k (k1 -> *) f) => Functor k (k -> *) (Copower2_1 k k x f) | |
(Contravariant * k x, Contravariant (k1 -> *) k f) => Contravariant (k -> *) k (Copower2_1 k k x f) | |
Functor (k -> *) ((k -> k -> *) -> k -> k -> *) (Copower2_1 k k) | |
Curried (k -> k -> *) (k -> k -> *) (k -> *) (Copower2_1 k k) (Lift1 (k -> *) (k -> *) k (Nat * k)) | |
Functor (k -> k -> *) (k -> k -> *) (Copower2_1 k k x) | |
type Curryable (k -> k1 -> *) (k -> k1 -> *) (k -> *) (Copower2_1 k k1) = Const (k -> *) Constraint () |
Kan extensions
Base Re-exports
data Constraint :: BOX
Prelude Re-Exports
undefined :: a
($) :: (a -> b) -> a -> b infixr 0
Application operator. This operator is redundant, since ordinary
application (f x)
means the same as (f
. However, $
x)$
has
low, right-associative binding precedence, so it sometimes allows
parentheses to be omitted; for example:
f $ g $ h x = f (g (h x))
It is also useful in higher-order situations, such as
,
or map
($
0) xs
.zipWith
($
) fs xs
data Either a b :: * -> * -> *
The Either
type represents values with two possibilities: a value of
type
is either Either
a b
or Left
a
.Right
b
The Either
type is sometimes used to represent a value which is
either correct or an error; by convention, the Left
constructor is
used to hold an error value and the Right
constructor is used to
hold a correct value (mnemonic: "right" also means "correct").
Tensor * Either | |
Semitensor * Either | |
Symmetric * * Either | |
Functor * * (Either e) | |
Foldable * * (Either a) | |
() :=> (Monad (Either a)) | |
() :=> (Functor (Either a)) | |
() :=> (Applicative (Either a)) | |
Traversable * (Either a) | |
Functor * (* -> *) Either | |
Foldable * (* -> *) Either | |
Monad (Either e) | |
Functor (Either a) | |
Applicative (Either e) | |
Foldable (Either a) | |
Traversable (Either a) | |
Generic1 (Either a) | |
(Eq a, Eq b) => Eq (Either a b) | |
(Ord a, Ord b) => Ord (Either a b) | |
(Read a, Read b) => Read (Either a b) | |
(Show a, Show b) => Show (Either a b) | |
Generic (Either a b) | |
Semigroup (Either a b) | |
Typeable (* -> * -> *) Either | |
(Eq a, Eq b) :=> (Eq (Either a b)) | |
(Ord a, Ord b) :=> (Ord (Either a b)) | |
(Read a, Read b) :=> (Read (Either a b)) | |
(Show a, Show b) :=> (Show (Either a b)) | |
Foldable (k -> *) (k -> *) (Lift1 * * k Either e) | |
Foldable (k -> k -> *) (k -> k -> *) (Lift2 (k -> *) (k -> *) k k (Lift1 * * k Either) e) | |
type I * Either = Void | |
type Tensorable * Either = Const * Constraint () | |
type Rep1 (Either a) = D1 D1Either ((:+:) (C1 C1_0Either (S1 NoSelector (Rec0 a))) (C1 C1_1Either (S1 NoSelector Par1))) | |
type Rep (Either a b) = D1 D1Either ((:+:) (C1 C1_0Either (S1 NoSelector (Rec0 a))) (C1 C1_1Either (S1 NoSelector (Rec0 b)))) | |
type (==) (Either k k1) a b = EqEither k k1 a b |
data Maybe a :: * -> *
The Maybe
type encapsulates an optional value. A value of type
either contains a value of type Maybe
aa
(represented as
),
or it is empty (represented as Just
aNothing
). Using Maybe
is a good way to
deal with errors or exceptional cases without resorting to drastic
measures such as error
.
The Maybe
type is also a monad. It is a simple kind of error
monad, where all errors are represented by Nothing
. A richer
error monad can be built using the Either
type.
Alternative Maybe | |
Monad Maybe | |
Functor Maybe | |
MonadPlus Maybe | |
Applicative Maybe | |
Foldable Maybe | |
Traversable Maybe | |
Generic1 Maybe | |
Traversable * Maybe | |
Functor * * Maybe | |
Foldable * * Maybe | |
() :=> (Alternative Maybe) | |
() :=> (Functor Maybe) | |
() :=> (MonadPlus Maybe) | |
() :=> (Applicative Maybe) | |
Eq a => Eq (Maybe a) | |
Ord a => Ord (Maybe a) | |
Read a => Read (Maybe a) | |
Show a => Show (Maybe a) | |
Generic (Maybe a) | |
Monoid a => Monoid (Maybe a) | Lift a semigroup into |
Semigroup a => Semigroup (Maybe a) | |
(Eq a) :=> (Eq (Maybe a)) | |
(Ord a) :=> (Ord (Maybe a)) | |
(Read a) :=> (Read (Maybe a)) | |
(Show a) :=> (Show (Maybe a)) | |
(Monoid a) :=> (Monoid (Maybe a)) | |
type Rep1 Maybe = D1 D1Maybe ((:+:) (C1 C1_0Maybe U1) (C1 C1_1Maybe (S1 NoSelector Par1))) | |
type Rep (Maybe a) = D1 D1Maybe ((:+:) (C1 C1_0Maybe U1) (C1 C1_1Maybe (S1 NoSelector (Rec0 a)))) | |
type (==) (Maybe k) a b = EqMaybe k a b |
Re-exports
newtype Tagged s b :: k -> * -> *
data Proxy t :: k -> *
A concrete, poly-kinded proxy type
Cartesian i ((~>) i) => Monoidal i * (Proxy i) | |
Precartesian i ((~>) i) => Semimonoidal * i (Proxy i) | |
Contravariant * k (Proxy k) | |
Functor k * (Proxy k) | |
Monad (Proxy *) | |
Functor (Proxy *) | |
Applicative (Proxy *) | |
Foldable (Proxy *) | |
Traversable (Proxy *) | |
Bounded (Proxy k s) | |
Enum (Proxy k s) | |
Eq (Proxy k s) | |
Ord (Proxy k s) | |
Read (Proxy k s) | |
Show (Proxy k s) | |
Ix (Proxy k s) | |
Generic (Proxy * t) | |
Monoid (Proxy * s) | |
type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1) |
class Category cat where
A class for categories. id and (.) must form a monoid.
Category * (->) | |
Category Constraint (:-) | |
Category () Unit | |
Category Void Empty | |
Monad m => Category * (Kleisli m) | |
Category k (Coercion k) | |
Category k ((:~:) k) | |
Category (Discrete k) ((|~>|) k) | |
Category j ((~>) j) => Category (i -> j) (Nat j i) | |
(Category i ((~>) i), Category j ((~>) j)) => Category ((,) i j) (Prod i j) |
data Void :: *
Eq Void | |
Data Void | |
Ord Void | |
Read Void | |
Show Void | |
Ix Void | |
Generic Void | |
Exception Void | |
Semigroup Void | |
Hashable Void | |
Typeable * Void | |
Category Void Empty | |
Comonoid * Void | |
Cosemigroup * Void | |
Semigroup * Void | |
Initial * Void | |
Groupoid Void Empty | |
Symmetric Void * Empty | |
Functor Void * No | |
Contravariant * Void (Empty a) | |
Functor Void * (Empty a) | |
Functor Void (Void -> *) Empty | |
Contravariant (Void -> *) Void Empty | |
Comonoid (k -> *) (Const1 k Void) | |
Cosemigroup (k -> *) (Const1 k Void) | |
Semigroup (k -> *) (Const1 k Void) | |
type Rep Void = D1 D1Void (C1 C1_0Void (S1 NoSelector (Rec0 Void))) | |
type Hom Void * = Empty | |
type Rel Void * = No |