Initial merge of comonad-transformers

comonad.cabal

@@ -1,6 +1,6 @@
 name:          comonad
 category:      Control, Comonads
-version:       3.1
+version:       3.2
 license:       BSD3
 cabal-version: >= 1.10
 license-file:  LICENSE
@@ -15,8 +15,11 @@ synopsis:      Haskell 98 compatible comonads
 description:   Haskell 98 compatible comonads
 build-type:    Custom
 extra-source-files:
+  .ghci
   .gitignore
   .travis.yml
+  .vim.custom
+  coq/Store.v
   README.markdown
   CHANGELOG.markdown
   examples/History.hs
@@ -36,14 +39,26 @@ library
   other-extensions: CPP
 
   build-depends:
-    base         >= 4       && < 5,
-    transformers >= 0.2     && < 0.4,
-    containers   >= 0.3     && < 0.6,
-    semigroups   >= 0.8.3   && < 1,
-    tagged       >= 0.1     && < 1
+    base          >= 4       && < 5,
+    containers    >= 0.3     && < 0.6,
+    contravariant >= 0.2.0.1 && < 1,
+    distributive  >= 0.2.2   && < 1,
+    semigroups    >= 0.8.3.1 && < 1,
+    tagged        >= 0.1     && < 1,
+    transformers  >= 0.2     && < 0.4
 
   exposed-modules:
     Control.Comonad
+    Control.Comonad.Hoist.Class
+    Control.Comonad.Trans.Class
+    Control.Comonad.Trans.Env
+    Control.Comonad.Trans.Identity
+    Control.Comonad.Trans.Store
+    Control.Comonad.Trans.Traced
+    Data.Functor.Coproduct
+    Data.Functor.Composition
+
+  extensions: CPP
 
   ghc-options: -Wall
 
@@ -65,4 +80,3 @@ test-suite doctests
 
   if impl(ghc<7.6.1)
     ghc-options: -Werror
-

coq/Store.v

@@ -0,0 +1,96 @@
+(* 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.
+

src/Control/Comonad/Hoist/Class.hs

@@ -0,0 +1,29 @@
+-----------------------------------------------------------------------------
+-- |
+-- 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

src/Control/Comonad/Trans/Class.hs

@@ -0,0 +1,26 @@
+{-# LANGUAGE CPP #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-----------------------------------------------------------------------------
+-- |
+-- 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 :: Comonad w => t w a -> w a
+
+-- avoiding orphans
+instance ComonadTrans IdentityT where
+  lower = runIdentityT

src/Control/Comonad/Trans/Cofree.hs

@@ -0,0 +1,167 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702
+{-# LANGUAGE Trustworthy #-}
+#endif
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Cofree
+-- Copyright   :  (C) 2008-2012 Edward Kmett,
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- Haskell 98 cofree comonads
+--
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Cofree
+  ( Cofree(..)
+  , section
+  , unwrap
+  , coiter
+  , unfold
+  ) where
+
+import Control.Applicative
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Data.Functor.Bind
+import Data.Distributive
+import Data.Foldable
+import Data.Semigroup
+import Data.Traversable
+import Data.Semigroup.Foldable
+import Data.Semigroup.Traversable
+
+#ifdef GHC_TYPEABLE
+import Data.Data
+#endif
+
+infixr 5 :<
+
+data Cofree f a = a :< f (Cofree f a)
+
+unwrap :: Cofree f a -> f (Cofree f a)
+unwrap (_ :< as) = as
+
+coiter :: Functor f => (a -> f a) -> a -> Cofree f a
+coiter psi a = a :< (coiter psi <$> psi a)
+
+unfold :: Functor f => (b -> (a, f b)) -> b -> Cofree f a
+unfold f c = case f c of
+  (x, d) -> x :< fmap (unfold f) d
+
+instance Distributive f => Distributive (Cofree f) where
+  distribute w = fmap extract w :< fmap distribute (collect unwrap w)
+
+instance Functor f => Functor (Cofree f) where
+  fmap f (a :< as) = f a :< fmap (fmap f) as
+  b <$ (_ :< as) = b :< fmap (b <$) as
+
+instance Functor f => Extend (Cofree f) where
+  extended f w = f w :< fmap (extended f) (unwrap w)
+  duplicated w = w :< fmap duplicated (unwrap w)
+
+instance Functor f => Comonad (Cofree f) where
+  extend f w = f w :< fmap (extend f) (unwrap w)
+  duplicate w = w :< fmap duplicate (unwrap w)
+  extract (a :< _) = a
+
+instance ComonadTrans Cofree where
+  lower (_ :< as) = fmap extract as
+
+-- | lower . section = id
+section :: Comonad f => f a -> Cofree f a
+section as = extract as :< extend section as
+
+instance Apply f => Apply (Cofree f) where
+  (f :< fs) <.> (a :< as) = f a :< ((<.>) <$> fs <.> as)
+  (f :< fs) <.  (_ :< as) = f :< ((<. ) <$> fs <.> as)
+  (_ :< fs)  .> (a :< as) = a :< (( .>) <$> fs <.> as)
+
+instance ComonadApply f => ComonadApply (Cofree f) where
+  (f :< fs) <@> (a :< as) = f a :< ((<@>) <$> fs <@> as)
+  (f :< fs) <@  (_ :< as) = f :< ((<@ ) <$> fs <@> as)
+  (_ :< fs)  @> (a :< as) = a :< (( @>) <$> fs <@> as)
+
+instance Applicative f => Applicative (Cofree f) where
+  pure a = as where as = a :< pure as
+  (f :< fs) <*> (a :< as) = f a :< ((<*>) <$> fs <*> as)
+  (f :< fs) <*  (_ :< as) = f :< ((<* ) <$> fs <*> as)
+  (_ :< fs)  *> (a :< as) = a :< (( *>) <$> fs <*> as)
+
+instance (Show (f (Cofree f a)), Show a) => Show (Cofree f a) where
+  showsPrec d (a :< as) = showParen (d > 5) $
+    showsPrec 6 a . showString " :< " . showsPrec 5 as
+
+instance (Read (f (Cofree f a)), Read a) => Read (Cofree f a) where
+  readsPrec d r = readParen (d > 5)
+                          (\r' -> [(u :< v,w) |
+                                  (u, s) <- readsPrec 6 r',
+                                  (":<", t) <- lex s,
+                                  (v, w) <- readsPrec 5 t]) r
+
+instance (Eq (f (Cofree f a)), Eq a) => Eq (Cofree f a) where
+  a :< as == b :< bs = a == b && as == bs
+
+instance (Ord (f (Cofree f a)), Ord a) => Ord (Cofree f a) where
+  compare (a :< as) (b :< bs) = case compare a b of
+    LT -> LT
+    EQ -> compare as bs
+    GT -> GT
+
+instance Foldable f => Foldable (Cofree f) where
+  foldMap f (a :< as) = f a `mappend` foldMap (foldMap f) as
+
+instance Foldable1 f => Foldable1 (Cofree f) where
+  foldMap1 f (a :< as) = f a <> foldMap1 (foldMap1 f) as
+
+instance Traversable f => Traversable (Cofree f) where
+  traverse f (a :< as) = (:<) <$> f a <*> traverse (traverse f) as
+
+instance Traversable1 f => Traversable1 (Cofree f) where
+  traverse1 f (a :< as) = (:<) <$> f a <.> traverse1 (traverse1 f) as
+
+#ifdef GHC_TYPEABLE
+instance (Typeable1 f) => Typeable1 (Cofree f) where
+  typeOf1 dfa = mkTyConApp cofreeTyCon [typeOf1 (f dfa)]
+    where
+      f :: Cofree f a -> f a
+      f = undefined
+
+instance (Typeable1 f, Typeable a) => Typeable (Cofree f a) where
+  typeOf = typeOfDefault
+
+cofreeTyCon :: TyCon
+#if __GLASGOW_HASKELL < 704
+cofreeTyCon = mkTyCon "Control.Comonad.Trans.Cofree.Cofree"
+#else
+cofreeTyCon = mkTyCon3 "comonad-transformers" "Control.Comonad.Trans.Cofree" "Cofree"
+#endif
+{-# NOINLINE cofreeTyCon #-}
+
+instance
+  ( Typeable1 f
+  , Data (f (Cofree f a))
+  , Data a
+  ) => Data (Cofree f a) where
+    gfoldl f z (a :< as) = z (:<) `f` a `f` as
+    toConstr _ = cofreeConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (k (z (:<)))
+        _ -> error "gunfold"
+    dataTypeOf _ = cofreeDataType
+    dataCast1 f = gcast1 f
+
+cofreeConstr :: Constr
+cofreeConstr = mkConstr cofreeDataType ":<" [] Infix
+{-# NOINLINE cofreeConstr #-}
+
+cofreeDataType :: DataType
+cofreeDataType = mkDataType "Control.Comonad.Trans.Cofree.Cofree" [cofreeConstr]
+{-# NOINLINE cofreeDataType #-}
+#endif