Control.Functor.KanExtension

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.

Right Kan Extensions

newtype Ran g h a

Right Kan Extension

Constructors

Ran

Fields

runRan :: forall b. (a -> g b) -> h b

Instances

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

liftRan :: Monad m => m a -> Ran m m a

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 a

The natural isomorphism between a monad m and the monad generated by m (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

Constructors

forall b . Lan (g b -> a) (h b)

Instances

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

liftLan :: Comonad w => w a -> Lan w w a

The natural isomorphism between a comonad w and the comonad generated by w (forwards).

lowerLan :: Comonad w => Lan w w a -> w a

The natural isomorphism between a comonad w and the comonad generated by w (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

Performance tweaks for (co)free (co)monads

improveFree :: Functor f => (forall m. MonadFree f m => m a) -> Free f a

Voigtlaender's asymptotic performance improvement for free monads

worsenCofree :: Functor f => (forall w. ComonadCofree f w => w a) -> Cofree f a