Ԝ      !"#$%&'()*+,-./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 typesSafe!"IN  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. The natural isomorphism between f and Rift f f.     "a     "a   ( x) -- definition  ( ( x)) -- definition ( x) ( ) -- beta reduction   . x -- Applicative identity law x Lower  by applying   to the continuation.See .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!"IN  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 +;>ILN .The Day convolution of two covariant functors.Day f g a -> h a is isomorphic to f a -> Rift g h a!Construct 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 !"7>L,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 !"7>ILN0Yoneda embedding for a presheaf3 3 . 4 "a  4 . 3 "a  01234012340123401234=(C) 2013-2014 Edward Kmett, Gershom Bazerman and Derek Elkins BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalportableNone +;>ILN 52The Day convolution of two contravariant functors.7Construct the Day convolution > (7 f g) = f ? (7 f g) = g 8>Break apart the Day convolution of two contravariant functors.9_Day convolution provides a monoidal product. The associativity of this monoid is witnessed by 9 and :. 9 . : =  : . 9 =   f  9 = 9   f :_Day convolution provides a monoidal product. The associativity of this monoid is witnessed by 9 and :. 9 . : =  : . 9 =   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. >  < =  > =   8  f  > = >   f ?}In Haskell we can do general purpose elimination, but in a more general setting it is only possible to eliminate the unit.  ?  = =  ? =   8  f  ? = ?   f @ Diagonalize the Day convolution: >  @ =  ?  @ =  8  @ = a -> (a,a)  f . @ = @ .  f AJApply a natural transformation to the left-hand side of a Day convolution.HThis respects the naturality of the natural transformation you supplied:  f  A fg = A fg   f BKApply a natural transformation to the right-hand side of a Day convolution.HThis respects the naturality of the natural transformation you supplied:  f  B fg = B fg   f 56789:;<=>?@AB56789:;<=>?@AB56789:;<=>?@AB56789:;<=>?@AB2008-2013 Edward KmettBSDEdward Kmett <ekmett@gmail.com> experimental rank 2 types Trustworthy!"INCThe 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 N :: 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 C: 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.F0The universal property of a right Kan extension.GF and G* witness a higher kinded adjunction. from (`Compose' g) to C g F . G "a  G . F "a  H H . I "a  I . H "a  J J . K "a  K . J "a  L M . L "a  L . M "a  NFThis is the natural transformation that defines a Right Kan extension.CDEFGHIJKLMNOPQRCDEFGHIJKLMNOPQRCDEFGNHIJKMLOPRQCDEFGHIJKLMNOPQR(C) 2011-2013 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalMPTCs, fundeps Trustworthy 3457>ILNS Yoneda f a- can be viewed as the partial application of  to its second argument.V The natural isomorphism between f and S f, given by the Yoneda lemma is witnessed by V and W V . W "a  W . V "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  = V XYoneda f- can be viewed as the right Kan extension of f along the  functor. X . Y "a  Y . X "a  ZYoneda f( can be viewed as the right Kan lift of f along the  functor. Z . [ "a  [ . Z "a  'STUVWXYZ[\]^_ STUVWXYZ[\]^_ STUVW\]^_XYZ[%STUVWXYZ[\]^_ (C) 2008-2013 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisional"non-portable (rank-2 polymorphism) Trustworthy+357IN`` 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.pdfc2This serves as the *left*-inverse (retraction) of . c .  "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.dThe `H monad of a right adjoint is isomorphic to the monad obtained from the . d . e "a  e . d "a  fThe ` monad of a representable / is isomorphic to the monad obtained from the  for which that  is the right adjoint. f . g "a  g . f "a  codensityToComposedRep = Q . h g g = i . R hThe `  of a  g is the right Kan extension (C) of g along itself. h . i "a  i . h "a  jFRight 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`abcdefghij `abcdefghij `abcdehifgj`abcdefghij 2008-2013 Edward KmettBSDEdward Kmett <ekmett@gmail.com> experimental rank 2 typesSafe!"INkThe left Kan extension of a  h along a  g.m/The universal property of a left Kan extension.nn and m. witness a (higher kinded) adjunction between k g and (Compose g) m . n "a  n . m "a  o o . p "a  p . o "a  qq and r) witness the natural isomorphism between Lan f h and  Compose h g given f -| g r . q "a  q . r "a  ss and t& witness the natural isomorphism from Lan f (Lan g h) and Lan (f o g) h s . t "a  t . s "a  uEThis is the natural transformation that defines a Left Kan extension.klmnopqrstu klmnopqrstu klmnustoprq klmnopqrstu (C) 2011-2013 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> provisionalGADTs, MPTCs, fundeps Trustworthy !"47>Lv A covariant  suitable for Yoneda reductionx Coyoneda f is the left Kan extension of f along the  functor. x . y "a  y . x "a  zv f is the left Kan lift of f along the  functor. z . { "a  { . z "a  |Yoneda "expansion" | . } "a  } . | "a   lowerCoyoneda (liftCoyoneda fa) = -- by definition lowerCoyoneda (Coyoneda id fa) = -- by definition fmap id fa = -- functor law fa  = | }>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 v as just the arguments to  tupled up.  = ~ = } ~Yoneda reduction given a . lets us walk under the existential and apply . You can view v as just the arguments to  tupled up.  = ~ = } "vwxyz{|}~ vwxyz{|}~ vw|}~xyz{!vwxyz{|}~ (C) 2008-2011 Edward Kmett BSD-style (see the file LICENSE)Edward Kmett <ekmett@gmail.com> experimentalnon-portable (GADTs, MPTCs)Safe!"7"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 (k) 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)Safe3457IN  w a ~  w  a !           !"#$%&'()*+,,-./01234567889:;;<=>,,-?./012@AB67CCDEFGHIJKLMNOPQ;;<=>RSTUVWXY Z Z [ \ ] ^ _ ` a b c d d e f g h i j k l m 8 8 n o p q 9 : r s s t u v w x y y z { | } ~                   kanex_94TGhGHQDaB0dC8Ns9oJXMData.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.KanLiftRiftrunRiftliftRift lowerRiftrapgrifttoRiftfromRift 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.BaseFunctorData.Functor.IdentityIdentityMonad.id<*>pure$fApplicativeRift $fFunctorRift $fFunctorLiftfmap$fRepresentableDay$fDistributiveDay$fApplicativeDay $fFunctorDaycontr_54MoMHlCGxXCixOzAN2CJ9Data.Functor.Contravariant Contravariant$fAdjunctionCoyonedaCoyoneda$fRepresentableCoyoneda$fContravariantCoyoneda$fAdjunctionYonedaYoneda$fRepresentableYoneda$fContravariantYoneda contramap Data.Tuplefstsnd$fContravariantDay $fFunctorRantrans_3eG64VdP2vzGjP6wJiCp5XControl.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$fFunctorYonedamtl_KMpng31YRYc5JfMWFZ3FCUControl.Monad.State.Class MonadStateControl.Monad.Reader.Class MonadReaderadjun_FuD3GmxQzLCCQVJnYO01oEData.Functor.Adjunction Adjunction$fMonadReaderrCodensity$fMonadStaterCodensity$fMonadFreefCodensity$fMonadPlusCodensity$fAlternativeCodensity$fPlusCodensity$fAltCodensity$fMonadTransCodensity$fMonadIOCodensity$fMonadCodensity$fApplicativeCodensity$fApplyCodensity$fFunctorCodensity$fApplicativeLan $fApplyLan $fFunctorLancomon_9aQQ8aTwu27IsTtOtLO8yDControl.Comonad.Trans.ClasslowerliftM $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