packages feed

comonad-transformers 2.0.3 → 4.0

raw patch · 25 files changed

Files

+ .ghci view
@@ -0,0 +1,1 @@+:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h
+ .gitignore view
@@ -0,0 +1,13 @@+dist+docs+wiki+TAGS+tags+wip+.DS_Store+.*.swp+.*.swo+*.o+*.hi+*~+*#
+ .travis.yml view
@@ -0,0 +1,8 @@+language: haskell+notifications:+  irc:+    channels:+      - "irc.freenode.org#haskell-lens"+    skip_join: true+    template:+      - "\x0313comonad-transformers\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
+ .vim.custom view
@@ -0,0 +1,31 @@+" Add the following to your .vimrc to automatically load this on startup++" if filereadable(".vim.custom")+"     so .vim.custom+" endif++function StripTrailingWhitespace()+  let myline=line(".")+  let mycolumn = col(".")+  silent %s/  *$//+  call cursor(myline, mycolumn)+endfunction++" enable syntax highlighting+syntax on++" search for the tags file anywhere between here and /+set tags=TAGS;/++" highlight tabs and trailing spaces+set listchars=tab:‗‗,trail:‗+set list++" f2 runs hasktags+map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR>++" strip trailing whitespace before saving+" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace()++" rebuild hasktags after saving+au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src"
− Control/Comonad/Hoist/Class.hs 
@@ -1,29 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Hoist.Class--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------------------------------------------------------------------------------module Control.Comonad.Hoist.Class (ComonadHoist(..)) where--import Control.Comonad-import Control.Monad.Trans.Identity-import Data.Functor.Identity--class ComonadHoist t where-  -- | Ideally we would offer a way to lift comonad homomorphisms-  -- but this isn't Haskell 98, so we settle for the most common case-  -- here.-  ---  -- > liftTrans :: (forall a. w a -> v a) -> t w a -> t v a -  -- > cohoist = liftTrans (Identity . extract)-  cohoist :: Comonad w => t w a -> t Identity a---- avoiding orphans--instance ComonadHoist IdentityT where-  cohoist = IdentityT . Identity . extract . runIdentityT
− Control/Comonad/Trans/Class.hs 
@@ -1,22 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Class--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------------------------------------------------------------------------------module Control.Comonad.Trans.Class -  ( ComonadTrans(..) ) where--import Control.Comonad-import Control.Monad.Trans.Identity--class ComonadTrans t where-  lower :: Extend w => t w a -> w a ---- avoiding orphans-instance ComonadTrans IdentityT where-  lower = runIdentityT
− Control/Comonad/Trans/Discont.hs 
@@ -1,20 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Discont--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The discontinuation comonad transformer.--- This version is lazy; for a strict version, see--- "Control.Comonad.Trans.Discont.Strict", which has the same interface.---------------------------------------------------------------------------------module Control.Comonad.Trans.Discont-  ( module Control.Comonad.Trans.Discont.Lazy-  ) where--import Control.Comonad.Trans.Discont.Lazy
− Control/Comonad/Trans/Discont/Lazy.hs 
@@ -1,78 +0,0 @@-{-# LANGUAGE RankNTypes #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Discont.Lazy--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable--- --- 'Discont' is the density comonad of a constant functor, just as 'Cont' is a --- Codensity monad of a constant functor. (For the definition of Density and--- Codensity, see the non-Haskell 98 'adjunctions' package)------ Note that while 'Discont' and 'Store' are isomorphic, 'DiscontT' and 'StoreT' --- are not.---------------------------------------------------------------------------------module Control.Comonad.Trans.Discont.Lazy-  ( -  -- * The 'discontinuation' comonad-    Discont-  , discont-  -- * The discontinuation comonad transformer-  , runDiscont-  , DiscontT(..)-  , runDiscontT-  ) where--import Data.Functor.Identity-import Control.Comonad-import Control.Comonad.Trans.Class--#ifdef __GLASGOW_HASKELL__-import Data.Typeable--instance (Typeable s, Typeable1 w) => Typeable1 (DiscontT s w) where-  typeOf1 dswa = mkTyConApp discontTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where -      s :: DiscontT s w a -> s-      s = undefined-      w :: DiscontT s w a -> w a-      w = undefined--discontTTyCon :: TyCon-discontTTyCon = mkTyCon "Control.Comonad.Trans.Discont.Lazy.DiscontT" -{-# NOINLINE discontTTyCon #-}--#endif--type Discont s = DiscontT s Identity--data DiscontT s w a = DiscontT (w s -> a) (w s)--discont :: (s -> a) -> s -> Discont s a -discont f s = DiscontT (f . runIdentity) (Identity s)--runDiscont :: Discont s a -> (s -> a, s) -runDiscont ~(DiscontT f (Identity s)) = (f . Identity,  s)--runDiscontT :: DiscontT s w a -> (w s -> a, w s)-runDiscontT ~(DiscontT f s) = (f, s)--instance Functor (DiscontT s w) where-  fmap g ~(DiscontT f ws) = DiscontT (g . f) ws--instance Extend (DiscontT s w) where-  duplicate ~(DiscontT f ws) = DiscontT (DiscontT f) ws--instance Comonad (DiscontT s w) where-  extract ~(DiscontT f ws) = f ws--instance ComonadTrans (DiscontT s) where-  lower ~(DiscontT f s) = extend f s---- instance Apply w => Apply (DiscontT s w) where-
− Control/Comonad/Trans/Discont/Memo.hs 
@@ -1,85 +0,0 @@-{-# LANGUAGE CPP, RankNTypes #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Discont.Memo--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable--- ------ 'Discont' is the density comonad of a constant functor, just as 'Cont' is a --- Codensity monad of a constant functor. (For the definition of Density and--- Codensity, see the non-Haskell 98 'adjunctions' package)------ Note that while 'Discont' and 'Store' are isomorphic, 'DiscontT' and 'StoreT' --- are not.------ Like the memoizing store comonad, version memoizes the result of applying --- the continuation to the current context. ---------------------------------------------------------------------------------module Control.Comonad.Trans.Discont.Memo-  ( -  -- * The 'discontinuation' comonad-    Discont-  , discont-  -- * The discontinuation comonad transformer-  , runDiscont-  , DiscontT-  , discontT -  , runDiscontT-  ) where--import Data.Functor.Identity-import Control.Comonad-import Control.Comonad.Trans.Class--#ifdef __GLASGOW_HASKELL__-import Data.Typeable--instance (Typeable s, Typeable1 w) => Typeable1 (DiscontT s w) where-  typeOf1 dswa = mkTyConApp discontTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where -      s :: DiscontT s w a -> s-      s = undefined-      w :: DiscontT s w a -> w a-      w = undefined--discontTTyCon :: TyCon-discontTTyCon = mkTyCon "Control.Comonad.Trans.Discont.Memo.DiscontT" -{-# NOINLINE discontTTyCon #-}--#endif--type Discont s = DiscontT s Identity--data DiscontT s w a = DiscontT (w s -> a) (w s) a--discont :: (s -> a) -> s -> Discont s a -discont f s = DiscontT (f . runIdentity) (Identity s) (f s)--discontT :: (w s -> a) -> w s -> DiscontT s w a -discontT f s = DiscontT f s (f s)--runDiscont :: Discont s a -> (s -> a, s) -runDiscont (DiscontT f (Identity s) _) = (f . Identity,  s)--runDiscontT :: DiscontT s w a -> (w s -> a, w s)-runDiscontT (DiscontT f s _) = (f, s)--instance Functor (DiscontT s w) where-  fmap g (DiscontT f ws a) = DiscontT (g . f) ws (g a)--instance Extend (DiscontT s w) where-  duplicate (DiscontT f ws _) = discontT (discontT f) ws--instance Comonad (DiscontT s w) where-  extract (DiscontT _ _ a) = a--instance ComonadTrans (DiscontT s) where-  lower (DiscontT f s _) = extend f s---- instance Apply w => Apply (DiscontT s w) where
− Control/Comonad/Trans/Discont/Strict.hs 
@@ -1,75 +0,0 @@-{-# LANGUAGE RankNTypes #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Discont.Strict--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ 'Discont' is the density comonad of a constant functor, just as 'Cont' is a --- Codensity monad of a constant functor. (For the definition of Density and--- Codensity, see the non-Haskell 98 'adjunctions' package)------ Note that while 'Discont' and 'Store' are isomorphic, 'DiscontT' and 'StoreT' --- are not.------------------------------------------------------------------------------module Control.Comonad.Trans.Discont.Strict-  ( -  -- * The 'discontinuation' comonad-    Discont-  , discont-  -- * The discontinuation comonad transformer-  , runDiscont-  , DiscontT(..)-  , runDiscontT-  ) where--import Data.Functor.Identity-import Control.Comonad-import Control.Comonad.Trans.Class--#ifdef __GLASGOW_HASKELL__-import Data.Typeable--instance (Typeable s, Typeable1 w) => Typeable1 (DiscontT s w) where-  typeOf1 dswa = mkTyConApp discontTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where -      s :: DiscontT s w a -> s-      s = undefined-      w :: DiscontT s w a -> w a -      w = undefined--discontTTyCon :: TyCon-discontTTyCon = mkTyCon "Control.Comonad.Trans.Discont.Strict.DiscontT" -{-# NOINLINE discontTTyCon #-}-#endif--type Discont s = DiscontT s Identity--data DiscontT s w a = DiscontT (w s -> a) (w s)--discont :: (s -> a) -> s -> Discont s a -discont f s = DiscontT (f . runIdentity) (Identity s)--runDiscont :: Discont s a -> (s -> a, s) -runDiscont (DiscontT f (Identity s)) = (f . Identity,  s)--runDiscontT :: DiscontT s w a -> (w s -> a, w s)-runDiscontT (DiscontT f s) = (f, s)--instance Functor (DiscontT s w) where-  fmap g (DiscontT f ws) = DiscontT (g . f) ws--instance Extend (DiscontT s w) where-  duplicate (DiscontT f ws) = DiscontT (DiscontT f) ws-  extend g (DiscontT f ws) = DiscontT (g . DiscontT f) ws--instance Comonad (DiscontT s w) where-  extract (DiscontT f ws) = f ws--instance ComonadTrans (DiscontT s) where-  lower (DiscontT f s) = extend f s-
− Control/Comonad/Trans/Env.hs 
@@ -1,20 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Context--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The environment comonad transformer (aka coreader).--- This version is lazy; for a strict version, see--- "Control.Comonad.Trans.Env.Strict", which has the same interface.---------------------------------------------------------------------------------module Control.Comonad.Trans.Env-  ( module Control.Comonad.Trans.Env.Lazy-  ) where--import Control.Comonad.Trans.Env.Lazy
− Control/Comonad/Trans/Env/Lazy.hs 
@@ -1,136 +0,0 @@-{-# LANGUAGE CPP, FlexibleContexts #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Env.Lazy--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The environment comonad transformer (aka coreader).--- This adds an extra value that can be accessed in the environment.------ Left adjoint to the reader comonad.------------------------------------------------------------------------------module Control.Comonad.Trans.Env.Lazy-  ( -  -- * The environment comonad-    Env-  , env-  , runEnv-  -- * The environment comonad transformer-  , EnvT(..)-  , runEnvT-  , lowerEnvT-  -- * Combinators-  , ask-  , asks-  , local-  -- , liftCallCV-  ) where--import Control.Applicative-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Functor.Apply-import Data.Functor.Identity-import Data.Foldable-import Data.Traversable-import Data.Semigroup--#ifdef __GLASGOW_HASKELL__-import Data.Data--instance (Typeable s, Typeable1 w) => Typeable1 (EnvT s w) where-  typeOf1 dswa = mkTyConApp envTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: EnvT s w a -> s-      s = undefined-      w :: EnvT s w a -> w a-      w = undefined--envTTyCon :: TyCon-envTTyCon = mkTyCon "Control.Comonad.Trans.Env.Lazy.EnvT"-{-# NOINLINE envTTyCon #-}--instance (Typeable s, Typeable1 w, Typeable a) => Typeable (EnvT s w a) where-  typeOf = typeOfDefault--instance-  ( Data e-  , Typeable1 w, Data (w a)-  , Data a-  ) => Data (EnvT e w a) where-    gfoldl f z (EnvT e wa) = z EnvT `f` e `f` wa-    toConstr _ = envTConstr-    gunfold k z c = case constrIndex c of-        1 -> k (k (z EnvT))-        _ -> error "gunfold"-    dataTypeOf _ = envTDataType-    dataCast1 f = gcast1 f--envTConstr :: Constr-envTConstr = mkConstr envTDataType "EnvT" [] Prefix-{-# NOINLINE envTConstr #-}--envTDataType :: DataType-envTDataType = mkDataType "Control.Comonad.Trans.Env.Lazy.EnvT" [envTConstr]-{-# NOINLINE envTDataType #-}--#endif--type Env e = EnvT e Identity-data EnvT e w a = EnvT e (w a)--env :: e -> a -> Env e a-env e a = EnvT e (Identity a)--runEnv :: Env e a -> (e, a)-runEnv ~(EnvT e (Identity a)) = (e, a)--runEnvT :: EnvT e w a -> (e, w a)-runEnvT ~(EnvT e wa) = (e, wa)--instance Functor w => Functor (EnvT e w) where-  fmap g ~(EnvT e wa) = EnvT e (fmap g wa)--instance Extend w => Extend (EnvT e w) where-  duplicate ~(EnvT e wa) = EnvT e (extend (EnvT e) wa)--instance Comonad w => Comonad (EnvT e w) where-  extract ~(EnvT _ wa) = extract wa--instance (Semigroup e, Apply w) => Apply (EnvT e w) where-  ~(EnvT ef wf) <.> ~(EnvT ea wa) = EnvT (ef <> ea) (wf <.> wa)--instance ComonadTrans (EnvT e) where-  lower (EnvT _ wa) = wa--instance ComonadHoist (EnvT e) where-  cohoist ~(EnvT e wa) = EnvT e (Identity (extract wa))--instance Foldable w => Foldable (EnvT e w) where-  foldMap f ~(EnvT _ w) = foldMap f w--instance Traversable w => Traversable (EnvT e w) where-  traverse f (EnvT e w) = EnvT e <$> traverse f w--ask :: EnvT e w a -> e-ask (EnvT e _) = e--asks :: (e -> f) -> EnvT e w a -> f-asks f = f . ask--local :: (e -> e) -> EnvT e w a -> EnvT e w a-local f ~(EnvT e wa) = EnvT (f e) wa--lowerEnvT :: EnvT e w a -> w a -lowerEnvT (EnvT _ wa) = wa--{--liftCallCV :: Functor w => (w (w (w a -> a) -> b) -> b) -> EnvT e w (EnvT e w (EnvT e w a -> a) -> b) -> b-liftCallCV callCV ~(EnvT e wa) = callCV $ \c -> ...--}
− Control/Comonad/Trans/Env/Strict.hs 
@@ -1,130 +0,0 @@-{-# LANGUAGE CPP, FlexibleContexts #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Env.Strict--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The environment comonad transformer (aka coreader).--- This adds an extra value that can be accessed in the environment.------ Left adjoint to the reader comonad.------------------------------------------------------------------------------module Control.Comonad.Trans.Env.Strict-  ( -  -- * The strict environment comonad-    Env-  , env-  , runEnv-  -- * The strict environment comonad transformer-  , EnvT(..)-  , runEnvT-  , lowerEnvT-  -- * Combinators-  , ask-  , asks-  , local-  ) where--import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Foldable-import Data.Traversable-import Data.Functor.Apply-import Data.Functor.Identity-import Data.Semigroup--#ifdef __GLASGOW_HASKELL__-import Data.Data--instance (Typeable s, Typeable1 w) => Typeable1 (EnvT s w) where-  typeOf1 dswa = mkTyConApp envTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: EnvT s w a -> s-      s = undefined-      w :: EnvT s w a -> w a-      w = undefined--envTTyCon :: TyCon-envTTyCon = mkTyCon "Control.Comonad.Trans.Env.Strict.EnvT"-{-# NOINLINE envTTyCon #-}--instance (Typeable s, Typeable1 w, Typeable a) => Typeable (EnvT s w a) where-  typeOf = typeOfDefault--instance-  ( Data e-  , Typeable1 w, Data (w a)-  , Data a-  ) => Data (EnvT e w a) where-    gfoldl f z (EnvT e wa) = z EnvT `f` e `f` wa-    toConstr _ = envTConstr-    gunfold k z c = case constrIndex c of-        1 -> k (k (z EnvT))-        _ -> error "gunfold"-    dataTypeOf _ = envTDataType-    dataCast1 f = gcast1 f--envTConstr :: Constr-envTConstr = mkConstr envTDataType "EnvT" [] Prefix-{-# NOINLINE envTConstr #-}--envTDataType :: DataType-envTDataType = mkDataType "Control.Comonad.Trans.Env.Strict.EnvT" [envTConstr]-{-# NOINLINE envTDataType #-}--#endif--type Env e = EnvT e Identity-data EnvT e w a = EnvT e (w a)--env :: e -> a -> Env e a-env e a = EnvT e (Identity a)--runEnv :: Env e a -> (e, a)-runEnv (EnvT e (Identity a)) = (e, a)--runEnvT :: EnvT e w a -> (e, w a)-runEnvT (EnvT e wa) = (e, wa)--instance Functor w => Functor (EnvT e w) where-  fmap g (EnvT e wa) = EnvT e (fmap g wa)--instance Extend w => Extend (EnvT e w) where-  duplicate (EnvT e wa) = EnvT e (extend (EnvT e) wa)--instance Comonad w => Comonad (EnvT e w) where-  extract (EnvT _ wa) = extract wa--instance ComonadTrans (EnvT e) where-  lower (EnvT _ wa) = wa--lowerEnvT :: EnvT e w a -> w a-lowerEnvT (EnvT _ wa) = wa--instance ComonadHoist (EnvT e) where-  cohoist (EnvT e wa) = EnvT e (Identity (extract wa))--instance (Semigroup e, Apply w) => Apply (EnvT e w) where-  EnvT ef wf <.> EnvT ea wa = EnvT (ef <> ea) (wf <.> wa)--instance Foldable w => Foldable (EnvT e w) where-  foldMap f (EnvT _ w) = foldMap f w--instance Traversable w => Traversable (EnvT e w) where-  traverse f (EnvT e w) = EnvT e <$> traverse f w--ask :: EnvT e w a -> e-ask (EnvT e _) = e--asks :: (e -> f) -> EnvT e w a -> f-asks f (EnvT e _) = f e--local :: (e -> e) -> EnvT e w a -> EnvT e w a-local f (EnvT e wa) = EnvT (f e) wa-
− Control/Comonad/Trans/Identity.hs 
@@ -1,16 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Identity--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable--- ------------------------------------------------------------------------------module Control.Comonad.Trans.Identity-  ( IdentityT(..)-  ) where--import Control.Monad.Trans.Identity
− Control/Comonad/Trans/Store.hs 
@@ -1,20 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Context--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The store comonad transformer (aka costate).--- This version is lazy; for a strict version, see--- "Control.Comonad.Trans.Store.Strict", which has the same interface.---------------------------------------------------------------------------------module Control.Comonad.Trans.Store-  ( module Control.Comonad.Trans.Store.Lazy-  ) where--import Control.Comonad.Trans.Store.Lazy
− Control/Comonad/Trans/Store/Lazy.hs 
@@ -1,119 +0,0 @@-{-# LANGUAGE CPP #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Store.Lazy--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The lazy store (state-in-context/costate) comonad transformer is subject to the laws:--- --- > x = seek (pos x) x--- > y = pos (seek y x)--- > seek y x = seek y (seek z x)------ Thanks go to Russell O'Connor and Daniel Peebles for their help formulating --- and proving the laws for this comonad transformer.------------------------------------------------------------------------------module Control.Comonad.Trans.Store.Lazy-  ( -  -- * The Store comonad-    Store, store, runStore-  -- * The Store comonad transformer-  , StoreT(..), runStoreT-  -- * Operations-  , pos-  , seek, seeks-  , peek, peeks-  ) where--import Control.Applicative-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Functor.Identity-import Data.Functor.Apply-import Data.Semigroup--#ifdef __GLASGOW_HASKELL__-import Data.Typeable-instance (Typeable s, Typeable1 w) => Typeable1 (StoreT s w) where-  typeOf1 dswa = mkTyConApp storeTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: StoreT s w a -> s-      s = undefined-      w :: StoreT s w a -> w a-      w = undefined--instance (Typeable s, Typeable1 w, Typeable a) => Typeable (StoreT s w a) where-  typeOf = typeOfDefault--storeTTyCon :: TyCon-storeTTyCon = mkTyCon "Control.Comonad.Trans.Store.Lazy.StoreT"-{-# NOINLINE storeTTyCon #-}-#endif--type Store s = StoreT s Identity--store :: (s -> a) -> s -> Store s a -store f s = StoreT (Identity f) s--runStore :: Store s a -> (s -> a, s)-runStore ~(StoreT (Identity f) s) = (f, s)--data StoreT s w a = StoreT (w (s -> a)) s--runStoreT :: StoreT s w a -> (w (s -> a), s)-runStoreT ~(StoreT wf s) = (wf, s)--instance Functor w => Functor (StoreT s w) where-  fmap f ~(StoreT wf s) = StoreT (fmap (f .) wf) s--instance (Apply w, Semigroup s) => Apply (StoreT s w) where-  ~(StoreT ff m) <.> ~(StoreT fa n) = StoreT ((<*>) <$> ff <.> fa) (m <> n)--instance (Applicative w, Semigroup s, Monoid s) => Applicative (StoreT s w) where-  pure a = StoreT (pure (const a)) mempty-  ~(StoreT ff m) <*> ~(StoreT fa n) = StoreT ((<*>) <$> ff <*> fa) (m `mappend` n)--instance Extend w => Extend (StoreT s w) where-  duplicate ~(StoreT wf s) = StoreT (extend StoreT wf) s-  extend f ~(StoreT wf s) = StoreT (extend (\wf' s' -> f (StoreT wf' s')) wf) s--instance Comonad w => Comonad (StoreT s w) where-  extract ~(StoreT wf s) = extract wf s--instance ComonadTrans (StoreT s) where-  lower ~(StoreT f s) = fmap ($s) f--instance ComonadHoist (StoreT s) where-  cohoist ~(StoreT f s) = StoreT (Identity (extract f)) s---- | Read the current position-pos :: StoreT s w a -> s-pos (StoreT _ s) = s---- | Seek to an absolute location------ > seek s = peek s . duplicate-seek :: Comonad w => s -> StoreT s w a -> StoreT s w a -seek s ~(StoreT f _) = StoreT f s---- | Seek to a relative location------ > seeks f = peeks f . duplicate-seeks :: Comonad w => (s -> s) -> StoreT s w a -> StoreT s w a-seeks f ~(StoreT g s) = StoreT g (f s)---- | Peek at a value at a given absolute location------ > peek x . extend (peek y) = peek y-peek :: Comonad w => s -> StoreT s w a -> a-peek s (StoreT g _) = extract g s---- | Peek at a value at a given relative location-peeks :: Comonad w => (s -> s) -> StoreT s w a -> a-peeks f ~(StoreT g s) = extract g (f s)
− Control/Comonad/Trans/Store/Memo.hs 
@@ -1,131 +0,0 @@-{-# LANGUAGE CPP #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Store.Memo--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The memoizing store (state-in-context/costate) comonad transformer is --- subject to the laws:--- --- > x = seek (pos x) x--- > y = pos (seek y x)--- > seek y x = seek y (seek z x)------ This version of the transformer lazily memoizes the result of applying the --- comonad to the current state. This can be useful for avoiding redundant --- computation if you reuse the same StoreT object multiple times.------------------------------------------------------------------------------module Control.Comonad.Trans.Store.Memo-  ( -  -- * The Store comonad-    Store, store, runStore-  -- * The Store comonad transformer-  , StoreT, storeT, runStoreT-  , lowerStoreT-  -- * Operations-  , pos-  , seek, seeks-  , peek, peeks-  ) where--import Control.Applicative-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Functor.Identity-import Data.Functor.Apply-import Data.Semigroup--#ifdef __GLASGOW_HASKELL__-import Data.Typeable-instance (Typeable s, Typeable1 w) => Typeable1 (StoreT s w) where-  typeOf1 dswa = mkTyConApp storeTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: StoreT s w a -> s-      s = undefined-      w :: StoreT s w a -> w a-      w = undefined--instance (Typeable s, Typeable1 w, Typeable a) => Typeable (StoreT s w a) where-  typeOf = typeOfDefault--storeTTyCon :: TyCon-storeTTyCon = mkTyCon "Control.Comonad.Trans.Store.Memo.StoreT"-{-# NOINLINE storeTTyCon #-}-#endif--type Store s = StoreT s Identity--store :: (s -> a) -> s -> Store s a -store f s = StoreT (Identity f) s (Identity (f s))--runStore :: Store s a -> (s -> a, s)-runStore (StoreT (Identity f) s _) = (f, s)---- inhabitants of @StoreT wf s w@ ensure that------ > w = ($s) <$> wf-data StoreT s w a = StoreT (w (s -> a)) s (w a)--runStoreT :: StoreT s w a -> (w (s -> a), s)-runStoreT (StoreT wf s _) = (wf, s)--storeT :: Functor w => w (s -> a) -> s -> StoreT s w a-storeT wf s = StoreT wf s (fmap ($s) wf)--instance Functor w => Functor (StoreT s w) where-  fmap f (StoreT wf s w) = StoreT (fmap (f .) wf) s (fmap f w)--instance (Apply w, Semigroup s) => Apply (StoreT s w) where-  StoreT ff m _ <.> StoreT fa n _ = storeT ((<*>) <$> ff <.> fa) (m <> n)--instance (Applicative w, Semigroup s, Monoid s) => Applicative (StoreT s w) where-  pure a = storeT (pure (const a)) mempty-  StoreT ff m _ <*> StoreT fa n _ = storeT ((<*>) <$> ff <*> fa) (m `mappend` n)--instance Extend w => Extend (StoreT s w) where-  duplicate (StoreT wf s _) = storeT (extend storeT wf) s --instance Comonad w => Comonad (StoreT s w) where-  extract (StoreT _ _ w) = extract w--instance ComonadTrans (StoreT s) where-  lower (StoreT _ _ w) = w--lowerStoreT :: StoreT s w a -> w a-lowerStoreT (StoreT _ _ w) = w--instance ComonadHoist (StoreT s) where-  cohoist (StoreT f s w) = StoreT (Identity (extract f)) s (Identity (extract w))---- | Read the current position-pos :: StoreT s w a -> s-pos (StoreT _ s _) = s---- | Seek to an absolute location------ > seek s = peek s . duplicate-seek :: Comonad w => s -> StoreT s w a -> StoreT s w a-seek s (StoreT f _ _) = storeT f s---- | Seek to a relative location------ > seeks f = peeks f . duplicate-seeks :: Comonad w => (s -> s) -> StoreT s w a -> StoreT s w a-seeks f (StoreT g s _) = storeT g (f s)---- | Peek at a value at a given absolute location------ > peek x . extend (peek y) = peek y-peek :: Comonad w => s -> StoreT s w a -> a-peek s (StoreT g _ _) = extract g s---- | Peek at a value at a given relative location-peeks :: Comonad w => (s -> s) -> StoreT s w a -> a-peeks f (StoreT g s _) = extract g (f s)-
− Control/Comonad/Trans/Store/Strict.hs 
@@ -1,120 +0,0 @@-{-# LANGUAGE CPP #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Store.Strict--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The strict store (state-in-context/costate) comonad transformer is subject to the laws:--- --- > x = seek (pos x) x--- > y = pos (seek y x)--- > seek y x = seek y (seek z x)------ Thanks go to Russell O'Connor and Daniel Peebles for their help formulating --- and proving the laws for this comonad transformer.------------------------------------------------------------------------------module Control.Comonad.Trans.Store.Strict-  ( -  -- * The Store comonad-    Store, store, runStore-  -- * The Store comonad transformer-  , StoreT(..), runStoreT-  -- * Operations-  , pos-  , seek, seeks-  , peek, peeks-  ) where--import Control.Applicative-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Functor.Identity-import Data.Functor.Apply-import Data.Semigroup--#ifdef __GLASGOW_HASKELL__-import Data.Typeable-instance (Typeable s, Typeable1 w) => Typeable1 (StoreT s w) where-  typeOf1 dswa = mkTyConApp storeTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: StoreT s w a -> s-      s = undefined-      w :: StoreT s w a -> w a-      w = undefined--instance (Typeable s, Typeable1 w, Typeable a) => Typeable (StoreT s w a) where-  typeOf = typeOfDefault--storeTTyCon :: TyCon-storeTTyCon = mkTyCon "Control.Comonad.Trans.Store.Strict.StoreT"-{-# NOINLINE storeTTyCon #-}-#endif--type Store s = StoreT s Identity--store :: (s -> a) -> s -> Store s a -store f s = StoreT (Identity f) s--runStore :: Store s a -> (s -> a, s)-runStore (StoreT (Identity f) s) = (f, s)--data StoreT s w a = StoreT (w (s -> a)) s--runStoreT :: StoreT s w a -> (w (s -> a), s)-runStoreT (StoreT wf s) = (wf, s)--instance Functor w => Functor (StoreT s w) where-  fmap f (StoreT wf s) = StoreT (fmap (f .) wf) s--instance (Apply w, Semigroup s) => Apply (StoreT s w) where-  StoreT ff m <.> StoreT fa n = StoreT ((<*>) <$> ff <.> fa) (m <> n)--instance (Applicative w, Semigroup s, Monoid s) => Applicative (StoreT s w) where-  pure a = StoreT (pure (const a)) mempty-  StoreT ff m <*> StoreT fa n = StoreT ((<*>) <$> ff <*> fa) (m `mappend` n)--instance Extend w => Extend (StoreT s w) where-  duplicate (StoreT wf s) = StoreT (extend StoreT wf) s-  extend f (StoreT wf s) = StoreT (extend (\wf' s' -> f (StoreT wf' s')) wf) s--instance Comonad w => Comonad (StoreT s w) where-  extract (StoreT wf s) = extract wf s--instance ComonadTrans (StoreT s) where-  lower (StoreT f s) = fmap ($s) f--instance ComonadHoist (StoreT s) where-  cohoist (StoreT f s) = StoreT (Identity (extract f)) s---- | Read the current position-pos :: StoreT s w a -> s-pos (StoreT _ s) = s---- | Seek to an absolute location------ > seek s = peek s . duplicate-seek :: Comonad w => s -> StoreT s w a -> StoreT s w a-seek s ~(StoreT f _) = StoreT f s---- | Seek to a relative location------ > seeks f = peeks f . duplicate-seeks :: Comonad w => (s -> s) -> StoreT s w a -> StoreT s w a-seeks f ~(StoreT g s) = StoreT g (f s)---- | Peek at a value at a given absolute location------ > peek x . extend (peek y) = peek y-peek :: Comonad w => s -> StoreT s w a -> a-peek s (StoreT g _) = extract g s---- | Peek at a value at a given relative location-peeks :: Comonad w => (s -> s) -> StoreT s w a -> a-peeks f ~(StoreT g s) = extract g (f s)-
− Control/Comonad/Trans/Traced.hs 
@@ -1,103 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Traced--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The trace comonad transformer (aka the cowriter or exponential comonad transformer).---------------------------------------------------------------------------------module Control.Comonad.Trans.Traced-  ( -  -- * Traced comonad-    Traced-  , traced-  , runTraced-  -- * Traced comonad transformer-  , TracedT(..)-  -- * Operations-  , trace-  , listen-  , listens-  , censor-  ) where--import Control.Applicative-import Control.Monad.Instances-import Control.Monad (ap)-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Distributive-import Data.Functor-import Data.Functor.Apply-import Data.Functor.Identity-import Data.Semigroup-import Data.Typeable--type Traced m = TracedT m Identity--traced :: (m -> a) -> Traced m a-traced f = TracedT (Identity f)--runTraced :: Traced m a -> m -> a-runTraced (TracedT (Identity f)) = f--newtype TracedT m w a = TracedT { runTracedT :: w (m -> a) }--instance Functor w => Functor (TracedT m w) where-  fmap g = TracedT . fmap (g .) . runTracedT--instance Apply w => Apply (TracedT m w) where-  TracedT wf <.> TracedT wa = TracedT (ap <$> wf <.> wa)--instance Applicative w => Applicative (TracedT m w) where-  pure = TracedT . pure . const -  TracedT wf <*> TracedT wa = TracedT (ap <$> wf <*> wa)--instance (Extend w, Semigroup m) => Extend (TracedT m w) where-  extend f = TracedT . extend (\wf m -> f (TracedT (fmap (. (<>) m) wf))) . runTracedT--instance (Comonad w, Semigroup m, Monoid m) => Comonad (TracedT m w) where-  extract (TracedT wf) = extract wf mempty--instance (Semigroup m, Monoid m) => ComonadTrans (TracedT m) where-  lower = fmap ($mempty) . runTracedT--instance (Semigroup m, Monoid m) => ComonadHoist (TracedT m) where-  cohoist = traced . extract . runTracedT--instance Distributive w => Distributive (TracedT m w) where-  distribute = TracedT . fmap (\tma m -> fmap ($m) tma) . collect runTracedT--trace :: (Comonad w, Monoid m) => m -> TracedT m w a -> a-trace m (TracedT wf) = extract wf m--listen :: Functor w => TracedT m w a -> TracedT m w (a, m)-listen = TracedT . fmap (\f m -> (f m, m)) . runTracedT--listens :: Functor w => (m -> b) -> TracedT m w a -> TracedT m w (a, b)-listens g = TracedT . fmap (\f m -> (f m, g m)) . runTracedT --censor :: Functor w => (m -> m) -> TracedT m w a -> TracedT m w a-censor g = TracedT . fmap (. g) . runTracedT--#ifdef __GLASGOW_HASKELL__--instance (Typeable s, Typeable1 w) => Typeable1 (TracedT s w) where-  typeOf1 dswa = mkTyConApp tracedTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: TracedT s w a -> s-      s = undefined-      w :: TracedT s w a -> w a-      w = undefined--tracedTTyCon :: TyCon-tracedTTyCon = mkTyCon "Control.Comonad.Trans.Traced.TracedT"-{-# NOINLINE tracedTTyCon #-}--#endif
− Control/Comonad/Trans/Traced/Memo.hs 
@@ -1,109 +0,0 @@-{-# LANGUAGE CPP #-}--------------------------------------------------------------------------------- |--- Module      :  Control.Comonad.Trans.Traced.Memo--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------ The memoized traced comonad transformer (aka the cowriter or --- exponential comonad transformer).---------------------------------------------------------------------------------module Control.Comonad.Trans.Traced.Memo-  ( -  -- * Traced comonad-    Traced-  , traced-  , runTraced-  -- * Traced comonad transformer-  , TracedT-  , tracedT-  , runTracedT-  -- * Operations-  , trace-  , listen-  , listens-  , censor-  ) where--import Control.Applicative-import Control.Monad.Instances-import Control.Monad (ap)-import Control.Comonad-import Control.Comonad.Hoist.Class-import Control.Comonad.Trans.Class-import Data.Functor-import Data.Functor.Apply-import Data.Functor.Identity-import Data.Semigroup-import Data.Typeable--type Traced m = TracedT m Identity--traced :: Monoid m => (m -> a) -> Traced m a-traced f = TracedT (Identity f) (Identity (f mempty))--runTraced :: Traced m a -> m -> a-runTraced (TracedT (Identity f) _) = f--data TracedT m w a = TracedT (w (m -> a)) (w a)--runTracedT :: TracedT m w a -> w (m -> a)-runTracedT (TracedT wf _) = wf--tracedT :: (Functor w, Monoid m) => w (m -> a) -> TracedT m w a -tracedT wf = TracedT wf (fmap ($ mempty) wf)--instance Functor w => Functor (TracedT m w) where-  fmap g (TracedT wf wa) = TracedT ((g .) <$> wf) (g <$> wa)--instance Apply w => Apply (TracedT m w) where-  TracedT wf wf' <.> TracedT wa wa' = TracedT (ap <$> wf <.> wa) (wf' <.> wa')--instance Applicative w => Applicative (TracedT m w) where-  pure a = TracedT (pure (const a)) (pure a)-  TracedT wf wf' <*> TracedT wa wa' = TracedT (ap <$> wf <*> wa) (wf' <*> wa')--instance (Extend w, Monoid m) => Extend (TracedT m w) where-  extend f = tracedT . extend (\wf m -> f (tracedT (fmap (. mappend m) wf))) . runTracedT--instance (Comonad w, Monoid m) => Comonad (TracedT m w) where-  extract (TracedT _ wa) = extract wa--instance ComonadTrans (TracedT m) where-  lower (TracedT _ wa) = wa--instance ComonadHoist (TracedT m) where-  cohoist (TracedT wf wa) = TracedT (Identity (extract wf)) (Identity (extract wa))--trace :: (Comonad w, Monoid m) => m -> TracedT m w a -> a-trace m (TracedT wf _) = extract wf m--listen :: (Functor w, Monoid m) => TracedT m w a -> TracedT m w (a, m)-listen (TracedT wf wa) = TracedT (fmap (\f m -> (f m, m)) wf) (fmap (\a -> (a,mempty)) wa)--listens :: (Functor w, Monoid m) => (m -> b) -> TracedT m w a -> TracedT m w (a, b)-listens g (TracedT wf wa) = TracedT (fmap (\f m -> (f m, g m)) wf) (fmap (\a -> (a, g mempty)) wa)--censor :: (Functor w, Monoid m) => (m -> m) -> TracedT m w a -> TracedT m w a-censor g = tracedT . fmap (. g) . runTracedT--#ifdef __GLASGOW_HASKELL__--instance (Typeable s, Typeable1 w) => Typeable1 (TracedT s w) where-  typeOf1 dswa = mkTyConApp tracedTTyCon [typeOf (s dswa), typeOf1 (w dswa)]-    where-      s :: TracedT s w a -> s-      s = undefined-      w :: TracedT s w a -> w a-      w = undefined--tracedTTyCon :: TyCon-tracedTTyCon = mkTyCon "Control.Comonad.Trans.Traced.Memo.TracedT"-{-# NOINLINE tracedTTyCon #-}--#endif
− Data/Functor/Composition.hs 
@@ -1,14 +0,0 @@-module Data.Functor.Composition -  ( Composition(..) ) where--import Data.Functor.Compose-  --- | We often need to distinguish between various forms of Functor-like composition in Haskell in order to please the type system.--- This lets us work with these representations uniformly.-class Composition o where-  decompose :: o f g x -> f (g x)-  compose :: f (g x) -> o f g x--instance Composition Compose where-  decompose = getCompose-  compose = Compose
− Data/Functor/Coproduct.hs 
@@ -1,64 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Data.Functor.Coproduct--- Copyright   :  (C) 2008-2011 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  provisional--- Portability :  portable------------------------------------------------------------------------------module Data.Functor.Coproduct-  ( Coproduct(..) -  , left-  , right-  , coproduct-  ) where--import Control.Comonad-import Data.Functor.Contravariant-import Data.Foldable-import Data.Traversable-import Data.Semigroup.Foldable-import Data.Semigroup.Traversable--newtype Coproduct f g a = Coproduct { getCoproduct :: Either (f a) (g a) }--left :: f a -> Coproduct f g a-left = Coproduct . Left--right :: g a -> Coproduct f g a-right = Coproduct . Right--coproduct :: (f a -> b) -> (g a -> b) -> Coproduct f g a -> b-coproduct f g = either f g . getCoproduct--instance (Functor f, Functor g) => Functor (Coproduct f g) where-  fmap f = Coproduct . coproduct (Left . fmap f) (Right . fmap f)--instance (Foldable f, Foldable g) => Foldable (Coproduct f g) where-  foldMap f = coproduct (foldMap f) (foldMap f)--instance (Foldable1 f, Foldable1 g) => Foldable1 (Coproduct f g) where-  foldMap1 f = coproduct (foldMap1 f) (foldMap1 f)--instance (Traversable f, Traversable g) => Traversable (Coproduct f g) where-  traverse f = coproduct-    (fmap (Coproduct . Left) . traverse f)  -    (fmap (Coproduct . Right) . traverse f)--instance (Traversable1 f, Traversable1 g) => Traversable1 (Coproduct f g) where-  traverse1 f = coproduct-    (fmap (Coproduct . Left) . traverse1 f)  -    (fmap (Coproduct . Right) . traverse1 f)-  -instance (Extend f, Extend g) => Extend (Coproduct f g) where-  extend f = Coproduct . coproduct-    (Left . extend (f . Coproduct . Left))-    (Right . extend (f . Coproduct . Right))--instance (Comonad f, Comonad g) => Comonad (Coproduct f g) where-  extract = coproduct extract extract--instance (Contravariant f, Contravariant g) => Contravariant (Coproduct f g) where-  contramap f = Coproduct . coproduct (Left . contramap f) (Right . contramap f)
+ README.markdown view
@@ -0,0 +1,19 @@+comonad-transformers+==========++[![Build Status](https://secure.travis-ci.org/ekmett/comonad-transformers.png?branch=master)](http://travis-ci.org/ekmett/comonad-transformers)++This package provides a standard set of comonad transformers for Haskell.++Like the `transformers` package this package is `Haskell 98`.++Clases for these types are provided by the [`comonads-fd`](/ekmett/comonads-fd) package.++Contact Information+-------------------++Contributions and bug reports are welcome!++Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.++-Edward Kmett
comonad-transformers.cabal view
@@ -1,6 +1,6 @@ name:          comonad-transformers category:      Control, Comonads-version:       2.0.3+version:       4.0 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -8,56 +8,21 @@ maintainer:    Edward A. Kmett <ekmett@gmail.com> stability:     provisional homepage:      http://github.com/ekmett/comonad-transformers/-copyright:     Copyright (C) 2008-2011 Edward A. Kmett-synopsis:      Comonad transformers-description:   Comonad transformers+bug-reports:   http://github.com/ekmett/comonad-transformers/issues+copyright:     Copyright (C) 2008-2013 Edward A. Kmett+synopsis:      This package has been merged into comonad 4.0+description:   This package has been merged into comonad 4.0 build-type:    Simple-extra-source-files: coq/Store.v+extra-source-files:+  README.markdown+  .travis.yml+  .ghci+  .gitignore+  .vim.custom  source-repository head   type: git   location: git://github.com/ekmett/comonad-transformers.git -flag DeriveDataTypeable-  manual: False-  default: True- library-  build-depends: -    base          >= 4       && < 5,-    comonad       >= 1.1.1.1 && < 1.2,-    containers    >= 0.3     && < 0.5,-    contravariant >= 0.1.2   && < 0.2,-    distributive  >= 0.2     && < 0.3,-    semigroupoids >= 1.2.6.1 && < 1.3,-    semigroups    >= 0.8     && < 0.9,-    transformers  >= 0.2.0   && < 0.3--  if flag(DeriveDataTypeable)-    extensions: DeriveDataTypeable-    cpp-options: -DLANGUAGE_DeriveDataTypeable--  extensions: CPP--  exposed-modules:-    Control.Comonad.Hoist.Class-    Control.Comonad.Trans.Class-    Control.Comonad.Trans.Discont-    Control.Comonad.Trans.Discont.Lazy-    Control.Comonad.Trans.Discont.Strict-    Control.Comonad.Trans.Discont.Memo-    Control.Comonad.Trans.Env-    Control.Comonad.Trans.Env.Lazy-    Control.Comonad.Trans.Env.Strict-    Control.Comonad.Trans.Identity-    Control.Comonad.Trans.Store-    Control.Comonad.Trans.Store.Lazy-    Control.Comonad.Trans.Store.Strict-    Control.Comonad.Trans.Store.Memo-    Control.Comonad.Trans.Traced-    Control.Comonad.Trans.Traced.Memo--    Data.Functor.Coproduct-    Data.Functor.Composition--  ghc-options:      -Wall +  build-depends: base >= 4 && < 5, comonad >= 4
− coq/Store.v 
@@ -1,96 +0,0 @@-(* Proof StoreT forms a comonad -- Russell O'Connor *)--Set Implict Arguments.-Unset Strict Implicit.--Require Import FunctionalExtensionality.--Record Comonad (w : Type -> Type) : Type :=- { extract : forall a, w a -> a- ; extend : forall a b, (w a -> b) -> w a -> w b- ; law1 : forall a x, extend _ _ (extract a) x = x- ; law2 : forall a b f x, extract b (extend a _ f x) = f x- ; law3 : forall a b c f g x, extend b c f (extend a b g x) = extend a c (fun y => f (extend a b g y)) x- }.--Section StoreT.--Variables (s : Type) (w:Type -> Type).-Hypothesis wH : Comonad w.--Definition map a b f x := extend _ wH a b (fun y => f (extract _ wH _ y)) x.--Lemma map_extend : forall a b c f g x, map b c f (extend _ wH a b g x) = extend _ wH _ _ (fun y => f (g y)) x.-Proof.-intros a b c f g x.-unfold map.-rewrite law3.-apply equal_f.-apply f_equal.-extensionality y.-rewrite law2.-reflexivity.-Qed.--Record StoreT (a:Type): Type := mkStoreT-  {store : w (s -> a)-  ;loc   : s}.--Definition extractST a (x:StoreT a) : a := - extract _ wH _ (store _ x) (loc _ x).--Definition mapST a b (f:a -> b) (x:StoreT a) : StoreT b :=- mkStoreT _ (map _ _ (fun g x => f (g x)) (store _ x)) (loc _ x).--Definition duplicateST a (x:StoreT a) : StoreT (StoreT a) :=- mkStoreT _ (extend _ wH _ _ (mkStoreT _) (store _ x)) (loc _ x).--Let extendST := fun a b f x => mapST _ b f (duplicateST a x).--Lemma law1ST : forall a x, extendST _ _ (extractST a) x = x.-Proof.-intros a [v b].-unfold extractST, extendST, duplicateST, mapST.-simpl.-rewrite map_extend.-simpl.-replace (fun (y : w (s -> a)) (x : s) => extract w wH (s -> a) y x)- with (extract w wH (s -> a)).- rewrite law1.- reflexivity.-extensionality y.-extensionality x.-reflexivity.-Qed.--Lemma law2ST : forall a b f x, extractST b (extendST a _ f x) = f x.-Proof.-intros a b f [v c].-unfold extendST, mapST, extractST.-simpl.-rewrite map_extend.-rewrite law2.-reflexivity.-Qed.--Lemma law3ST : forall a b c f g x, extendST b c f (extendST a b g x) = extendST a c (fun y => f (extendST a b g y)) x.-Proof.-intros a b c f g [v d].-unfold extendST, mapST, extractST.-simpl.-repeat rewrite map_extend.-rewrite law3.-repeat (apply equal_f||apply f_equal).-extensionality y.-extensionality x.-rewrite map_extend.-reflexivity.-Qed.--Definition StoreTComonad : Comonad StoreT :=- Build_Comonad _ _ _ law1ST law2ST law3ST.--End StoreT.--Check StoreTComonad.-