kan-extensions-3.7: Kan extensions, Kan lifts, various forms of the Yoneda lemma, and (co)density (co)monads

Portability non-portable (rank-2 polymorphism) provisional Edward Kmett Trustworthy

Description

Synopsis

# Documentation

newtype Codensity m a Source

`Codensity f` is the Monad generated by taking the right Kan extension of any `Functor` `f` along itself (`Ran f f`).

This can often be more "efficient" to construct than `f` itself using repeated applications of `(>>=)`.

Constructors

 Codensity FieldsrunCodensity :: forall b. (a -> m b) -> m b

Instances

lowerCodensity :: Monad m => Codensity m a -> m aSource

This serves as the *left*-inverse (retraction) of `lift`.

``` 'lowerCodensity . lift' ≡ `id`
```

In general this is not a full 2-sided inverse, merely a retraction, as `Codensity m` is often considerably larger than `m`.

e.g. `Codensity ((->) s)) a ~ forall r. (a -> s -> r) -> s -> r` could support a full complement of `MonadState s` actions, while `(->) s` is limited to `MonadReader s` actions.

codensityToAdjunction :: Adjunction f g => Codensity g a -> g (f a)Source

The `Codensity` monad of a right adjoint is isomorphic to the monad obtained from the `Adjunction`.

``` `codensityToAdjunction` . `adjunctionToCodensity` ≡ `id`
`adjunctionToCodensity` . `codensityToAdjunction` ≡ `id`
```

codensityToRan :: Codensity g a -> Ran g g aSource

The `Codensity` `Monad` of a `Functor` `g` is the right Kan extension (`Ran`) of `g` along itself.

``` `codensityToRan` . `ranToCodensity` ≡ `id`
`ranToCodensity` . `codensityToRan` ≡ `id`
```

codensityToComposedRep :: Representable u => Codensity u a -> u (Key u, a)Source

The `Codensity` monad of a representable `Functor` is isomorphic to the monad obtained from the `Adjunction` for which that `Functor` is the right adjoint.

``` `codensityToComposedRep` . `composedRepToCodensity` ≡ `id`
`composedRepToCodensity` . `codensityToComposedRep` ≡ `id`
```
``` codensityToComposedRep = `ranToComposedRep` . `codensityToRan`
```

composedRepToCodensity :: Representable u => u (Key u, a) -> Codensity u aSource

``` `composedRepToCodensity` = `ranToCodensity` . `composedRepToRan`
```

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

Right associate all binds in a computation that generates a free monad

This can improve the asymptotic efficiency of the result, while preserving semantics.