Copyright	2013-2016 Edward Kmett and Dan Doel
License	BSD
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	rank N types
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Functor.Day.Curried

Contents

Right Kan lifts

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

newtype Curried (g :: Type -> Type) (h :: Type -> Type) a = Curried {
- runCurried :: forall r. g (a -> r) -> h r
}
toCurried :: forall (g :: Type -> Type) k h a. (forall x. Day g k x -> h x) -> k a -> Curried g h a
fromCurried :: forall (f :: Type -> Type) k h b. Functor f => (forall a. k a -> Curried f h a) -> Day f k b -> h b
applied :: forall (f :: Type -> Type) g a. Functor f => Day f (Curried f g) a -> g a
unapplied :: forall g a (f :: Type -> Type). g a -> Curried f (Day f g) a
adjointToCurried :: forall (f :: Type -> Type) u a. Adjunction f u => u a -> Curried f Identity a
curriedToAdjoint :: forall (f :: Type -> Type) u a. Adjunction f u => Curried f Identity a -> u a
composedAdjointToCurried :: forall h (f :: Type -> Type) u a. (Functor h, Adjunction f u) => u (h a) -> Curried f h a
curriedToComposedAdjoint :: forall (f :: Type -> Type) u h a. Adjunction f u => Curried f h a -> u (h a)
liftCurried :: Applicative f => f a -> Curried f f a
lowerCurried :: forall (f :: Type -> Type) g a. Applicative f => Curried f g a -> g a
rap :: forall (f :: Type -> Type) (g :: Type -> Type) a b (h :: Type -> Type). Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b

Right Kan lifts

newtype Curried (g :: Type -> Type) (h :: Type -> Type) a Source #

Constructors

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

Instances

Instances details

(Functor g, g ~ h) => Applicative (Curried g h) Source #
Instance details Defined in Data.Functor.Day.Curried Methods pure :: 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 #
Functor g => Functor (Curried g h) Source #
Instance details Defined in Data.Functor.Day.Curried Methods fmap :: (a -> b) -> Curried g h a -> Curried g h b # (<$) :: a -> Curried g h b -> Curried g h a #
(Functor g, g ~ h) => Apply (Curried g h) Source #
Instance details Defined in Data.Functor.Day.Curried Methods (<.>) :: Curried g h (a -> b) -> Curried g h a -> Curried g h b # (.>) :: Curried g h a -> Curried g h b -> Curried g h b # (<.) :: Curried g h a -> Curried g h b -> Curried g h a # liftF2 :: (a -> b -> c) -> Curried g h a -> Curried g h b -> Curried g h c #

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

The universal property of Curried

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

toCurried . fromCurried ≡ id
fromCurried . toCurried ≡ id

applied :: forall (f :: Type -> Type) g a. Functor f => Day f (Curried f g) a -> g a Source #

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

unapplied :: forall g a (f :: Type -> Type). g a -> Curried f (Day f g) a Source #

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

adjointToCurried :: forall (f :: Type -> Type) u a. 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 :: forall (f :: Type -> Type) u a. 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 :: forall h (f :: Type -> Type) u a. (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 :: forall (f :: Type -> Type) u h a. 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 :: forall (f :: Type -> Type) g a. Applicative f => Curried f g a -> g a Source #

Lower Curried by applying pure id to the continuation.

See liftCurried.

rap :: forall (f :: Type -> Type) (g :: Type -> Type) a b (h :: Type -> Type). Functor f => Curried f g (a -> b) -> Curried g h a -> Curried f h b Source #

Indexed applicative composition of right Kan lifts.