Portability | rank N types |
---|---|
Stability | experimental |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Safe Haskell | Trustworthy |
Right and Left Kan lifts for functors over Hask, where they exist.
- newtype Rift g h a = Rift {
- runRift :: forall r. g (a -> r) -> h r
- toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a
- fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b
- grift :: Adjunction f u => f (Rift f k a) -> k a
- composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a
- decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a
- adjointToRift :: Adjunction f u => u a -> Rift f Identity a
- riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a
- composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a
- riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)
- rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b
- newtype Lift g f a = Lift {}
- toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b
- fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)
- glift :: Adjunction l g => k a -> g (Lift g k a)
- composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a
- decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a
- adjointToLift :: Adjunction f u => f a -> Lift u Identity a
- liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a
- liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)
- composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a
Right Kan lifts
g . Rift
g f => f
This could alternately be defined directly from the (co)universal propertly
in which case, we'd get toRift
= UniversalRift
, but then the usage would
suffer.
dataUniversalRift
g f a = forall z.Functor
z =>UniversalRift
(forall x. g (z x) -> f x) (z a)
We can witness the isomorphism between Rift and UniversalRift using:
riftIso1 :: Functor g => UniversalRift g f a -> Rift g f a riftIso1 (UniversalRift h z) = Rift $ g -> h $ fmap (k -> k $ z) g
riftIso2 :: Rift g f a -> UniversalRift g f a riftIso2 (Rift e) = UniversalRift e id
riftIso1 (riftIso2 (Rift h)) = riftIso1 (UniversalRift h id) = -- by definition Rift $ g -> h $ fmap (k -> k $ id) g -- by definition Rift $ g -> h $ fmap id g -- $ = (.) and (.id) Rift $ g -> h g -- by functor law Rift h -- eta reduction
The other direction is left as an exercise for the reader.
There are several monads that we can form from Rift
.
When g
is corepresentable (e.g. is a right adjoint) then there exists x
such that g ~ (->) x
, then it follows that
Rift g g a ~ forall r. (x -> a -> r) -> x -> r ~ forall r. (a -> x -> r) -> x -> r ~ forall r. (a -> g r) -> g r ~ Codensity g r
When f
is a left adjoint, so that f -| g
then
Rift f f a ~ forall r. f (a -> r) -> f r ~ forall r. (a -> r) -> g (f r) ~ forall r. (a -> r) -> Adjoint f g r ~ Yoneda (Adjoint f g r)
An alternative way to view that is to note that whenever f
is a left adjoint then f -|
, and since Rift
f Identity
is isomorphic to Rift
f f
, this is the Rift
f Identity
(f a)Monad
formed by the adjunction.
can be a Rift
w f ~ CoT
w fMonad
for any Comonad
w
.
can be a Rift
Identity
mMonad
for any Monad
m
, as it is isomorphic to
.
Yoneda
m
toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h aSource
The universal property of Rift
fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h bSource
grift :: Adjunction f u => f (Rift f k a) -> k aSource
composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h aSource
composeRift
.decomposeRift
≡id
decomposeRift
.composeRift
≡id
decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) aSource
adjointToRift :: Adjunction f u => u a -> Rift f Identity aSource
Rift f Identity a
is isomorphic to the right adjoint to f
if one exists.
adjointToRift
.riftToAdjoint
≡id
riftToAdjoint
.adjointToRift
≡id
riftToAdjoint :: Adjunction f u => Rift f Identity a -> u aSource
Rift f Identity a
is isomorphic to the right adjoint to f
if one exists.
composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h aSource
Rift f h a
is isomorphic to the post-composition of the right adjoint of f
onto h
if such a right adjoint exists.
riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)Source
| Rift f h a
is isomorphic to the post-composition of the right adjoint of f
onto h
if such a right adjoint exists.
riftToComposedAdjoint
.composedAdjointToRift
≡id
composedAdjointToRift
.riftToComposedAdjoint
≡id
rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h bSource
Indexed applicative composition of right Kan lifts.
Left Kan lifts
f => g . Lift g f (forall z. f => g . z) -> Lift g f => z -- couniversal
Here we use the universal property directly as how we extract from our definition of Lift
.
toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z bSource
The universal property of Lift
fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)Source
glift :: Adjunction l g => k a -> g (Lift g k a)Source
f => g (Lift
g f a)
composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h aSource
composeLift
.decomposeLift
=id
decomposeLift
.composeLift
=id
decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) aSource
adjointToLift :: Adjunction f u => f a -> Lift u Identity aSource
Lift u Identity a
is isomorphic to the left adjoint to u
if one exists.
adjointToLift
.liftToAdjoint
≡id
liftToAdjoint
.adjointToLift
≡id
liftToAdjoint :: Adjunction f u => Lift u Identity a -> f aSource
Lift u Identity a
is isomorphic to the left adjoint to u
if one exists.
liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)Source
Lift u h a
is isomorphic to the post-composition of the left adjoint of u
onto h
if such a left adjoint exists.
liftToComposedAdjoint
.composedAdjointToLift
≡id
composedAdjointToLift
.liftToComposedAdjoint
≡id
composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h aSource
Lift u h a
is isomorphic to the post-composition of the left adjoint of u
onto h
if such a left adjoint exists.