Portability | non-portable (rank-2 polymorphism) |
---|---|
Stability | experimental |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Left and right Kan extensions, expressed as higher order functors
Included is the 'monad generated by a functor' Ran f f
and the comonad cogenerated by a functor Lan f f
and machinery for lifting (co)monads into and lowering (co)monads out of
Kan extensions.
- 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
- liftRan :: Monad m => m a -> Ran m m a
- lowerRan :: Monad m => Ran m m a -> m a
- 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)
- liftLan :: Comonad w => w a -> Lan w w a
- lowerLan :: Comonad w => Lan w w a -> w a
- 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
- improveFree :: Functor f => (forall m. MonadFree f m => m a) -> Free f a
- worsenCofree :: Functor f => (forall w. ComonadCofree f w => w a) -> Cofree f a
Right Kan Extensions
Right Kan Extension
MonadReader r m => MonadReader r (Ran m m) | |
MonadState s m => MonadState s (Ran m m) | |
MonadFree f m => MonadFree f (Ran m m) | |
HFunctor (Ran g) | |
Monad (Ran f f) | |
Functor (Ran g h) | |
MonadIO m => MonadIO (Ran m m) | |
Pointed (Ran f f) |
toRan :: (Composition o, Functor k) => ((k `o` g) :~> h) -> k :~> Ran g hSource
Nat(k o
g, h) is isomorphic to Nat(k, Ran g h) (forwards)
fromRan :: Composition o => (k :~> Ran g h) -> (k `o` g) :~> hSource
Nat(k o
g, h) is isomorphic to Nat(k, Ran g h) (backwards)
liftRan :: Monad m => m a -> Ran m m aSource
Lift a monad into its right Kan extension along itself. This is the same operation as is performed by Voightlaender's rep in http://wwwtcs.inf.tu-dresden.de/%7Evoigt/mpc08.pdf and the ContT monad's lift operation. This is also viewable as the forward half of the natural isomorphism between a monad m and the monad generated by m.
lowerRan :: Monad m => Ran m m a -> m aSource
The natural isomorphism between a monad m and the monad generated by m (backwards)
adjointToRan :: Adjunction f g => f :~> Ran g IdentitySource
f -| g
iff Ran g Identity
exists (forward)
ranToAdjoint :: Adjunction f g => Ran g Identity :~> fSource
f -| g
iff Ran g Identity
exists (backwards)
ranToComposedAdjoint :: (Composition o, Adjunction f g) => Ran g h :~> (h `o` f)Source
composedAdjointToRan :: (Functor h, Composition o, Adjunction f g) => (h `o` f) :~> Ran g hSource
composeRan :: Composition o => Ran f (Ran g h) :~> Ran (f `o` g) hSource
The natural isomorphism from Ran f (Ran g h)
to Ran (f
(forwards)
o
g) h
decomposeRan :: (Functor f, Composition o) => Ran (f `o` g) h :~> Ran f (Ran g h)Source
The natural isomorphism from Ran f (Ran g h)
to Ran (f
(backwards)
o
g) h
Left Kan Extensions
Left Kan Extension
forall b . Lan (g b -> a) (h b) |
ComonadContext e m => ComonadContext e (Lan m m) | |
ComonadCofree f w => ComonadCofree f (Lan w w) | |
Functor g => HFunctor (Lan g) | |
Functor (Lan f g) | |
Copointed (Lan f f) | |
Comonad (Lan f f) |
toLan :: (Composition o, Functor f) => (h :~> (f `o` g)) -> Lan g h :~> fSource
Nat(h, f.g)
is isomorphic to Nat (Lan g h, f)
(forwards)
fromLan :: Composition o => (Lan g h :~> f) -> h :~> (f `o` g)Source
Nat(h, f.g)
is isomorphic to Nat (Lan g h, f)
(backwards)
liftLan :: Comonad w => w a -> Lan w w aSource
The natural isomorphism between a comonad w and the comonad generated by w (forwards).
lowerLan :: Comonad w => Lan w w a -> w aSource
The natural isomorphism between a comonad w and the comonad generated by w (backwards).
adjointToLan :: Adjunction f g => g :~> Lan f IdentitySource
f -| g iff Lan f Identity is inhabited (forwards)
lanToAdjoint :: Adjunction f g => Lan f Identity :~> gSource
f -| g iff Lan f Identity is inhabited (backwards)
composeLan :: (Functor f, Composition o) => Lan f (Lan g h) :~> Lan (f `o` g) hSource
the natural isomorphism from Lan f (Lan g h)
to Lan (f
(forwards)
o
g) h
decomposeLan :: Composition o => Lan (f `o` g) h :~> Lan f (Lan g h)Source
the natural isomorphism from Lan f (Lan g h)
to Lan (f
(backwards)
o
g) h
lanToComposedAdjoint :: (Functor h, Composition o, Adjunction f g) => Lan f h :~> (h `o` g)Source
composedAdjointToLan :: (Composition o, Adjunction f g) => (h `o` g) :~> Lan f hSource
Performance tweaks for (co)free (co)monads
improveFree :: Functor f => (forall m. MonadFree f m => m a) -> Free f aSource
Voigtlaender's asymptotic performance improvement for free monads
worsenCofree :: Functor f => (forall w. ComonadCofree f w => w a) -> Cofree f aSource