Permalink
Browse files

initialized

  • Loading branch information...
0 parents commit e772b6693d1ae21899dfc5caf532f452d14db46d @ekmett committed Feb 5, 2011
Showing with 651 additions and 0 deletions.
  1. +2 −0 .gitignore
  2. +50 −0 Control/Comonad/Density.hs
  3. +62 −0 Control/Monad/Codensity.hs
  4. +81 −0 Data/Functor/KanExtension.hs
  5. +205 −0 Data/Functor/Yoneda.hs
  6. +169 −0 Data/Functor/Yoneda/Contravariant.hs
  7. +30 −0 LICENSE
  8. +7 −0 Setup.lhs
  9. +45 −0 kan-extensions.cabal
@@ -0,0 +1,2 @@
+_darcs
+dist
@@ -0,0 +1,50 @@
+{-# LANGUAGE MultiParamTypeClasses, GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Control.Comonad.Density
+-- Copyright : (C) 2008-2011 Edward Kmett
+-- License : BSD-style (see the file LICENSE)
+--
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability : experimental
+-- Portability : non-portable (GADTs, MPTCs)
+--
+-- The density comonad for a functor. aka the comonad generated by a functor
+-- The ''density'' term dates back to Dubuc''s 1974 thesis. The term
+-- ''monad genererated by a functor'' dates back to 1972 in Street''s
+-- ''Formal Theory of Monads''.
+----------------------------------------------------------------------------
+module Control.Comonad.Density
+ ( DensityT(..)
+ , liftDensityT
+ , densityTToAdjunction, adjunctionToDensityT
+ ) where
+
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Data.Functor.Adjunction
+
+data DensityT k a where
+ DensityT :: (k b -> a) -> k b -> DensityT k a
+
+instance Functor (DensityT f) where
+ fmap f (DensityT g h) = DensityT (f . g) h
+
+instance Extend (DensityT f) where
+ duplicate (DensityT f ws) = DensityT (DensityT f) ws
+
+instance Comonad (DensityT f) where
+ extract (DensityT f a) = f a
+
+instance ComonadTrans DensityT where
+ lower (DensityT f c) = extend f c
+
+-- | The natural isomorphism between a comonad w and the comonad generated by w (forwards).
+liftDensityT :: Comonad w => w a -> DensityT w a
+liftDensityT = DensityT extract
+
+densityTToAdjunction :: Adjunction f g => DensityT f a -> f (g a)
+densityTToAdjunction (DensityT f v) = fmap (leftAdjunct f) v
+
+adjunctionToDensityT :: Adjunction f g => f (g a) -> DensityT f a
+adjunctionToDensityT = DensityT counit
@@ -0,0 +1,62 @@
+{-# LANGUAGE Rank2Types #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module : Control.Monad.Codensity
+-- Copyright : (C) 2008-2011 Edward Kmett
+-- License : BSD-style (see the file LICENSE)
+--
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability : provisional
+-- Portability : non-portable (rank-2 polymorphism)
+--
+----------------------------------------------------------------------------
+module Control.Monad.Codensity
+ ( CodensityT(..)
+ , lowerCodensityT
+ , codensityTToAdjunction
+ , adjunctionToCodensityT
+ ) where
+
+import Control.Applicative
+import Control.Monad (ap)
+import Data.Functor.Adjunction
+import Data.Functor.Apply
+import Control.Monad.Trans.Class
+import Control.Monad.IO.Class
+
+{-
+type Codensity = CodensityT Identity
+codensity :: (forall b. (a -> b) -> b) -> Codensity a
+runCodensity :: Codensity a -> (a -> b) -> a
+-}
+
+newtype CodensityT m a = CodensityT { runCodensityT :: forall b. (a -> m b) -> m b }
+
+instance Functor (CodensityT k) where
+ fmap f (CodensityT m) = CodensityT (\k -> m (k . f))
+
+instance Apply (CodensityT f) where
+ (<.>) = ap
+
+instance Applicative (CodensityT f) where
+ pure x = CodensityT (\k -> k x)
+ (<*>) = ap
+
+instance Monad (CodensityT f) where
+ return x = CodensityT (\k -> k x)
+ m >>= k = CodensityT (\c -> runCodensityT m (\a -> runCodensityT (k a) c))
+
+instance MonadIO m => MonadIO (CodensityT m) where
+ liftIO = lift . liftIO
+
+instance MonadTrans CodensityT where
+ lift m = CodensityT (m >>=)
+
+lowerCodensityT :: Monad m => CodensityT m a -> m a
+lowerCodensityT a = runCodensityT a return
+
+codensityTToAdjunction :: Adjunction f g => CodensityT g a -> g (f a)
+codensityTToAdjunction r = runCodensityT r unit
+
+adjunctionToCodensityT :: Adjunction f g => g (f a) -> CodensityT g a
+adjunctionToCodensityT f = CodensityT (\a -> fmap (rightAdjunct a) f)
@@ -0,0 +1,81 @@
+{-# LANGUAGE Rank2Types, GADTs #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module : Data.Functor.KanExtension
+-- Copyright : 2008-2011 Edward Kmett
+-- License : BSD
+--
+-- Maintainer : Edward Kmett <ekmett@gmail.com>
+-- Stability : experimental
+-- Portability : rank 2 types
+--
+-------------------------------------------------------------------------------------------
+module Data.Functor.KanExtension where
+
+import Data.Functor.Identity
+import Data.Functor.Adjunction
+import Data.Functor.Composition
+
+newtype Ran g h a = Ran { runRan :: forall b. (a -> g b) -> h b }
+
+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)
+
+fromRan :: Composition compose => (forall a. k a -> Ran g h a) -> compose k g b -> h b
+fromRan s = flip runRan id . s . decompose
+
+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)
+
+decomposeRan :: (Composition compose, Functor f) => Ran (compose f g) h a -> Ran f (Ran g h) a
+decomposeRan r = Ran (\f -> Ran (\g -> runRan r (compose . fmap g . f)))
+
+adjointToRan :: Adjunction f g => f a -> Ran g Identity a
+adjointToRan f = Ran (\a -> Identity $ rightAdjunct a f)
+
+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)
+
+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))
+
+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
+
+fromLan :: (Composition compose) => (forall a. Lan g h a -> f a) -> h b -> compose f g b
+fromLan s = compose . s . Lan id
+
+instance Functor (Lan f g) where
+ fmap f (Lan g h) = Lan (f . g) h
+
+adjointToLan :: Adjunction f g => g a -> Lan f Identity a
+adjointToLan = Lan counit . Identity
+
+lanToAdjoint :: Adjunction f g => Lan f Identity a -> g a
+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)
+
+composedAdjointToLan :: Composition compose => Adjunction f g => compose h g a -> Lan f h a
+composedAdjointToLan = Lan counit . decompose
+
+-- | '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
+composeLan (Lan f (Lan g h)) = Lan (f . fmap g . decompose) h
+
+decomposeLan :: Composition compose => Lan (compose f g) h a -> Lan f (Lan g h) a
+decomposeLan (Lan f h) = Lan (f . compose) (Lan id h)
+
Oops, something went wrong.

0 comments on commit e772b66

Please sign in to comment.