({      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_` a b c d e f g h i j k l m n o p q r s t u v w x y z  rank N types experimentalEdward Kmett <ekmett@gmail.com> Trustworthy  g .  g f => fLThis could alternately be defined directly from the (co)universal propertly  in which case, we'd get  =  UniversalRift, but then the usage would  suffer.    data  UniversalRift g f a = forall z. { z =>   UniversalRift" (forall x. g (z x) -> f x) (z a) EWe 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 $ g2 -> 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) 9An alternative way to view that is to note that whenever f is a left adjoint then f -|  f | , and since  f f is isomorphic to  f | (f a), this is the } formed by the adjunction.  w f ~   w f can be a } for any Comonad w.  | m can be a } for any } m, as it is isomorphic to Yoneda m. 4Indexed applicative composition of right Kan lifts. The universal property of  When f -| u, then f -| Rift f Identity and    .  "a ~   .  "a ~ Rift f Identity a' is isomorphic to the right adjoint to f if one exists.    .  "a ~   .  "a ~ Rift f Identity a' is isomorphic to the right adjoint to f if one exists.     .   "a ~    .   "a ~   Rift f h a? is isomorphic to the post-composition of the right adjoint of f onto h! if such a right adjoint exists.     .   "a ~    .   "a ~   Rift f h a? is isomorphic to the post-composition of the right adjoint of f onto h! if such a right adjoint exists.        rank N types experimentalEdward Kmett <ekmett@gmail.com> Trustworthy   f => g . Lift g f 8 (forall z. f => g . z) -> Lift g f => z -- couniversal UHere we use the universal property directly as how we extract from our definition of  .  f => g (  g f a)The universal property of   When the adjunction exists    .  "a ~   .  "a ~     .  = ~   .  = ~ Lift u Identity a& is isomorphic to the left adjoint to u if one exists.    .  "a ~   .  "a ~ Lift u Identity a& is isomorphic to the left adjoint to u if one exists.     .  "a ~   .  "a ~  Lift u h a> is isomorphic to the post-composition of the left adjoint of u onto h if such a left adjoint exists.    .  "a ~   .  "a ~  Lift u h a> is isomorphic to the post-composition of the left adjoint of u onto h if such a left adjoint exists.     .  "a ~   .  "a ~     GADTs, TFs, MPTCs provisionalEdward Kmett <ekmett@gmail.com> TrustworthyA 7 functor (aka presheaf) suitable for Yoneda reduction. Yoneda  expansion of a presheaf    .   "a ~    .  "a ~  Yoneda reduction on a presheaf     GADTs, TFs, MPTCs provisionalEdward Kmett <ekmett@gmail.com> Trustworthy! Yoneda embedding for a presheaf $   $ . % "a ~  % . $ "a ~  !"#$%!"#$%!"#$%!"#$% rank 2 types experimentalEdward Kmett <ekmett@gmail.com> Trustworthy&The right Kan extension of a { h along a { g. dWe can define a right Kan extension in several ways. The definition here is obtained by reading off k the definition in of a right Kan extension in terms of an End, but we can derive an equivalent definition  from the universal property. Given a {  h : C -> D and a {  g : C -> C', we want to find extend h back along g  to give  Ran g h : C' -> C', such that the natural transformation 1 :: Ran g h (g a) -> h a exists. ;In some sense this is trying to approximate the inverse of g by using one of N its adjoints, because if the adjoint and the inverse both exist, they match!   Hask -h-> Hask  | +  g /  | Ran g h  v /  Hask -' `The Right Kan extension is unique (up to isomorphism) by taking this as its universal property. That is to say given any K : C' -> C1 such that we have a natural transformation from k.g to h  (forall x. k (g x) -> h x)6 there exists a canonical natural transformation from k to Ran g h.  (forall x. k x -> Ran g h x). BWe could literally read this off as a valid Rank-3 definition for &:    data Ran' g h a = forall z. { z => Ran'" (forall x. z (g x) -> h x) (z a) ]This definition is isomorphic the simpler Rank-2 definition we use below as witnessed by the    ranIso1 :: Ran g f x -> Ran' g f x  ranIso1 (Ran e) = Ran' e id  ranIso2 :: Ran' g f x -> Ran g f x  ranIso2 (Ran' h z) = Ran $ k -> h (k  $ z)   . ranIso2 (ranIso1 (Ran e)) "a -- by definition  ranIso2 (Ran' e id) "a -- by definition  Ran $ k -> e (k  $ id) -- by definition  Ran $ k" -> e (k . id) -- f . id = f  Ran $ k% -> e k -- eta reduction  Ran e ;The other direction is left as an exercise for the reader. )1The universal property of a right Kan extension. *) and ** witness a higher kinded adjunction. from ( `'Compose'` g) to & g   ) . * "a ~  * . ) "a ~ +   + . , "a ~  , . + "a ~ -   - . . "a ~  . . - "a ~ /   0 . / "a ~  / . 0 "a ~ 1GThis is the natural transformation that defines a Right Kan extension. &'()*+,-./012345&'()*+,-./012345&'()*1+,-.0/2354&'()*+,-./012345MPTCs, fundeps provisionalEdward Kmett <ekmett@gmail.com> Trustworthy;Yoneda f is the right Kan extension of f along the | functor.   ; . < "a ~  < . ; "a ~ =Yoneda f is the right Kan lift of f along the | functor.   = . > "a ~  > . = "a ~ 16789:;<=>?@AB 6789:;<=>?@AB 6789:?@AB;<=>/6789:;<=>?@AB"non-portable (rank-2 polymorphism) provisionalEdward Kmett <ekmett@gmail.com> TrustworthyCC f: is the Monad generated by taking the right Kan extension  of any { f along itself (Ran f f). This can often be more " efficient" to construct than f itself using  repeated applications of (>>=). See "7Asymptotic Improvement of Computations over Free Monads" by Janis 4 Voightlnder for more information about this type.  (http://www.iai.uni-bonn.de/~jv/mpc08.pdf F2This serves as the *left*-inverse (retraction) of .    'lowerCodensity . lift' "a ~ GIn general this is not a full 2-sided inverse, merely a retraction, as  C m is often considerably larger than m. e.g. C0 ((->) s)) a ~ forall r. (a -> s -> r) -> s -> r $ could support a full complement of  s actions, while (->) s  is limited to  s actions. GThe C/ monad of a right adjoint is isomorphic to the  monad obtained from the .   G . H "a ~  H . G "a ~ IThe C monad of a representable { is isomorphic to the  monad obtained from the  for which that { is the right  adjoint.    I . J "a ~  J . I "a ~    codensityToComposedRep = 4 . K J   J = L . 5 KThe C } of a { g is the right Kan extension (&)  of g along itself.   K . L "a ~  L . K "a ~ MGRight associate all binds in a computation that generates a free monad KThis can improve the asymptotic efficiency of the result, while preserving  semantics. See "7Asymptotic Improvement of Computations over Free Monads" by Janis : Voightlnder for more information about this combinator.  (http://www.iai.uni-bonn.de/~jv/mpc08.pdf CDEFGHIJKLM CDEFGHIJKLM CDEFGHKLIJMCDEFGHIJKLM"non-portable (rank-2 polymorphism) provisionalEdward Kmett <ekmett@gmail.com> TrustworthyN   N w m a ~   w m a  Q w a ~   w | a NOPQRSTUVWXYZ[\]^_NOPQRSTUVWXYZ[\]^_QRSNOPTUVWXYZ[\]^_NOPQRSTUVWXYZ[\]^_  rank 2 types experimentalEdward Kmett <ekmett@gmail.com> Trustworthy`The left Kan extension of a { h along a { g. b0The universal property of a left Kan extension. cc and b. witness a (higher kinded) adjunction between ` g and (Compose g)   b . c "a ~  c . b "a ~ d   d . e "a ~  e . d "a ~ ff and g) witness the natural isomorphism between Lan f h and  Compose h g given f -| g   g . f "a ~  f . g "a ~ hh and i& witness the natural isomorphism from Lan f (Lan g h) and Lan (f o g) h   h . i "a ~  i . h "a ~ jFThis is the natural transformation that defines a Left Kan extension. `abcdefghij `abcdefghij `abcjhidegf `abcdefghij GADTs, MPTCs, fundeps provisionalEdward Kmett <ekmett@gmail.com> Trustworthyk%A form suitable for Yoneda reduction mYoneda f is the left Kan extension of f along the | functor.   m . n "a ~  n . m "a ~ oYoneda f is the left Kan lift of f along the | functor.   o . p "a ~  p . o "a ~ qYoneda  expansion    q . r "a ~  r . q "a ~     = q rYoneda reduction    = s = r sYoneda reduction given a }.    = s = r +klmnopqrs klmnopqrs klqrsmnop*klmnopqrs non-portable (GADTs, MPTCs) experimentalEdward Kmett <ekmett@gmail.com> Trustworthyv"The natural transformation from a  w to the  generated by w (forwards). ,This is merely a right-inverse (section) of , rather than a full inverse.    . v "a ~ w The Density ( of a left adjoint is isomorphic to the  formed by that . !This isomorphism is witnessed by w and x.   w . x "a ~  x . w "a ~ yThe t  of a { f. is obtained by taking the left Kan extension  (`) of f0 along itself. This isomorphism is witnessed by y and z   y . z "a ~  z . y "a ~  tuvwxyztuvwxyztuvwxzy tuvwxyz !"#$%&'())*+)),*+--./0123456789:;)),*+<=>?@ABCDDEFGHIJKLM  NOPQRSTUVWXYZ[\] ^ ^ _ ` a b c d e f g ) ) h i j k * + l m m n o p q rstuvwxstystz{|}~v  kan-extensions-3.6.2Data.Functor.Kan.RiftData.Functor.Kan.Lift+Data.Functor.Contravariant.Yoneda.Reduction!Data.Functor.Contravariant.YonedaData.Functor.Kan.RanData.Functor.YonedaControl.Monad.CodensityControl.Monad.CoData.Functor.Kan.LanData.Functor.Yoneda.ReductionControl.Comonad.DensityCoTData.Functor.KanLiftRiftrunRiftrapgrifttoRiftfromRift adjointToRift riftToAdjoint composeRift decomposeRiftriftToComposedAdjointcomposedAdjointToRiftLiftrunLiftglifttoLiftfromLift composeLift decomposeLift adjointToLift liftToAdjoint repToLift liftToRepliftToComposedAdjointcomposedAdjointToLiftliftToComposedRepcomposedRepToLiftYoneda liftYoneda lowerYoneda runYonedaRanrunRantoRanfromRan composeRan decomposeRan adjointToRan ranToAdjointranToComposedAdjointcomposedAdjointToRangranrepToRanranToRepranToComposedRepcomposedRepToRan yonedaToRan ranToYoneda yonedaToRift riftToYonedamaxFminFmaxMminM Codensity runCodensitylowerCodensitycodensityToAdjunctionadjunctionToCodensitycodensityToComposedRepcomposedRepToCodensitycodensityToRanranToCodensityimproverunCoTCocorunColiftCoT0 lowerCoT0lowerCo0liftCoT1 lowerCoT1lowerCo1posWpeekWpeeksWaskWasksWtraceWLantoLanfromLan adjointToLan lanToAdjointlanToComposedAdjointcomposedAdjointToLan composeLan decomposeLanglan yonedaToLan lanToYoneda yonedaToLift liftToYonedalowerMDensity liftDensitydensityToAdjunctionadjunctionToDensity lanToDensity densityToLanbaseGHC.BaseFunctortransformers-0.3.0.0Data.Functor.IdentityIdentityMonadid$fApplicativeRift $fPointedRift $fFunctorRift$fCopointedLift $fFunctorLiftcontravariant-0.4.3Data.Functor.Contravariant Contravariant$fAdjunctionYonedaYoneda$fRepresentableYoneda$fCoindexedYoneda$fValuedYoneda$fContravariantYoneda $fFunctorRan$fComonadTransYoneda$fComonadYoneda$fExtendYoneda$fMonadFreefYoneda$fMonadTransYoneda$fMonadPlusYoneda$fMonadFixYoneda $fMonadYoneda $fBindYoneda$fAlternativeYoneda $fPlusYoneda $fAltYoneda $fOrdYoneda $fEqYoneda $fReadYoneda $fShowYoneda$fLookupYoneda$fIndexableYoneda$fDistributiveYoneda$fTraversableWithKey1Yoneda$fTraversable1Yoneda$fTraversableWithKeyYoneda$fTraversableYoneda$fFoldableWithKey1Yoneda$fFoldableWithKeyYoneda$fFoldable1Yoneda$fFoldableYoneda$fZipWithKeyYoneda $fZipYoneda$fApplicativeYoneda $fApplyYoneda $fKeyedYoneda$fFunctorYoneda$fMonadSpecYonedaControl.Monad.Trans.Classlift mtl-2.1.2Control.Monad.State.Class MonadStateControl.Monad.Reader.Class MonadReaderadjunctions-3.2.1Data.Functor.Adjunction Adjunction$fMonadStaterCodensity$fMonadFreefCodensity$fMonadPlusCodensity$fAlternativeCodensity$fPlusCodensity$fAltCodensity$fMonadTransCodensity$fMonadIOCodensity$fMonadCodensity$fApplicativeCodensity$fApplyCodensity$fFunctorCodensity$fMonadSpecCodensity$fMonadErroreCoT$fMonadWritereCoT$fMonadStatesCoT$fMonadReadereCoT $fMonadIOCoT$fMonadTransCoT $fMonadCoT$fApplicativeCoT $fBindCoT $fApplyCoT $fFunctorCoT$fMonadSpecCoT$fApplicativeLan $fApplyLan $fFunctorLancomonad-transformers-3.0.4Control.Comonad.Trans.Classlower comonad-3.1Control.ComonadComonad$fApplicativeDensity$fApplyDensity$fComonadTransDensity$fComonadDensity$fExtendDensity$fFunctorDensity