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

Copyright 2013-2016 Edward Kmett and Dan Doel BSD Edward Kmett experimental rank N types None Haskell98

Data.Functor.Day.Curried

Contents

Description

``Day` f -| `Curried` f`

`Day f ~ Compose f` when f preserves colimits / is a left adjoint. (Due in part to the strength of all functors in Hask.)

So by the uniqueness of adjoints, when f is a left adjoint, `Curried f ~ Rift f`

Synopsis

# Right Kan lifts

newtype Curried g h a Source

Constructors

 Curried FieldsrunCurried :: forall r. g (a -> r) -> h r

Instances

 Functor g => Functor (Curried g h) Source (Functor g, (~) (* -> *) g h) => Applicative (Curried g h) Source

toCurried :: (forall x. Day g k x -> h x) -> k a -> Curried g h a Source

The universal property of `Curried`

fromCurried :: Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b Source

````toCurried` . `fromCurried` ≡ `id`
`fromCurried` . `toCurried` ≡ `id`
```

applied :: Functor f => Day f (Curried f g) a -> g a Source

This is the counit of the `Day f -| Curried f` adjunction

unapplied :: g a -> Curried f (Day f g) a Source

This is the unit of the `Day f -| Curried f` adjunction

adjointToCurried :: Adjunction f u => u a -> Curried f Identity a Source

`Curried f Identity a` is isomorphic to the right adjoint to `f` if one exists.

````adjointToCurried` . `curriedToAdjoint` ≡ `id`
`curriedToAdjoint` . `adjointToCurried` ≡ `id`
```

curriedToAdjoint :: Adjunction f u => Curried f Identity a -> u a Source

`Curried f Identity a` is isomorphic to the right adjoint to `f` if one exists.

composedAdjointToCurried :: (Functor h, Adjunction f u) => u (h a) -> Curried f h a Source

`Curried f h a` is isomorphic to the post-composition of the right adjoint of `f` onto `h` if such a right adjoint exists.

curriedToComposedAdjoint :: Adjunction f u => Curried f h a -> u (h a) Source

`Curried f h a` is isomorphic to the post-composition of the right adjoint of `f` onto `h` if such a right adjoint exists.

````curriedToComposedAdjoint` . `composedAdjointToCurried` ≡ `id`
`composedAdjointToCurried` . `curriedToComposedAdjoint` ≡ `id`
```

liftCurried :: Applicative f => f a -> Curried f f a Source

The natural isomorphism between `f` and `Curried f f`. ``` lowerCurried . liftCurried ≡ id liftCurried . lowerCurried ≡ id ```

````lowerCurried` (`liftCurried` x)     -- definition
`lowerCurried` (`Curried` (`<*>` x))   -- definition
(`<*>` x) (`pure` `id`)          -- beta reduction
`pure` `id` `<*>` x              -- Applicative identity law
x
```

lowerCurried :: Applicative f => Curried f g a -> g a Source

Lower `Curried` by applying `pure` `id` to the continuation.

See `liftCurried`.

rap :: Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b Source

Indexed applicative composition of right Kan lifts.