kan-extensions-5.2: Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads

Copyright 2013-2016 Edward Kmett and Dan Doel BSD Edward Kmett experimental rank N types Safe 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 #

Constructors

 Curried FieldsrunCurried :: forall r. g (a -> r) -> h r
Instances
 Functor g => Functor (Curried g h) # Instance detailsDefined in Data.Functor.Day.Curried Methodsfmap :: (a -> b) -> Curried g h a -> Curried g h b #(<\$) :: a -> Curried g h b -> Curried g h a # (Functor g, g ~ h) => Applicative (Curried g h) # Instance detailsDefined in Data.Functor.Day.Curried Methodspure :: a -> Curried g h a #(<*>) :: Curried g h (a -> b) -> Curried g h a -> Curried g h b #liftA2 :: (a -> b -> c) -> Curried g h a -> Curried g h b -> Curried g h c #(*>) :: Curried g h a -> Curried g h b -> Curried g h b #(<*) :: Curried g h a -> Curried g h b -> Curried g h a #

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

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

This is the unit 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)     -- 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 #

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 #

Indexed applicative composition of right Kan lifts.