Copyright  20132016 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 postcomposition 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 postcomposition 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
.