hask-0: Categories

Copyright(c) Edward Kmett 2008-2014 and Sjoerd Visscher 2014
LicenseBSD3
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Hask.Core

Contents

Description

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.

Synopsis

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

Instances

type Hom * * = (->) 
type Hom Constraint * = (:-) 
type Hom Constraint Constraint = (|-) 
type Hom () * = Unit 
type Hom Void * = Empty 
type Hom (Discrete k) * = (|~>|) k 
type Hom (k1 -> k) * = Nat k k1 
type Hom ((,) k k1) * = Prod k k1 
type Hom (k2 -> k1) (k2 -> k) = Lift k k1 k1 k2 (Hom k1 k) 

type (~>) = (Hom :: i -> i -> *) infixr 0 Source

type (^) a b = Internal Hom b a infixr 8 Source

type Dom f = (Hom :: i -> i -> *) Source

type Cod f = (Hom :: j -> j -> *) Source

type Cod2 f = (Hom :: k -> k -> *) Source

type Arr a = (Hom :: i -> i -> *) Source

type Enriched k = (Hom :: i -> i -> j) Source

type Internal k = (Hom :: i -> i -> i) Source

type External k = (Hom :: i -> i -> *) Source

type Natural k = (Hom :: (i -> j) -> (i -> j) -> *) Source

Natural transformations

newtype Nat f g infixr 0 Source

Constructors

Nat infixr 0 

Fields

runNat :: forall a. f a ~> g a
 

Instances

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 -> *) 

nat2 :: (forall a b. f a b ~> g a b) -> f ~> g Source

nat3 :: (forall a b c. f a b c ~> g a b c) -> f ~> g Source

nat4 :: (forall a b c d. f a b c d ~> g a b c d) -> f ~> g Source

runNat2 :: Nat (k1 -> k) k2 f g -> Hom k * (f a1 a) (g a1 a) Source

runNat3 :: Nat (k2 -> k1 -> k) k3 f g -> Hom k * (f a2 a1 a) (g a2 a1 a) Source

runNat4 :: Nat (k3 -> k2 -> k1 -> k) k4 f g -> Hom k * (f a3 a2 a1 a) (g a3 a2 a1 a) Source

Functors

class Functor f where Source

Methods

fmap :: (a ~> b) -> f a ~> f b Source

Instances

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) 

first :: Functor f => (a ~> b) -> f a c ~> f b c Source

class Contravariant f where Source

Methods

contramap :: (b ~> a) -> f a ~> f b Source

Instances

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

class (hom ~ Hom) => Composed hom | k -> hom where Source

Associated Types

type Compose :: (j -> k) -> (i -> j) -> i -> k Source

Methods

compose :: f (g a) `hom` Compose f g a Source

decompose :: Compose f g a `hom` f (g a) Source

Instances

Composed * (->) 
Composed Constraint (:-) 
Composed (k -> *) (Nat * k) 

type · = Compose infixr 9 Source

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

class LimC (f `·` p) => Post f p Source

Instances

LimC k (· Constraint k1 k f p) => Post k k f p 

Derived notions

fmap1 :: forall p a b c. Post Functor p => (a ~> b) -> p c a ~> p c b Source

contramap1 :: forall p a b c. Post Contravariant p => (a ~> b) -> p c b ~> p c a Source

fmap2 :: forall p a b c d. Post (Post Functor) p => (a ~> b) -> p c d a ~> p c d b Source

class (Functor p, Post Functor p) => Bifunctor p Source

Instances

(Functor k (k1 -> k2) p, Post k (k1 -> k2) (Functor k1 k2) p) => Bifunctor k k k p 

bimap :: (Bifunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p a c ~> p b d Source

class (Contravariant p, Post Functor p) => Profunctor p Source

Instances

(Contravariant (k1 -> k2) k p, Post k (k1 -> k2) (Functor k1 k2) p) => Profunctor k k k p 

dimap :: (Profunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p b c ~> p a d Source

class (Contravariant p, Functor p) => Phantom p Source

Instances

(Contravariant k1 k p, Functor k k1 p) => Phantom k k p 

Colim -| Const -| Lim

class (k ~ (~>)) => Cocomplete k where Source

Minimal complete definition

colim

Associated Types

type Colim :: (i -> j) -> j Source

Methods

colim :: k (f a) (Colim f) Source

cocomplete :: Dict ((Colim :: (i -> j) -> j) -| Const) Source

Instances

Cocomplete * (->) 
Cocomplete (i -> *) (Nat * i) 

class (Const ~ k) => Constant k | j i -> k where Source

Minimal complete definition

Nothing

Associated Types

type Const :: j -> i -> j Source

Methods

_Const :: Iso (k b a) (k b' a') b b' Source

Instances

Constant k Constraint (ConstC k) 
Constant k * (Const1 k) 
Constant k (k -> *) (Const2 k k) 

class (hom ~ Hom) => Complete hom | j -> hom where Source

A complete category has all small limits.

Minimal complete definition

elim

Associated Types

type Lim :: (i -> j) -> j Source

Methods

elim :: hom (Lim g) (g a) Source

complete :: Dict (Const -| (Lim :: (i -> j) -> j)) Source

Instances

Complete * (->) 
Complete Constraint (:-) 
Complete (i -> *) (Nat * i) 

Natural Isomorphisms

type Iso s t a b = forall p. Profunctor p => p a b -> p s t Source

type Iso' s a = Iso s s a a 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

Methods

adj :: Iso (f a ~> b) (f a' ~> b') (a ~> u b) (a' ~> u b') Source

Instances

(-|) * * 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) 

unitAdj :: (f -| u, Category (Dom u)) => a ~> u (f a) Source

counitAdj :: (f -| u, Category (Dom f)) => f (u b) ~> b Source

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

absurdL :: (f -| u, Initial z) => Iso z z (f z) (f z) 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

Minimal complete definition

curry, uncurry | apply, unapply

Associated Types

type Curryable p :: k -> Constraint Source

Methods

curry :: Curryable p a => (p a b ~> c) -> a ~> e b c Source

uncurry :: (a ~> e b c) -> p a b ~> c Source

apply :: p (e a b) a ~> b Source

unapply :: Curryable p a => a ~> e b (p a b) Source

Instances

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

Associated Types

type Cocurryable u :: k -> Constraint Source

Methods

cocurry :: (f a b ~> c) -> b ~> u c a Source

uncocurry :: Cocurryable u c => (b ~> u c a) -> f a b ~> c Source

Instances

Cocurried (k -> k) (k -> *) (k -> *) (Lan1 k k) (Compose1 k k) 
Cocurried (k -> k) (k -> k -> *) (k -> k -> *) (Lan2 k k k) (Compose2 k k k) 

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

Minimal complete definition

Nothing

Associated Types

type Lift :: (j -> k -> l) -> (i -> j) -> (i -> k) -> i -> l Source

Methods

_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

Instances

Lifted * (->) 
Lifted Constraint (:-) 
Lifted (i -> *) (Nat * i) 
Lifted (i -> Constraint) (Nat Constraint i) 

Constraints

data Dict $a :: Constraint -> * where

Constructors

Dict :: a => Dict a 

Instances

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) 

(\\) :: a => (b -> r) -> (:-) a b -> r

_Sub :: Iso (p :- q) (p' :- q') (Dict p -> Dict q) (Dict p' -> Dict q') Source

_Implies :: Iso (p :- q) (p' :- q') (Dict (p |- q)) (Dict (p' |- q')) Source

class Class b h | h -> b where

Methods

cls :: (:-) h b

Instances

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

Methods

ins :: (:-) b h

Instances

() :=> () 
a :=> (Read (Dict a)) 
a :=> (Monoid (Dict a)) 
a :=> (Enum (Dict a)) 
a :=> (Bounded (Dict a)) 
() :=> (Alternative []) 
() :=> (Alternative Maybe) 
() :=> (Bounded Bool) 
() :=> (Bounded Char) 
() :=> (Bounded Int) 
() :=> (Bounded Ordering) 
() :=> (Bounded ()) 
() :=> (Enum Bool) 
() :=> (Enum Char) 
() :=> (Enum Double) 
() :=> (Enum Float) 
() :=> (Enum Int) 
() :=> (Enum Integer) 
() :=> (Enum Ordering) 
() :=> (Enum ()) 
() :=> (Eq Bool) 
() :=> (Eq Double) 
() :=> (Eq Float) 
() :=> (Eq Int) 
() :=> (Eq Integer) 
() :=> (Eq ()) 
() :=> (Eq (Dict a)) 
() :=> (Eq ((:-) a b)) 
() :=> (Floating Double) 
() :=> (Floating Float) 
() :=> (Fractional Double) 
() :=> (Fractional Float) 
() :=> (Integral Int) 
() :=> (Integral Integer) 
() :=> (Monad ((->) a)) 
() :=> (Monad []) 
() :=> (Monad IO) 
() :=> (Monad (Either a)) 
() :=> (Functor ((->) a)) 
() :=> (Functor []) 
() :=> (Functor IO) 
() :=> (Functor (Either a)) 
() :=> (Functor ((,) a)) 
() :=> (Functor Maybe) 
() :=> (Num Double) 
() :=> (Num Float) 
() :=> (Num Int) 
() :=> (Num Integer) 
() :=> (Ord Bool) 
() :=> (Ord Char) 
() :=> (Ord Double) 
() :=> (Ord Float) 
() :=> (Ord Int) 
() :=> (Ord Integer) 
() :=> (Ord ()) 
() :=> (Ord (Dict a)) 
() :=> (Ord ((:-) a b)) 
() :=> (Read Bool) 
() :=> (Read Char) 
() :=> (Read Ordering) 
() :=> (Read ()) 
() :=> (Real Double) 
() :=> (Real Float) 
() :=> (Real Int) 
() :=> (Real Integer) 
() :=> (RealFloat Double) 
() :=> (RealFloat Float) 
() :=> (RealFrac Double) 
() :=> (RealFrac Float) 
() :=> (Show Bool) 
() :=> (Show Char) 
() :=> (Show Ordering) 
() :=> (Show ()) 
() :=> (Show (Dict a)) 
() :=> (Show ((:-) a b)) 
() :=> (MonadPlus []) 
() :=> (MonadPlus Maybe) 
() :=> (Applicative ((->) a)) 
() :=> (Applicative []) 
() :=> (Applicative IO) 
() :=> (Applicative (Either a)) 
() :=> (Applicative Maybe) 
() :=> (Monoid [a]) 
() :=> (Monoid Ordering) 
() :=> (Monoid ()) 
Class () ((:=>) b a) 
Class b a => () :=> (Class b a) 
(:=>) b a => () :=> ((:=>) b a) 
(Eq a) :=> (Eq [a]) 
(Eq a) :=> (Eq (Maybe a)) 
(Eq a) :=> (Eq (Complex a)) 
(Eq a) :=> (Eq (Ratio a)) 
(Integral a) :=> (RealFrac (Ratio a)) 
(Integral a) :=> (Real (Ratio a)) 
(Integral a) :=> (Ord (Ratio a)) 
(Integral a) :=> (Num (Ratio a)) 
(Integral a) :=> (Fractional (Ratio a)) 
(Integral a) :=> (Enum (Ratio a)) 
(Monad m) :=> (Functor (WrappedMonad m)) 
(Monad m) :=> (Applicative (WrappedMonad m)) 
(Ord a) :=> (Ord (Maybe a)) 
(Ord a) :=> (Ord [a]) 
(Read a) :=> (Read (Complex a)) 
(Read a) :=> (Read [a]) 
(Read a) :=> (Read (Maybe a)) 
(RealFloat a) :=> (Num (Complex a)) 
(RealFloat a) :=> (Fractional (Complex a)) 
(RealFloat a) :=> (Floating (Complex a)) 
(Show a) :=> (Show (Complex a)) 
(Show a) :=> (Show [a]) 
(Show a) :=> (Show (Maybe a)) 
(MonadPlus m) :=> (Alternative (WrappedMonad m)) 
(Monoid a) :=> (Monoid (Maybe a)) 
(Monoid a) :=> (Applicative ((,) a)) 
(f (g a)) :=> (ComposeC k k f g a) 
(Bounded a, Bounded b) :=> (Bounded (a, b)) 
(Eq a, Eq b) :=> (Eq (a, b)) 
(Eq a, Eq b) :=> (Eq (Either a b)) 
(Integral a, Show a) :=> (Show (Ratio a)) 
(Integral a, Read a) :=> (Read (Ratio a)) 
(Ord a, Ord b) :=> (Ord (a, b)) 
(Ord a, Ord b) :=> (Ord (Either a b)) 
(Read a, Read b) :=> (Read (a, b)) 
(Read a, Read b) :=> (Read (Either a b)) 
(Show a, Show b) :=> (Show (a, b)) 
(Show a, Show b) :=> (Show (Either a b)) 
(Monoid a, Monoid b) :=> (Monoid (a, b)) 
((|-) ((~) k i j) a) :=> (CoatC k a i j) 
((&) a ((~) k i j)) :=> (AtC k a i j) 

Lens Esoterica

The Yoneda embedding

newtype Get r a b Source

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.

Constructors

Get 

Fields

runGet :: a ~> r
 

Instances

Contravariant * k (Get k k r a) 
Functor k * (Get k k r a) 
Category i ((~>) i) => Functor i (i -> k -> *) (Get k i) 
Precartesian i ((~>) i) => Strong i (Get i i r) 
Category k (Arr k r) => Contravariant (k -> *) k (Get k k r) 

_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

get :: (Category c, c ~ (~>)) => (Get a a a -> Get a s s) -> c s a Source

newtype Beget r a b 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.

Constructors

Beget 

Fields

runBeget :: r ~> b
 

Instances

Category i ((~>) i) => Functor i * (Beget k i r a) 
Functor k (k -> *) (Beget k k r) 
Precocartesian i ((~>) i) => Choice i (Beget i i r) 
Category i ((~>) i) => Contravariant (k -> i -> *) i (Beget k i) 
Contravariant (k -> *) k (Beget k k r) 

_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

beget :: (Category c, c ~ (~>)) => (Beget b b b -> Beget b t t) -> c b t Source

(#) :: (Beget b b b -> Beget b t t) -> b -> t Source

Inverting natural isomorphisms

newtype Un p a b s t Source

Constructors

Un 

Fields

runUn :: p t s ~> p b a
 

Instances

(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

un :: (Un p a b a b -> Un p a b s t) -> p t s -> p b a Source

data Via a b s t where Source

Constructors

Via :: (s ~> a) -> (b ~> t) -> Via a b s t 

Instances

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

newtype Self a b Source

Constructors

Self 

Fields

runSelf :: a ~> b
 

Instances

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

Associated Types

type Tensorable p :: x -> Constraint Source

Methods

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

Instances

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 family I p :: x Source

Instances

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

Methods

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

Instances

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

Methods

swap :: p a b ~> p b a Source

Instances

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

Minimal complete definition

Nothing

Methods

iota :: Iso (Internal k (I (Internal k)) a) (Internal k (I (Internal k)) b) a b Source

jot :: I (Internal k) ~> Internal k a a Source

Instances

Closed * (->) 
Closed Constraint (:-) 
Closed (i -> Constraint) (Nat Constraint i) 
Closed (i -> *) (Nat * i) 

Terminal and Initial Objects

class (One ~ t) => Terminal t | i -> t where Source

Associated Types

type One :: i Source

Methods

terminal :: a ~> t Source

Instances

Terminal * () 
Terminal Constraint () 
Terminal () () 
Terminal (k -> Constraint) (ConstC k ()) 
Terminal * t => Terminal (k -> *) (Const1 k t) 
Terminal (k -> *) t => Terminal (k -> k -> *) (Const2 k k t) 

class (Zero ~ t) => Initial t | i -> t where Source

Associated Types

type Zero :: i Source

Methods

initial :: t ~> a Source

Instances

Initial * Void 
Initial () () 
Initial Constraint ((~) * () Bool) 
Initial Constraint i => Initial (k -> Constraint) (ConstC k i) 
Initial * i => Initial (k -> *) (Const1 k i) 
Initial (k -> *) i => Initial (k -> k -> *) (Const2 k k i) 

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

Instances

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 (,) 

type * = (Copower :: i -> i -> i) infixl 7 Source

class (h ~ (~>), Symmetric (* :: i -> i -> i), Semitensor (* :: i -> i -> i)) => Precartesian h | i -> h where Source

Methods

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

Instances

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

Instances

((~) (i -> i -> *) h ((~>) i), Tensor i (* i), Terminal i (I i (* i)), Precartesian i h) => Cartesian i h 

class (h ~ (~>), Symmetric ((+) :: i -> i -> i), Semitensor ((+) :: i -> i -> i)) => Precocartesian h | i -> h where Source

Associated Types

type (+) :: i -> i -> i infixl 6 Source

Methods

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

Instances

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

Instances

((~) (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

Methods

distribute :: forall a b c a' b' c'. Iso ((a * b) + (a * c)) ((a' * b') + (a' * c')) (a * (b + c)) (a' * (b' + c')) Source

Instances

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

Instances

(Cartesian x k, Closed x k, Curried x x x (* x) (Internal x k), (~) x (I x (Internal x k)) (I x (* x)), Curryable x x x (* x) (I x (Internal x k))) => CCC x k 

Monoidal Functors

class (Precartesian ((~>) :: x -> x -> *), Precartesian ((~>) :: y -> y -> *), Functor f) => Semimonoidal f where Source

Methods

ap2 :: (f a * f b) ~> f (a * b) Source

Instances

Semimonoidal * Constraint Dict 
Semimonoidal * * (EnvC p) 
Semimonoidal * * ((|=) e) 
Semimonoidal * Constraint ((:-) f) 
Precartesian i ((~>) i) => Semimonoidal * i (Proxy i) 
Semimonoidal Constraint Constraint ((|-) f) 
Semimonoidal * * (Tagged k s) 
Semimonoidal * k f => Semimonoidal * k (Id1 k f) 
Precartesian x (Arr x a) => Semimonoidal * x (Self x a) 
(Semigroup * b, Precartesian i ((~>) i)) => Semimonoidal * i (Const1 i b) 
(Semigroup Constraint b, Precartesian i ((~>) i)) => Semimonoidal Constraint i (ConstC i b) 
Semimonoidal * k f => Semimonoidal * k (Power1 k v f) 
(Semimonoidal * k1 f, Semimonoidal k1 k g) => Semimonoidal * k (Compose1 k k f g) 
Semimonoidal k1 k f => Semimonoidal * k (Down k k f a) 
Precartesian k (Cod k k1 f) => Semimonoidal * k (Up k k f a) 
(Semimonoidal Constraint k1 f, Semimonoidal k1 k g) => Semimonoidal Constraint k (ComposeC k k f g) 
Semimonoidal * (k -> *) (Lim1 k) 
Semimonoidal Constraint (k -> Constraint) (LimC k) 
Semimonoidal * (i -> Constraint) (Nat Constraint i f) 
Semimonoidal * (i -> *) (Nat * i f) 
Semimonoidal (k -> k -> Constraint) Constraint (CoatC k) 
Semimonoidal (k -> k -> *) * (Coat0 k) 
(Semigroup (j -> *) b, Precartesian i ((~>) i)) => Semimonoidal (j -> *) i (Const2 j i b) 
(Semimonoidal (k2 -> *) k1 f, Semimonoidal k1 k g) => Semimonoidal (k -> *) k (Compose2 k k k f g) 
Semimonoidal (k -> *) (k -> *) (Id1 k) 
Semimonoidal (k -> *) (k -> *) (Power1 k v) 

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

Methods

ap0 :: One ~> f One Source

Instances

Monoidal Constraint * Dict 
Monoid Constraint p => Monoidal * * (EnvC p) 
Monoidal * * ((|=) e) 
Monoidal Constraint * ((:-) f) 
Monoidal Constraint Constraint ((|-) f) 
Cartesian i ((~>) i) => Monoidal i * (Proxy i) 
Monoidal * * (Tagged k s) 
Monoidal k * f => Monoidal k * (Id1 k f) 
Cartesian x (Arr x a) => Monoidal x * (Self x a) 
(Monoid Constraint b, Cartesian i ((~>) i)) => Monoidal i Constraint (ConstC i b) 
(Monoid * b, Cartesian i ((~>) i)) => Monoidal i * (Const1 i b) 
Monoidal k * f => Monoidal k * (Power1 k v f) 
(Monoidal k1 Constraint f, Monoidal k k1 g) => Monoidal k Constraint (ComposeC k k f g) 
(Monoidal k1 * f, Monoidal k k1 g) => Monoidal k * (Compose1 k k f g) 
Monoidal k k1 f => Monoidal k * (Down k k f a) 
Cartesian k (Cod k k1 f) => Monoidal k * (Up k k f a) 
Monoidal * (k -> k -> *) (Coat0 k) 
Monoidal Constraint (k -> k -> Constraint) (CoatC k) 
(Monoid (j -> *) b, Cartesian i ((~>) i)) => Monoidal i (j -> *) (Const2 j i b) 
(Monoidal k1 (k2 -> *) f, Monoidal k k1 g) => Monoidal k (k -> *) (Compose2 k k k f g) 
Monoidal (k -> Constraint) Constraint (LimC k) 
Monoidal (k -> *) * (Lim1 k) 
Monoidal (i -> Constraint) * (Nat Constraint i f) 
Monoidal (i -> *) * (Nat * i f) 
Monoidal (k -> *) (k -> *) (Id1 k) 
Monoidal (k -> *) (k -> *) (Power1 k v) 

return :: (Monoidal f, Strength f, CCC (Dom f), Tensorable * a) => a ~> f a Source

class (Precocartesian ((~>) :: x -> x -> *), Precocartesian ((~>) :: y -> y -> *), Functor f) => Cosemimonoidal f where Source

Methods

op2 :: f (a + b) ~> (f a + f b) Source

Instances

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

Methods

op0 :: f Zero ~> Zero Source

Instances

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

Minimal complete definition

join | bind

Methods

join :: m (m a) ~> m a Source

bind :: Semimonad m => (a ~> m b) ~> (m a ~> m b) Source

Instances

Semimonad * (EnvC p) 
Semimonad * ((|=) e) 
Semimonad * f => Semimonad * (Down * * f a) 
Semimonad * (Up * k f a) 
Semimonad (k -> *) (Id1 k) 

class (Monoidal m, Semimonad m) => Monad m Source

Instances

(Monoidal k k m, Semimonad k m) => Monad k m 
Monad (k -> *) (Id1 k) 

class (Functor f, Category (Dom f)) => Cosemimonad f where Source

Minimal complete definition

duplicate | extend

Methods

duplicate :: f a ~> f (f a) Source

extend :: (f a ~> b) -> f a ~> f b Source

Instances

Cosemimonad * (Store0 s) 
Cosemimonad * (EnvC p) 
Cosemimonad * ((|=) e) 
Cosemimonad (k -> *) (Id1 k) 
Cosemimonad (k -> *) (Store1 k s) 

class Cosemimonad f => Comonad f where Source

Methods

extract :: f a ~> a Source

Instances

Comonad * (Store0 s) 
Comonad * (EnvC p) 
Monoid Constraint e => Comonad * ((|=) e) 
Comonad (k -> *) (Id1 k) 
Comonad (k -> *) (Store1 k s) 

Monoids

class Precartesian (Arr m) => Semigroup m where Source

Methods

mult :: (m * m) ~> m Source

Instances

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) 

multM :: (Semimonoidal u, Semigroup m) => (u m * u m) ~> u m Source

class (Semigroup m, Cartesian (Arr m)) => Monoid m where Source

Methods

one :: One ~> m Source

Instances

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) 

oneM :: (Monoidal u, Monoid m) => One ~> u m Source

mappend :: (Semigroup m, CCC (Arr m), Curryable * m) => m ~> (m ^ m) Source

class Precocartesian (Arr m) => Cosemigroup m where Source

Methods

comult :: m ~> (m + m) Source

Instances

Cosemigroup * Void 
Cosemigroup * m => Cosemigroup * (Id0 m) 
Cosemigroup * m => Cosemigroup * (e, m) 
Cosemigroup (k -> *) m => Cosemigroup * (Colim1 k m) 
Cosemigroup * m => Cosemigroup * (Tagged k s m) 
(Cosemimonoidal k * f, Cosemigroup k m) => Cosemigroup * (Id1 k f m) 
Cosemigroup * b => Cosemigroup * (Const1 k b a) 
Cosemigroup Constraint b => Cosemigroup Constraint (ConstC k b a) 
(Cosemimonoidal k * f, Cosemimonoidal k1 k g, Cosemigroup k1 m) => Cosemigroup * (Compose1 k k f g m) 
(Cosemimonoidal k Constraint f, Cosemimonoidal k1 k g, Cosemigroup k1 m) => Cosemigroup Constraint (ComposeC k k f g m) 
Cosemigroup (k -> *) (Const1 k Void) 
Cosemigroup (k -> *) m => Cosemigroup (k -> *) (Id1 k m) 
Cosemigroup * m => Cosemigroup (k -> k -> *) (At0 k m) 
Cosemigroup (k -> *) b => Cosemigroup (k -> *) (Const2 k k b a) 
(Cosemimonoidal k (k1 -> *) f, Cosemimonoidal k2 k g, Cosemigroup k2 m) => Cosemigroup (k -> *) (Compose2 k k k f g m) 
Cosemigroup (k -> *) m => Cosemigroup (k -> *) (Lift1 * * k (,) e m) 

class (Cosemigroup m, Cocartesian (Arr m)) => Comonoid m where Source

Methods

zero :: m ~> Zero Source

Instances

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 => Strength f where Source

Methods

strength :: (a * f b) ~> f (a * b) Source

Instances

Functor * * f => Strength * f 

class Functor f => Costrength f where Source

Methods

costrength :: f (a + b) ~> (a + f b) Source

Instances

(Functor * * f, Traversable f) => Costrength * f 

Identity functors

class (f -| f, Id ~ f) => Identity f | i -> f where Source

Minimal complete definition

Nothing

Associated Types

type Id :: i -> i Source

Methods

_Id :: Iso (f a) (f a') a a' Source

Instances

Kan extensions

class (c ~ Hom) => HasRan c | k -> c where Source

Minimal complete definition

iotaRan, jotRan

Associated Types

type Ran :: (i -> j) -> (i -> k) -> j -> k Source

Methods

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

Instances

HasRan * (->) 

class (c ~ Hom) => HasLan c | k -> c where Source

Minimal complete definition

epsilonLan

Associated Types

type Lan :: (i -> j) -> (i -> k) -> j -> k Source

Methods

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

Instances

HasLan * (->) 
HasLan (i -> *) (Nat * i) 

Categories

Products

data Prod :: (i, j) -> (i, j) -> * where Source

Constructors

Want :: Prod a a 
Have :: (a ~> b) -> (c ~> d) -> Prod `(a, c)` `(b, d)` 

Instances

(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

runFst :: forall a b c d. Category ((~>) :: i -> i -> *) => Prod `(a, c)` `(b, d)` -> a ~> b Source

runSnd :: forall a b c d. Category ((~>) :: j -> j -> *) => Prod `(a, c)` `(b, d)` -> 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

data Unit a b Source

Constructors

Unit 

Empty

data No a Source

Instances

Candidates for Removal:

class (Profunctor p, p ~ (~>)) => Semicategory p Source

Instances

(Profunctor k k * p, (~) (k -> k -> *) p ((~>) k)) => Semicategory k p 

Internals

Categories

Composition

newtype Compose1 f g a Source

Constructors

Compose 

Fields

getCompose :: f (g a)
 

Instances

(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

Constructors

Compose2 

Fields

getCompose2 :: f (g a) b
 

Instances

((-|) 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

Instances

f (g a) => ComposeC k k f g a 
(Comonoidal k1 Constraint f, Comonoidal k k1 g) => Comonoidal k Constraint (ComposeC k k f g) 
(Cosemimonoidal k1 Constraint f, Cosemimonoidal k k1 g) => Cosemimonoidal k Constraint (ComposeC k k f g) 
(Monoidal k1 Constraint f, Monoidal k k1 g) => Monoidal k Constraint (ComposeC k k f g) 
(Semimonoidal Constraint k1 f, Semimonoidal k1 k g) => Semimonoidal Constraint k (ComposeC k k f g) 
(Functor k1 Constraint f, Functor k k1 g) => Functor k Constraint (ComposeC k k f 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') 
(Comonoidal k Constraint f, Comonoidal k1 k g, Comonoid k1 m) => Comonoid Constraint (ComposeC k k f g m) 
(Cosemimonoidal k Constraint f, Cosemimonoidal k1 k g, Cosemigroup k1 m) => Cosemigroup Constraint (ComposeC k k f g m) 
(Monoidal k Constraint f, Monoidal k1 k g, Monoid k1 m) => Monoid Constraint (ComposeC k k f g m) 
Class (f (g a)) (ComposeC k k f g a) 
(f (g a)) :=> (ComposeC k k f g a) 
Tensor (Constraint -> Constraint) (ComposeC Constraint Constraint) 
Semitensor (Constraint -> Constraint) (ComposeC Constraint Constraint) 
Functor (k -> Constraint) ((k -> k) -> k -> Constraint) (ComposeC k k) 
Contravariant Constraint k f => Contravariant (k -> Constraint) (k -> k) (ComposeC k k f) 
Functor k Constraint f => Functor (k -> k) (k -> Constraint) (ComposeC k k f) 
type I (Constraint -> Constraint) (ComposeC Constraint Constraint) = Id Constraint 
type Tensorable (Constraint -> Constraint) (ComposeC Constraint Constraint) = Functor Constraint Constraint 

Limits

newtype Lim1 f Source

Constructors

Lim 

Fields

getLim :: forall x. f x
 

Instances

Monoid (k -> *) m => Monoid * (Lim1 k m) 
Semigroup (k -> *) m => Semigroup * (Lim1 k m) 
Semimonoidal * (k -> *) (Lim1 k) 
(~|) (k -> *) * * (Const1 k) (Lim1 k) 
Monoidal (k -> *) * (Lim1 k) 
Functor (k -> *) * (Lim1 k) 
(-|) (k -> *) * (Const1 k) (Lim1 k) 

newtype Lim2 f y Source

Constructors

Lim2 

Fields

getLim2 :: forall x. f x y
 

Instances

Functor (k -> k -> *) (k -> *) (Lim2 k k) 
(-|) (k -> k -> *) (k -> *) (Const2 k k) (Lim2 k k) 
(~|) (k -> k -> *) (k -> *) (k -> *) (Const2 k k) (Lim2 k k) 

newtype Lim3 f y z Source

Constructors

Lim3 

Fields

getLim3 :: forall x. f x y z
 

class LimC p where Source

LimC :: (i -> Constraint) -> Constraint takes limits in the category of constraints

type instance Lim = LimC

Methods

limDict :: Dict (p a) Source

newtype Const1 b a Source

Constructors

Const 

Fields

getConst :: b
 

Instances

Constant k * (Const1 k) 
(Comonoid * b, Cocartesian i ((~>) i)) => Comonoidal i * (Const1 i b) 
(Cosemigroup * b, Precocartesian i ((~>) i)) => Cosemimonoidal i * (Const1 i b) 
(Monoid * b, Cartesian i ((~>) i)) => Monoidal i * (Const1 i b) 
(Semigroup * b, Precartesian i ((~>) i)) => Semimonoidal * i (Const1 i b) 
Contravariant * k (Const1 k b) 
Functor k * (Const1 k b) 
Functor * (k -> *) (Const1 k) 
RelMonad * (k -> *) (Const1 k) 
(-|) * (k -> *) (Colim1 k) (Const1 k) 
(~|) * (i -> *) (i -> *) (Colim1 i) (Const1 i) 
Comonoid * b => Comonoid * (Const1 k b a) 
Cosemigroup * b => Cosemigroup * (Const1 k b a) 
Monoid * b => Monoid * (Const1 k b a) 
Semigroup * b => Semigroup * (Const1 k b a) 
(~|) (k -> *) * * (Const1 k) (Lim1 k) 
RelComposed (k -> *) * (Const1 k) 
(-|) (k -> *) * (Const1 k) (Lim1 k) 
Comonoid (k -> *) (Const1 k Void) 
Cosemigroup (k -> *) (Const1 k Void) 
Monoid (k -> *) (Const1 k ()) 
Semigroup (k -> *) (Const1 k Void) 
Semigroup (k -> *) (Const1 k ()) 
Initial * i => Initial (k -> *) (Const1 k i) 
Terminal * t => Terminal (k -> *) (Const1 k t) 

newtype Const2 f a c Source

Constructors

Const2 

Fields

getConst2 :: f c
 

Instances

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) 

data Colim1 f where Source

Constructors

Colim :: f x -> Colim1 f 

Instances

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) 

data Colim2 f x where Source

Constructors

Colim2 :: f y x -> Colim2 f x 

Instances

Functor (k -> k -> *) (k -> *) (Colim2 k k) 
(-|) (k -> *) (k -> k -> *) (Colim2 k k) (Const2 k k) 

Identities

newtype Id0 a Source

Constructors

Id 

Fields

runId :: a
 

Instances

newtype Id1 f a Source

Constructors

Id1 

Fields

runId1 :: f a
 

Instances

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

newtype Lift1 p f g a Source

Constructors

Lift 

Fields

lower :: p (f a) (g a)
 

Instances

(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

Constructors

Lift2 

Fields

lower2 :: p (f a) (g a) b
 

Instances

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

Instances

r (p a) (q a) => LiftC k k k r p q a 
Curried Constraint k1 Constraint p q => Curried (k -> Constraint) (k -> k) (k -> Constraint) (LiftC Constraint k k p) (LiftC k Constraint k q) 
Symmetric k Constraint p => Symmetric (k -> k) (k -> Constraint) (LiftC k k k p) 
Contravariant (k1 -> Constraint) k p => Contravariant ((k -> k) -> k -> Constraint) (k -> k) (LiftC k k k p) 
Functor k (k1 -> Constraint) p => Functor (k -> k) ((k -> k) -> k -> Constraint) (LiftC 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 -> Constraint) (Functor k1 Constraint) p => Functor (k -> k) (k -> Constraint) (LiftC k k k p e) 
Tensor Constraint p => Tensor (k -> Constraint) (LiftC Constraint Constraint k p) 
Semitensor Constraint p => Semitensor (k -> Constraint) (LiftC Constraint Constraint k p) 
type Curryable (k1 -> Constraint) (k1 -> k) (k1 -> Constraint) (LiftC Constraint k k1 p) = Post k1 Constraint (Curryable Constraint k Constraint p) 
type I (k -> Constraint) (LiftC Constraint Constraint k p) = ConstC k (I Constraint p) 
type Tensorable (k -> Constraint) (LiftC Constraint Constraint k p) = Post k Constraint (Tensorable Constraint p) 

class r (f a) (g a) b => LiftC2 r f g a b Source

Instances

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

data Copower1 x f a Source

Constructors

Copower x (f a) 

Instances

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 () 

data Copower2 x f a b Source

Constructors

Copower2 x (f a b) 

Instances

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

Constructors

Copower2_1 (x a) (f a b) 

Instances

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

data Ran1 f g a Source

Constructors

forall z . Functor z => Ran (Compose z f ~> g) (z a) 

Instances

Functor k * (Ran1 k k f g) 
Contravariant ((k -> *) -> k -> *) (k -> k) (Ran1 k k) 
Curried (k -> *) (k -> k) (k -> *) (Compose1 k k) (Ran1 k k) 
Category j (Hom j *) => Functor (i -> *) (j -> *) (Ran1 j i f) 

newtype Lan1 f g a Source

Constructors

Lan 

Fields

runLan :: forall z. Functor z => (g ~> Compose z f) ~> z a
 

Instances

Functor k * (Lan1 k k f g) 
Contravariant ((k -> *) -> k -> *) (k -> k) (Lan1 k k) 
Cocurried (k -> k) (k -> *) (k -> *) (Lan1 k k) (Compose1 k k) 
Category j (Hom j *) => Functor (i -> *) (j -> *) (Lan1 j i f) 

newtype Lan2 f g a b Source

Constructors

Lan2 

Fields

runLan2 :: forall z. Functor z => (g ~> Compose z f) ~> z a b
 

Instances

Functor k (k -> *) (Lan2 k k k f g) 
Cocurried (k -> k) (k -> k -> *) (k -> k -> *) (Lan2 k k k) (Compose2 k k k) 
Contravariant ((k -> k -> *) -> k -> k -> *) (k -> k) (Lan2 k k k) 
Category j (Hom j *) => Functor (i -> k -> *) (j -> k -> *) (Lan2 j i k f) 

Base Re-exports

data Constraint :: BOX

Instances

Category Constraint (:-) 
Monoid Constraint () 
Semigroup Constraint p 
Identity Constraint IdC 
Precocartesian Constraint (:-) 
Precartesian Constraint (:-) 
Terminal Constraint () 
Closed Constraint (:-) 
Tensor Constraint (&) 
Semitensor Constraint (&) 
Lifted Constraint (:-) 
Complete Constraint (:-) 
Composed Constraint (:-) 
Ended Constraint (:-) 
Strong Constraint (:-) 
HasAt Constraint (:-) 
Monoidal Constraint * Dict 
Semimonoidal * Constraint Dict 
Symmetric Constraint Constraint (&) 
Functor Constraint * Dict 
Functor Constraint Constraint IdC 
Subst Constraint * (:-) 
Subst Constraint Constraint (|-) 
RelMonad Constraint Constraint IdC 
Powered Constraint Constraint (|-) 
(-|) Constraint Constraint IdC IdC 
Corepresentable Constraint * * (|=) 
Corepresentable Constraint * Constraint (:-) 
Corepresentable Constraint Constraint Constraint (|-) 
Representable Constraint * Constraint (:-) 
Curried Constraint Constraint Constraint (&) (|-) 
(~|) Constraint Constraint Constraint IdC IdC 
Monoidal Constraint * ((:-) f) 
Monoidal Constraint Constraint ((|-) f) 
Semimonoidal * Constraint ((:-) f) 
Semimonoidal Constraint Constraint ((|-) f) 
Constant k Constraint (ConstC k) 
Functor Constraint * ((:-) f) 
Functor Constraint Constraint ((|-) p) 
Functor Constraint Constraint ((&) p) 
Foldable Constraint Constraint ((&) e) 
(-|) Constraint Constraint ((&) p) ((|-) p) 
(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) 
(Comonoidal k1 Constraint f, Comonoidal k k1 g) => Comonoidal k Constraint (ComposeC k k f g) 
(Cosemimonoidal k1 Constraint f, Cosemimonoidal k k1 g) => Cosemimonoidal k Constraint (ComposeC k k f g) 
(Monoidal k1 Constraint f, Monoidal k k1 g) => Monoidal k Constraint (ComposeC k k f g) 
(Semimonoidal Constraint k1 f, Semimonoidal k1 k g) => Semimonoidal Constraint k (ComposeC k k f g) 
(Functor k1 Constraint f, Functor k k1 g) => Functor k Constraint (ComposeC k k f 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') 
Monoid Constraint m => Monoid Constraint ((|-) f m) 
Monoid (k -> Constraint) m => Monoid Constraint (LimC k m) 
Functor Constraint (* -> *) EnvC 
Functor Constraint (Constraint -> Constraint) (&) 
Monoidal Constraint (k -> k -> Constraint) (CoatC k) 
Semimonoidal Constraint (k -> Constraint) (LimC k) 
Functor Constraint (k -> Constraint) (ConstC k) 
Functor Constraint (k -> k -> Constraint) (CoatC k) 
Functor Constraint (k -> k -> Constraint) (AtC k) 
RelMonad Constraint (k -> Constraint) (ConstC k) 
Semimonoidal * (i -> Constraint) (Nat Constraint i f) 
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) 
Initial Constraint ((~) * () Bool) 
(Comonoidal k Constraint f, Comonoidal k1 k g, Comonoid k1 m) => Comonoid Constraint (ComposeC k k f g m) 
(Cosemimonoidal k Constraint f, Cosemimonoidal k1 k g, Cosemigroup k1 m) => Cosemigroup Constraint (ComposeC k k f g m) 
(Monoidal k Constraint f, Monoidal k1 k g, Monoid k1 m) => Monoid Constraint (ComposeC k k f g m) 
Typeable ((* -> *) -> Constraint) Alternative 
Typeable ((* -> *) -> Constraint) Applicative 
Typeable (* -> Constraint) Monoid 
Contravariant (* -> *) Constraint (|=) 
Contravariant (Constraint -> *) Constraint (:-) 
Contravariant (Constraint -> Constraint) Constraint (|-) 
(~|) (k -> Constraint) Constraint Constraint (ConstC k) (LimC k) 
Monoidal (k -> Constraint) Constraint (LimC k) 
Semimonoidal (k -> k -> Constraint) Constraint (CoatC k) 
Functor (k -> Constraint) Constraint (LimC k) 
Functor (k -> k -> Constraint) Constraint (EndC k) 
(-|) (k -> Constraint) Constraint (ConstC k) (LimC k) 
Monoidal (i -> Constraint) * (Nat Constraint i f) 
Monoid Constraint m => Monoid (k -> k -> Constraint) (CoatC k m) 
Semigroup Constraint m => Semigroup (k -> k -> Constraint) (CoatC k m) 
Precartesian (i -> j -> Constraint) (Nat (j -> Constraint) i) 
Precartesian (i -> Constraint) (Nat Constraint i) 
Initial Constraint i => Initial (k -> Constraint) (ConstC k i) 
Terminal (k -> Constraint) (ConstC k ()) 
Closed (i -> Constraint) (Nat Constraint i) 
Tensor (Constraint -> Constraint) (ComposeC Constraint Constraint) 
Semitensor (Constraint -> Constraint) (ComposeC Constraint Constraint) 
Lifted (i -> Constraint) (Nat Constraint i) 
Strong (i -> Constraint) (Nat Constraint i) 
Functor (k -> Constraint) ((k -> k) -> k -> Constraint) (ComposeC 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 (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) 
Contravariant Constraint k f => Contravariant (k -> Constraint) (k -> k) (ComposeC k k f) 
Functor k Constraint f => Functor (k -> k) (k -> Constraint) (ComposeC k k f) 
Symmetric k Constraint p => Symmetric (k -> k) (k -> Constraint) (LiftC k k k p) 
Contravariant (k1 -> Constraint) k p => Contravariant ((k -> k) -> k -> Constraint) (k -> k) (LiftC k k k p) 
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) 
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) 
Post k (k1 -> Constraint) (Contravariant Constraint k1) p => Contravariant (k -> Constraint) (k -> k) (LiftC k k k p e) 
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 -> 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 Constraint p => Tensor (k -> Constraint) (LiftC Constraint Constraint k p) 
Semitensor Constraint p => Semitensor (k -> Constraint) (LiftC Constraint Constraint k p) 
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 Id Constraint = IdC 
type (+) Constraint 
type Zero Constraint = (~) * () Bool 
type One Constraint = () 
type Copower Constraint Constraint = (&) 
type I Constraint (|-) = () 
type I Constraint (&) = () 
type Tensorable Constraint (&) = Const Constraint Constraint () 
type Lim Constraint k = LimC k 
type Const k Constraint = ConstC k 
type Hom Constraint * = (:-) 
type Hom Constraint Constraint = (|-) 
type End Constraint k = EndC k 
type (==) k Constraint = (~) k 
type Coreflected Constraint Constraint = IdC 
type Reflected Constraint Constraint = IdC 
type Rel Constraint * = Dict 
type Rel Constraint Constraint = IdC 
type Power Constraint Constraint = (|-) 
type At Constraint k = AtC k 
type Coat Constraint k = CoatC k 
type Compose Constraint k k1 = ComposeC k k1 
type Curryable Constraint Constraint Constraint (&) = Const Constraint Constraint () 
type Lift Constraint k k1 k2 = LiftC k k1 k2 
type Corep Constraint * * (|=) = Dict 
type Corep Constraint * Constraint (:-) = Id Constraint 
type Corep Constraint Constraint Constraint (|-) = IdC 
type Rep Constraint * Constraint (:-) = Id Constraint 
type Const k (k1 -> Constraint) 
type Rel Constraint (k -> Constraint) = ConstC k 
type Zero (k -> Constraint) = ConstC k (Zero Constraint) 
type One (k -> k1 -> Constraint) 
type One (k -> Constraint) = ConstC k () 
type Coreflected (k -> Constraint) Constraint = LimC k 
type Lift (k3 -> Constraint) k k1 k2 = LiftC2 k k1 k3 k2 
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 I (Constraint -> Constraint) (ComposeC Constraint Constraint) = Id Constraint 
type Tensorable (Constraint -> Constraint) (ComposeC Constraint Constraint) = Functor Constraint Constraint 
type Curryable (k1 -> Constraint) (k1 -> k) (k1 -> Constraint) (LiftC Constraint k k1 p) = Post k1 Constraint (Curryable Constraint k Constraint 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 -> Constraint) (LiftC Constraint Constraint k p) = ConstC k (I Constraint p) 
type Tensorable (k -> Constraint) (LiftC Constraint Constraint k p) = Post k Constraint (Tensorable 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) 

Prelude Re-Exports

undefined :: a

A special case of error. It is expected that compilers will recognize this and insert error messages which are more appropriate to the context in which undefined appears.

($) :: (a -> b) -> a -> b infixr 0

Application operator. This operator is redundant, since ordinary application (f x) means the same as (f $ x). However, $ 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 map ($ 0) xs, or zipWith ($) fs xs.

data Either a b :: * -> * -> *

The Either type represents values with two possibilities: a value of type Either a b is either Left a or 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").

Constructors

Left a 
Right b 

Instances

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 Maybe a either contains a value of type a (represented as Just a), or it is empty (represented as Nothing). 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.

Constructors

Nothing 
Just a 

Instances

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 Maybe forming a Monoid according to http://en.wikipedia.org/wiki/Monoid: "Any semigroup S may be turned into a monoid simply by adjoining an element e not in S and defining e*e = e and e*s = s = s*e for all s ∈ S." Since there is no "Semigroup" typeclass providing just mappend, we use Monoid instead.

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 -> * -> *

Constructors

Tagged 

Fields

unTagged :: b
 

Instances

Comonoidal * * (Tagged k s) 
Cosemimonoidal * * (Tagged k s) 
Monoidal * * (Tagged k s) 
Semimonoidal * * (Tagged k s) 
Functor * * (Tagged k e) 
Choice * (Tagged *) 
Functor k (* -> *) (Tagged k) 
Comonoid * m => Comonoid * (Tagged k s m) 
Cosemigroup * m => Cosemigroup * (Tagged k s m) 
Monoid * m => Monoid * (Tagged k s m) 
Semigroup * m => Semigroup * (Tagged k s m) 
Monad (Tagged k s) 
Functor (Tagged k s) 
Applicative (Tagged k s) 
Foldable (Tagged k s) 
Traversable (Tagged k s) 
Contravariant (* -> *) k (Tagged k) 
Typeable (k -> * -> *) (Tagged k) 
Bounded b => Bounded (Tagged k s b) 
Enum a => Enum (Tagged k s a) 
Eq b => Eq (Tagged k s b) 
Floating a => Floating (Tagged k s a) 
Fractional a => Fractional (Tagged k s a) 
Integral a => Integral (Tagged k s a) 
(Data s, Data b) => Data (Tagged * s b) 
Num a => Num (Tagged k s a) 
Ord b => Ord (Tagged k s b) 
Read b => Read (Tagged k s b) 
Real a => Real (Tagged k s a) 
RealFloat a => RealFloat (Tagged k s a) 
RealFrac a => RealFrac (Tagged k s a) 
Show b => Show (Tagged k s b) 
Ix b => Ix (Tagged k s b) 
Monoid a => Monoid (Tagged k s a) 

data Proxy t :: k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy 

Instances

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.

Methods

id :: cat a a

the identity morphism

(.) :: cat b c -> cat a b -> cat a c infixr 9

morphism composition

Instances

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 :: *

absurd :: Void -> a