category-extras-0.51.3: Various modules and constructs inspired by category theory

Portabilitynon-portable (rank-2 polymorphism)
Stabilityexperimental
MaintainerEdward Kmett <ekmett@gmail.com>

Control.Functor.KanExtension

Contents

Description

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.

Synopsis

Right Kan Extensions

newtype Ran g h a Source

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

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 o g) h (forwards)

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 o g) h (backwards)

Left Kan Extensions

data Lan g h a Source

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 :~> 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 o g) h (forwards)

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 o g) h (backwards)

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