| category-extras-0.53.6: Various modules and constructs inspired by category theory | Contents | Index |
|
Control.Functor.KanExtension | Portability | non-portable (rank-2 polymorphism) | Stability | experimental | Maintainer | Edward Kmett <ekmett@gmail.com> |
|
|
|
|
|
Description |
Left and right Kan extensions, expressed as higher order functors
See http://comonad.com/reader/2008/kan-extensions/
and http://comonad.com/reader/2008/kan-extensions-ii/
for motivation.
NB: Yoneda, CoYoneda, Density, Codensity have been factored
out into separate modules.
|
|
Synopsis |
|
newtype Ran g h a = Ran {runRan :: forall b. (a -> g b) -> h b | } | | toRan :: (Composition o, Functor k) => ((k `o` g) :~> h) -> k :~> Ran g h | | fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> h | | adjointToRan :: Adjunction f g => f :~> Ran g Identity | | ranToAdjoint :: Adjunction f g => Ran g Identity :~> f | | ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f) | | composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g h | | composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) h | | decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h) | | data Lan g h a = forall b . Lan (g b -> a) (h b) | | toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> f | | fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g) | | adjointToLan :: Adjunction f g => g :~> Lan f Identity | | lanToAdjoint :: Adjunction f g => Lan f Identity :~> g | | composeLan :: (Functor f, Composition o) => Lan f (Lan g h) :~> Lan (f `o` g) h | | decomposeLan :: Composition o => Lan (f `o` g) h :~> Lan f (Lan g h) | | lanToComposedAdjoint :: (Functor h, Composition o, Adjunction f g) => Lan f h :~> (h `o` g) | | composedAdjointToLan :: (Composition o, Adjunction f g) => (h `o` g) :~> Lan f h |
|
|
|
Right Kan Extensions
|
|
newtype Ran g h a |
The right Kan Extension of h along g.
An alternative definition in terms of Ends.
newtype RanT g h a b b' { (a -> g b) -> h b' } type Ran g h a = End (RanT g h a) | Constructors | Ran | | runRan :: forall b. (a -> g b) -> h b | |
|
| Instances | |
|
|
toRan :: (Composition o, Functor k) => ((k `o` g) :~> h) -> k :~> Ran g h |
Nat(k o g, h) is isomorphic to Nat(k, Ran g h) (forwards)
|
|
fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> h |
Nat(k o g, h) is isomorphic to Nat(k, Ran g h) (backwards)
|
|
adjointToRan :: Adjunction f g => f :~> Ran g Identity |
f -| g iff Ran g Identity exists (forward)
|
|
ranToAdjoint :: Adjunction f g => Ran g Identity :~> f |
f -| g iff Ran g Identity exists (backwards)
|
|
ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f) |
|
composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g h |
|
composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) h |
The natural isomorphism from Ran f (Ran g h) to Ran (f o g) h (forwards)
|
|
decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h) |
The natural isomorphism from Ran f (Ran g h) to Ran (f o g) h (backwards)
|
|
Left Kan Extensions
|
|
data Lan g h a |
Left Kan Extension
newtype LanT g h a b b' { (g b -> a, h b') } type Lan g h a = Coend (LanT g h a) | Constructors | forall b . Lan (g b -> a) (h b) | |
| Instances | |
|
|
toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> f |
Nat(h, f.g) is isomorphic to Nat (Lan g h, f) (forwards)
|
|
fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g) |
Nat(h, f.g) is isomorphic to Nat (Lan g h, f) (backwards)
|
|
adjointToLan :: Adjunction f g => g :~> Lan f Identity |
f -| g iff Lan f Identity is inhabited (forwards)
|
|
lanToAdjoint :: Adjunction f g => Lan f Identity :~> g |
f -| g iff Lan f Identity is inhabited (backwards)
|
|
composeLan :: (Functor f, Composition o) => Lan f (Lan g h) :~> Lan (f `o` g) h |
the natural isomorphism from Lan f (Lan g h) to Lan (f o g) h (forwards)
|
|
decomposeLan :: Composition o => Lan (f `o` g) h :~> Lan f (Lan g h) |
the natural isomorphism from Lan f (Lan g h) to Lan (f o g) h (backwards)
|
|
lanToComposedAdjoint :: (Functor h, Composition o, Adjunction f g) => Lan f h :~> (h `o` g) |
|
composedAdjointToLan :: (Composition o, Adjunction f g) => (h `o` g) :~> Lan f h |
|
Produced by Haddock version 2.1.0 |