!"#$%&'()*+,-./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 { | } ~  2013 Edward Kmett and Dan DoelBSDEdward Kmett <ekmett@gmail.com> experimental rank N types Trustworthy!"HM  g .  g f => feThis 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) DWe 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  UriftIso2 :: Rift g f a -> UniversalRift g f a riftIso2 (Rift e) = UniversalRift e id  HriftIso1 (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) 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.  m can be a  for any  m, as it is isomorphic to Yoneda m.3Indexed 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.      2013 Edward Kmett and Dan DoelBSDEdward Kmett <ekmett@gmail.com> experimental rank N types Trustworthy!"HM  Hf => g . Lift g f (forall z. f => g . z) -> Lift g f => z -- couniversalUHere 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      (C) 2014 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalportableNone +:=HKM .The Day convolution of two covariant functors.Day f g a -> h a is isomorphic to f a -> Rift g h aConstruct the Day convolution _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 > convolution on the cartesian monoidal structure is symmetric.  f  " = "   f # is the unit of  convolution #  % =  %  # =  $ is the unit of  convolution $  & =  &  $ =  % is the unit of  convolution #  % =  %  # =  & is the unit of  convolution $  & =  &  $ =  ' Collapse via a monoidal functor. ' ( f g) = f  g (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 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGADTs, TFs, MPTCs Trustworthy !"6=K*A 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) 2013 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGADTs, TFs, MPTCs Trustworthy !"6=HKM.Yoneda embedding for a presheaf1 1 . 2 "a  2 . 1 "a  ./012./012./012./012=(C) 2013-2014 Edward Kmett, Gershom Bazerman and Derek Elkins BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalportable Trustworthy +:=HKM 32The Day convolution of two contravariant functors.5Construct the Day convolution < (5 f g) = f = (5 f g) = g 6>Break apart the Day convolution of two contravariant functors.7_Day convolution provides a monoidal product. The associativity of this monoid is witnessed by 7 and 8. 7 . 8 =  8 . 7 =   f  7 = 7   f 8_Day convolution provides a monoidal product. The associativity of this monoid is witnessed by 7 and 8. 7 . 8 =  8 . 7 =   f  8 = 8   f 9The monoid for Day convolution  in Haskell is symmetric.  f  9 = 9   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. <  : =  < =   6  f  < = <   f =}In Haskell we can do general purpose elimination, but in a more general setting it is only possible to eliminate the unit.  =  ; =  = =   6  f  = = =   f > Diagonalize the Day convolution: <  > =  =  > =  6  > = 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 3456789:;<=>?@3456789:;<=>?@3456789:;<=>?@3456789:;<=>?@2008-2013 Edward KmettBSDEdward Kmett <ekmett@gmail.com> experimental rank 2 types Trustworthy!"HMAThe 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 find extend h back along g to give Ran g h : C' -> C', such that the natural transformation L :: 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 A: 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.D0The universal property of a right Kan extension.ED and E* witness a higher kinded adjunction. from (`'Compose'` g) to A g D . E "a  E . D "a  F F . G "a  G . F "a  H H . I "a  I . H "a  J K . J "a  J . K "a  LFThis is the natural transformation that defines a Right Kan extension.ABCDEFGHIJKLMNOPABCDEFGHIJKLMNOPABCDELFGHIKJMNPOABCDEFGHIJKLMNOP(C) 2011-2013 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalMPTCs, fundeps Trustworthy 2346=HKMQ Yoneda f a- can be viewed as the partial application of  to its second argument.T The natural isomorphism between f and Q f, given by the Yoneda lemma is witnessed by T and U T . U "a  U . T "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  = T VYoneda f- can be viewed as the right Kan extension of f along the  functor. V . W "a  W . V "a  XYoneda f( can be viewed as the right Kan lift of f along the  functor. X . Y "a  Y . X "a  'QRSTUVWXYZ[\] QRSTUVWXYZ[\] QRSTUZ[\]VWXY%QRSTUVWXYZ[\] (C) 2008-2013 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisional"non-portable (rank-2 polymorphism) Trustworthy+246HM^^ 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 (>>=).zSee "Asymptotic Improvement of Computations over Free Monads" by Janis Voightlnder for more information about this type. (http://www.iai.uni-bonn.de/~jv/mpc08.pdfa2This serves as the *left*-inverse (retraction) of . a .  "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.bThe ^H monad of a right adjoint is isomorphic to the monad obtained from the . b . c "a  c . b "a  dThe ^ monad of a representable / is isomorphic to the monad obtained from the  for which that  is the right adjoint. d . e "a  e . d "a  codensityToComposedRep = O . f e e = g . P fThe ^  of a  g is the right Kan extension (A) of g along itself. f . g "a  g . f "a  hFRight 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^_`abcdefgh ^_`abcdefgh ^_`abcfgdeh^_`abcdefgh 2008-2013 Edward KmettBSDEdward Kmett <ekmett@gmail.com> experimental rank 2 types Trustworthy!"HMiThe left Kan extension of a  h along a  g.k/The universal property of a left Kan extension.ll and k. witness a (higher kinded) adjunction between i g and (Compose g) k . l "a  l . k "a  m m . n "a  n . m "a  oo and p) witness the natural isomorphism between Lan f h and  Compose h g given f -| g p . o "a  o . p "a  qq and r& witness the natural isomorphism from Lan f (Lan g h) and Lan (f o g) h q . r "a  r . q "a  sEThis is the natural transformation that defines a Left Kan extension.ijklmnopqrs ijklmnopqrs ijklsqrmnpo ijklmnopqrs (C) 2011-2013 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGADTs, MPTCs, fundeps Trustworthy !"36=Kt A covariant  suitable for Yoneda reductionv Coyoneda f is the left Kan extension of f along the  functor. v . w "a  w . v "a  xt f is the left Kan lift of f along the  functor. x . y "a  y . x "a  zYoneda "expansion" z . { "a  { . z "a   lowerCoyoneda (liftCoyoneda fa) = -- by definition lowerCoyoneda (Coyoneda id fa) = -- by definition fmap id fa = -- functor law fa  = z {>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 t as just the arguments to  tupled up.  = | = { |Yoneda reduction given a . lets us walk under the existential and apply . You can view t as just the arguments to  tupled up.  = | = { "tuvwxyz{| tuvwxyz{| tuz{|vwxy!tuvwxyz{| (C) 2008-2011 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> experimentalnon-portable (GADTs, MPTCs) Trustworthy!"6"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 (i) of f0 along itself. This isomorphism is witnessed by  and   .  "a   .  "a  }~}~}~ }~ (C) 2011 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisional"non-portable (rank-2 polymorphism) Trustworthy2346HM  w a ~  w  a !           !"#$%&'()**+,-./012345667899:;<**+=,-./0>?@45AABCDEFGHIJKLMNO99:;<PQRSTUVW X X Y Z [ \ ] ^ _ ` a b b c d e f g h i j k 6 6 l m n o 7 8 p q q r s t u v w w x y z { | } ~                  kan-extensions-4.2Data.Functor.Kan.RiftData.Functor.Kan.LiftData.Functor.Day#Data.Functor.Contravariant.Coyoneda!Data.Functor.Contravariant.YonedaData.Functor.Contravariant.DayData.Functor.Kan.RanData.Functor.YonedaControl.Monad.CodensityData.Functor.Kan.LanData.Functor.CoyonedaControl.Comonad.DensityControl.Monad.CoData.Functor.KanLiftRiftrunRiftrapgrifttoRiftfromRift adjointToRift riftToAdjoint composeRift decomposeRiftriftToComposedAdjointcomposedAdjointToRiftLiftrunLiftglifttoLiftfromLift composeLift decomposeLift adjointToLift liftToAdjoint repToLift liftToRepliftToComposedAdjointcomposedAdjointToLiftliftToComposedRepcomposedRepToLiftDaydayassocdisassocswappedintro1intro2elim1elim2daptrans1trans2Coyoneda liftCoyoneda lowerCoyonedaYoneda runYoneda liftYoneda lowerYonedarunDayday1day2diagRanrunRantoRanfromRan composeRan decomposeRan adjointToRan ranToAdjointranToComposedAdjointcomposedAdjointToRangranrepToRanranToRepranToComposedRepcomposedRepToRan yonedaToRan ranToYoneda yonedaToRift riftToYonedamaxFminFmaxMminM Codensity runCodensitylowerCodensitycodensityToAdjunctionadjunctionToCodensitycodensityToComposedRepcomposedRepToCodensitycodensityToRanranToCodensityimproveLantoLanfromLan adjointToLan lanToAdjointlanToComposedAdjointcomposedAdjointToLan composeLan decomposeLanglan coyonedaToLan lanToCoyonedacoyonedaToLiftliftToCoyonedalowerMDensity liftDensitydensityToAdjunctionadjunctionToDensity lanToDensity densityToLanCoTrunCoTCocorunColiftCoT0 lowerCoT0lowerCo0liftCoT1 lowerCoT1lowerCo1posWpeekWpeeksWaskWasksWtraceW liftCoT0M liftCoT1MditerdctrlMbaseGHC.BaseFunctortransformers-0.3.0.0Data.Functor.IdentityIdentityMonadid$fApplicativeRift $fFunctorRift $fFunctorLiftfmap.Control.Applicative<*>$fRepresentableDay$fDistributiveDay$fApplicativeDay $fFunctorDaycontravariant-1.2Data.Functor.Contravariant Contravariant$fAdjunctionCoyonedaCoyoneda$fRepresentableCoyoneda$fContravariantCoyoneda$fAdjunctionYonedaYoneda$fRepresentableYoneda$fContravariantYoneda contramap Data.Tuplefstsnd$fContravariantDay $fFunctorRanControl.Monad.Trans.Classlift$fComonadTransYoneda$fComonadYoneda$fExtendYoneda$fMonadFreefYoneda$fMonadTransYoneda$fMonadPlusYoneda$fMonadFixYoneda $fMonadYoneda $fBindYoneda$fAlternativeYoneda $fPlusYoneda $fAltYoneda $fOrdYoneda $fEqYoneda $fReadYoneda $fShowYoneda$fDistributiveYoneda$fTraversable1Yoneda$fTraversableYoneda$fFoldable1Yoneda$fFoldableYoneda$fApplicativeYoneda $fApplyYoneda$fFunctorYoneda mtl-2.1.3.1Control.Monad.State.Class MonadStateControl.Monad.Reader.Class MonadReaderadjunctions-4.2Data.Functor.Adjunction Adjunction$fMonadReaderrCodensity$fMonadStaterCodensity$fMonadFreefCodensity$fMonadPlusCodensity$fAlternativeCodensity$fPlusCodensity$fAltCodensity$fMonadTransCodensity$fMonadIOCodensity$fMonadCodensity$fApplicativeCodensity$fApplyCodensity$fFunctorCodensity$fApplicativeLan $fApplyLan $fFunctorLan comonad-4.2.2Control.Comonad.Trans.Classlower Control.MonadliftM $fOrdCoyoneda $fEqCoyoneda$fReadCoyoneda$fShowCoyoneda$fDistributiveCoyoneda$fTraversable1Coyoneda$fTraversableCoyoneda$fFoldable1Coyoneda$fFoldableCoyoneda$fComonadTransCoyoneda$fComonadCoyoneda$fExtendCoyoneda$fMonadPlusCoyoneda$fMonadFixCoyoneda$fMonadTransCoyoneda$fMonadCoyoneda$fBindCoyoneda$fPlusCoyoneda $fAltCoyoneda$fAlternativeCoyoneda$fApplicativeCoyoneda$fApplyCoyoneda$fFunctorCoyonedaControl.ComonadComonad$fApplicativeDensity$fApplyDensity$fComonadTransDensity$fComonadDensity$fExtendDensity$fFunctorDensity$fMonadErroreCoT$fMonadWritereCoT$fMonadStatesCoT$fMonadReadereCoT $fMonadIOCoT$fMonadTransCoT $fMonadCoT$fApplicativeCoT $fBindCoT $fApplyCoT $fFunctorCoT