!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ 2008-2016 Edward KmettBSDEdward Kmett <ekmett@gmail.com> experimental rank 2 types Trustworthy%&OTThe right Kan extension of a  h along a  g.We can define a right Kan extension in several ways. The definition here is obtained by reading off 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 extend h back along g to give Ran g h : C' -> C', such that the natural transformation   :: Ran g h (g a) -> h a exists.;In some sense this is trying to approximate the inverse of g^ by using one of its adjoints, because if the adjoint and the inverse both exist, they match! EHask -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  PranIso2 :: 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.0The universal property of a right Kan extension. and * witness a higher kinded adjunction. from (`Compose' g) to  g  .  "a   .  "a    .  "a   .  "a    .  "a   .  "a    .   "a    .   "a  FThis is the natural transformation that defines a Right Kan extension.     (C) 2011-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalMPTCs, fundeps Trustworthy 9:;<=DORT Yoneda f a- can be viewed as the partial application of  to its second argument. The natural isomorphism between f and  f, given by the Yoneda lemma is witnessed by  and   .  "a   .  "a   lowerYoneda (liftYoneda fa) = -- definition lowerYoneda (Yoneda (f -> fmap f a)) -- definition (f -> fmap f fa) id -- beta reduction fmap id fa -- functor law fa  =  Yoneda f- can be viewed as the right Kan extension of f along the  functor.  .  "a   .  "a  % !"#$%&'()*+,-./012345  # !"#$%&'()*+,-./0123452008-2016 Edward KmettBSDEdward Kmett <ekmett@gmail.com> experimental rank 2 typesSafe%&OT6The left Kan extension of a  h along a  g.8/The universal property of a left Kan extension.99 and 8. witness a (higher kinded) adjunction between 6 g and (Compose g) 8 . 9 "a  9 . 8 "a  : : . ; "a  ; . : "a  << and =) witness the natural isomorphism between Lan f h and  Compose h g given f -| g = . < "a  < . = "a  >> and ?& witness the natural isomorphism from Lan f (Lan g h) and Lan (f o g) h > . ? "a  ? . > "a  @EThis is the natural transformation that defines a Left Kan extension.6789:;<=>?@ABC 6789:;<=>?@ 6789@>?:;=< 6789:;<=>?@ABC(C) 2014-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalportableNone 0ADORT D.The Day convolution of two covariant functors.Day f g a -> h a is isomorphic to f a -> Rift g h aFConstruct the Day convolutionG_Day convolution provides a monoidal product. The associativity of this monoid is witnessed by G and H. G . H =  H . G =   f  G = G   f H_Day convolution provides a monoidal product. The associativity of this monoid is witnessed by G and H. G . H =  H . G =   f  H = H   f IThe monoid for D> convolution on the cartesian monoidal structure is symmetric.  f  I = I   f J is the unit of D convolution J  L =  L  J =  K is the unit of D convolution K  M =  M  K =  L is the unit of D convolution J  L =  L  J =  M is the unit of D convolution K  M =  M  K =  N Collapse via a monoidal functor. N (F f g) = f  g OJApply a natural transformation to the left-hand side of a Day convolution.HThis respects the naturality of the natural transformation you supplied:  f  O fg = O fg   f PKApply a natural transformation to the right-hand side of a Day convolution.HThis respects the naturality of the natural transformation you supplied:  f  P fg = P fg   f DEFGHIJKLMNOPQRSTUVW DEFGHIJKLMNOP DEFNGHIJKLMOPDEFGHIJKLMNOPQRSTUVW#2013-2016 Edward Kmett and Dan DoelBSDEdward Kmett <ekmett@gmail.com> experimental rank N typesNone%&OT [ The natural isomorphism between f and  Curried f f.  \  [ "a  [  \ "a  \ ([ x) -- definition \ (X ( x)) -- definition ( x) ( ) -- beta reduction   . x -- Applicative identity law x \Lower X by applying   to the continuation.See [.]3Indexed applicative composition of right Kan lifts.^This is the counit of the Day f -| Curried f adjunction_This is the unit of the Day f -| Curried f adjunction`The universal property of Xa ` . a "a  a . ` "a  bCurried f Identity a' is isomorphic to the right adjoint to f if one exists. b . c "a  c . b "a  cCurried f Identity a' is isomorphic to the right adjoint to f if one exists.d Curried f h a? is isomorphic to the post-composition of the right adjoint of f onto h if such a right adjoint exists. d . e "a  e . d "a  e Curried f h a? is isomorphic to the post-composition of the right adjoint of f onto h if such a right adjoint exists.XYZ[\]^_`abcdefgXYZ[\]^_`abcdeXYZ`a^_bced[\]XYZ[\]^_`abcdefg(C) 2011-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGADTs, MPTCs, fundeps Trustworthy %&:<=DORTh A covariant  suitable for Yoneda reductionj Coyoneda f is the left Kan extension of f along the  functor. Coyoneda f is always a functor, even if f) is not. In this case, it is called the free functor over f1. Note the following categorical fine print: If f is not a functor,  Coyoneda f, is actually not the left Kan extension of f along the L functor, but along the inclusion functor from the discrete subcategory of HaskK which contains only identity functions as morphisms to the full category Hask. (This is because f, not being a proper functor, can only be interpreted as a categorical functor by restricting the source category to only contain identities.) j . k "a  k . j "a  lYoneda "expansion" l . m "a  m . l "a   lowerCoyoneda (liftCoyoneda fa) = -- by definition lowerCoyoneda (Coyoneda id fa) = -- by definition fmap id fa = -- functor law fa  = l m>Yoneda reduction lets us walk under the existential and apply .NMnemonically, "Yoneda reduction" sounds like and works a bit like -reduction. -http://ncatlab.org/nlab/show/Yoneda+reduction You can view h as just the arguments to  tupled up.  = n = m nYoneda reduction given a . lets us walk under the existential and apply . You can view h as just the arguments to  tupled up.  = n = m o#Lift a natural transformation from f to g# to a natural transformation from  Coyoneda f to  Coyoneda g.!hijklmnopqrstuvwxyz{|}~hijklmnohilmnojk hijklmnopqrstuvwxyz{|}~(C) 2013-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGADTs, TFs, MPTCs Trustworthy %&<=DORTYoneda embedding for a presheaf  .  "a   .  "a  =(C) 2013-2016 Edward Kmett, Gershom Bazerman and Derek Elkins BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalportableNone 0ADORT 2The Day convolution of two contravariant functors.Construct the Day convolution  ( f g) = f  ( f g) = g >Break apart the Day convolution of two contravariant functors._Day convolution provides a monoidal product. The associativity of this monoid is witnessed by  and .  .  =   .  =   f   =    f _Day convolution provides a monoidal product. The associativity of this monoid is witnessed by  and .  .  =   .  =   f   =    f The monoid for Day convolution  in Haskell is symmetric.  f   =    f ,Proxy serves as the unit of Day convolution.    =   f   =    f ,Proxy serves as the unit of Day convolution.    =   f   =    f {In Haskell we can do general purpose elimination, but in a more general setting it is only possible to eliminate the unit.    =   =     f   =    f }In Haskell we can do general purpose elimination, but in a more general setting it is only possible to eliminate the unit.     =   =     f   =    f  Diagonalize the Day convolution:    =     =     = a -> (a,a)  f .  =  .  f JApply a natural transformation to the left-hand side of a Day convolution.HThis respects the naturality of the natural transformation you supplied:  f   fg =  fg   f KApply a natural transformation to the right-hand side of a Day convolution.HThis respects the naturality of the natural transformation you supplied:  f   fg =  fg   f  (C) 2013-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGADTs, TFs, MPTCs Trustworthy %&<=DRA 6 functor (aka presheaf) suitable for Yoneda reduction. -http://ncatlab.org/nlab/show/Yoneda+reduction"Coyoneda "expansion" of a presheaf  .  "a   .  "a   Coyoneda reduction on a presheaf (C) 2008-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisional"non-portable (rank-2 polymorphism) Trustworthy 09;<=OT fB is the Monad generated by taking the right Kan extension of any  f along itself (Ran f f).5This can often be more "efficient" to construct than f( itself using repeated applications of (>>=).ySee "Asymptotic Improvement of Computations over Free Monads" by Janis Voigtlnder for more information about this type. (http://www.iai.uni-bonn.de/~jv/mpc08.pdf2This serves as the *left*-inverse (retraction) of .  .  "a  HIn general this is not a full 2-sided inverse, merely a retraction, as  m% is often considerably "larger" than m.e.g. 0 ((->) s)) a ~ forall r. (a -> s -> r) -> s -> r% could support a full complement of  s actions, while (->) s is limited to  s actions.The H monad of a right adjoint is isomorphic to the monad obtained from the .  .  "a   .  "a  The  monad of a representable / is isomorphic to the monad obtained from the  for which that  is the right adjoint.  .  "a   .  "a  codensityToComposedRep =  .   =  .  The   of a  g is the right Kan extension () of g along itself.  .  "a   .  "a  FRight associate all binds in a computation that generates a free monadVThis can improve the asymptotic efficiency of the result, while preserving semantics.See "Asymptotic Improvement of Computations over Free Monads" by Janis Voightlnder for more information about this combinator. (http://www.iai.uni-bonn.de/~jv/mpc08.pdf  (C) 2008-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> experimentalnon-portable (GADTs, MPTCs)Safe%&<="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.  .  "a   The Density ( of a left adjoint is isomorphic to the  formed by that .!This isomorphism is witnessed by  and .  .  "a   .  "a  The   of a  f0 is obtained by taking the left Kan extension (6) of f0 along itself. This isomorphism is witnessed by  and   .  "a   .  "a    (C) 2011-2016 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisional"non-portable (rank-2 polymorphism)Safe 9:;<=OT  w a ~   w  a "  !"#$%&'()*+,-./0123456789:;<=>?@ABCCDEFGHIJKLMNOPPQRSTUVWXYZ[\]^_`abccdefghijklmnopqrrstuvwxyz{|}~ !"9:PPQRSTUVZ[_ r r u v y        +kan-extensions-5.0.2-GGmHfRO2chK96u2KOmRqoVData.Functor.Kan.RanData.Functor.YonedaData.Functor.Kan.LanData.Functor.DayData.Functor.Day.CurriedData.Functor.Coyoneda!Data.Functor.Contravariant.YonedaData.Functor.Contravariant.Day#Data.Functor.Contravariant.CoyonedaControl.Monad.CodensityControl.Comonad.DensityControl.Monad.CoData.Functor.Kan.RiftRiftRanrunRantoRanfromRan composeRan decomposeRan adjointToRan ranToAdjointranToComposedAdjointcomposedAdjointToRangranrepToRanranToRepranToComposedRepcomposedRepToRan $fFunctorRanYoneda runYoneda liftYoneda lowerYoneda yonedaToRan ranToYonedamaxFminFmaxMminM$fComonadTransYoneda$fComonadYoneda$fExtendYoneda$fMonadFreefYoneda$fMonadTransYoneda$fMonadPlusYoneda$fMonadFixYoneda $fMonadYoneda $fBindYoneda$fAlternativeYoneda $fPlusYoneda $fAltYoneda $fOrdYoneda $fEqYoneda $fReadYoneda $fShowYoneda$fAdjunctionYonedaYoneda$fRepresentableYoneda$fDistributiveYoneda$fTraversable1Yoneda$fTraversableYoneda$fFoldable1Yoneda$fFoldableYoneda$fApplicativeYoneda $fApplyYoneda$fFunctorYonedaLantoLanfromLan adjointToLan lanToAdjointlanToComposedAdjointcomposedAdjointToLan composeLan decomposeLanglan$fApplicativeLan $fApplyLan $fFunctorLanDaydayassocdisassocswappedintro1intro2elim1elim2daptrans1trans2$fComonadTransDay$fComonadApplyDay $fComonadDay$fRepresentableDay$fDistributiveDay$fApplicativeDay $fFunctorDayCurried runCurried liftCurried lowerCurriedrapapplied unapplied toCurried fromCurriedadjointToCurriedcurriedToAdjointcurriedToComposedAdjointcomposedAdjointToCurried$fApplicativeCurried$fFunctorCurriedCoyoneda coyonedaToLan lanToCoyoneda liftCoyoneda lowerCoyonedalowerM hoistCoyoneda$fAdjunctionCoyonedaCoyoneda $fOrdCoyoneda $fEqCoyoneda$fReadCoyoneda$fShowCoyoneda$fDistributiveCoyoneda$fTraversable1Coyoneda$fTraversableCoyoneda$fFoldable1Coyoneda$fFoldableCoyoneda$fComonadTransCoyoneda$fComonadCoyoneda$fExtendCoyoneda$fRepresentableCoyoneda$fMonadPlusCoyoneda$fMonadFixCoyoneda$fMonadTransCoyoneda$fMonadCoyoneda$fBindCoyoneda$fPlusCoyoneda $fAltCoyoneda$fAlternativeCoyoneda$fApplicativeCoyoneda$fApplyCoyoneda$fFunctorCoyoneda$fContravariantYonedarunDayday1day2diag$fContravariantDay$fContravariantCoyoneda Codensity runCodensitylowerCodensitycodensityToAdjunctionadjunctionToCodensitycodensityToComposedRepcomposedRepToCodensitycodensityToRanranToCodensityimprove$fMonadReaderrCodensity$fMonadStaterCodensity$fMonadFreefCodensity$fMonadPlusCodensity$fAlternativeCodensity$fPlusCodensity$fAltCodensity$fMonadTransCodensity$fMonadIOCodensity$fMonadFailCodensity$fMonadCodensity$fApplicativeCodensity$fApplyCodensity$fFunctorCodensityDensity liftDensitydensityToAdjunctionadjunctionToDensity lanToDensity densityToLan$fApplicativeDensity$fApplyDensity$fComonadTransDensity$fComonadDensity$fExtendDensity$fFunctorDensityCoTrunCoTCocorunColiftCoT0 lowerCoT0lowerCo0liftCoT1 lowerCoT1lowerCo1posWpeekWpeeksWaskWasksWtraceW liftCoT0M liftCoT1MditerdctrlM$fMonadErroreCoT$fMonadWritereCoT$fMonadStatesCoT$fMonadReadereCoT $fMonadIOCoT$fMonadTransCoT$fMonadFailCoT $fMonadCoT$fApplicativeCoT $fBindCoT $fApplyCoT $fFunctorCoTbaseGHC.BaseFunctoridfmaptransformers-0.5.2.0Control.Monad.Trans.ClassliftData.Functor.IdentityIdentity.<*>pure$comonad-5.0.1-FHedNTWD5OfFOXvt2xmF2uControl.Comonad.Trans.ClasslowerMonadliftM(contravariant-1.4-2ZEIQcIYz4Q4N5hzlLOWcgData.Functor.Contravariant contramap Data.Tuplefstsnd Contravariant mtl-2.2.1-BLKBelFsPB3BoFeSWSOYj6Control.Monad.State.Class MonadStateControl.Monad.Reader.Class MonadReader&adjunctions-4.3-9lUmUzx9pBEEnoHInNeXViData.Functor.Adjunction AdjunctionControl.ComonadComonad