Copyright | 2013-2016 Edward Kmett and Dan Doel |
---|---|
License | BSD |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | experimental |
Portability | rank N types |
Safe Haskell | None |
Language | Haskell98 |
- newtype Curried g h a = Curried {
- runCurried :: forall r. g (a -> r) -> h r
- toCurried :: (forall x. Day g k x -> h x) -> k a -> Curried g h a
- fromCurried :: Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b
- applied :: Functor f => Day f (Curried f g) a -> g a
- unapplied :: g a -> Curried f (Day f g) a
- adjointToCurried :: Adjunction f u => u a -> Curried f Identity a
- curriedToAdjoint :: Adjunction f u => Curried f Identity a -> u a
- composedAdjointToCurried :: (Functor h, Adjunction f u) => u (h a) -> Curried f h a
- curriedToComposedAdjoint :: Adjunction f u => Curried f h a -> u (h a)
- liftCurried :: Applicative f => f a -> Curried f f a
- lowerCurried :: Applicative f => Curried f g a -> g a
- rap :: Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b
Right Kan lifts
Curried | |
|
toCurried :: (forall x. Day g k x -> h x) -> k a -> Curried g h a #
The universal property of Curried
fromCurried :: Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b #
toCurried
.fromCurried
≡id
fromCurried
.toCurried
≡id
applied :: Functor f => Day f (Curried f g) a -> g a #
This is the counit of the Day f -| Curried f
adjunction
adjointToCurried :: Adjunction f u => u a -> Curried f Identity a #
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 #
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 #
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) #
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 #
The natural isomorphism between f
and Curried f f
.
lowerCurried
.
liftCurried
≡ id
liftCurried
.
lowerCurried
≡ id
lowerCurried
(liftCurried
x) -- definitionlowerCurried
(Curried
(<*>
x)) -- definition (<*>
x) (pure
id
) -- beta reductionpure
id
<*>
x -- Applicative identity law x
lowerCurried :: Applicative f => Curried f g a -> g a #
Lower Curried
by applying pure
id
to the continuation.
See liftCurried
.