diff --git a/effect-monad.cabal b/effect-monad.cabal
--- a/effect-monad.cabal
+++ b/effect-monad.cabal
@@ -1,21 +1,20 @@
 name:                   effect-monad
-version:                0.6.1
-synopsis:               Embeds effect systems into Haskell using parameteric effect monads
+version:                0.7.0.0
+synopsis:               Embeds effect systems into Haskell using graded 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>. 
-  .
+   Provides the graded monad structure to Haskell with a number of analogs 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
+copyright:              2013-16 University of Cambridge
 author:                 Dominic Orchard
 maintainer:             Dominic Orchard
 stability:              experimental
 build-type:             Simple
 cabal-version:          >= 1.6
-tested-with:            GHC == 7.8.2
+tested-with:            GHC == 7.10.3, GHC == 8.0.1
 
 extra-source-files:     examples/*.hs
 
@@ -39,7 +38,7 @@
                         Control.Effect.Parameterised
                         Control.Effect.Reader
                         Control.Effect.ReadOnceReader
-                        Control.Effect.State
+                        Control.Effect.State	
                         Control.Effect.Update
                         Control.Effect.Vector
                         Control.Effect.WriteOnceWriter
@@ -47,6 +46,4 @@
                         Control.Effect.Helpers.List
                         
   build-depends:        base < 5,
-                        ghc-prim,
-                        type-level-sets >= 0.5
-
+                        type-level-sets == 0.8.0.0
diff --git a/examples/ArrayReader.hs b/examples/ArrayReader.hs
--- a/examples/ArrayReader.hs
+++ b/examples/ArrayReader.hs
@@ -1,18 +1,17 @@
 {-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances,
              FlexibleContexts, DataKinds, UndecidableInstances, ScopedTypeVariables #-}
 
-module ArrayReader where 
+module ArrayReader where
 
-import GHC.TypeLits 
+import GHC.TypeLits
 import Data.Array
-import Prelude hiding (Monad(..)) 
+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) 
+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)
@@ -26,7 +25,7 @@
     type Plus (Stencil a) s t = Union s t -- append specs
     type Unit (Stencil a)     = '[]       -- empty spec
 
-    (Stencil f) >>= k = 
+    (Stencil f) >>= k =
         Stencil (\(MkA a) -> let (Stencil f') = k (f (MkA a))
                                  in f' (MkA a))
     return a = Stencil (\_ -> a)
@@ -47,4 +46,3 @@
 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
--- a/examples/Counter.hs
+++ b/examples/Counter.hs
@@ -1,19 +1,19 @@
-{-# LANGUAGE RebindableSyntax, EmptyDataDecls, GADTs, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, TypeOperators #-}
+{-# LANGUAGE RebindableSyntax, EmptyDataDecls, GADTs, TypeFamilies, UndecidableInstances, MultiParamTypeClasses, TypeOperators, ScopedTypeVariables, ImplicitParams #-}
 
-import Prelude hiding (Monad(..))
+import Prelude hiding (Monad(..),map)
 import Control.Effect
 import Control.Effect.Counter
 
 import Debug.Trace
 
-{- 
+{-
 
-The 'Counter' indexed monad is useful for counting computations
+The 'Counter' graded 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). 
+than a disk write).
 
-By default, zero counts are tracked, e.g., 
+By default, zero counts are tracked, e.g.,
 
 -}
 
@@ -29,9 +29,14 @@
           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! 
+zero :: Counter Z Int
+zero = do x <- return 2
+          y <- return 4
+          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:
 -}
 
@@ -39,11 +44,9 @@
     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 -}
+type family n :* m where
+            Z     :* m = Z
+            (S n) :* m = m :+ (n :* m)
 
 map' :: (a -> Counter t b) -> Vector n a -> Counter (n :* t) (Vector n b)
 map' f Nil         = return Nil
@@ -51,7 +54,36 @@
                         xs' <- map' f xs
                         return (Cons x' xs')
 
-{- The types show us that if the function counts 't' things, then applying 'map'
+
+
+
+
+
+
+
+
+
+
+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')
+
+class Bar n where
+instance Bar Z where
+instance Bar n => Bar (S n) where
+
+data Listy n a where
+    Nily :: Listy Z a
+    Consy :: (Bar n) => a -> Listy n a -> Listy (S n) a
+
+fooo :: Listy n a -> Int
+fooo Nily = 0
+fooo (Consy x (Consy y xs)) = 2 + (fooo xs)
+fooo (Consy x xs) = 1 + (fooo 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 #-}
@@ -59,12 +91,15 @@
 call :: Int -> Counter (S Z) ()
 call = undefined
 
-singleCall = map' call (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))
+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
+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
@@ -72,4 +107,4 @@
 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'
+lineraMap = map
diff --git a/examples/CounterNat.hs b/examples/CounterNat.hs
--- a/examples/CounterNat.hs
+++ b/examples/CounterNat.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, GADTs, TypeFamilies, UndecidableInstances #-}
+{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, GADTs,
+             TypeFamilies, UndecidableInstances #-}
 
 import Prelude hiding (Monad(..))
 import Control.Effect
@@ -8,12 +9,12 @@
 
 import Debug.Trace
 
-{- 
+{-
 
-The 'Counter' indexed monad is useful for counting computations
+The 'Counter' graded 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). 
+than a disk write).
 
 By default, zero counts are tracked, e.g., -}
 
@@ -27,10 +28,10 @@
 -- foo2 :: Counter (S Z) Int
 foo2 = do x <- tick 2
           y <- return 3
-          return (x * y) 
+          return (x * y)
 
-{- This can be used for other cool things, like proving that 'map' has 
- linear complexity of 'map' at the type-level! 
+{- 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:
 -}
@@ -46,7 +47,7 @@
 
 {- map' is then defined as follows -}
 
-{- CAN'T TYPE CHECK, see Counter.hs 
+{- 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
@@ -55,4 +56,3 @@
                         return (Cons x' xs')
 
 -}
-
diff --git a/examples/ImplicitP.hs b/examples/ImplicitP.hs
--- a/examples/ImplicitP.hs
+++ b/examples/ImplicitP.hs
@@ -4,31 +4,33 @@
 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)
+example1 :: (Num a, ?x :: a, ?y :: a) => a -> a
+example1 z = ?x + ?y
 
-foo' :: (Num a, ?y :: a) => a -> a
-foo' = let ?x = 42
-       in \z -> ?x + ?y + z
+example1M :: (Num a) => a -> Reader '["?x" :-> a, "?y" :-> a] a
+example1M z = do x <- ask (Var::(Var "?x"))
+                 y <- ask (Var::(Var "?y"))
+                 return (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))
+example2 :: (Num a, ?y :: a) => a -> a
+example2 = let ?x = 42
+            in \z -> ?x + ?y + z
 
+example2M :: Num a => Reader '["?x" :-> a] (a -> Reader '["?y" :-> a] a)
+example2M = merge (\z -> do x <- ask (Var::(Var "?x"))
+                            y <- ask (Var::(Var "?y"))
+                            return (x + y + z))
+
 with f x = runReader f x
+runExample2 = example2M `with` (Ext Var (42 :: Int) Empty)
+runExample2' x y z = (example2M `with` (Ext Var (x :: Int) Empty) $ z)
+                                `with` (Ext Var y Empty)
 
-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
-
-     
+example3M :: Int -> Reader '["?y" :-> Int] Int
+example3M =
+  let x = Ext (Var::(Var "?x")) (42 :: Int) 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/Inc.hs b/examples/Inc.hs
new file mode 100644
--- /dev/null
+++ b/examples/Inc.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+module EffectsInHaskellProblem where
+
+import           Control.Effect
+import           Control.Effect.State
+import           GHC.TypeLits
+import           Prelude               hiding (log, Monad(..), (>>))
+
+varX :: Var "x"
+varX = Var
+
+inc :: State '["x" :-> Int :! 'RW] ()
+inc =
+    get varX >>= (put varX . (+1))
+
+-- No instance for (Control.Effect.State.Nubable '["x" :-> (Int :! 'W)] '[])
+inc2 =
+    inc >>=
+    \_ ->
+         inc
diff --git a/examples/Monad.hs b/examples/Monad.hs
--- a/examples/Monad.hs
+++ b/examples/Monad.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE TypeFamilies, RebindableSyntax #-}
+{-# Language TypeFamilies, RebindableSyntax #-}
 
 import Control.Effect
 import Control.Effect.Monad
-import Prelude hiding (Monad(..)) 
+import Prelude hiding (Monad(..))
 
 putStrLn' = Wrap . putStrLn
 
diff --git a/examples/Problem1.hs b/examples/Problem1.hs
--- a/examples/Problem1.hs
+++ b/examples/Problem1.hs
@@ -2,6 +2,13 @@
 
 import Control.Monad.State.Lazy
 
+appendBuffer x = do buff <- get
+                    put (buff ++ x)
+
+hello :: Monad m => StateT String (StateT String m) ()
+hello = do name <- get
+           lift $ appendBuffer $ "hello " ++ name
+
 incSC :: (Monad m) => StateT Int m ()
 incSC = do x <- get
            put (x + 1)
@@ -26,5 +33,3 @@
                  lift $ lift $ incSC
 
 runHellowCount = runStateT (runStateT (runStateT hellowCount "") 0) 1
-
-
diff --git a/examples/ReadOnceReader.hs b/examples/ReadOnceReader.hs
--- a/examples/ReadOnceReader.hs
+++ b/examples/ReadOnceReader.hs
@@ -6,17 +6,17 @@
 import Control.Effect.ReadOnceReader
 
 foo = do x <- ask
-         y <- ask 
+         y <- ask
          return ("Name " ++ x ++ " age " ++ (show y))
 
 --foo_eval = foo (HCons' 'a' (HCons' "bc" HNil'))
 
-foo2 = do x <- ask 
+foo2 = do x <- ask
           y <- ask
           xs <- ask
           return (x : (y : xs))
 
-foo2' = do x <- ask 
+foo2' = do x <- ask
            xs' <- do y <- ask
                      xs <- ask
                      return (y:xs)
diff --git a/examples/Reader.hs b/examples/Reader.hs
--- a/examples/Reader.hs
+++ b/examples/Reader.hs
@@ -1,40 +1,30 @@
-{-# LANGUAGE RebindableSyntax, NoMonomorphismRestriction, DataKinds, TypeOperators, 
-   FlexibleContexts, ConstraintKinds #-}
+{-# LANGUAGE ImplicitParams, DataKinds, RebindableSyntax, TypeOperators, ScopedTypeVariables #-}
 import Prelude hiding (Monad(..))
 import Control.Effect
 import Control.Effect.Reader
 
+import Data.Type.Map
+
 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)
+-- example :: Reader '["x" :-> a, "xs" :-> [a]] [a]
+example = 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
+init1 = Ext Var 1 (Ext Var [2, 3] Empty)
+runExample = runReader example 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
+example' :: (Submap '["x" :-> Int, "xs" :-> [Int]] t) => Reader t [Int]
+example' = sub example
 
-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))
+init2 :: Map '["x" :-> Int, "xs" :-> [Int], "z" :-> a]
+init2 =  Ext Var 1 (Ext Var [2, 3] (Ext Var undefined Empty))
+runExample' = runReader example' init2
diff --git a/examples/Solution1-alt.hs b/examples/Solution1-alt.hs
deleted file mode 100644
--- a/examples/Solution1-alt.hs
+++ /dev/null
@@ -1,22 +0,0 @@
-{-# 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
--- a/examples/Solution1.hs
+++ b/examples/Solution1.hs
@@ -1,47 +1,61 @@
-{-# LANGUAGE FlexibleContexts, DataKinds, TypeOperators, 
+{-# 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"
+c1 = Var::(Var "c1")
+c2 = Var::(Var "c2")
+out  = Var::(Var "out")
 
 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)
+writeS y = do x <- get out
+              put out (x ++ y)
 
 write ::  [a] -> State '["c1" :-> Int :! RW, "out" :-> [a] :! RW] ()
 write x = do  writeS x
-              incC c1_var
+              incC c1
 
-initState0 = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty)
+initState0 = Ext (c1 :-> ((0::Int) :! Eff)) (Ext (out :-> ("" :! Eff)) Empty)
 runWrite = runState (write "hello") initState0
 
+hellow :: State '["c1" :-> Int :! RW, "nom" :-> String :! R, "out" :-> String :! RW] ()
 hellow = do write "hello"
             write " "
-            write "world"
+            name <- get (Var::(Var "nom"))
+            write (name::String)
 
-initState = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty)
+
+-- appendBuffer :: String -> State '["buff" :-> String :! RW] ()
+appendBuffer x = do let bvar = Var::(Var "buff")
+                    buff <- get bvar
+                    put bvar (buff ++ x)
+
+hello :: State '["buff" :-> String :! RW, "name" :-> String :! R] ()
+hello = do name <- get (Var::(Var "name"))
+           appendBuffer $ "hello " ++ name
+
+initState = Ext (c1 :-> ((0::Int) :! Eff)) (Ext (out :-> ("" :! Eff)) Empty)
 runHellow = runState hellow initState
 
 hellowCount = do hellow
-                 incC c2_var
+                 incC c2
 
-initState' = Ext (c1_var :-> ((0::Int) :! Eff)) (Ext (c2_var :-> ((1::Int) :! Eff)) (Ext (o_var :-> ("" :! Eff)) Empty))
+initState' = Ext (c1 :-> ((0::Int) :! Eff)) (Ext (c2 :-> ((1::Int) :! Eff)) (Ext (out :-> ("" :! Eff)) Empty))
 runHellowCount = runState hellowCount initState'
+
+-- Show instances
+
+instance Show (Var "out") where
+    show _ = "out"
+
+instance Show (Var "c1") where
+    show _ = "c1"
+
+instance Show (Var "c2") where
+    show _ = "c2"
diff --git a/examples/Solution2.hs b/examples/Solution2.hs
--- a/examples/Solution2.hs
+++ b/examples/Solution2.hs
@@ -1,5 +1,6 @@
-{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, FlexibleInstances, 
-              ConstraintKinds, FlexibleContexts, TypeFamilies #-}
+{-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures,
+             FlexibleInstances, ConstraintKinds, FlexibleContexts,
+             TypeFamilies #-}
 
 import Prelude hiding (Monad(..))
 import Control.Effect
@@ -7,7 +8,7 @@
 import Control.Effect.State
 import GHC.Conc.Sync
 
-parMap :: (IsSet f, StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] 
+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]
@@ -16,7 +17,7 @@
                      return (y : ys)
 
 
-parMap2 :: (StateSet f, Writes f ~ '[]) => (a -> State f b) -> [a] -> State f [b] 
+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
--- a/examples/State.hs
+++ b/examples/State.hs
@@ -7,21 +7,28 @@
 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)
+{- Computation with a read effect on variable "x" and a
+   read-write (update) effect on variable "y" -}
+-- example :: State '["x" :-> Int :! R, "y" :-> [Int] :! RW] [Int]
+example = 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))
+initS =  Ext (x_var :-> (1 :! Eff)) (Ext (y_var :-> ([2,3] :! Eff)) Empty)
+example_run = runState example initS
 
---foo2 :: State '["x" :-> Int :! RW] Int
-foo2 = do x <- get (Var::(Var "x"))
-          put (Var::(Var "x")) (x+1)
-          return x
+--example2 :: State '["x" :-> Int :! RW] Int
+example2 = do
+  x <- get (Var::(Var "x"))
+  put (Var::(Var "x")) (x+1)
+  return x
 
-foo2_run = (runState foo2) (Ext (x_var :-> 10 :! Eff) Empty)
+example2_run = (runState example2) (Ext (x_var :-> 10 :! Eff) Empty)
 
+example3 :: State '["x" :-> String :! RW] ()
+example3 = do
+  x <- get x_var
+  put x_var (x ++ " ok !")
diff --git a/examples/StencilSpecs.hs b/examples/StencilSpecs.hs
--- a/examples/StencilSpecs.hs
+++ b/examples/StencilSpecs.hs
@@ -27,7 +27,7 @@
 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 
+                             return $ a + b
 -}
 
 -- fooFwd has a 'forward' pattern to depth of 2
@@ -46,7 +46,7 @@
 
 -- Symmetrical stencils (derived from Forward and Backward stencils of the same depth)
 
-type Symmetrical depth = AsSet ((IntT (Pos 0)) ': (Append (ForwardP depth) (BackwardP depth)))
+type Symmetrical depth = AsSet ((IntT (Pos 0)) ': ((ForwardP depth) :++ (BackwardP depth)))
 
 -- Backward-oriented stencils
 
@@ -54,4 +54,4 @@
 
 type family  BackwardP depth where
              BackwardP 0 = '[]
-             BackwardP n = (IntT (Neg n)) ': (BackwardP (n - 1)) 
+             BackwardP n = (IntT (Neg n)) ': (BackwardP (n - 1))
diff --git a/examples/WriteOnceWriter.hs b/examples/WriteOnceWriter.hs
--- a/examples/WriteOnceWriter.hs
+++ b/examples/WriteOnceWriter.hs
@@ -2,7 +2,7 @@
 
 import Prelude hiding (Monad(..))
 import Control.Effect
-import Control.Effect.WriteOnceWriter 
+import Control.Effect.WriteOnceWriter
 
 foo = do put 42
          put "hello"
diff --git a/examples/Writer.hs b/examples/Writer.hs
--- a/examples/Writer.hs
+++ b/examples/Writer.hs
@@ -1,13 +1,13 @@
-{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, RebindableSyntax, FlexibleInstances, 
-             ConstraintKinds, FlexibleContexts, TypeFamilies, ScopedTypeVariables
-  #-}
+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, RebindableSyntax,
+             FlexibleInstances, ConstraintKinds, FlexibleContexts,
+             TypeFamilies, ScopedTypeVariables #-}
 
+import Prelude hiding (Monad(..))
 import Control.Effect
 import Control.Effect.Writer
 
 import Data.Monoid
 
-import Prelude hiding (Monad(..))
 
 instance Monoid Int where
     mappend = (+)
@@ -17,30 +17,33 @@
 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 = 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"
+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]) => 
+test2 :: (IsMap f, Unionable f '["y" :-> String]) =>
          (Int -> Writer f t) -> Writer (Union f '["y" :-> String]) ()
-test2 f = do f 3 
-             put var_y ". hi"
+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) => 
+foo2 :: (IsMap 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
-
+foo2 f = do
+    y <- f 3
+    put var_x (42::Int)
+    put var_y y
diff --git a/src/Control/Coeffect.hs b/src/Control/Coeffect.hs
--- a/src/Control/Coeffect.hs
+++ b/src/Control/Coeffect.hs
@@ -3,7 +3,7 @@
 
 module Control.Coeffect where 
 
-import GHC.Prim
+import GHC.Exts ( Constraint )
 
 {- Coeffect parameterised comonad
 
diff --git a/src/Control/Coeffect/Coreader.hs b/src/Control/Coeffect/Coreader.hs
--- a/src/Control/Coeffect/Coreader.hs
+++ b/src/Control/Coeffect/Coreader.hs
@@ -1,14 +1,15 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs, 
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs,
              ConstraintKinds, TypeOperators, DataKinds, UndecidableInstances #-}
 
 module Control.Coeffect.Coreader where
 
 import Control.Coeffect
-import Data.Type.Set
+import Data.Type.Map
+import GHC.TypeLits
 
 {-| 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) }
+data IxCoreader (s :: [Mapping Symbol *]) a = IxR { runCoreader :: (a, Map s) }
 
 instance Coeffect IxCoreader where
     type Inv IxCoreader s t = (Unionable s t, Split s t (Union s t))
@@ -29,5 +30,4 @@
 
 {-| '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
-
+ask _ = \(IxR (_, Ext Var a Empty)) -> a
diff --git a/src/Control/Effect.hs b/src/Control/Effect.hs
--- a/src/Control/Effect.hs
+++ b/src/Control/Effect.hs
@@ -3,8 +3,7 @@
 module Control.Effect where 
 
 import Prelude hiding (Monad(..))
-import GHC.Prim
-
+import GHC.Exts ( Constraint )    
 
 {-| Specifies "parametric effect monads" which are essentially monads but
      annotated by a type-level monoid formed by 'Plus' and 'Unit' -}
@@ -25,6 +24,7 @@
 
    {-| 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
@@ -35,3 +35,4 @@
 {-| 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
--- a/src/Control/Effect/Cond.hs
+++ b/src/Control/Effect/Cond.hs
@@ -2,7 +2,7 @@
 
 module Control.Effect.Cond where
 
-import GHC.Prim
+import GHC.Exts ( Constraint )
 
 {-| Provides a conditional using an 'alternation' operation, as opposed to using
    'Subeffect' -}
diff --git a/src/Control/Effect/Helpers/List.hs b/src/Control/Effect/Helpers/List.hs
--- a/src/Control/Effect/Helpers/List.hs
+++ b/src/Control/Effect/Helpers/List.hs
@@ -1,21 +1,23 @@
-{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, 
-             MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, FlexibleContexts, 
+             MultiParamTypeClasses, FlexibleInstances, PolyKinds, KindSignatures #-}
 
 module Control.Effect.Helpers.List where
 
+import Data.Proxy 
+
 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)
+type family (:++) (s :: [*]) (t :: [*]) :: [*] where
+    '[] :++ ys       = ys
+    (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
+class Split (s :: [*]) (t :: [*]) where
     split :: List (s :++ t) -> (List s, List t)
 
 instance Split '[] xs where
@@ -24,3 +26,27 @@
 instance Split xs ys => Split (x ': xs) ys where
     split (Cons x xs) = let (xs', ys') = split xs
                     in (Cons x xs', ys')
+
+lengthL :: List xs -> Int
+lengthL Nil = 0
+lengthL (Cons _ xs) = 1 + lengthL xs
+
+type family LookupT  k xs where
+    LookupT k '[] = Maybe ()
+    LookupT k ((k , x) ': xs) = Maybe x
+    LookupT k ((j , x) ': xs) = LookupT k xs
+
+class LookUpA k xs (LookupT k xs) => Lookup k xs where
+    lookup :: List xs -> Proxy k -> Maybe (LookupT k xs) 
+    lookup = lookupA
+
+class LookUpA k xs x where
+    lookupA :: List xs -> Proxy k -> Maybe x
+
+instance LookUpA k ((k, x) ': xs) x where
+    lookupA (Cons (_, x) _) k = Just x 
+
+instance LookUpA k xs y => LookUpA k ((j, x) ': xs) y where
+    lookupA (Cons _ xs) k = lookupA xs k
+
+
diff --git a/src/Control/Effect/Monad.hs b/src/Control/Effect/Monad.hs
--- a/src/Control/Effect/Monad.hs
+++ b/src/Control/Effect/Monad.hs
@@ -12,11 +12,11 @@
 -}
 
 {-| Wrap regular monads up -}
-data Monad m t a where
+data Monad m f 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 :: P.Monad m => Monad m f a -> m a
 unWrap (Wrap m) = m
 
 instance (P.Monad m) => Effect (Monad m) where
diff --git a/src/Control/Effect/Reader.hs b/src/Control/Effect/Reader.hs
--- a/src/Control/Effect/Reader.hs
+++ b/src/Control/Effect/Reader.hs
@@ -1,22 +1,24 @@
-{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, 
-             UndecidableInstances, RebindableSyntax, DataKinds, TypeOperators, PolyKinds, 
-             ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts,
+             MultiParamTypeClasses, UndecidableInstances, RebindableSyntax,
+             DataKinds, TypeOperators, PolyKinds, ConstraintKinds,
+             KindSignatures #-}
 
-module Control.Effect.Reader (Reader(..), ask, merge, (:->)(..), Var(..), Subset, Set(..)) where
+module Control.Effect.Reader (Reader(..), ask, merge, Mapping(..),
+                              Var(..), Submap, Map(..)) where
 
 import Control.Effect
-import Data.Type.Set
+import Data.Type.Map
 import Prelude hiding (Monad(..))
 import GHC.TypeLits
-import GHC.Prim
+import GHC.Exts ( Constraint )
 
 {-| 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 }
+newtype Reader (s :: [Mapping Symbol *]) a = IxR { runReader :: Map s -> a }
 
 instance Effect Reader where
-    type Inv Reader f g = (IsSet f, IsSet g, Split f g (Union f g))
+    type Inv Reader f g = (IsMap f, IsMap g, Split f g (Union f g))
 
     {-| A trivial effect is the empty set -}
     type Unit Reader = '[]
@@ -29,17 +31,20 @@
     (IxR e) >>= k = IxR $ \fg -> let (f, g) = split fg
                                  in (runReader $ k (e f)) g
 
+-- Values of the same type can be combined
+type instance Combine v v = v
+
 {-| '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
+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
+instance Submap s t => Subeffect Reader s t where
+    sub (IxR e) = IxR $ \st -> let s = submap st in e s
 
 {-
 {-| Define the operation for removing duplicates using mappend -}
diff --git a/src/Control/Effect/State.hs b/src/Control/Effect/State.hs
--- a/src/Control/Effect/State.hs
+++ b/src/Control/Effect/State.hs
@@ -1,25 +1,26 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,  
-             UndecidableInstances, RebindableSyntax,  DataKinds, 
-             TypeOperators, PolyKinds, FlexibleContexts, ConstraintKinds, 
-             OverlappingInstances, IncoherentInstances 
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
+             UndecidableInstances, RebindableSyntax,  DataKinds,
+             TypeOperators, PolyKinds, FlexibleContexts, ConstraintKinds,
+             IncoherentInstances, GADTs
              #-}
 
 module Control.Effect.State (Set(..), get, put, State(..), (:->)(..), (:!)(..),
-                                  Eff(..), Action(..), Var(..), union, UnionS, 
-                                     Reads(..), Writes(..), Unionable, Sortable, SetLike, 
-                                      StateSet, 
+                                  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 Data.Type.Map (Mapping(..), Var(..))
 
 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 
+{-| 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. -}
 
 
@@ -35,8 +36,38 @@
 instance Show (Action RW) where
     show _ = "RW"
 
+infixl 2 :->
+data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
+
+data Var (k :: Symbol) where Var :: Var k
+                             {- Some special defaults for some common names -}
+                             X   :: Var "x"
+                             Y   :: Var "y"
+                             Z   :: Var "z"
+
+
+instance (Show (Var k), Show v) => Show (k :-> v) where
+    show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
+instance Show (Var "x") where
+    show X   = "x"
+    show Var = "Var"
+instance Show (Var "y") where
+    show Y   = "y"
+    show Var = "Var"
+instance Show (Var "z") where
+    show Z   = "z"
+    show Var = "Var"
+instance Show (Var v) where
+    show _ = "Var"
+
+{-| Symbol comparison -}
+type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u
+
+
+
 {-| Describes an effect action 's' on a value of type 'a' -}
-data (:!) (a :: *) (s :: Eff) = a :! (Action s) 
+--data EffMapping a (s :: Eff) = a :! (Action s)
+data a :! (s :: Eff) = a :! (Action s)
 
 instance (Show (Action f), Show a) => Show (a :! f) where
     show (a :! f) = show a ++ " ! " ++ show f
@@ -44,8 +75,8 @@
 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))),
+type UnionS s t = Nub (Sort (s :++ t))
+type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)) (Nub (Sort (s :++ t))),
                       Split s t (Union s t))
 
 {-| Union operation for state effects -}
@@ -70,15 +101,15 @@
 instance Nubable '[e] '[e] where
     nub (Ext e Empty) = (Ext e Empty)
 
-instance Nubable ((k :-> b :! s) ': as) as' => 
+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' => 
+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' => 
+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))
 
@@ -90,7 +121,7 @@
 instance Update xs '[] where
     update _ = Empty
 
-instance Update '[e] '[e] where 
+instance Update '[e] '[e] where
     update s = s
 
 {-
@@ -106,7 +137,7 @@
 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)
+type IntersectR s t = (Sortable (s :++ t), Update (Sort (s :++ t)) t)
 
 {-| Intersects a set of write effects and a set of read effects, updating any read effects with
     any corresponding write value -}
@@ -141,19 +172,19 @@
 {-| 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, 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), 
+                          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 -}
@@ -164,17 +195,16 @@
 
     return x = State $ \Empty -> (x, Empty)
 
-    (State e) >>= k = 
+    (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) 
+                       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 
+    sub (State e) = IxR $ \st -> let (s, t) = split st
+                                           _ = ReflP p t
                                  in e s
 -}
-
diff --git a/src/Control/Effect/Writer.hs b/src/Control/Effect/Writer.hs
--- a/src/Control/Effect/Writer.hs
+++ b/src/Control/Effect/Writer.hs
@@ -1,57 +1,61 @@
-{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, 
-             MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, 
+{-# 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
+module Control.Effect.Writer(Writer(..), Symbol, put, Mapping(..),
+                             IsMap, Map(..), union, Var(..),
+                             Union, Unionable) where
 
-import Control.Effect 
-import Data.Type.Set
+import Control.Effect
+import Data.Type.Map
 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. -}
+   are maps of variable-type pairs, providing an effect system for writer effects. -}
 
-data Writer w a = Writer { runWriter :: (a, Set w) }
+data Writer (w :: [Mapping Symbol *]) a = Writer { runWriter :: (a, Map w) }
 
 instance Effect Writer where
-    type Inv Writer s t = (IsSet s, IsSet t, Unionable s t)
+    type Inv Writer s t = (IsMap s, IsMap t, Unionable s t)
 
-    {-| A trivial effect is the empty set -}
+    {-| A trivial effect is the empty map -}
     type Unit Writer = '[]
-    {-| Effects are combined by set union -}
+    {-| Effects are combined by map 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 
+    {-| 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)
+put v a = Writer ((), Ext v a Empty)
 
+-- Values of the same type can be combined
+type instance Combine v v = v
+
 {-| 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)
+    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))
+instance Supermap s t => Subeffect Writer s t where
+    sub (Writer (a, w)) = Writer (a, (supermap w)::(Map t))
 
-{-| Computes supersets of sets of variable-type mappings, using the 'mempty' operation  -}
-class Superset s t where
-    superset :: Set s -> Set t
+{-| Computes supermaps of maps of variable-type mappings, using the 'mempty' operation  -}
+class Supermap s t where
+    supermap :: Map s -> Map t
 
-instance Superset '[] '[] where
-    superset Empty = Empty
+instance Supermap '[] '[] where
+    supermap Empty = Empty
 
-instance (Monoid x, Superset '[] s) => Superset '[] ((k :-> x) ': s) where
-    superset Empty = Ext (Var :-> mempty) (superset Empty)
+instance (Monoid x, Supermap '[] s) => Supermap '[] ((k :-> x) ': s) where
+    supermap Empty = Ext Var mempty (supermap Empty)
 
-instance Superset s t => Superset ((k :-> v) ': s) ((k :-> v) ': t) where
-    superset (Ext x xs) = Ext x (superset xs)
+instance Supermap s t => Supermap ((k :-> v) ': s) ((k :-> v) ': t) where
+    supermap (Ext k x xs) = Ext k x (supermap xs)