kan-extensions 3.1.2 → 3.4

raw patch · 6 files changed

+338/−25 lines, 6 filesdep +pointeddep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: pointed

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +9/−0
• README.markdown +9/−1
• kan-extensions.cabal +7/−5
• src/Control/Monad/Co.hs +12/−2
• src/Data/Functor/KanExtension.hs +17/−17
• src/Data/Functor/KanLift.hs +284/−0

@@ -1,3 +1,12 @@+3.3+---+* Rift is now `Applicative`. Added `rap`.++3.2+---+* Added right and left Kan lifts under `Data.Functor.KanLift`.+* Decreased reliance on the `Composition` class where unnecessary in the API+ 3.1.2 ----- * Marked modules `Trustworthy` as required for `SafeHaskell` in the presence of these extensions.

@@ -3,7 +3,15 @@  [![Build Status](https://secure.travis-ci.org/ekmett/kan-extensions.png?branch=master)](http://travis-ci.org/ekmett/kan-extensions) -This package provides tools for working with left and right Kan extensions in Haskell.+This package provides tools for working with various Kan extensions and Kan lifts in Haskell.++Among the interesting bits included are:++* Right and left Kan extensions (`Ran` and `Lan`)+* Right and left Kan lifts (`Rift` and `Lift`)+* Both forms of the Yoneda lemma as Kan extensions (`Yoneda`)+* The `Codensity` monad, which can be used to improve the asymptotic complexity of code over free monads (`Codensity`, `Density`)+* A "comonad to monad-transformer transformer" that is a special case of a right Kan lift. (`CoT`, `Co`)  Contact Information -------------------

@@ -1,6 +1,6 @@ name:          kan-extensions category:      Data Structures, Monads, Comonads, Functors-version:       3.1.2+version:       3.4 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -9,12 +9,12 @@ stability:     provisional homepage:      http://github.com/ekmett/kan-extensions/ bug-reports:   http://github.com/ekmett/kan-extensions/issues-copyright:     Copyright (C) 2011-2012 Edward A. Kmett-synopsis:      Kan extensions, the Yoneda lemma, and (co)density (co)monads-description:   Kan extensions, the Yoneda lemma, and (co)density (co)monads+copyright:     Copyright (C) 2011-2013 Edward A. Kmett+synopsis:      Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads+description:   Kan extensions, Kan lifts, the Yoneda lemma, and (co)density (co)monads build-type:    Simple -extra-source-files: +extra-source-files:   .travis.yml   .gitignore   .ghci@@ -52,6 +52,7 @@     free                   >= 3       && < 4,     keys                   >= 3       && < 4,     mtl                    >= 2.0.1   && < 2.2,+    pointed                >= 3       && < 4,     representable-functors >= 3.0.0.1 && < 4,     semigroupoids          >= 3       && < 4,     speculation            >= 1.4.1   && < 2,@@ -62,6 +63,7 @@     Control.Monad.Co     Control.Monad.Codensity     Data.Functor.KanExtension+    Data.Functor.KanLift     Data.Functor.Yoneda     Data.Functor.Yoneda.Contravariant 

@@ -12,7 +12,6 @@ #endif ----------------------------------------------------------------------------- -- |--- Module      :  Control.Monad.Co -- Copyright   :  (C) 2011 Edward Kmett -- License     :  BSD-style (see the file LICENSE) --@@ -22,8 +21,14 @@ -- -- Monads from Comonads ----- http://comonad.com/reader/2011/monads-from-comonads/+-- <http://comonad.com/reader/2011/monads-from-comonads/> --+-- 'Co' and 'CoT' just special cases of the general notion of a+-- Right Kan lift.+--+-- TODO: We could consider unifying the definition of 'CoT' and 'Rift', but+-- 'Rift' f f also forms a Codensity-like 'Monad', so there is a reasonable+-- case for keeping them separate. ---------------------------------------------------------------------------- module Control.Monad.Co   (@@ -69,6 +74,11 @@ runCo :: Functor w => Co w a -> w (a -> r) -> r runCo m = runIdentity . runCoT m . fmap (fmap Identity) +-- |+-- @+-- 'CoT' w m a ~ 'Data.Functor.KanLift.Rift' w m a+-- 'Co' w a ~ 'Data.Functor.KanLift.Rift' w 'Identity' a+-- @ newtype CoT w m a = CoT { runCoT :: forall r. w (a -> m r) -> m r }  instance Functor w => Functor (CoT w m) where

@@ -26,13 +26,13 @@  instance Functor (Ran g h) where   fmap f m = Ran (\k -> runRan m (k . f))- + -- | 'toRan' and 'fromRan' witness a higher kinded adjunction. from @(`'Compose'` g)@ to @'Ran' g@-toRan :: (Composition compose, Functor k) => (forall a. compose k g a -> h a) -> k b -> Ran g h b-toRan s t = Ran (s . compose . flip fmap t)+toRan :: Functor k => (forall a. k (g a) -> h a) -> k b -> Ran g h b+toRan s t = Ran (s . flip fmap t) -fromRan :: Composition compose => (forall a. k a -> Ran g h a) -> compose k g b -> h b-fromRan s = flip runRan id . s . decompose+fromRan :: (forall a. k a -> Ran g h a) -> k (g b) -> h b+fromRan s = flip runRan id . s  composeRan :: Composition compose => Ran f (Ran g h) a -> Ran (compose f g) h a composeRan r = Ran (\f -> runRan (runRan r (decompose . f)) id)@@ -46,21 +46,21 @@ ranToAdjoint :: Adjunction f g => Ran g Identity a -> f a ranToAdjoint r = runIdentity (runRan r unit) -ranToComposedAdjoint :: (Composition compose, Adjunction f g) => Ran g h a -> compose h f a-ranToComposedAdjoint r = compose (runRan r unit)+ranToComposedAdjoint :: Adjunction f g => Ran g h a -> h (f a)+ranToComposedAdjoint r = runRan r unit -composedAdjointToRan :: (Composition compose, Adjunction f g, Functor h) => compose h f a -> Ran g h a-composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) (decompose f))+composedAdjointToRan :: (Adjunction f g, Functor h) => h (f a) -> Ran g h a+composedAdjointToRan f = Ran (\a -> fmap (rightAdjunct a) f)  data Lan g h a where   Lan :: (g b -> a) -> h b -> Lan g h a  -- 'fromLan' and 'toLan' witness a (higher kinded) adjunction between @'Lan' g@ and @(`Compose` g)@-toLan :: (Composition compose, Functor f) => (forall a. h a -> compose f g a) -> Lan g h b -> f b-toLan s (Lan f v) = fmap f . decompose $ s v+toLan :: Functor f => (forall a. h a -> f (g a)) -> Lan g h b -> f b+toLan s (Lan f v) = fmap f (s v) -fromLan :: (Composition compose) => (forall a. Lan g h a -> f a) -> h b -> compose f g b-fromLan s = compose . s . Lan id+fromLan :: (forall a. Lan g h a -> f a) -> h b -> f (g b)+fromLan s = s . Lan id  instance Functor (Lan f g) where   fmap f (Lan g h) = Lan (f . g) h@@ -81,11 +81,11 @@ lanToAdjoint (Lan f v) = leftAdjunct f (runIdentity v)  -- | 'lanToComposedAdjoint' and 'composedAdjointToLan' witness the natural isomorphism between @Lan f h@ and @Compose h g@ given @f -| g@-lanToComposedAdjoint :: (Composition compose, Functor h, Adjunction f g) => Lan f h a -> compose h g a-lanToComposedAdjoint (Lan f v) = compose (fmap (leftAdjunct f) v)+lanToComposedAdjoint :: (Functor h, Adjunction f g) => Lan f h a -> h (g a)+lanToComposedAdjoint (Lan f v) = fmap (leftAdjunct f) v -composedAdjointToLan :: Composition compose => Adjunction f g => compose h g a -> Lan f h a-composedAdjointToLan = Lan counit . decompose+composedAdjointToLan :: Adjunction f g => h (g a) -> Lan f h a+composedAdjointToLan = Lan counit  -- | 'composeLan' and 'decomposeLan' witness the natural isomorphism from @Lan f (Lan g h)@ and @Lan (f `o` g) h@ composeLan :: (Composition compose, Functor f) => Lan f (Lan g h) a -> Lan (compose f g) h a

@@ -0,0 +1,284 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE GADTs #-}++#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702+{-# LANGUAGE Trustworthy #-}+#endif+-------------------------------------------------------------------------------------------+-- |+-- Copyright 	: 2013 Edward Kmett and Dan Doel+-- License	: BSD+--+-- Maintainer	: Edward Kmett <ekmett@gmail.com>+-- Stability	: experimental+-- Portability	: rank N types+--+-- Right and Left Kan lifts for functors over Hask, where they exist.+--+-- <http://ncatlab.org/nlab/show/Kan+lift>+-------------------------------------------------------------------------------------------+module Data.Functor.KanLift+  (+  -- * Right Kan lifts+    Rift(..)+  , toRift, fromRift, grift+  , composeRift, decomposeRift+  , adjointToRift, riftToAdjoint+  , composedAdjointToRift, riftToComposedAdjoint+  , rap+  -- * Left Kan lifts+  , Lift(..)+  , toLift, fromLift, glift+  , composeLift, decomposeLift+  , adjointToLift, liftToAdjoint+  , liftToComposedAdjoint, composedAdjointToLift+  ) where++import Control.Applicative+import Data.Copointed+import Data.Functor.Adjunction+import Data.Functor.Composition+import Data.Functor.Compose+import Data.Functor.Identity+import Data.Pointed++-- * Right Kan Lift++-- |+--+-- @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.+--+-- @+-- data 'UniversalRift' 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 -| 'Rift' f 'Identity'@, and since @'Rift' f f@ is isomorphic to @'Rift' f 'Identity' (f a)@, this is the 'Monad' formed by the adjunction.+--+-- @'Rift' w f ~ 'Control.Monad.Co.CoT' w f@ can be a 'Monad' for any 'Comonad' @w@.+--+-- @'Rift' 'Identity' m@ can be a 'Monad' for any 'Monad' @m@, as it is isomorphic to @'Yoneda' m@.++newtype Rift g h a =+  Rift { runRift :: forall r. g (a -> r) -> h r }++instance Functor g => Functor (Rift g h) where+  fmap f (Rift g) = Rift (g . fmap (.f))+  {-# INLINE fmap #-}++instance (Functor g, g ~ h) => Pointed (Rift g h) where+  point a = Rift (fmap ($a))+  {-# INLINE point #-}++instance (Functor g, g ~ h) => Applicative (Rift g h) where+  pure a = Rift (fmap ($a))+  {-# INLINE pure #-}+  Rift mf <*> Rift ma = Rift (ma . mf . fmap (.))+  {-# INLINE (<*>) #-}++-- | Indexed applicative composition of right Kan lifts.+rap :: Functor f => Rift f g (a -> b) -> Rift g h a -> Rift f h b+rap (Rift mf) (Rift ma) = Rift (ma . mf . fmap (.))+{-# INLINE rap #-}++grift :: Adjunction f u => f (Rift f k a) -> k a+grift = rightAdjunct (\r -> leftAdjunct (runRift r) id)+{-# INLINE grift #-}++-- | The universal property of 'Rift'+toRift :: (Functor g, Functor k) => (forall x. g (k x) -> h x) -> k a -> Rift g h a+toRift h z = Rift $ \g -> h $ fmap (<$> z) g+{-# INLINE toRift #-}++-- |+-- When @f -| u@, then @f -| Rift f Identity@ and+--+-- @+-- 'toRift' . 'fromRift' ≡ 'id'+-- 'fromRift' . 'toRift' ≡ 'id'+-- @+fromRift :: Adjunction f u => (forall a. k a -> Rift f h a) -> f (k b) -> h b+fromRift f = grift . fmap f+{-# INLINE fromRift #-}++-- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.+--+-- @+-- 'adjointToRift' . 'riftToAdjoint' ≡ 'id'+-- 'riftToAdjoint' . 'adjointToRift' ≡ 'id'+-- @+adjointToRift :: Adjunction f u => u a -> Rift f Identity a+adjointToRift ua = Rift (Identity . rightAdjunct (<$> ua))+{-# INLINE adjointToRift #-}++-- | @Rift f Identity a@ is isomorphic to the right adjoint to @f@ if one exists.+riftToAdjoint :: Adjunction f u => Rift f Identity a -> u a+riftToAdjoint (Rift m) = leftAdjunct (runIdentity . m) id+{-# INLINE riftToAdjoint #-}++-- |+--+-- @+-- 'composeRift' . 'decomposeRift' ≡ 'id'+-- 'decomposeRift' . 'composeRift' ≡ 'id'+-- @+composeRift :: (Composition compose, Adjunction g u) => Rift f (Rift g h) a -> Rift (compose g f) h a+composeRift (Rift f) = Rift (grift . fmap f . decompose)+{-# INLINE composeRift #-}++decomposeRift :: (Composition compose, Functor f, Functor g) => Rift (compose g f) h a -> Rift f (Rift g h) a+decomposeRift (Rift f) = Rift $ \far -> Rift (f . compose . fmap (\rs -> fmap (rs.) far))+{-# INLINE decomposeRift #-}+++-- |+-- | @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'+-- @++riftToComposedAdjoint :: Adjunction f u => Rift f h a -> u (h a)+riftToComposedAdjoint (Rift m) = leftAdjunct m id+{-# INLINE riftToComposedAdjoint #-}++-- | @Rift f h a@ is isomorphic to the post-composition of the right adjoint of @f@ onto @h@ if such a right adjoint exists.+composedAdjointToRift :: (Functor h, Adjunction f u) => u (h a) -> Rift f h a+composedAdjointToRift uha = Rift $ rightAdjunct (\b -> fmap b <$> uha)+{-# INLINE composedAdjointToRift #-}++-- * Left Kan Lift++-- |+-- > 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'.+newtype Lift g f a = Lift { runLift :: forall z. Functor z => (forall x. f x -> g (z x)) -> z a }++instance Functor (Lift g h) where+  fmap f (Lift g) = Lift (fmap f . g)+  {-# INLINE fmap #-}++instance (Functor g, g ~ h) => Copointed (Lift g h) where+  copoint x = runIdentity (runLift x (fmap Identity))+  {-# INLINE copoint #-}++-- |+--+-- @f => g ('Lift' g f a)@+glift :: Adjunction l g => k a -> g (Lift g k a)+glift = leftAdjunct (\lka -> Lift (\k2gz -> rightAdjunct k2gz lka))+{-# INLINE glift #-}++-- | The universal property of 'Lift'+toLift :: Functor z => (forall a. f a -> g (z a)) -> Lift g f b -> z b+toLift = flip runLift+{-# INLINE toLift #-}++-- toLift decompose :: Compose f => Lift g (compose g f) a -> f a++-- | When the adjunction exists+--+-- @+-- 'fromLift' . 'toLift' ≡ 'id'+-- 'toLift' . 'fromLift' ≡ 'id'+-- @+fromLift :: Adjunction l u => (forall a. Lift u f a -> z a) -> f b -> u (z b)+fromLift f = fmap f . glift+{-# INLINE fromLift #-}++-- |+--+-- @+-- 'composeLift' . 'decomposeLift' = 'id'+-- 'decomposeLift' . 'composeLift' = 'id'+-- @+composeLift :: (Composition compose, Functor f, Functor g) => Lift f (Lift g h) a -> Lift (compose g f) h a+composeLift (Lift m) = Lift $ \h -> m $ decompose . toLift (fmap Compose . decompose . h)+{-# INLINE composeLift #-}++decomposeLift :: (Composition compose, Adjunction l g) => Lift (compose g f) h a -> Lift f (Lift g h) a+decomposeLift (Lift m) = Lift $ \h -> m (compose . fmap h . glift)+{-# INLINE decomposeLift #-}++-- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.+--+-- @+-- 'adjointToLift' . 'liftToAdjoint' ≡ 'id'+-- 'liftToAdjoint' . 'adjointToLift' ≡ 'id'+-- @+adjointToLift :: Adjunction f u => f a -> Lift u Identity a+adjointToLift fa = Lift $ \k -> rightAdjunct (k . Identity) fa+{-# INLINE adjointToLift #-}++-- | @Lift u Identity a@ is isomorphic to the left adjoint to @u@ if one exists.+liftToAdjoint :: Adjunction f u => Lift u Identity a -> f a+liftToAdjoint = toLift (unit . runIdentity)+{-# INLINE liftToAdjoint #-}++-- | @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'+-- @+liftToComposedAdjoint :: (Adjunction f u, Functor h) => Lift u h a -> f (h a)+liftToComposedAdjoint (Lift m) = decompose $ m (leftAdjunct Compose)+{-# INLINE liftToComposedAdjoint #-}++-- | @Lift u h a@ is isomorphic to the post-composition of the left adjoint of @u@ onto @h@ if such a left adjoint exists.+composedAdjointToLift :: Adjunction f u => f (h a) -> Lift u h a+composedAdjointToLift = rightAdjunct glift+{-# INLINE composedAdjointToLift #-}