Data.Functor.KanExtension

Documentation

newtype Ran g h a

Constructors

Ran

Fields

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

Instances

Functor (Ran g h)

toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b

toRan and fromRan witness a higher kinded adjunction. from (`'Compose'` g) to Ran g

fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b

composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a

decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a

adjointToRan :: Adjunction f g => f a -> Ran g Identity a

ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a

ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)

composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a

data Lan g h a where

Constructors

Lan :: (g b -> a) -> h b -> Lan g h a

Instances

Functor (Lan f g)

(Functor g, Applicative h) => Applicative (Lan g h)

(Functor g, Apply h) => Apply (Lan g h)

toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b

fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)

adjointToLan :: Adjunction f g => g a -> Lan f Identity a

lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a

lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)

lanToComposedAdjoint and composedAdjointToLan witness the natural isomorphism between Lan f h and Compose h g given f -| g

composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a

composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a

composeLan and decomposeLan witness the natural isomorphism from Lan f (Lan g h) and Lan (f o g) h

decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a