packages feed

effect-monad (empty) → 0.6

raw patch · 38 files changed

+1461/−0 lines, 38 filesdep +basedep +ghc-primdep +type-level-setssetup-changed

Dependencies added: base, ghc-prim, type-level-sets

Files

+ LICENSE view
@@ -0,0 +1,26 @@+Copyright (c) 2014, Dominic Orchard++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * 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.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"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 COPYRIGHT+OWNER 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.hs view
@@ -0,0 +1,6 @@+module Main (main) where++import Distribution.Simple++main :: IO ()+main = defaultMain
+ effect-monad.cabal view
@@ -0,0 +1,52 @@+name:                   effect-monad+version:                0.6+synopsis:               Embeds effect systems into Haskell using parameteric effect monads+description:            +   Provides the 'parametric effect monad' structure to Haskell with a number of analogous of familiar monads (Reader, Writer, State, Maybe, Counter, Update) and a wrapper over normal monads (Control.Effect.Monad). This provides a way to embed effect systems into Haskell. For more information see with paper \"Embedding effect systems in Haskell\" by Orchard and Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell, 2014) and the examples in <https://github.com/dorchard/effect-monad/tree/master/examples>. +  .+  (note, this package was previously called 'ixmonad' until September 2014). ++license:                BSD3+license-file:           LICENSE+category:               Control, Monads+copyright:              2013-14 University of Cambridge+author:                 Dominic Orchard+maintainer:             Dominic Orchard+stability:              experimental+build-type:             Simple+cabal-version:          >= 1.6+tested-with:            GHC == 7.8.2++extra-source-files:     examples/*.hs+++source-repository head+  type: git+  location: https://github.com/dorchard/effect-monad++library+  hs-source-dirs:       src+++  exposed-modules:      Control.Coeffect+                        Control.Coeffect.Coreader+                        Control.Effect+                        Control.Effect.Cond+                        Control.Effect.Counter+                        Control.Effect.CounterNat+                        Control.Effect.Maybe+                        Control.Effect.Monad+                        Control.Effect.Parameterised+                        Control.Effect.Reader+                        Control.Effect.ReadOnceReader+                        Control.Effect.State+                        Control.Effect.Update+                        Control.Effect.Vector+                        Control.Effect.WriteOnceWriter+                        Control.Effect.Writer+                        Control.Effect.Helpers.List+                        +  build-depends:        base < 5,+                        ghc-prim,+                        type-level-sets >= 0.5+
+ examples/ArrayReader.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances,+             FlexibleContexts, DataKinds, UndecidableInstances, ScopedTypeVariables #-}++module ArrayReader where ++import GHC.TypeLits +import Data.Array+import Prelude hiding (Monad(..)) ++import Data.Proxy+import Control.Effect+import Data.Type.Set++-- Array with a cursor+data CArray (x::[*]) a = MkA (Array Int a, Int) ++-- Computations from 'a' to 'b' with an array parameter+data Stencil a (r::[*]) b = Stencil (CArray r a -> b)++-- Get the nth index from the array, relative to the 'cursor'+ix :: (ToValue (IntT x) Int) => IntT x -> Stencil a '[IntT x] a+ix n = Stencil (\(MkA (a, cursor)) -> a ! (cursor + toValue n))++instance Effect (Stencil a) where+    type Inv (Stencil a) s t = ()+    type Plus (Stencil a) s t = Union s t -- append specs+    type Unit (Stencil a)     = '[]       -- empty spec++    (Stencil f) >>= k = +        Stencil (\(MkA a) -> let (Stencil f') = k (f (MkA a))+                                 in f' (MkA a))+    return a = Stencil (\_ -> a)++data Sign n = Pos n | Neg n+data IntT (n :: Sign Nat) = IntT++class ToValue t t' where+    toValue :: t -> t'++instance (KnownNat n) => ToValue (IntT (Pos (n :: Nat))) Int where+    toValue _ = fromInteger $ natVal (Proxy :: (Proxy n))++instance (KnownNat n) => ToValue (IntT (Neg (n :: Nat))) Int where+    toValue _ = - (fromInteger $ natVal (Proxy :: (Proxy n)))++type instance Cmp (IntT (Pos n)) (IntT (Pos m)) = CmpNat n m+type instance Cmp (IntT (Neg n)) (IntT (Neg m)) = CmpNat n m+type instance Cmp (IntT (Pos n)) (IntT (Neg m)) = GT+type instance Cmp (IntT (Neg n)) (IntT (Pos m)) = LT+
+ examples/Counter.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE RebindableSyntax, EmptyDataDecls, GADTs, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, TypeOperators #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.Counter++import Debug.Trace++{- ++The 'Counter' indexed monad is useful for counting computations+of a particular kind (e.g., counting number of calls to a websocket)+or estimating resource usage (e.g., a websocket call is more expensive+than a disk write). ++By default, zero counts are tracked, e.g., ++-}++foo :: Counter Z Int+foo = do x <- return 2+         y <- return 4+         return (x + y)++{- the 'tick' function lifts a value to be counted once, e.g. -}++-- foo2 :: Counter (S Z) Int+foo2 = do x <- tick 2+          y <- return 3+          return (x * y)++{- This can be used for other cool things, like proving that 'map' has + linear complexity of 'map' at the type-level! ++For this we need sized lists:+-}++data Vector n a where+    Nil :: Vector Z a+    Cons :: a -> Vector n a -> Vector (S n) a++type family n :* m +type instance Z :* m = Z+type instance (S n) :* m = m :+ (n :* m)++{- map' is then defined as follows -}++map' :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)+map' f Nil         = return Nil+map' f (Cons x xs) = do x' <- f x+                        xs' <- map' f xs+                        return (Cons x' xs')++{- The types show us that if the function counts 't' things, then applying 'map'+to an n-vector counts 'tn' things -}++{- Example: web socket calls- how many do we do per instances #-}++call :: Int -> Counter (S Z) ()+call = undefined++singleCall = map' call (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))++doubleCall x = map' (\n -> do {a <- call n; b <- call n; return ()}) x++doubleCallExample = doubleCall (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))++{- are we definitely linear in the number of elements, even if we have closed over the vector? -}++class LT n m+instance LT Z (S n)+instance LT n m => LT (S n) (S m)++lineraMap :: LT t n => (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)+lineraMap = map'
+ examples/CounterNat.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, GADTs, TypeFamilies, UndecidableInstances #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.CounterNat++import GHC.TypeLits++import Debug.Trace++{- ++The 'Counter' indexed monad is useful for counting computations+of a particular kind (e.g., counting number of calls to a websocket)+or estimating resource usage (e.g., a websocket call is more expensive+than a disk write). ++By default, zero counts are tracked, e.g., -}++foo :: Counter 0 Int+foo = do x <- return 2+         y <- return 4+         return (x + y)++{- the 'one' function lifts a value to be counted once, e.g.  -}++-- foo2 :: Counter (S Z) Int+foo2 = do x <- tick 2+          y <- return 3+          return (x * y) ++{- This can be used for other cool things, like proving that 'map' has + linear complexity of 'map' at the type-level! ++For this we need sized lists:+-}+++data Vector (n :: Nat) a where+    Nil :: Vector 0 a+    Cons :: a -> Vector n a -> Vector (n + 1) a++type family (n :: Nat) :* (m :: Nat) :: Nat where+       0 :* m = 0+       n :* m = m + ((n - 1) :* m)++{- map' is then defined as follows -}++{- CAN'T TYPE CHECK, see Counter.hs ++map' :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)+map' f Nil         = return Nil+map' f (Cons x xs) = do x' <- f x+                        xs' <- map' f xs+                        return (Cons x' xs')++-}+
+ examples/ImplicitP.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE ImplicitParams, DataKinds, RebindableSyntax, TypeOperators #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.Reader++foo :: (Num a, ?x :: a, ?y :: a) => a -> a+foo z = ?x + ?y++fooM :: (Num a) => a -> Reader '["?x" :-> a, "?y" :-> a] a+fooM z = do x <- ask (Var::(Var "?x"))+            y <- ask (Var::(Var "?y"))+            return (x + y + z)++foo' :: (Num a, ?y :: a) => a -> a+foo' = let ?x = 42+       in \z -> ?x + ?y + z++fooM' :: Num a => Reader '["?x" :-> a] (a -> Reader '["?y" :-> a] a)+fooM' = merge (\z -> do x <- ask (Var::(Var "?x"))+                        y <- ask (Var::(Var "?y"))+                        return (x + y + z))++with f x = runReader f x++fooM'' = fooM' `with` (Ext (Var :-> 42) Empty)++sum2 :: Num a => a -> Reader '["?y" :-> a] a+sum2 = let x = (Ext ((Var::(Var "?x")) :-> 42) Empty) +       in runReader (merge (\z -> do x <- ask (Var::(Var "?x"))+                                     y <- ask (Var::(Var "?y"))+                                     return (x + y + z))) x++
+ examples/Maybe.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.Cond+import Control.Effect.Maybe++headM x = ifM (x == []) (INothing) (IJust (head x))++foo x y = do x' <- headM x+             y' <- headM y+             return [x', y']
+ examples/Monad.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE TypeFamilies, RebindableSyntax #-}++import Control.Effect+import Control.Effect.Monad+import Prelude hiding (Monad(..)) ++putStrLn' = Wrap . putStrLn++printer = do putStrLn' "Hello"+             putStrLn' "I am really regular IO monad"+             putStrLn' "hiding as the free indexed monad version"+             return ()
+ examples/Problem1.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE NoMonomorphismRestriction, FlexibleContexts #-}++import Control.Monad.State.Lazy++incSC :: (Monad m) => StateT Int m ()+incSC = do x <- get+           put (x + 1)++writeS :: (Monad m) => [a] -> StateT [a] m ()+writeS y = do x <- get+              put (x ++ y)++write :: (Monad m) => [a] -> StateT [a] (StateT Int m) ()+write x = do  writeS x+              lift $ incSC++hellow = do write "hello"+            write " "+            write "world"++runHellow = runStateT (runStateT hellow "") 0++-- prog2 :: (Monad m) => StateT Int (StateT String (StateT Int (StateT String m))) ()++hellowCount = do hellow+                 lift $ lift $ incSC++runHellowCount = runStateT (runStateT (runStateT hellowCount "") 0) 1++
+ examples/ReadOnceReader.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.Cond+import Control.Effect.ReadOnceReader++foo = do x <- ask+         y <- ask +         return ("Name " ++ x ++ " age " ++ (show y))++--foo_eval = foo (HCons' 'a' (HCons' "bc" HNil'))++foo2 = do x <- ask +          y <- ask+          xs <- ask+          return (x : (y : xs))++foo2' = do x <- ask +           xs' <- do y <- ask+                     xs <- ask+                     return (y:xs)+           return (x : xs')++foo2_eval foo2 = runReader foo2 (Cons 'a' (Cons 'b' (Cons "c" Nil)))++foo3 = do x <- ask+          ifM x ask (return 0)++foo3_eval = runReader foo3 (Cons False (Cons 42 Nil))
+ examples/Reader.hs view
@@ -0,0 +1,40 @@+{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction, DataKinds, TypeOperators, +   FlexibleContexts, ConstraintKinds #-}+import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.Reader++import GHC.TypeLits++{- Examples -}++-- foo :: Reader '["x" :-> a, "xs" :-> [a]] [a]+foo = do x <- ask (Var::(Var "x"))+         xs <- ask (Var::(Var "xs"))+         x' <- ask (Var::(Var "x"))+         return (x:x':xs)++init1 = Ext (Var :-> 1) (Ext (Var :-> [2, 3]) Empty)+runFoo = runReader foo init1++-- Examples with subeffecting (need to refine the types a bit to 'run')++bar :: (Subset '["x" :-> Int, "xs" :-> [Int]] t) => Reader t [Int]+bar = sub foo++init2 :: Set '["x" :-> Int, "xs" :-> [Int], "z" :-> a]+init2 =  Ext (Var :-> 1) (Ext (Var :-> [2, 3]) (Ext (Var :-> undefined) Empty))+runBar = runReader bar init2++-- Note: GHC currently has trouble with+--init2a = asSet (append init1 (Ext (Var :-> undefined) Empty))++{-+foo_b = do x <- ask (Var::(Var "x"))+           y <- ask (Var::(Var "x"))+           return (not x,not y)++foo_b = +-}++-- runFoob = runReader foo_b (Ext (Var :-> 1) (Ext (Var :-> [1,2,3]) Empty))
+ examples/Solution1-alt.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}++import Control.Monad.State.Lazy++class Monad m => Streaming a m where+    writeS :: [a] -> m ()++class Monad m => Counting m where+    incC :: m ()++-- write :: (Streaming a m, Counting m) => [a] -> m ()+write x = do { writeS x; incC }++instance Monad m => Streaming a (StateT [a] m) where+    writeS y = do x <- get+                  put (x ++ y)++instance Monad m => Counting (StateT Int m) where+    incC = do x <- get+              put (x + 1)++foo = runStateT 0 $ runStateT "" $ write "message"
+ examples/Solution1.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE FlexibleContexts, DataKinds, TypeOperators, +              RebindableSyntax, FlexibleInstances #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.State++c1_var = Var::(Var "c1")+c2_var = Var::(Var "c2")+o_var  = Var::(Var "out")++instance Show (Var "out") where+    show _ = "out"++instance Show (Var "c1") where+    show _ = "c1"++instance Show (Var "c2") where+    show _ = "c2"++incC :: Var v -> State '[v :-> Int :! RW] ()+incC var = do x <- get var+              put var (x + 1)++writeS :: [a] -> State '["out" :-> [a] :! RW] ()+writeS y = do x <- get o_var+              put o_var (x ++ y)++write ::  [a] -> State '["c1" :-> Int :! RW, "out" :-> [a] :! RW] ()+write x = do  writeS x+              incC c1_var++initState0 = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty)+runWrite = runState (write "hello") initState0++hellow = do write "hello"+            write " "+            write "world"++initState = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty)+runHellow = runState hellow initState++hellowCount = do hellow+                 incC c2_var++initState' = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (c2_var :-> ((1::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty))+runHellowCount = runState hellowCount initState'
+ examples/Solution2.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, FlexibleInstances, +              ConstraintKinds, FlexibleContexts, TypeFamilies #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Data.Type.Set+import Control.Effect.State+import GHC.Conc.Sync++parMap :: (IsSet f, StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] +-- parMap k [] = sub (return [])+parMap k [x] = do y <- k x+                  return [y]+parMap k (x:xs) = do y  <- k x+                     ys <- parMap k xs+                     return (y : ys)+++parMap2 :: (StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] +parMap2 k [] = sub (return [])+parMap2 k (x:xs) = do (y, ys)  <- (k x) `par` parMap2 k xs+                      return (y : ys)
+ examples/State.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE DataKinds, RebindableSyntax, TypeOperators, FlexibleInstances #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.State++x_var = Var::(Var "x")+y_var = Var::(Var "y")++{- Computation with a read effect on variable "x" and a read-write (update) effect on variable "y" -}+foo :: State '["x" :-> Int :! R, "y" :-> [Int] :! RW] [Int]+foo = do x <- get x_var+         y <- get y_var+         put y_var (x:y)+         z <- get y_var+         return (x:z)++foo_run = runState foo (Ext (x_var :-> (1 :! Eff)) (Ext (y_var :-> ([2,3] :! Eff)) Empty))++foo2 :: State '["x" :-> Int :! RW] Int+foo2 = do x <- get x_var+          put x_var (x+1)+          return x++foo2_run = (runState foo2) (Ext (x_var :-> 10 :! Eff) Empty)+
+ examples/StencilSpecs.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE RebindableSyntax, GADTs, TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}++import Prelude hiding (Monad(..))++import GHC.TypeLits hiding (Nat)+import Data.Type.Set+import Control.Effect+import ArrayReader++localMean :: (Num a, Fractional a) => Stencil a (Symmetrical 1) a+--localMean :: (Num a, Fractional a) => Stencil a '[IntT (Neg 1), IntT (Pos 0), IntT (Pos 1)] a+localMean = do a <- ix (IntT :: (IntT (Pos 0)))+               b <- ix (IntT :: (IntT (Pos 1)))+               c <- ix (IntT :: (IntT (Neg 1)))+               return $ (a + b + c) / 3.0++fooFwd :: Num a => Stencil a (Forward 2) a+fooFwd = do a <- ix (IntT :: (IntT (Pos 0)))+            b <- ix (IntT :: (IntT (Pos 1)))+            c <- ix (IntT :: (IntT (Pos 2)))+            return $ a + b + c++ {-+--  The following causes a type error as it violates the specification+--  of symmetry++fooSymBroken :: (Num a) => StencilM a (Symmetrical (S Z)) a a+fooSymBroken = StencilM $ do a <- ix (Pos Z)+                             b <- ix (Pos (S Z))+                             return $ a + b +-}++-- fooFwd has a 'forward' pattern to depth of 2++-- Specification definitions++-- Forward-oriented stencil specification++type Forward sten = AsSet ((IntT (Pos 0)) ': (ForwardP sten))++-- ForwardP excludes the zero point+type family ForwardP depth where+            ForwardP 0 = '[]+            ForwardP n = (IntT (Pos n)) ': (ForwardP (n - 1))+++-- Symmetrical stencils (derived from Forward and Backward stencils of the same depth)++type Symmetrical depth = AsSet ((IntT (Pos 0)) ': (Append (ForwardP depth) (BackwardP depth)))++-- Backward-oriented stencils++type Backward sten = AsSet ((IntT (Pos 0)) ': (BackwardP sten))++type family  BackwardP depth where+             BackwardP 0 = '[]+             BackwardP n = (IntT (Neg n)) ': (BackwardP (n - 1))
+ examples/Update.hs view
@@ -0,0 +1,10 @@+{-# LANGUAGE RebindableSyntax, DataKinds #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.Update++foo :: Update (Just String) ()+foo = do put 42+         put "hello"+         return ()
+ examples/WriteOnceWriter.hs view
@@ -0,0 +1,9 @@+{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction #-}++import Prelude hiding (Monad(..))+import Control.Effect+import Control.Effect.WriteOnceWriter ++foo = do put 42+         put "hello"+         return ()
+ examples/Writer.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, RebindableSyntax, FlexibleInstances, +             ConstraintKinds, FlexibleContexts, TypeFamilies, ScopedTypeVariables+  #-}++import Control.Effect+import Control.Effect.Writer++import Data.Monoid++import Prelude hiding (Monad(..))++instance Monoid Int where+    mappend = (+)+    mempty  = 0++var_x = Var::(Var "x")+var_y = Var::(Var "y")++test :: Writer '["x" :-> Int, "y" :-> String] ()+test = do put var_x (42::Int)+          put var_y "hello"+          put var_x (58::Int)+          put var_y " world"++--test' :: forall a . (Monoid a, Num a) => a -> Writer '["x" :-> a, "y" :-> String] ()+test' (n::a) = do put var_x (42::a)+                  put var_y "hello"+                  put var_x (n::a)+                  put var_y " world"++{-- Polymorphism test -}+test2 :: (IsSet f, Unionable f '["y" :-> String]) => +         (Int -> Writer f t) -> Writer (Union f '["y" :-> String]) ()+test2 f = do f 3 +             put var_y ". hi"++{-- Subeffecting test -}+test3 :: Writer '["x" :-> Int, "y" :-> String, "z" :-> Int] ()+test3 = sub (test2 test')++foo2 :: (IsSet f, Unionable f '["x" :-> Int, "y" :-> t], Num a) => +       (a -> Writer f t) -> Writer (Union f '["x" :-> Int, "y" :-> t]) ()+foo2 f = do y <- f 3+            put var_x (42::Int)+            put var_y y+
+ examples/WriterM.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE FlexibleInstances #-}++import Data.Monoid++data Writer w a = Writer { runWriter :: (a, w) }++instance Monoid w => Monad (Writer w) where+   return a = Writer (a, mempty)+   (Writer (a, w)) >>= k = let (b, w') = runWriter (k a)+                           in Writer (b, w `mappend` w')++instance Monad (Writer (Maybe a)) where+   return a = Writer (a, Nothing)+   (Writer (a, w)) >>= k = let (b, w') = runWriter (k a)+                           in case w' of +                                Nothing -> Writer (b, w)+                                Just w' -> Writer (b, Just w')
+ src/Control/Coeffect.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}+{-# LANGUAGE ConstraintKinds, PolyKinds, ScopedTypeVariables, DataKinds #-}++module Control.Coeffect where ++import GHC.Prim++{- Coeffect parameterised comonad++Also called "indexed comonads". +For more details see "Coeffects: Unified static analysis of context-dependence"+by Petricek, Orchard, Mycroft: http://www.cl.cam.ac.uk/~dao29/publ/coeffects-icalp13.pdf++-}++{-| Specifies "parametric coeffect comonads" which are essentially comonads but+     annotated by a type-level monoid formed by 'Plus' and 'Unit' -}+class Coeffect (c :: k -> * -> *) where+    type Inv c (s :: k) (t :: k) :: Constraint+    type Inv c s t = ()++    type Unit c :: k +    type Plus c (s :: k) (t :: k) :: k++    {-| Coeffect-parameterised version of 'extract', +         annotated with the 'Unit m' effect, denoting pure contexts -}+    extract :: c (Unit c) a -> a++    {-| Coeffect-parameterise version of 'extend'.+        The two coeffec annotations 's' and 't' on its parameter computations+          get combined in the parameter computation by 'Plus' -}+    extend :: Inv c s t => (c t a -> b) -> c (Plus c s t) a -> c s b++{-| Zips two coeffecting computations together -}+class CoeffectZip (c :: k -> * -> *) where+    type Meet c (s :: k) (t :: k) :: k+    type CzipInv c (s :: k) (t :: k) :: Constraint+    czip :: CzipInv c s t => c s a -> c t b -> c (Meet c s t) (a, b)++{-| Specifies sub-coeffecting behaviour -}+class Subcoeffect (c :: k -> * -> *) s t where+    subco :: c s a -> c t a
+ src/Control/Coeffect/Coreader.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs, +             ConstraintKinds, TypeOperators, DataKinds, UndecidableInstances #-}++module Control.Coeffect.Coreader where++import Control.Coeffect+import Data.Type.Set++{-| Provides 'reader monad'-like behaviour but as a comonad, using an indexed+    version of the product comonad -}+data IxCoreader s a = IxR { runCoreader :: (a, Set s) }++instance Coeffect IxCoreader where+    type Inv IxCoreader s t = (Unionable s t, Split s t (Union s t))++    type Unit IxCoreader = '[]+    type Plus IxCoreader s t = Union s t++    extract (IxR (x, Empty)) = x+    extend k (IxR (x, st)) = let (s, t) = split st+                             in IxR (k (IxR (x, t)), s)++instance CoeffectZip IxCoreader where+    type Meet IxCoreader s t    = Union s t+    type CzipInv IxCoreader s t = (Unionable s t)++    czip (IxR (a, s)) (IxR (b, t)) = IxR ((a, b), union s t)+++{-| 'ask' for the value of variable 'v', e.g., 'ask (Var::(Var "x"))' -}+ask :: Var v -> IxCoreader '[v :-> a] b -> a+ask _ = \(IxR (_, Ext (Var :-> a) Empty)) -> a+
+ src/Control/Effect.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE KindSignatures, TypeFamilies, ConstraintKinds, PolyKinds, MultiParamTypeClasses #-}++module Control.Effect where ++import Prelude hiding (Monad(..))+import GHC.Prim+++{-| Specifies "parametric effect monads" which are essentially monads but+     annotated by a type-level monoid formed by 'Plus' and 'Unit' -}+class Effect (m :: k -> * -> *) where++   {-| Effect of a trivially effectful computation |-}+   type Unit m :: k+   {-| Cominbing effects of two subcomputations |-}+   type Plus m (f :: k) (g :: k) :: k++   {-| 'Inv' provides a way to give instances of 'Effect' their own constraints for '>>=' -}+   type Inv m (f :: k) (g :: k) :: Constraint+   type Inv m f g = ()++   {-| Effect-parameterised version of 'return'. Annotated with the 'Unit m' effect, +    denoting pure compuation -}+   return :: a -> m (Unit m) a++   {-| Effect-parameterise version of '>>=' (bind). Combines +    two effect annotations 'f' and 'g' on its parameter computations into 'Plus' -}+   (>>=) :: (Inv m f g) => m f a -> (a -> m g b) -> m (Plus m f g) b++   (>>) :: (Inv m f g) => m f a -> m g b -> m (Plus m f g) b+   x >> y = x >>= (\_ -> y)+  +fail = undefined++{-| Specifies subeffecting behaviour -}+class Subeffect (m :: k -> * -> *) f g where+    sub :: m f a -> m g a
+ src/Control/Effect/Cond.hs view
@@ -0,0 +1,22 @@+{-# LANGUAGE TypeFamilies, ConstraintKinds, PolyKinds #-}++module Control.Effect.Cond where++import GHC.Prim++{-| Provides a conditional using an 'alternation' operation, as opposed to using+   'Subeffect' -}++class Cond (m :: k -> * -> *) where+    type AltInv m (s :: k) (t :: k) :: Constraint+    type AltInv m s t = ()++    {-| Type family for describing how to combine effects of the two+        branches of an if -}+    type Alt m (s :: k) (t :: k) :: k ++    {-| Conditional on effectful operations -}+    ifM :: AltInv m s t => Bool -> m s a -> m t a -> m (Alt m s t) a++-- Related to indexed 'applicative' functors/idioms+--            which are indexed monoidal functors
+ src/Control/Effect/Counter.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators #-}++module Control.Effect.Counter(Z, S, Counter, tick, (:+)) where++import Control.Effect+import Prelude hiding (Monad(..))++{-| Provides a way to 'count' in the type-level with a monadic interface+    to sum up the individual counts of subcomputations -}++{-| Define type constructors for natural numbers -}+data Z+data S n++{-| The counter has no semantic meaning -}+data Counter n a = Counter { forget :: a }++{-| Type-level addition -}+type family n :+ m +type instance n :+ Z     = n+type instance n :+ (S m) = S (n :+ m)++instance Effect Counter where+    type Inv Counter n m = ()++    {-| Trivial effect annotation is 0 -}+    type Unit Counter = Z+    {-| Compose effects by addition -}+    type Plus Counter n m = n :+ m++    return a = Counter a+    (Counter a) >>= k = Counter . forget $ k a++{-| A 'tick' provides a way to increment the counter -}+tick :: a -> Counter (S Z) a+tick x = Counter x++
+ src/Control/Effect/CounterNat.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds #-}++module Control.Effect.CounterNat where++import Control.Effect+import GHC.TypeLits+import Prelude hiding (Monad(..))++{-| Provides a way to 'count' in the type-level with a monadic interface+    to sum up the individual counts of subcomputations. Instead +    of using our own inductive natural number typ, this uses the 'Nat' kind from 'GHC.TypeLits' -}++{-| The counter has no semantic meaning -}+data Counter (n :: Nat) a = Counter { forget :: a }++instance Effect Counter where+    type Inv Counter n m = ()+    {-| Trivial effect annotation is 0 -}+    type Unit Counter = 0+    {-| Compose effects by addition -}+    type Plus Counter n m = n + m++    return a = Counter a   +    (Counter a) >>= k = Counter . forget $ k a++{-| A 'tick' provides a way to increment the counter -}+tick :: a -> Counter 1 a+tick x = Counter x
+ src/Control/Effect/Helpers/List.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, +             MultiParamTypeClasses, FlexibleInstances #-}++module Control.Effect.Helpers.List where++data List (l::[*]) where+    Nil   :: List '[]+    Cons  :: x -> List xs -> List (x ': xs)++type family (:++) (s :: [*]) (t :: [*]) :: [*]+type instance '[] :++ ys       = ys+type instance (x ': xs) :++ ys = x ': (xs :++ ys)++append :: List s -> List t -> List (s :++ t)+append Nil xs = xs+append (Cons x xs) ys = Cons x (append xs ys)++class Split s t where+    split :: List (s :++ t) -> (List s, List t)++instance Split '[] xs where+    split xs = (Nil, xs)++instance Split xs ys => Split (x ': xs) ys where+    split (Cons x xs) = let (xs', ys') = split xs+                    in (Cons x xs', ys')
+ src/Control/Effect/Maybe.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE EmptyDataDecls, TypeFamilies, GADTs #-}++module Control.Effect.Maybe where++import Prelude hiding (Monad(..))++import Control.Effect+import Control.Effect.Cond++{-| Provides an indexed version of the |Maybe| monad -}++data F +data T +data U++data IMaybe p a where+    INothing ::               IMaybe F a +    IJust    :: a          -> IMaybe T a +    IDyn     :: IMaybe s a -> IMaybe U a -- dynamic partiality++instance Show a => Show (IMaybe p a) where+    show INothing  = "Nothing"+    show (IJust a) = "Just " ++ show a+    show (IDyn a)  = show a++instance Effect IMaybe where+  type Inv IMaybe s t = ()+  type Unit IMaybe = T++  type Plus IMaybe F s = F -- conjunction+  type Plus IMaybe T s = s+  type Plus IMaybe U s = U++  return x = IJust x++  -- static+  (IJust x) >>= k = k x+  INothing  >>= k = INothing++  -- dynamic (statically undecidable)+  (IDyn (IJust a))  >>= k = IDyn (k a)+  (IDyn (INothing)) >>= k = IDyn INothing +  +instance Cond IMaybe where+    type AltInv IMaybe s t = ()++    type Alt IMaybe T T = T+    type Alt IMaybe F F = F++    type Alt IMaybe F T = U+    type Alt IMaybe T F = U++    -- statically decidable+    ifM True  (IJust x) (IJust y) = IJust x+    ifM False (IJust x) (IJust y) = IJust y+    ifM True  INothing  INothing  = INothing+    ifM False INothing  INothing  = INothing++    -- dynamic (statically undecidable)+    ifM True  INothing  (IJust x) = IDyn INothing+    ifM False INothing  (IJust x) = IDyn (IJust x)+    ifM True  (IJust x) INothing  = IDyn (IJust x)+    ifM False (IJust x) INothing  = IDyn INothing
+ src/Control/Effect/Monad.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE TypeFamilies, GADTs #-}++module Control.Effect.Monad where++import Control.Effect+import Prelude hiding (Monad(..))+import qualified Prelude as P+++{-| All monads are parametric effect monads with a trivial singleton-monoid index. +This wrapper wraps normal monads into the Effect interface using the 'M' contructor.+-}++{-| Wrap regular monads up -}+data Monad m t a where+    Wrap :: P.Monad m => m a -> Monad m () a++{-| Unwrap a monad -}+unWrap :: P.Monad m => Monad m t a -> m a+unWrap (Wrap m) = m++instance (P.Monad m) => Effect (Monad m) where+    {-| Trivial singleton monoid -}+    type Inv (Monad m) s t    = ()+    type Unit (Monad m)       = ()+    type Plus (Monad m) s t   = ()++    return x = Wrap (P.return x)+    (Wrap x) >>= f = Wrap ((P.>>=) x (unWrap . f))+    ++
+ src/Control/Effect/Parameterised.hs view
@@ -0,0 +1,25 @@+{-# LANGUAGE KindSignatures, TypeFamilies, ConstraintKinds, PolyKinds, DataKinds #-}++module Control.Effect.Parameterised where++import Control.Effect++{-| Implements Bob Atkey's 'parametric monads', +    and also the Control.Monad.Indexed package, by emulating+    indexing by morphisms -}++{-| Data type of morphisms -}+newtype T (i :: Morph * *) a = T a++{-| Data type denoting either a morphisms with source and target types, or identity -}+data Morph a b = M a b | Id++instance Effect (T :: ((Morph * *) -> * -> *)) where+    type Unit T = Id+    type Plus T (M a b) (M c d) = M a d+    type Plus T Id (M a b) = M a b+    type Plus T (M a b) Id = M a b+    type Inv  T (M a b) (M c d) = c ~ d++    return a = T a+    (T x) >>= k = let T y = k x in T y
+ src/Control/Effect/ReadOnceReader.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, DataKinds,+             TypeOperators #-}++module Control.Effect.ReadOnceReader (ask,Reader(..),List(..)) where++import Control.Effect+import Control.Effect.Cond+import Control.Effect.Helpers.List+import Prelude    hiding (Monad(..))++{-| Provides a weak reader monad, which can only read an item once. Provides+   an effect system as a list of the items that have been read -}++data Reader (r :: [*]) a = R { runReader :: (List r -> a) }++instance Effect Reader where+    type Inv Reader s t = Split s t++    type Unit Reader = '[]+    type Plus Reader s t = s :++ t++    return x = R $ \Nil -> x+    (R e) >>= k = R $ \xs -> let (s, t) = split xs+                             in (runReader $ k (e s)) t++{-| 'ask' for a value of type 'a' -}+ask :: Reader '[a] a+ask = R $ \(Cons a Nil) -> a++instance Cond Reader where+    type AltInv Reader s t = Split s t+    type Alt Reader s t = s :++ t++    ifM True (R x) (R y) = R $ \rs -> let (r, s) = split rs+                                          _      = y s +                                      in x r+    ifM False (R x) (R y) = R $ \rs -> let (r, s) = split rs+                                           _      = x r +                                       in y s
+ src/Control/Effect/Reader.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, +             UndecidableInstances, RebindableSyntax, DataKinds, TypeOperators, PolyKinds, +             ConstraintKinds #-}++module Control.Effect.Reader (Reader(..), ask, merge, (:->)(..), Var(..), Subset, Set(..)) where++import Control.Effect+import Data.Type.Set+import Prelude hiding (Monad(..))+import GHC.TypeLits+import GHC.Prim++{-| Provides a effect-parameterised version of the class reader monad. Effects+   are sets of variable-type pairs, providing an effect system for reader effects. -}++data Reader s a = IxR { runReader :: Set s -> a }++instance Effect Reader where+    type Inv Reader f g = (IsSet f, IsSet g, Split f g (Union f g))++    {-| A trivial effect is the empty set -}+    type Unit Reader = '[]+    {-| Effects are combined by set union -}+    type Plus Reader f g = Union f g++    {-| Trivially pure computation has an empty reader environment -}+    return x = IxR $ \Empty -> x+    {-| Composing copmutations splits the reader requirements between the two -}+    (IxR e) >>= k = IxR $ \fg -> let (f, g) = split fg+                                 in (runReader $ k (e f)) g++{-| 'ask' for a variable 'v' of type 'a', raising an effect -}+ask :: Var v -> Reader '[v :-> a] a+ask Var = IxR $ \(Ext (Var :-> a) Empty) -> a++{-| Provides a way to emulated the ImplicitParams features of GHC/Haskell -}+merge :: (Unionable s t) => (a -> Reader (Union s t) b) -> Reader s (a -> Reader t b)+merge k = IxR $ \s -> \a -> IxR $ \t -> runReader (k a) (union s t)++{-| If 's' is a subset of 't' then, 's' is a subeffect of 't' -}+instance Subset s t => Subeffect Reader s t where+    sub (IxR e) = IxR $ \st -> let s = subset st in e s++{-+{-| Define the operation for removing duplicates using mappend -}+instance (Nubable (e ': s)) => Nubable (e ': e ': s) where+    nub (Ext _ (Ext x xs)) = nub (Ext x xs)+-}
+ src/Control/Effect/State.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,  +             UndecidableInstances, RebindableSyntax,  DataKinds, +             TypeOperators, PolyKinds, FlexibleContexts, ConstraintKinds, +             OverlappingInstances, IncoherentInstances +             #-}++module Control.Effect.State (Set(..), get, put, State(..), (:->)(..), (:!)(..),+                                  Eff(..), Action(..), Var(..), union, UnionS, +                                     Reads(..), Writes(..), Unionable, Sortable, SetLike, +                                      StateSet, +                                          --- may not want to export these+                                          IntersectR, Update, Sort, Split) where++import Control.Effect+import Data.Type.Set hiding (Unionable, union, SetLike, Nub, Nubable(..))+import qualified Data.Type.Set as Set++import Prelude hiding (Monad(..),reads)+import GHC.TypeLits++{-| Provides an effect-parameterised version of the state monad, which gives an +   effect system for stateful computations with annotations that are sets of +   variable-type-action triples. -}+++{-| Distinguish reads, writes, and read-writes -}+data Eff = R | W | RW+{-| Provides a wrapper for effect actions -}+data Action (s :: Eff) = Eff++instance Show (Action R) where+    show _ = "R"+instance Show (Action W) where+    show _ = "W"+instance Show (Action RW) where+    show _ = "RW"++{-| Describes an effect action 's' on a value of type 'a' -}+data (:!) (a :: *) (s :: Eff) = a :! (Action s) ++instance (Show (Action f), Show a) => Show (a :! f) where+    show (a :! f) = show a ++ " ! " ++ show f++infixl 3 :!++type SetLike s = Nub (Sort s)+type UnionS s t = Nub (Sort (Append s t))+type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)) (Nub (Sort (Append s t))),+                      Split s t (Union s t))++{-| Union operation for state effects -}+union :: (Unionable s t) => Set s -> Set t -> Set (UnionS s t)+union s t = nub (quicksort (append s t))++{-| Type-level remove duplicates from a type-level list and turn different sorts into 'RW'| -}+type family Nub t where+    Nub '[]       = '[]+    Nub '[e]      = '[e]+    Nub (e ': e ': as) = Nub (e ': as)+    Nub ((k :-> a :! s) ': (k :-> a :! t) ': as) = Nub ((k :-> a :! RW) ': as)+    Nub (e ': f ': as) = e ': Nub (f ': as)++{-| Value-level remove duplicates from a type-level list and turn different sorts into 'RW'| -}+class Nubable t v where+    nub :: Set t -> Set v++instance Nubable '[] '[] where+    nub Empty = Empty++instance Nubable '[e] '[e] where+    nub (Ext e Empty) = (Ext e Empty)++instance Nubable ((k :-> b :! s) ': as) as' => +    Nubable ((k :-> a :! s) ': (k :-> b :! s) ': as) as' where+    nub (Ext _ (Ext x xs)) = nub (Ext x xs)++instance Nubable ((k :-> a :! RW) ': as) as' => +    Nubable ((k :-> a :! s) ': (k :-> a :! t) ': as) as' where+    nub (Ext _ (Ext (k :-> (a :! _)) xs)) = nub (Ext (k :-> (a :! (Eff::(Action RW)))) xs)++instance Nubable ((j :-> b :! t) ': as) as' => +    Nubable ((k :-> a :! s) ': (j :-> b :! t) ': as) ((k :-> a :! s) ': as') where+    nub (Ext (k :-> (a :! s)) (Ext (j :-> (b :! t)) xs)) = Ext (k :-> (a :! s)) (nub (Ext (j :-> (b :! t)) xs))+++{-| Update reads, that is any writes are pushed into reads, a bit like intersection -}+class Update s t where+    update :: Set s -> Set t++instance Update xs '[] where+    update _ = Empty++instance Update '[e] '[e] where +    update s = s++{-+instance Update ((v :-> b :! R) ': as) as' => Update ((v :-> a :! s) ': (v :-> b :! s) ': as) as' where+    update (Ext _ (Ext (v :-> (b :! _)) xs)) = update (Ext (v :-> (b :! (Eff::(Action R)))) xs) -}++instance Update ((v :-> a :! R) ': as) as' => Update ((v :-> a :! W) ': (v :-> b :! R) ': as) as' where+    update (Ext (v :-> (a :! _)) (Ext _ xs)) = update (Ext (v :-> (a :! (Eff::(Action R)))) xs)++instance Update ((u :-> b :! s) ': as) as' => Update ((v :-> a :! W) ': (u :-> b :! s) ': as) as' where+    update (Ext _ (Ext e xs)) = update (Ext e xs)++instance Update ((u :-> b :! s) ': as) as' => Update ((v :-> a :! R) ': (u :-> b :! s) ': as) ((v :-> a :! R) ': as') where+    update (Ext e (Ext e' xs)) = Ext e $ update (Ext e' xs)++type IntersectR s t = (Sortable (Append s t), Update (Sort (Append s t)) t)++{-| Intersects a set of write effects and a set of read effects, updating any read effects with+    any corresponding write value -}+intersectR :: (Reads t ~ t, Writes s ~ s, IsSet s, IsSet t, IntersectR s t) => Set s -> Set t -> Set t+intersectR s t = update (quicksort (append s t))++{-| Parametric effect state monad -}+data State s a = State { runState :: Set (Reads s) -> (a, Set (Writes s)) }++{-| Calculate just the reader effects -}+type family Reads t where+    Reads '[]                    = '[]+    Reads ((k :-> a :! R) ': xs)  = (k :-> a :! R) ': (Reads xs)+    Reads ((k :-> a :! RW) ': xs) = (k :-> a :! R) ': (Reads xs)+    Reads ((k :-> a :! W) ': xs)  = Reads xs++{-| Calculate just the writer effects -}+type family Writes t where+    Writes '[]                     = '[]+    Writes ((k :-> a :! W) ': xs)  = (k :-> a :! W) ': (Writes xs)+    Writes ((k :-> a :! RW) ': xs) = (k :-> a :! W) ': (Writes xs)+    Writes ((k :-> a :! R) ': xs)  = Writes xs++{-| Read from a variable 'v' of type 'a'. Raise a read effect. -}+get :: Var v -> State '[v :-> a :! R] a+get _ = State $ \(Ext (v :-> (a :! _)) Empty) -> (a, Empty)++{-| Write to a variable 'v' with a value of type 'a'. Raises a write effect -}+put :: Var v -> a -> State '[k :-> a :! W] ()+put _ a = State $ \Empty -> ((), Ext (Var :-> a :! Eff) Empty)++{-| Captures what it means to be a set of state effects -}+type StateSet f = (StateSetProperties f, StateSetProperties (Reads f), StateSetProperties (Writes f))+type StateSetProperties f = (IntersectR f '[], IntersectR '[] f,+                             UnionS f '[] ~ f, Split f '[] f, +                             UnionS '[] f ~ f, Split '[] f f, +                             UnionS f f ~ f, Split f f f,+                             Unionable f '[], Unionable '[] f)+                   +-- Indexed monad instance+instance Effect State where+    type Inv State s t = (IsSet s, IsSet (Reads s), IsSet (Writes s),+                          IsSet t, IsSet (Reads t), IsSet (Writes t),+                          Reads (Reads t) ~ Reads t, Writes (Writes s) ~ Writes s, +                            Split (Reads s) (Reads t) (Reads (UnionS s t)), +                            Unionable (Writes s) (Writes t), +                            IntersectR (Writes s) (Reads t), +                            Writes (UnionS s t) ~ UnionS (Writes s) (Writes t))++    {-| Pure state effect is the empty state -}+    type Unit State = '[]+    {-| Combine state effects via specialised union (which combines R and W effects on the same+      variable into RW effects -}+    type Plus State s t = UnionS s t++    return x = State $ \Empty -> (x, Empty)++    (State e) >>= k = +        State $ \st -> let (sR, tR) = split st+                           (a, sW)  = e sR+                           (b, tW) = (runState $ k a) (sW `intersectR` tR)+                       in  (b, sW `union` tW) +++{-+instance (Split s t (Union s t), Sub s t) => Subeffect State s t where+    sub (State e) = IxR $ \st -> let (s, t) = split st +                                           _ = ReflP p t +                                 in e s+-}+
+ src/Control/Effect/Update.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, RebindableSyntax, +             GADTs, EmptyDataDecls, DataKinds #-}++module Control.Effect.Update where ++import Control.Effect+import Prelude hiding (Monad(..))++{-| Parametric effect update monad. A bit like a writer monad specialised to the 'Maybe' monoid, +   providing a single memory cell that can be updated, but with heterogeneous behaviour. +   Provides an effect system that explains whether a single memory cell has been updated or not -}++data Eff (w :: Maybe *) where+   Put :: a -> Eff (Just a)+   NoPut :: Eff Nothing++data Update w a = Update { runUpdate :: (a, Eff w) }++-- Uupdate monad+instance Effect Update where +    type Inv Update s t = ()+    type Unit Update = Nothing+    type Plus Update s Nothing  = s+    type Plus Update s (Just t) = Just t++    return x = Update (x, NoPut)+    (Update (a, w)) >>= k =+         Update $ update w (runUpdate $ k a)+           where                    +             update :: Eff s -> (b, Eff t) -> (b, Eff (Plus Update s t))+             update w (b, NoPut)   = (b, w)+             update _ (b, Put w'') = (b, Put w'')++{-| Update the memory cell with a new value of type 'a' -}+put :: a -> Update (Just a) ()+put x = Update ((), Put x)
+ src/Control/Effect/Vector.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls, UndecidableInstances, MultiParamTypeClasses, TypeSynonymInstances, FlexibleContexts #-}++module Control.Effect.Vector where++import Prelude hiding (Monad(..))+import Control.Effect++-- Sized-vector type++data Z+data S n ++data Vector n a where+    Nil :: Vector Z a+    Cons ::a -> Vector n a -> Vector (S n) a++-- Append function which adds indices++type family Add s t+type instance Add Z     m = m+type instance Add (S n) m = S (Add n m)++append :: Vector n a -> Vector m a -> Vector (Add n m) a+append Nil         ys = ys+append (Cons x xs) ys = Cons x (append xs ys)++instance Effect Vector where+    -- Effect monoid is (N, *, 1)+    type Inv Vector s t = ()++    type Unit Vector = S Z++    -- Multiplies indicies+    type Plus Vector Z     m = Z+    type Plus Vector (S n) m = Add m (Plus Vector n m)++    return x = Cons x Nil+    Nil         >>= f  = Nil+    (Cons x xs) >>= f  = append (f x) (xs >>= f)+++
+ src/Control/Effect/WriteOnceWriter.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, +             TypeOperators, DataKinds, KindSignatures #-}++module Control.Effect.WriteOnceWriter (put, WriteOnce(..)) where++import Control.Effect+import Control.Effect.Helpers.List+import Prelude hiding (Monad(..))++{-| Provides a kind of writer monad, which can only write an item once +   (no accumulation), an effect system as a list of the items that have been written -}++data WriteOnce (w :: [*]) a = W { runWriteOnce :: (a, List w) }++instance Effect WriteOnce where+    type Inv WriteOnce s t = ()++    {-| Pure effect is the empty list -}+    type Unit WriteOnce = '[]++    {-| Combine effects by appending effect information -}+    type Plus WriteOnce s t = s :++ t++    return x = W (x, Nil)+    (W (a, r)) >>= k = let (W (b, s)) = k a in W (b, r `append` s)++{-| Write a value of type 'a' -}+put :: a -> WriteOnce '[a] ()+put x = W ((), Cons x Nil)+++
+ src/Control/Effect/Writer.hs view
@@ -0,0 +1,57 @@+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, +             MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, +             ScopedTypeVariables, PolyKinds, FlexibleContexts #-}++module Control.Effect.Writer(Writer(..), Symbol, put, (:->), IsSet, Set(..), union, Var(..), +                              Union, Unionable) where++import Control.Effect +import Data.Type.Set+import Data.Monoid+import GHC.TypeLits+import Prelude hiding (Monad(..))++{-| Provides an effect-parameterised version of the writer monad. Effects+   are sets of variable-type pairs, providing an effect system for writer effects. -}++data Writer w a = Writer { runWriter :: (a, Set w) }++instance Effect Writer where+    type Inv Writer s t = (IsSet s, IsSet t, Unionable s t)++    {-| A trivial effect is the empty set -}+    type Unit Writer = '[]+    {-| Effects are combined by set union -}+    type Plus Writer s t = Union s t++    {-| Trivially pure computation produces an empty state -}+    return x = Writer (x, Empty)+    {-| Composing copmutations takes the union of the writer states, using the monoid +        operation to combine writes to the same variable -}+    (Writer (a, w)) >>= k = let Writer (b, w') = k a+                            in  Writer (b, w `union` w')++{-| Write to variable 'v' with value of type 'a' -}+put :: Var v -> a -> Writer '[v :-> a] ()+put v a = Writer ((), Ext (v :-> a) Empty)++{-| Define the operation for removing duplicates using mappend -}+instance (Monoid u, Nubable ((k :-> u) ': s)) => Nubable ((k :-> u) ': (k :-> u) ': s) where+    nub (Ext (_ :-> u) (Ext (k :-> v) s)) = nub (Ext (k :-> (u `mappend` v)) s)++{- Sub effecting for the parametric effect monad -}+instance Superset s t => Subeffect Writer s t where+    sub (Writer (a, w)) = Writer (a, (superset w)::(Set t))++{-| Computes supersets of sets of variable-type mappings, using the 'mempty' operation  -}+class Superset s t where+    superset :: Set s -> Set t++instance Superset '[] '[] where+    superset Empty = Empty++instance (Monoid x, Superset '[] s) => Superset '[] ((k :-> x) ': s) where+    superset Empty = Ext (Var :-> mempty) (superset Empty)++instance Superset s t => Superset ((k :-> v) ': s) ((k :-> v) ': t) where+    superset (Ext x xs) = Ext x (superset xs)