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

Portability non-portable (rank-2 polymorphism) experimental Edward Kmett

Control.Functor.KanExtension

Description

Left and right Kan extensions, expressed as higher order functors

NB: `Yoneda`, `CoYoneda`, `Density`, `Codensity` have been factored out into separate modules.

Synopsis

# Right Kan Extensions

newtype Ran g h a Source

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 FieldsrunRan :: forall b. (a -> g b) -> h b

Instances

 HFunctor (Ran g) Functor (Ran g h)

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)

adjointToRan :: Adjunction f g => f :~> Ran g IdentitySource

`f -| g` iff `Ran g Identity` exists (forward)

`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

`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

 Functor g => HFunctor (Lan g) Functor (Lan f g)

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)

adjointToLan :: Adjunction f g => g :~> Lan f IdentitySource

f -| g iff Lan f Identity is inhabited (forwards)

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)