Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data COMPOSE = Compose
- type Compose = (Any Compose :: (i -> i -> *) -> (j -> j -> *) -> (k -> k -> *) -> (j -> k) -> (i -> j) -> i -> k)
- class Category e => Composed e where
- data ID = Id
- type Id = (Any Id :: (i -> i -> *) -> i -> i)
- class Category c => Identified c where
- associateCompose :: forall b c d e f g h f' g' h'. (Category b, Category c, Composed d, Composed e, FunctorOf d e f, FunctorOf c d g, FunctorOf b c h, FunctorOf d e f', FunctorOf c d g', FunctorOf b c h') => Iso (Nat b e) (Nat b e) (->) (Compose b c e (Compose c d e f g) h) (Compose b c e (Compose c d e f' g') h') (Compose b d e f (Compose b c d g h)) (Compose b d e f' (Compose b c d g' h'))
- lambdaCompose :: forall a a' c. (Identified c, Composed c, Ob (Nat c c) a, Ob (Nat c c) a') => Iso (Nat c c) (Nat c c) (->) (Compose c c c (Id c) a) (Compose c c c (Id c) a') a a'
- rhoCompose :: forall a a' c. (Identified c, Composed c, Ob (Nat c c) a, Ob (Nat c c) a') => Iso (Nat c c) (Nat c c) (->) (Compose c c c a (Id c)) (Compose c c c a' (Id c)) a a'
- class (Functor m, Dom m ~ Cod m, Monoid (Compose (Dom m) (Dom m) (Dom m)) m, Identified (Dom m), Composed (Dom m)) => Monad m
- return :: forall m a. (Monad m, Ob (Dom m) a) => Dom m a (m a)
- bind :: forall m a b. (Monad m, Ob (Dom m) b) => Dom m a (m b) -> Dom m (m a) (m b)
Compose
(Category k c, Category k2 d, Composed k1 e, Functor k2 k1 f, Functor k k2 g, (~) (k1 -> k1 -> *) e (Cod k2 k1 f), (~) (k2 -> k2 -> *) d (Cod k k2 g), (~) (k2 -> k2 -> *) d (Dom k2 k1 f), (~) (k -> k -> *) c (Dom k k2 g)) => Functor k k (Compose k k k c d e f g) | |
(Category k c, Category k1 d, Category Constraint e) => Class (f (g a)) (Compose k k Constraint c d e f g a) | |
(Category k c, Category k1 d, Category Constraint e) => (f (g a)) :=> (Compose k k Constraint c d e f g a) | |
(Category k c, Category k1 d, Composed k2 e) => Functor (k -> k) ((k -> k) -> k -> k) (Compose k k k c d e) | |
(Category k c, Category k1 d, Composed k2 e, Functor k1 k2 f, (~) (k2 -> k2 -> *) e (Cod k1 k2 f), (~) (k1 -> k1 -> *) d (Dom k1 k2 f)) => Functor (k -> k) (k -> k) (Compose k k k c d e f) | |
(Identified i c, Composed i c) => Tensor' (i -> i) (Compose i i i c c c) | |
(Composed i c, (~) (i -> i -> *) c c', (~) (i -> i -> *) c' c'') => Semitensor (i -> i) (Compose i i i c c' c'') | |
(Identified k c, Composed k c) => Comonoid' (k -> k) (Compose k k k c c c) (Id k c) | |
(Identified k c, Composed k c) => Cosemigroup (k -> k) (Compose k k k c c c) (Id k c) | |
(Identified k c, Composed k c) => Monoid' (k -> k) (Compose k k k c c c) (Id k c) | |
(Identified k c, Composed k c) => Semigroup (k -> k) (Compose k k k c c c) (Id k c) | |
type Dom k k1 (Compose k k2 k1 c d e f g) = c | |
type Cod k k1 (Compose k k2 k1 c d e f g) = e | |
type Dom (k1 -> k2) ((k -> k1) -> k -> k2) (Compose k k1 k2 c d e) = Nat k1 k2 d e | |
type Cod (k1 -> k2) ((k -> k1) -> k -> k2) (Compose k k1 k2 c d e) = Nat (k -> k1) (k -> k2) (Nat k k1 c d) (Nat k k2 c e) | |
type Dom (k -> k1) (k -> k2) (Compose k k1 k2 c d e f) = Nat k k1 c d | |
type Cod (k -> k1) (k -> k2) (Compose k k1 k2 c d e f) = Nat k k2 c e | |
type I (k -> k) (Compose k k k c c c) = Id k c |
type Compose = (Any Compose :: (i -> i -> *) -> (j -> j -> *) -> (k -> k -> *) -> (j -> k) -> (i -> j) -> i -> k) Source
class Category e => Composed e where Source
Nothing
Identified k c => Functor k k (Id k c) | |
Category Constraint c => Class a (Id Constraint c a) | |
Category Constraint c => a :=> (Id Constraint c a) | |
(Identified k c, Composed k c) => Comonoid' (k -> k) (Compose k k k c c c) (Id k c) | |
(Identified k c, Composed k c) => Cosemigroup (k -> k) (Compose k k k c c c) (Id k c) | |
(Identified k c, Composed k c) => Monoid' (k -> k) (Compose k k k c c c) (Id k c) | |
(Identified k c, Composed k c) => Semigroup (k -> k) (Compose k k k c c c) (Id k c) | |
type Dom k k (Id k c) = c | |
type Cod k k (Id k c) = c |
class Category c => Identified c where Source
Nothing
Identified * (->) | |
Identified Constraint (:-) | |
(Category k c, Identified k1 d) => Identified (k -> k) (Nat k k c d) |
associateCompose :: forall b c d e f g h f' g' h'. (Category b, Category c, Composed d, Composed e, FunctorOf d e f, FunctorOf c d g, FunctorOf b c h, FunctorOf d e f', FunctorOf c d g', FunctorOf b c h') => Iso (Nat b e) (Nat b e) (->) (Compose b c e (Compose c d e f g) h) (Compose b c e (Compose c d e f' g') h') (Compose b d e f (Compose b c d g h)) (Compose b d e f' (Compose b c d g' h')) Source
lambdaCompose :: forall a a' c. (Identified c, Composed c, Ob (Nat c c) a, Ob (Nat c c) a') => Iso (Nat c c) (Nat c c) (->) (Compose c c c (Id c) a) (Compose c c c (Id c) a') a a' Source
rhoCompose :: forall a a' c. (Identified c, Composed c, Ob (Nat c c) a, Ob (Nat c c) a') => Iso (Nat c c) (Nat c c) (->) (Compose c c c a (Id c)) (Compose c c c a' (Id c)) a a' Source