diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,6 @@
+module Main (main) where
+
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/effect-monad.cabal b/effect-monad.cabal
new file mode 100644
--- /dev/null
+++ b/effect-monad.cabal
@@ -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
+
diff --git a/examples/ArrayReader.hs b/examples/ArrayReader.hs
new file mode 100644
--- /dev/null
+++ b/examples/ArrayReader.hs
@@ -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
+
diff --git a/examples/Counter.hs b/examples/Counter.hs
new file mode 100644
--- /dev/null
+++ b/examples/Counter.hs
@@ -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'
diff --git a/examples/CounterNat.hs b/examples/CounterNat.hs
new file mode 100644
--- /dev/null
+++ b/examples/CounterNat.hs
@@ -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')
+
+-}
+
diff --git a/examples/ImplicitP.hs b/examples/ImplicitP.hs
new file mode 100644
--- /dev/null
+++ b/examples/ImplicitP.hs
@@ -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
+
+     
diff --git a/examples/Maybe.hs b/examples/Maybe.hs
new file mode 100644
--- /dev/null
+++ b/examples/Maybe.hs
@@ -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']
diff --git a/examples/Monad.hs b/examples/Monad.hs
new file mode 100644
--- /dev/null
+++ b/examples/Monad.hs
@@ -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 ()
diff --git a/examples/Problem1.hs b/examples/Problem1.hs
new file mode 100644
--- /dev/null
+++ b/examples/Problem1.hs
@@ -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
+
+
diff --git a/examples/ReadOnceReader.hs b/examples/ReadOnceReader.hs
new file mode 100644
--- /dev/null
+++ b/examples/ReadOnceReader.hs
@@ -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))
diff --git a/examples/Reader.hs b/examples/Reader.hs
new file mode 100644
--- /dev/null
+++ b/examples/Reader.hs
@@ -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))
diff --git a/examples/Solution1-alt.hs b/examples/Solution1-alt.hs
new file mode 100644
--- /dev/null
+++ b/examples/Solution1-alt.hs
@@ -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"
diff --git a/examples/Solution1.hs b/examples/Solution1.hs
new file mode 100644
--- /dev/null
+++ b/examples/Solution1.hs
@@ -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'
diff --git a/examples/Solution2.hs b/examples/Solution2.hs
new file mode 100644
--- /dev/null
+++ b/examples/Solution2.hs
@@ -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)
diff --git a/examples/State.hs b/examples/State.hs
new file mode 100644
--- /dev/null
+++ b/examples/State.hs
@@ -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)
+
diff --git a/examples/StencilSpecs.hs b/examples/StencilSpecs.hs
new file mode 100644
--- /dev/null
+++ b/examples/StencilSpecs.hs
@@ -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)) 
diff --git a/examples/Update.hs b/examples/Update.hs
new file mode 100644
--- /dev/null
+++ b/examples/Update.hs
@@ -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 ()
diff --git a/examples/WriteOnceWriter.hs b/examples/WriteOnceWriter.hs
new file mode 100644
--- /dev/null
+++ b/examples/WriteOnceWriter.hs
@@ -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 ()
diff --git a/examples/Writer.hs b/examples/Writer.hs
new file mode 100644
--- /dev/null
+++ b/examples/Writer.hs
@@ -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
+
diff --git a/examples/WriterM.hs b/examples/WriterM.hs
new file mode 100644
--- /dev/null
+++ b/examples/WriterM.hs
@@ -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')
diff --git a/src/Control/Coeffect.hs b/src/Control/Coeffect.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Coeffect.hs
@@ -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
diff --git a/src/Control/Coeffect/Coreader.hs b/src/Control/Coeffect/Coreader.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Coeffect/Coreader.hs
@@ -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
+
diff --git a/src/Control/Effect.hs b/src/Control/Effect.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect.hs
@@ -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
diff --git a/src/Control/Effect/Cond.hs b/src/Control/Effect/Cond.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Cond.hs
@@ -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
diff --git a/src/Control/Effect/Counter.hs b/src/Control/Effect/Counter.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Counter.hs
@@ -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
+
+    
diff --git a/src/Control/Effect/CounterNat.hs b/src/Control/Effect/CounterNat.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/CounterNat.hs
@@ -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
diff --git a/src/Control/Effect/Helpers/List.hs b/src/Control/Effect/Helpers/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Helpers/List.hs
@@ -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')
diff --git a/src/Control/Effect/Maybe.hs b/src/Control/Effect/Maybe.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Maybe.hs
@@ -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
diff --git a/src/Control/Effect/Monad.hs b/src/Control/Effect/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Monad.hs
@@ -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))
+    
+
+    
diff --git a/src/Control/Effect/Parameterised.hs b/src/Control/Effect/Parameterised.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Parameterised.hs
@@ -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
diff --git a/src/Control/Effect/ReadOnceReader.hs b/src/Control/Effect/ReadOnceReader.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/ReadOnceReader.hs
@@ -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
diff --git a/src/Control/Effect/Reader.hs b/src/Control/Effect/Reader.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Reader.hs
@@ -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)
+-}
diff --git a/src/Control/Effect/State.hs b/src/Control/Effect/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/State.hs
@@ -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
+-}
+
diff --git a/src/Control/Effect/Update.hs b/src/Control/Effect/Update.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Update.hs
@@ -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)
diff --git a/src/Control/Effect/Vector.hs b/src/Control/Effect/Vector.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Vector.hs
@@ -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)
+
+
+
diff --git a/src/Control/Effect/WriteOnceWriter.hs b/src/Control/Effect/WriteOnceWriter.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/WriteOnceWriter.hs
@@ -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)
+
+
+
diff --git a/src/Control/Effect/Writer.hs b/src/Control/Effect/Writer.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Writer.hs
@@ -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)