packages feed

comonad-transformers (empty) → 0.1.0

raw patch · 11 files changed

+517/−0 lines, 11 filesdep +arraydep +basedep +comonadsetup-changed

Dependencies added: array, base, comonad, transformers

Files

+ Control/Comonad/Trans/Class.hs view
@@ -0,0 +1,21 @@+-----------------------------------------------------------------------------+-- |+-- 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
+ Control/Comonad/Trans/Discont.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE RankNTypes #-}+-----------------------------------------------------------------------------+-- |+-- 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+-- +-- Discont is the Density comonad of a constant functor, just as Cont is a +-- Codensity monad of a constant functor.+--+-- Note that Discont and Context are isomorphic, but DiscontT and ContextT are+-- not.+--+----------------------------------------------------------------------------+module Control.Comonad.Trans.Discont+  ( Discont+  , discont+  , runDiscont+  , DiscontT(..)+  , runDiscontT+  , callCV+  ) where++import Data.Functor.Identity+import Control.Comonad+import Control.Comonad.Trans.Class++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 w => Functor (DiscontT s w) where+  fmap g (DiscontT f ws) = DiscontT (g . f) ws++instance Comonad w => Comonad (DiscontT s w) where+  extract (DiscontT f ws) = f ws+  duplicate (DiscontT f ws) = DiscontT (DiscontT f) ws++instance ComonadTrans (DiscontT s) where+  lower (DiscontT f s) = extend f s++callCV :: DiscontT s w (DiscontT s w (DiscontT s w a -> a) -> b) -> b+callCV (DiscontT k s) = k s (DiscontT (\s' (DiscontT k' _) -> k' s') s)
+ Control/Comonad/Trans/Env.hs view
@@ -0,0 +1,52 @@+-----------------------------------------------------------------------------+-- |+-- 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 adds an extra value that can be accessed in the environment.+--+-- Left adjoint to the reader comonad.+----------------------------------------------------------------------------+module Control.Comonad.Trans.Env+  ( Env+  , env+  , runEnv+  , EnvT(..)+  , runEnvT+  , ask+  ) where++import Control.Comonad+import Control.Comonad.Trans.Class+import Data.Functor.Identity++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 Comonad w => Comonad (EnvT e w) where+  extract (EnvT _ wa) = extract wa+  duplicate p@(EnvT e wa) = EnvT e (p <$ wa)++instance ComonadTrans (EnvT e) where+  lower (EnvT _ wa) = wa++ask :: EnvT e w a -> e+ask (EnvT e _) = e
+ Control/Comonad/Trans/Identity.hs view
@@ -0,0 +1,29 @@+-----------------------------------------------------------------------------+-- |+-- 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++-- Provided by Control.Comonad to avoid an orphan+{-+instance Comonad w => Comonad (IdentityT w) where+  extract = extract . runIdentityT+  extend f (IdentityT m) = IdentityT (extend (f . IdentityT) m)+-}++-- Provided by Control.Comonad.Trans.Class to avoid an orphan+{-+instance ComonadTrans IdentityT where+  colift = IdentityT+-}
+ Control/Comonad/Trans/Store.hs view
@@ -0,0 +1,71 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Control.Comonad.Trans.Store+-- 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 (state-in-context/costate) comonad transformer is subject to the laws:+-- +-- > x = put (get x) x+-- > y = get (put y x)+-- > put y x = put y (put 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 +  ( +  -- * The Store comonad+    Store, store, runStore+  -- * The Store comonad transformer+  , StoreT(..), runStoreT+  -- * Operations+  , get+  , put+  , modify+  , experiment+  ) where++import Control.Comonad+import Control.Comonad.Trans.Class+import Data.Functor.Identity++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 Comonad w => Comonad (StoreT s w) where+  extract (StoreT wf s) = extract wf s+  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 ComonadTrans (StoreT s) where+  lower (StoreT f s) = fmap ($s) f++get :: StoreT s w a -> s+get (StoreT _ s) = s++put :: Comonad w => s -> StoreT s w a -> a +put s (StoreT f _) = extract f s++modify :: Comonad w => (s -> s) -> StoreT s w a -> a+modify f (StoreT g s) = extract g (f s)++experiment :: (Comonad w, Functor f) => f (s -> s) -> StoreT s w a -> f a+experiment fs (StoreT g s) = fmap (\f -> extract g (f s)) fs
+ Control/Comonad/Trans/Stream.hs view
@@ -0,0 +1,70 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Control.Comonad.Trans.Stream+-- Copyright   :  (C) 2008-2011 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  provisional+-- Portability :  portable+--+-- The f-branching stream comonad, aka the cofree comonad for a Functor f.+-- +-- Provided here as a comonad-transformer version of the 'ListT done right' +-- monad transformer.+----------------------------------------------------------------------------+module Control.Comonad.Trans.Stream +  ( +  -- * The Stream comonad+    Stream, stream, runStream+  -- * The Stream comonad transformer+  , StreamT(..)+  -- * Operations+  , tails+  , unfolds+  , unfoldsW+  ) where++import Control.Applicative+import Control.Comonad+import Control.Comonad.Trans.Class+import Data.Functor.Identity+import Data.Foldable+import Data.Monoid+import Data.Traversable++type Stream f = StreamT f Identity++stream :: a -> f (Stream f a) -> Stream f a +stream a as = StreamT (Identity (a, as))++runStream :: Stream f a -> (a, f (Stream f a))+runStream = runIdentity . runStreamT++data StreamT f w a = StreamT { runStreamT :: w (a, f (StreamT f w a)) }++instance (Functor w, Functor f) => Functor (StreamT f w) where+  fmap f = StreamT . fmap (\(a, as) -> (f a, fmap f <$> as)) . runStreamT++instance (Comonad w, Functor f) => Comonad (StreamT f w) where+  extract = fst . extract . runStreamT+  duplicate = StreamT . extend (\w -> (StreamT w, duplicate <$> snd (extract w))) . runStreamT+  extend f = StreamT . extend (\w -> (f (StreamT w), extend f <$> snd (extract w))) . runStreamT++instance Functor f => ComonadTrans (StreamT f) where+  lower = fmap fst . runStreamT++instance (Foldable w, Foldable f) => Foldable (StreamT f w) where+  foldMap f = foldMap (\(a, as) -> f a `mappend` foldMap (foldMap f) as) . runStreamT++instance (Traversable w, Traversable f) => Traversable (StreamT f w) where+  traverse f (StreamT w) = StreamT <$> traverse (\(a, as) -> (,) <$> f a <*> traverse (traverse f) as) w++tails :: Comonad w => StreamT f w a -> f (StreamT f w a)+tails = snd . extract . runStreamT++unfolds :: Functor f => (a -> (b, f a)) -> a -> Stream f b+unfolds f a = let (h, t) = f a in stream h (unfolds f <$> t)++unfoldsW :: (Comonad w, Functor f) => (w a -> (b, f a)) -> w a -> StreamT f w b+unfoldsW f = StreamT . extend (\s -> let (h, t) = f s in (h, fmap (\a -> unfoldsW f (a <$ s)) t))
+ Control/Comonad/Trans/Traced.hs view
@@ -0,0 +1,52 @@+-----------------------------------------------------------------------------+-- |+-- 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+  ) where++import Control.Comonad+import Control.Comonad.Trans.Class+import Data.Functor.Identity+import Data.Monoid++type Traced m = TracedT m Identity++traced :: (m -> a) -> Traced m a+traced f = TracedT (Identity f)++runTraced :: Monoid m => 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 (Comonad w, Monoid m) => Comonad (TracedT m w) where+  extract (TracedT wf) = extract wf mempty+  extend f = TracedT . extend (\wf m -> f (TracedT (fmap (. mappend m) wf))) . runTracedT++instance Monoid m => ComonadTrans (TracedT m) where+  lower = fmap ($mempty) . runTracedT++trace :: (Comonad w, Monoid m) => m -> TracedT m w a -> a+trace m (TracedT wf) = extract wf m
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright 2008-2011 Edward Kmett++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ Setup.lhs view
@@ -0,0 +1,7 @@+#!/usr/bin/runhaskell+> module Main (main) where++> import Distribution.Simple++> main :: IO ()+> main = defaultMain
+ comonad-transformers.cabal view
@@ -0,0 +1,33 @@+name:          comonad-transformers+category:      Control, Comonads+version:       0.1.0+license:       BSD3+cabal-version: >= 1.2+license-file:  LICENSE+author:        Edward A. Kmett+maintainer:    Edward A. Kmett <ekmett@gmail.com>+stability:     provisional+homepage:      http://comonad.com/reader/+copyright:     Copyright (C) 2008-2011 Edward A. Kmett+synopsis:      Comonad transformers+description:   Comonad transformers+build-type:    Simple+extra-source-files: coq/Store.v++library+  build-depends: +    base > 4 && < 5,+    array >= 0.3.0.1 && < 0.4,+    comonad >= 0.1.0 && < 0.2,+    transformers >= 0.2.0 && <= 0.3++  exposed-modules:+    Control.Comonad.Trans.Class+    Control.Comonad.Trans.Discont+    Control.Comonad.Trans.Env+    Control.Comonad.Trans.Identity+    Control.Comonad.Trans.Store+    Control.Comonad.Trans.Traced+    Control.Comonad.Trans.Stream++  ghc-options:      -Wall
+ coq/Store.v view
@@ -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.+