Modulekan-extensions-5.2.7Haskell2010

Data.Functor.Day.Curried

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

1 type
11 values

Packagekan-extensions-5.2.7
Exports12
LanguageHaskell2010
LicenceBSD-3-Clause
SourceCurried.hs

Right Kan lifts

12 declarations

newtypenewtype Curried (g :: Type -> Type) (h :: Type -> Type) a

Constructors

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

Instances3Functor, Applicative, Apply

Functor g => Functor (Curried g h)Defined in kan-extensions-5.2.7 · Data.Functor.Day.Curried
(Functor g, g ~ h) => Applicative (Curried g h)Defined in kan-extensions-5.2.7 · Data.Functor.Day.Curried
(Functor g, g ~ h) => Apply (Curried g h)Defined in kan-extensions-5.2.7 · Data.Functor.Day.Curried

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

The universal property of Curried

valuefromCurried

:: Functor f
=> forall a. k a -> Curried f h a
-> Day f k b
-> h b

toCurried . fromCurried ≡ id
fromCurried . toCurried ≡ id

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

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

valueunapplied :: g a -> Curried f (Day f g) a

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

valueadjointToCurried :: 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

valuecurriedToAdjoint :: Adjunction f u => Curried f Identity a -> u a

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

valuecomposedAdjointToCurried

:: (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.

valuecurriedToComposedAdjoint :: 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

valueliftCurried :: 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

valuelowerCurried :: Applicative f => Curried f g a -> g a

Lower Curried by applying pure id to the continuation.

See liftCurried.

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

Indexed applicative composition of right Kan lifts.