Hask.Core

Contents

• Natural transformations
• Functors
• Functor composition
  • In the limit
  • Derived notions
• Colim -| Const -| Lim
• Natural Isomorphisms
• Adjunctions
  • Currying
  • Cocurrying
• Automatic Lifting
• Constraints
• Lens Esoterica
  • The Yoneda embedding
  • Inverting natural isomorphisms
  • Hom as a Profunctor
• Monoidal Categories
• Closed Categories
• Terminal and Initial Objects
• Copowers and Cartesian Categories
• Distributive bicartesian categories
• CCC's
• Monoidal Functors
• Monads
• Monoids
• Strength
• Identity functors
• Kan extensions
• Categories
  • Products
  • Unit
  • Empty
• Candidates for Removal:
• Internals
  • Categories
  • Composition
  • Limits
  • Identities
  • Lifts
  • Copowers
  • Kan extensions
  • Base Re-exports
  • Prelude Re-Exports
  • Re-exports

Description

Synopsis

• type family Hom :: i -> i -> k
• type (~>) = (Hom :: i -> i -> *)
• type (^) a b = Internal Hom b a
• type Dom f = (Hom :: i -> i -> *)
• type Cod f = (Hom :: j -> j -> *)
• type Cod2 f = (Hom :: k -> k -> *)
• type Arr a = (Hom :: i -> i -> *)
• type Enriched k = (Hom :: i -> i -> j)
• type Internal k = (Hom :: i -> i -> i)
• type External k = (Hom :: i -> i -> *)
• type Natural k = (Hom :: (i -> j) -> (i -> j) -> *)
• newtype Nat f g = Nat {
  • runNat :: forall a. f a ~> g a
  }
• nat2 :: (forall a b. f a b ~> g a b) -> f ~> g
• nat3 :: (forall a b c. f a b c ~> g a b c) -> f ~> g
• nat4 :: (forall a b c d. f a b c d ~> g a b c d) -> f ~> g
• runNat2 :: Nat (k1 -> k) k2 f g -> Hom k * (f a1 a) (g a1 a)
• runNat3 :: Nat (k2 -> k1 -> k) k3 f g -> Hom k * (f a2 a1 a) (g a2 a1 a)
• runNat4 :: Nat (k3 -> k2 -> k1 -> k) k4 f g -> Hom k * (f a3 a2 a1 a) (g a3 a2 a1 a)
• class Functor f where
  • fmap :: (a ~> b) -> f a ~> f b
• first :: Functor f => (a ~> b) -> f a c ~> f b c
• class Contravariant f where
  • contramap :: (b ~> a) -> f a ~> f b
• lmap :: Contravariant f => (a ~> b) -> f b c ~> f a c
• class (hom ~ Hom) => Composed hom | k -> hom where
  • type Compose :: (j -> k) -> (i -> j) -> i -> k
  • compose :: f (g a) `hom` Compose f g a
  • decompose :: Compose f g a `hom` f (g a)
• type · = Compose
• composed :: (Functor k1 k2 (p (Any k)), Contravariant (k1 -> k2) k p, Composed k1 (Hom k1 *), Composed k (Hom k *), Category k2 (Hom k2 *)) => (~>) k2 (p (f (g a)) (f1 (g1 a1))) (p (Compose k k3 k4 f g a) (Compose k1 k5 k6 f1 g1 a1))
• associateCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Functor k8 k3 f1, Functor k5 k1 f, Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k8 (Hom k8 *), Composed k5 (Hom k5 *), Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Category k3 (Hom k3 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p (Compose k1 k5 k2 f (Compose k5 k6 k2 g g1)) (Compose k3 k8 k4 f1 (Compose k8 k7 k4 g3 g2))) (p (Compose k1 k6 k2 (Compose k1 k5 k6 f g) g1) (Compose k3 k7 k4 (Compose k3 k8 k7 f1 g3) g2))
• whiskerComposeL :: (Functor k * (Hom k * (Any k)), Contravariant (k -> *) k (Hom k *), Composed k (Hom k *)) => Nat k k2 f g1 -> Nat k k1 (Compose k k2 k1 f g) (Compose k k2 k1 g1 g)
• whiskerComposeR :: (Functor x k f, Functor k * (Hom k * (Any k)), Contravariant (k -> *) k (Hom k *), Composed k (Hom k *)) => Nat x k1 g g1 -> Nat k k1 (Compose k x k1 f g) (Compose k x k1 f g1)
• lambdaCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Identity k3 (Id k3), Identity k1 (Id k1), Category k3 (Hom k3 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p b c) (p (Compose k1 k1 k2 (Id k1) b) (Compose k3 k3 k4 (Id k3) c))
• rhoCompose :: (Functor (k4 -> k3) k (p (Any (k2 -> k1))), Functor k4 k3 c, Functor k2 k1 b, Contravariant ((k4 -> k3) -> k) (k2 -> k1) p, Composed k3 (Hom k3 *), Composed k1 (Hom k1 *), Identity k4 (Id k4), Identity k2 (Id k2), Category k4 (Hom k4 *), Category k3 (Hom k3 *), Category k2 (Hom k2 *), Category k1 (Hom k1 *), Category k (Hom k *)) => (~>) k (p b c) (p (Compose k1 k2 k2 b (Id k2)) (Compose k3 k4 k4 c (Id k4)))
• class LimC (f `·` p) => Post f p
• fmap1 :: forall p a b c. Post Functor p => (a ~> b) -> p c a ~> p c b
• contramap1 :: forall p a b c. Post Contravariant p => (a ~> b) -> p c b ~> p c a
• fmap2 :: forall p a b c d. Post (Post Functor) p => (a ~> b) -> p c d a ~> p c d b
• class (Functor p, Post Functor p) => Bifunctor p
• bimap :: (Bifunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p a c ~> p b d
• class (Contravariant p, Post Functor p) => Profunctor p
• dimap :: (Profunctor p, Category (Cod2 p)) => (a ~> b) -> (c ~> d) -> p b c ~> p a d
• class (Contravariant p, Functor p) => Phantom p
• class (k ~ (~>)) => Cocomplete k where
  • type Colim :: (i -> j) -> j
  • colim :: k (f a) (Colim f)
  • cocomplete :: Dict ((Colim :: (i -> j) -> j) -| Const)
• class (Const ~ k) => Constant k | j i -> k where
  • type Const :: j -> i -> j
  • _Const :: Iso (k b a) (k b' a') b b'
• class (hom ~ Hom) => Complete hom | j -> hom where
  • type Lim :: (i -> j) -> j
  • elim :: hom (Lim g) (g a)
  • complete :: Dict (Const -| (Lim :: (i -> j) -> j))
• type Iso s t a b = forall p. Profunctor p => p a b -> p s t
• type Iso' s a = Iso s s a a
• class (Functor f, Functor u) => f -| u | f -> u, u -> f where
  • adj :: Iso (f a ~> b) (f a' ~> b') (a ~> u b) (a' ~> u b')
• unitAdj :: (f -| u, Category (Dom u)) => a ~> u (f a)
• counitAdj :: (f -| u, Category (Dom f)) => f (u b) ~> b
• zipR :: (f -| u, Cartesian (Dom u), Cartesian (Cod u)) => Iso (u a * u b) (u a' * u b') (u (a * b)) (u (a' * b'))
• absurdL :: (f -| u, Initial z) => Iso z z (f z) (f z)
• cozipL :: (f -| u, Cocartesian (Cod u), Cocartesian (Cod f)) => Iso (f (a + b)) (f (a' + b')) (f a + f b) (f a' + f b')
• class Curried p e | p -> e, e -> p where
  • type Curryable p :: k -> Constraint
  • curry :: Curryable p a => (p a b ~> c) -> a ~> e b c
  • uncurry :: (a ~> e b c) -> p a b ~> c
  • apply :: p (e a b) a ~> b
  • unapply :: Curryable p a => a ~> e b (p a b)
• curried :: (Curried p e, Curryable p a) => Iso (p a b ~> c) (p a' b' ~> c') (a ~> e b c) (a' ~> e b' c')
• ccc :: (Category (Cod2 p), Symmetric p, Curried p e, Curryable p a) => Iso (p i a ~> b) (p i' a' ~> b') (a ~> e i b) (a' ~> e i' b')
• class Cocurried f u | f -> u, u -> f where
  • type Cocurryable u :: k -> Constraint
  • cocurry :: (f a b ~> c) -> b ~> u c a
  • uncocurry :: Cocurryable u c => (b ~> u c a) -> f a b ~> c
• cocurried :: (Cocurried f u, Cocurryable u c') => Iso (f a b ~> c) (f a' b' ~> c') (b ~> u c a) (b' ~> u c' a')
• class (hom ~ Hom) => Lifted hom where
  • type Lift :: (j -> k -> l) -> (i -> j) -> (i -> k) -> i -> l
  • _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))
• newtype a :- b :: Constraint -> Constraint -> * = Sub (a -> Dict b)
• data Dict $a :: Constraint -> * where
  • Dict :: a => Dict a
• (\\) :: a => (b -> r) -> (:-) a b -> r
• class (p, q) => p & q
• class p |- q where
  • implies :: p :- q
• _Sub :: Iso (p :- q) (p' :- q') (Dict p -> Dict q) (Dict p' -> Dict q')
• _Implies :: Iso (p :- q) (p' :- q') (Dict (p |- q)) (Dict (p' |- q'))
• class Class b h | h -> b where
  • cls :: (:-) h b
• class b :=> h | h -> b where
  • ins :: (:-) b h
• newtype Get r a b = Get {
  • runGet :: a ~> 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))
• get :: (Category c, c ~ (~>)) => (Get a a a -> Get a s s) -> c s a
• newtype Beget r a b = Beget {
  • runBeget :: r ~> b
  }
• _Beget :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k2 * r b) (Hom k4 * r1 b1)) (p (Beget k1 k2 r a b) (Beget k3 k4 r1 a1 b1))
• beget :: (Category c, c ~ (~>)) => (Beget b b b -> Beget b t t) -> c b t
• (#) :: (Beget b b b -> Beget b t t) -> b -> t
• newtype Un p a b s t = Un {
  • runUn :: p t s ~> p b a
  }
• _Un :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k1 * (p1 t s) (p1 b a)) (Hom k2 * (p2 t1 s1) (p2 b1 a1))) (p (Un i k1 p1 a b s t) (Un i1 k2 p2 a1 b1 s1 t1))
• un :: (Un p a b a b -> Un p a b s t) -> p t s -> p b a
• data Via a b s t where
  • Via :: (s ~> a) -> (b ~> t) -> Via a b s t
• via :: forall a b r p c t u. Category p => (Via a b a b -> Via r (p c c) u t) -> (t -> u) -> r
• mapping :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s) (f' t) (f a) (f' b)
• lmapping :: (Contravariant f, Contravariant f', Category (Dom f)) => (Via s t s t -> Via s t a b) -> Iso (f s x) (f' t y) (f a x) (f' b y)
• swapping :: (Profunctor f, Profunctor f', Category (Dom f), Category (Cod2 f), Category (Cod2 f')) => (Via a b a b -> Via a b s t) -> Iso (f a s) (f' b t) (f s a) (f' t b)
• mapping1 :: (Post Functor f, Post Functor f', Category (Dom1 f)) => (Via a b a b -> Via a b s t) -> Iso (f i s) (f' j t) (f i a) (f' j b)
• firstly :: (Functor f, Functor f', Category (Dom f)) => (Via a b a b -> Via a b s t) -> Iso (f s x) (f' t y) (f a x) (f' b y)
• post :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (i ~> s) (j ~> t) (i ~> a) (j ~> b)
• pre :: Category (Arr i) => (Via a b a b -> Via a b s t) -> Iso (a ~> i) (b ~> j) (s ~> i) (t ~> j)
• newtype Self a b = Self {
  • runSelf :: a ~> b
  }
• _Self :: (Functor * k (p (Any *)), Contravariant (* -> k) * p, Category k (Hom k *)) => (~>) k (p (Hom k1 * a b) (Hom k2 * a1 b1)) (p (Self k1 a b) (Self k2 a1 b1))
• class (Functor p, Profunctor (Cod2 p), Category (Cod2 p)) => Semitensor p where
  • type Tensorable p :: x -> Constraint
  • second :: Tensorable p c => (a ~> b) -> p c a ~> p c b
  • associate :: (Tensorable p a, Tensorable p b, Tensorable p c, Tensorable p a', Tensorable p b', Tensorable p c') => Iso (p (p a b) c) (p (p a' b') c') (p a (p b c)) (p a' (p b' c'))
• type family I p :: x
• class Semitensor p => Tensor p where
  • lambda :: (Tensorable p a, Tensorable p a') => Iso (p (I p) a) (p (I p) a') a a'
  • rho :: (Tensorable p a, Tensorable p a') => Iso (p a (I p)) (p a' (I p)) a a'
• class Bifunctor p => Symmetric p where
  • swap :: p a b ~> p b a
• class (Profunctor (Internal k), Category k, k ~ Hom) => Closed k where
  • iota :: Iso (Internal k (I (Internal k)) a) (Internal k (I (Internal k)) b) a b
  • jot :: I (Internal k) ~> Internal k a a
• class (One ~ t) => Terminal t | i -> t where
  • type One :: i
  • terminal :: a ~> t
• class (Zero ~ t) => Initial t | i -> t where
  • type Zero :: i
  • initial :: t ~> a
• type family Copower :: i -> j -> j
• type * = (Copower :: i -> i -> i)
• class (h ~ (~>), Symmetric (* :: i -> i -> i), Semitensor (* :: i -> i -> i)) => Precartesian h | i -> h where
  • fst :: forall a b. (a * b) ~> a
  • snd :: forall a b. (a * b) ~> b
  • (&&&) :: forall a b c. (a ~> b) -> (a ~> c) -> a ~> (b * c)
• class (h ~ (~>), Tensor (* :: i -> i -> i), Terminal (I (* :: i -> i -> i)), Precartesian h) => Cartesian h | i -> h
• class (h ~ (~>), Symmetric ((+) :: i -> i -> i), Semitensor ((+) :: i -> i -> i)) => Precocartesian h | i -> h where
  • type (+) :: i -> i -> i
  • inl :: forall a b. a ~> (a + b)
  • inr :: forall a b. b ~> (a + b)
  • (|||) :: forall a b c. (a ~> c) -> (b ~> c) -> (a + b) ~> c
• class (h ~ (~>), Tensor ((+) :: i -> i -> i), Initial (I ((+) :: i -> i -> i)), Precocartesian h) => Cocartesian h | i -> h
• class (Cartesian k, Cocartesian k) => Distributive k | i -> k where
  • distribute :: forall a b c a' b' c'. Iso ((a * b) + (a * c)) ((a' * b') + (a' * c')) (a * (b + c)) (a' * (b' + c'))
• class (Cartesian k, Closed k, Curried * (Internal k), I (Internal k) ~ I *, Curryable * (I (Internal k))) => CCC k | x -> k
• class (Precartesian ((~>) :: x -> x -> *), Precartesian ((~>) :: y -> y -> *), Functor f) => Semimonoidal f where
  • ap2 :: (f a * f b) ~> f (a * b)
• ap :: (Semimonoidal f, CCC (Dom f), CCC (Cod f), Curryable * (f (b ^ a))) => f (b ^ a) ~> (f b ^ f a)
• ap2Applicative :: Applicative f => (f a * f b) -> f (a * b)
• class (Cartesian ((~>) :: x -> x -> *), Cartesian ((~>) :: y -> y -> *), Semimonoidal f) => Monoidal f where
  • ap0 :: One ~> f One
• return :: (Monoidal f, Strength f, CCC (Dom f), Tensorable * a) => a ~> f a
• class (Precocartesian ((~>) :: x -> x -> *), Precocartesian ((~>) :: y -> y -> *), Functor f) => Cosemimonoidal f where
  • op2 :: f (a + b) ~> (f a + f b)
• class (Cocartesian ((~>) :: x -> x -> *), Cocartesian ((~>) :: y -> y -> *), Cosemimonoidal f) => Comonoidal f where
  • op0 :: f Zero ~> Zero
• class Semimonoidal (m :: x -> x) => Semimonad m where
  • join :: m (m a) ~> m a
  • bind :: Semimonad m => (a ~> m b) ~> (m a ~> m b)
• class (Monoidal m, Semimonad m) => Monad m
• class (Functor f, Category (Dom f)) => Cosemimonad f where
  • duplicate :: f a ~> f (f a)
  • extend :: (f a ~> b) -> f a ~> f b
• class Cosemimonad f => Comonad f where
  • extract :: f a ~> a
• class Precartesian (Arr m) => Semigroup m where
  • mult :: (m * m) ~> m
• multM :: (Semimonoidal u, Semigroup m) => (u m * u m) ~> u m
• class (Semigroup m, Cartesian (Arr m)) => Monoid m where
  • one :: One ~> m
• oneM :: (Monoidal u, Monoid m) => One ~> u m
• mappend :: (Semigroup m, CCC (Arr m), Curryable * m) => m ~> (m ^ m)
• class Precocartesian (Arr m) => Cosemigroup m where
  • comult :: m ~> (m + m)
• zeroOp :: (Comonoidal f, Comonoid m) => f m ~> Zero
• class (Cosemigroup m, Cocartesian (Arr m)) => Comonoid m where
  • zero :: m ~> Zero
• comultOp :: (Cosemimonoidal f, Cosemigroup m) => f m ~> (f m + f m)
• class Functor f => Strength f where
  • strength :: (a * f b) ~> f (a * b)
• class Functor f => Costrength f where
  • costrength :: f (a + b) ~> (a + f b)
• class (f -| f, Id ~ f) => Identity f | i -> f where
  • type Id :: i -> i
  • _Id :: Iso (f a) (f a') a a'
• class (c ~ Hom) => HasRan c | k -> c where
  • type Ran :: (i -> j) -> (i -> k) -> j -> k
  • ranCurried :: Dict (Curried Compose (Ran :: (i -> j) -> (i -> k) -> j -> k))
  • ranProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Ran :: (i -> j) -> (i -> k) -> j -> k))
  • ranFunctor :: Dict (Functor (Ran f g :: j -> k))
  • iotaRan :: forall f g id. (Category (Cod f), Category (Dom f), Functor g, Identity id) => Iso (Ran id f) (Ran id g) f g
  • jotRan :: forall f. Id ~> Ran f f
• class (c ~ Hom) => HasLan c | k -> c where
  • type Lan :: (i -> j) -> (i -> k) -> j -> k
  • lanCocurried :: Dict (Cocurried (Lan :: (i -> j) -> (i -> k) -> j -> k) Compose)
  • lanProfunctor :: Category (Hom :: j -> j -> *) => Dict (Profunctor (Lan :: (i -> j) -> (i -> k) -> j -> k))
  • lanFunctor :: Dict (Functor (Lan f g :: j -> k))
  • epsilonLan :: forall f g id. (Category (Cod f), Category (Dom f), Functor f, Identity id) => Iso (Lan id f) (Lan id g) f g
• data Prod :: (i, j) -> (i, j) -> * where
  • Want :: Prod a a
  • Have :: (a ~> b) -> (c ~> d) -> Prod `(a, c)` `(b, d)`
• runProd :: forall a b c d. (Category ((~>) :: i -> i -> *), Category ((~>) :: j -> j -> *)) => Prod `(a, c)` `(b, d)` -> (a ~> b, c ~> d)
• runFst :: forall a b c d. Category ((~>) :: i -> i -> *) => Prod `(a, c)` `(b, d)` -> a ~> b
• runSnd :: forall a b c d. Category ((~>) :: j -> j -> *) => Prod `(a, c)` `(b, d)` -> c ~> d
• diagProdAdj :: forall a b c a' b' c'. Cartesian ((~>) :: i -> i -> *) => Iso (`(a, a)` ~> `(b, c)`) (`(a', a')` ~> `(b', c')`) (a ~> (b * c)) (a' ~> (b' * c'))
• sumDiagAdj :: forall a b c a' b' c'. Cocartesian ((~>) :: i -> i -> *) => Iso ((b + c) ~> a) ((b' + c') ~> a') (`(b, c)` ~> `(a, a)`) (`(b', c')` ~> `(a', a')`)
• data Unit a b = Unit
• newtype Empty a b = Empty (Empty a b)
• data No a
• class (Profunctor p, p ~ (~>)) => Semicategory p
• newtype Compose1 f g a = Compose {
  • getCompose :: f (g a)
  }
• newtype Compose2 f g a b = Compose2 {
  • getCompose2 :: f (g a) b
  }
• class f (g a) => ComposeC f g a
• newtype Lim1 f = Lim {
  • getLim :: forall x. f x
  }
• newtype Lim2 f y = Lim2 {
  • getLim2 :: forall x. f x y
  }
• newtype Lim3 f y z = Lim3 {
  • getLim3 :: forall x. f x y z
  }
• class LimC p where
  • limDict :: Dict (p a)
• newtype Const1 b a = Const {
  • getConst :: b
  }
• newtype Const2 f a c = Const2 {
  • getConst2 :: f c
  }
• class b => ConstC b a
• data Colim1 f where
  • Colim :: f x -> Colim1 f
• data Colim2 f x where
  • Colim2 :: f y x -> Colim2 f x
• newtype Id0 a = Id {
  • runId :: a
  }
• newtype Id1 f a = Id1 {
  • runId1 :: f a
  }
• class c => IdC c
• newtype Lift1 p f g a = Lift {
  • lower :: p (f a) (g a)
  }
• newtype Lift2 p f g a b = Lift2 {
  • lower2 :: p (f a) (g a) b
  }
• class r (p a) (q a) => LiftC r p q a
• class r (f a) (g a) b => LiftC2 r f g a b
• data Copower1 x f a = Copower x (f a)
• data Copower2 x f a b = Copower2 x (f a b)
• data Copower2_1 x f a b = Copower2_1 (x a) (f a b)
• data Ran1 f g a = forall z . Functor z => Ran (Compose z f ~> g) (z a)
• newtype Lan1 f g a = Lan {
  • runLan :: forall z. Functor z => (g ~> Compose z f) ~> z a
  }
• newtype Lan2 f g a b = Lan2 {
  • runLan2 :: forall z. Functor z => (g ~> Compose z f) ~> z a b
  }
• data Constraint :: BOX
• undefined :: a
• ($) :: (a -> b) -> a -> b
• data Either a b :: * -> * -> *
  • = Left a
  • | Right b
• data Maybe a :: * -> *
  • = Nothing
  • | Just a
• newtype Tagged s b :: k -> * -> * = Tagged {
  • unTagged :: b
  }
• data Proxy t :: k -> * = Proxy
• class Category cat where
  • id :: cat a a
  • (.) :: cat b c -> cat a b -> cat a c
• data Void :: *
• absurd :: Void -> a

Documentation

Natural transformations

Functors

Functor composition

In the limit

Derived notions

Colim -| Const -| Lim

Natural Isomorphisms

Adjunctions

Currying

Cocurrying

Automatic Lifting

Constraints

Lens Esoterica

The Yoneda embedding

Inverting natural isomorphisms

get   = via _Get
beget = via _Beget
un    = via _Un

Hom as a Profunctor

Monoidal Categories

Closed Categories

Terminal and Initial Objects

Copowers and Cartesian Categories

Distributive bicartesian categories

CCC's

Monoidal Functors