diff --git a/effect-monad.cabal b/effect-monad.cabal
--- a/effect-monad.cabal
+++ b/effect-monad.cabal
@@ -1,20 +1,34 @@
 name:                   effect-monad
-version:                0.7.0.0
-synopsis:               Embeds effect systems into Haskell using graded monads
-description:            
-   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). 
+version:                0.8.0.0
+synopsis:               Embeds effect systems and program logics into Haskell using graded monads and parameterised monads
+description:
+   Provides the graded monad structure to Haskell via Control.Effect
+   with a number of analogs of familiar monads and some new things:
+        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 the paper
+   \"Embedding effect systems in Haskell\" by Orchard and Petricek
+   <http://dorchard.co.uk/publ/haskell14-effects.pdf> (Haskell, 2014)
+
+   Also provides the parameterised monad structure due to Atkey in
+   Control.Effect.Parameterised along with some instances:
+       AtomicState, SafeFiles, ExtensibleState
+
+   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-16 University of Cambridge
+copyright:              2013-18 University of Kent
 author:                 Dominic Orchard
 maintainer:             Dominic Orchard
 stability:              experimental
 build-type:             Simple
 cabal-version:          >= 1.6
-tested-with:            GHC == 7.10.3, GHC == 8.0.1
+tested-with:            GHC == 7.10.3, GHC == 8.0.1, GHC == 8.2.2
 
 extra-source-files:     examples/*.hs
 
@@ -35,15 +49,20 @@
                         Control.Effect.CounterNat
                         Control.Effect.Maybe
                         Control.Effect.Monad
-                        Control.Effect.Parameterised
+                        Control.Effect.ParameterisedAsGraded
                         Control.Effect.Reader
                         Control.Effect.ReadOnceReader
-                        Control.Effect.State	
+                        Control.Effect.State
                         Control.Effect.Update
                         Control.Effect.Vector
                         Control.Effect.WriteOnceWriter
                         Control.Effect.Writer
                         Control.Effect.Helpers.List
-                        
+                        Control.Effect.Parameterised
+                        Control.Effect.Parameterised.AtomicState
+                        Control.Effect.Parameterised.ExtensibleState
+                        Control.Effect.Parameterised.SafeFiles
+                        Control.Effect.Parameterised.State
+
   build-depends:        base < 5,
-                        type-level-sets == 0.8.0.0
+                        type-level-sets >= 0.8.7.0
diff --git a/examples/AtomicState.hs b/examples/AtomicState.hs
new file mode 100644
--- /dev/null
+++ b/examples/AtomicState.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE RebindableSyntax #-}
+
+-- Bye Monads... as we know them
+import Prelude hiding (Monad(..))
+-- Hello parameterised monads
+import Control.Effect.Parameterised
+import Control.Effect.Parameterised.AtomicState
+
+-----------------------------
+-- Examples
+
+myProgram :: State (Closed Int) (Closed Int) String
+myProgram = do
+  x <- get
+  put (x+1)
+  a <- somethingPurish x
+  return (a ++ show x)
+
+somethingPurish :: Int -> State (Closed Int) (Closed Int) String
+somethingPurish n = do
+  x <- get
+  put (x + 1)
+  return $ if n == 0 then "hello" else "goodbye"
diff --git a/examples/ExtensibleState.hs b/examples/ExtensibleState.hs
new file mode 100644
--- /dev/null
+++ b/examples/ExtensibleState.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+import Prelude hiding (Monad(..))
+import Control.Effect.Parameterised
+import Control.Effect.Parameterised.ExtensibleState
+import GHC.TypeLits
+import Data.Type.Map
+
+-- Example map
+exMap :: Map '["x" ':-> Int, "flag" ':-> Bool]
+exMap = Ext (Var @ "x") (42 :: Int)
+      $ Ext (Var @ "flag") False
+        Empty
+
+increment :: (Update "x" Int m) => State (Map m) (Map m) ()
+increment = do
+   (n :: Int) <- get (Var @ "x")
+   put (Var @ "x") (n+1)
+
+example = do
+   flag <- get (Var @ "flag")
+   increment
+   (n :: Int) <- get (Var @"x")
+   put (Var @ "flag") ((n > 0) || flag)
+
+
+go :: ((), Map '["x" ':-> Int, "flag" ':-> Bool])
+go = runState example exMap
+
+example2 :: (Get "flag" Bool m, Update "x" Int m, Put "y" Int m m) => State (Map m) (Map m) ()
+example2 = do
+   flag <- get (Var @ "flag")
+   if flag
+     then modify (Var @ "x") (\(x :: Int) -> x + 1)
+     else put (Var @ "y") (42 :: Int)
diff --git a/examples/Inc.hs b/examples/Inc.hs
deleted file mode 100644
--- a/examples/Inc.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# 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/SafeFiles.hs b/examples/SafeFiles.hs
new file mode 100644
--- /dev/null
+++ b/examples/SafeFiles.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+-- Bye Monads... as we know them
+import Prelude hiding (Monad(..))
+import Control.Effect.Parameterised.SafeFiles
+import qualified System.IO as IO
+
+example :: IO ()
+example = runSafeFiles $ do
+  h  <- openFile "foo" IO.ReadWriteMode
+  h' <- openFile "bar" IO.ReadWriteMode
+  x <- hGetChar h
+  hPutChar h' x
+  hClose h'
+  hClose h
+  return ()
+
+example2 :: IO ()
+example2 = runSafeFiles $ do
+  h1  <- openFile "foo" IO.ReadWriteMode
+  h2 <- openFile "bar" IO.ReadWriteMode
+  loopy h1 h2
+
+loopy h1 h2 = do
+  isEmpty <- hIsEOF h1
+  if isEmpty
+    then do
+      hClose h1
+      hClose h2
+    else do
+      x <- hGetChar h1
+      hPutChar h2 x
+      loopy h1 h2
diff --git a/examples/WriterM.hs b/examples/WriterM.hs
deleted file mode 100644
--- a/examples/WriterM.hs
+++ /dev/null
@@ -1,17 +0,0 @@
-{-# 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/Effect/Parameterised.hs b/src/Control/Effect/Parameterised.hs
--- a/src/Control/Effect/Parameterised.hs
+++ b/src/Control/Effect/Parameterised.hs
@@ -1,25 +1,31 @@
-{-# LANGUAGE KindSignatures, TypeFamilies, ConstraintKinds, PolyKinds, DataKinds #-}
+-- Used to make the types extra clear
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
 
-module Control.Effect.Parameterised where
+-- This module implement parameterised monads due to Bob Atkey
+-- (see 'Parameterised Notions of Computing' JFP 2009)
+-- also defined in Control.Monad.Indexed (category-extras)
 
-import Control.Effect
+module Control.Effect.Parameterised ((>>), PMonad(..), fail, ifThenElse) where
 
-{-| Implements Bob Atkey's 'parametric monads', 
-    and also the Control.Monad.Indexed package, by emulating
-    indexing by morphisms -}
+-- Bye Monads... as we know them
+import Prelude hiding (Monad(..))
 
-{-| Data type of morphisms -}
-newtype T (i :: Morph * *) a = T a
+-- Hello Parameterised Monads
+class PMonad (pm :: k -> k -> * -> *) where
+  -- Lift pure values into effect-invariant computations
+  return :: a -> pm inv inv a
 
-{-| Data type denoting either a morphisms with source and target types, or identity -}
-data Morph a b = M a b | Id
+  -- Sequentially compose effectful computations
+  (>>=) :: pm pre interm t -> (t -> pm interm post t') -> pm pre post t'
 
-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
+-- Other boilerplate
+(>>) :: PMonad pm => pm pre mid t -> pm mid post t' -> pm pre post t'
+x >> y = x >>= const y
 
-    return a = T a
-    (T x) >>= k = let T y = k x in T y
+fail :: String -> m inv inv a
+fail = error
+
+ifThenElse :: Bool -> a -> a -> a
+ifThenElse True x _ = x
+ifThenElse False _ y = y
diff --git a/src/Control/Effect/Parameterised/AtomicState.hs b/src/Control/Effect/Parameterised/AtomicState.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Parameterised/AtomicState.hs
@@ -0,0 +1,22 @@
+-- For clarity in type classes instances
+{-# LANGUAGE InstanceSigs #-}
+
+module Control.Effect.Parameterised.AtomicState
+        (get, put, Closed, Open, State(..)) where
+
+-- Bye Monads... as we know them
+import Prelude hiding (Monad(..))
+-- Hello parameterised monads
+import Control.Effect.Parameterised
+import Control.Effect.Parameterised.State
+
+newtype Closed s = Closed s deriving Show
+newtype Open   s = Open s   deriving Show
+
+-- get :: State s s
+get :: State (Closed s) (Open s) s
+get = State $ \(Closed s) -> (s, Open s)
+
+-- put :: s -> State s ()
+put :: t -> State (Open s) (Closed t) ()
+put tx = State $ \(Open _) -> ((), Closed tx)
diff --git a/src/Control/Effect/Parameterised/ExtensibleState.hs b/src/Control/Effect/Parameterised/ExtensibleState.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Parameterised/ExtensibleState.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RebindableSyntax #-}
+
+module Control.Effect.Parameterised.ExtensibleState
+          (State(..), Get, Put, Update, get, put, modify
+          , PMonad(..), (>>), ifThenElse, fail) where
+
+import Prelude hiding (Monad(..))
+import Control.Effect.Parameterised
+import Control.Effect.Parameterised.State
+import Data.Type.Map
+
+-- Fine-grained get, put, and modify
+get :: IsMember v t m => Var v -> State (Map m) (Map m) t
+get v = State $ \s -> (lookp v s, s)
+
+put :: Updatable v t m n => Var v -> t -> State (Map m) (Map n) ()
+put v t = State $ \s -> ((), update s v t)
+
+modify :: (IsMember v s m, Updatable v t m n) => Var v -> (s -> t) -> State (Map m) (Map n) ()
+modify v f = do
+  x <- get v
+  put v (f x)
+
+-- Aliases for our operations
+type Get v t m = IsMember v t m
+type Put v t m n = Updatable v t m n
+type Update v t m = (Get v t m, Put v t m m)
diff --git a/src/Control/Effect/Parameterised/SafeFiles.hs b/src/Control/Effect/Parameterised/SafeFiles.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Parameterised/SafeFiles.hs
@@ -0,0 +1,99 @@
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Control.Effect.Parameterised.SafeFiles
+         (openFile, hGetChar, hPutChar, hClose, hIsEOF, runSafeFiles
+         , SafeFiles, SafeHandle, St
+         , PMonad(..), (>>), ifThenElse, fail) where
+
+-- Bye Monads... as we know them
+import Prelude hiding (Monad(..))
+import Control.Effect.Parameterised
+
+-- Import qualified versions of standard code we want to wrap
+import qualified Prelude as P
+import qualified System.IO as IO
+
+import GHC.TypeLits -- gives us type-level natural numbers
+
+{-
+
+-- openFile :: FilePath -> IOMode -> IO Handle
+-- hGetChar :: Handle -> IO Char
+-- hPutChar :: Handle -> Char -> IO ()
+-- hClose :: Handle -> IO ()
+
+-- hIsOpen :: Handle -> IO Bool
+-- hIsClosed :: Handle -> IO Bool
+
+-}
+
+-- Wrap the IO monad
+newtype SafeFiles pre post a = SafeFiles { unSafeFiles :: IO a }
+
+instance PMonad SafeFiles where
+   -- return :: a -> SafeFiles p p a
+   return = SafeFiles . P.return
+   -- (>>=) :: SafeFiles p q a -> (a -> SafeFiles q r b) -> SafeFiles p r b
+   (SafeFiles m) >>= k = SafeFiles (m P.>>= (unSafeFiles . k))
+
+-- Safe handlers are indexed by a (unique) number
+newtype SafeHandle (n :: Nat) =
+       SafeHandle { unsafeHandle :: IO.Handle }
+
+-- Protocol states are a pair of a type-level nat and list of naturals
+data St (n :: Nat) (opens :: [Nat])
+
+-- openFile :: FilePath -> IOMode -> IO Handle
+-- Opens a file, returns a handler with a fresh name
+openFile ::
+    IO.FilePath
+ -> IO.IOMode
+ -> SafeFiles (St h opens) (St (h + 1) (h ': opens)) (SafeHandle h)
+openFile f mode = SafeFiles $ fmap SafeHandle (IO.openFile f mode)
+
+-- hClose :: Handle -> IO ()
+hClose :: Member h opens =>
+     SafeHandle h
+  -> SafeFiles (St n opens) (St n (Delete h opens)) ()
+hClose (SafeHandle h) = SafeFiles (IO.hClose h)
+
+-- Delete a handler name from a list
+type family Delete (n :: Nat) (ns :: [Nat]) where
+            Delete n '[] = '[]
+            Delete n (n ': ns) = ns
+            Delete n (m ': ns) = m ': Delete n ns
+
+-- Membership predicate
+class Member (x :: Nat) (xs :: [Nat]) where
+instance {-# OVERLAPS #-} Member x (x ': xs) where
+instance Member x xs => Member x (y ': xs)
+
+-- hGetChar :: Handle -> IO Char
+hGetChar :: Member h opens =>
+     SafeHandle h
+  -> SafeFiles (St n opens) (St n opens) Char
+hGetChar (SafeHandle h) = SafeFiles (IO.hGetChar h)
+
+-- hPutChar :: Handle -> Char -> IO ()
+hPutChar :: Member h opens =>
+     SafeHandle h
+  -> Char -> SafeFiles (St n opens) (St n opens) ()
+hPutChar (SafeHandle h) c = SafeFiles (IO.hPutChar h c)
+
+-- hIsEOF :: Handler -> IO Bool
+hIsEOF :: Member h opens =>
+  SafeHandle h -> SafeFiles (St n opens) (St n opens) Bool
+hIsEOF (SafeHandle h) = SafeFiles (IO.hIsEOF h)
+
+-- Only allow running when every file is closed at the end
+runSafeFiles :: SafeFiles (St 0 '[]) (St n '[]) () -> IO ()
+runSafeFiles = unSafeFiles
diff --git a/src/Control/Effect/Parameterised/State.hs b/src/Control/Effect/Parameterised/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Parameterised/State.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE InstanceSigs #-}
+
+module Control.Effect.Parameterised.State where
+
+-- Bye Monads... as we know them
+import Prelude hiding (Monad(..))
+import Control.Effect.Parameterised
+
+newtype State s1 s2 a = State { runState :: s1 -> (a, s2) }
+
+-- State parameterised monad
+-- ... just like the
+instance PMonad State where
+  return :: a -> State s s a
+  return x = State (\s -> (x, s))
+
+  (>>=) :: State s1 s2 a -> (a -> State s2 s3 b) -> State s1 s3 b
+  (State m) >>= k =
+      State $ \s0 -> let (a, s1) = m s0
+                         State m' = k a in m' s1
diff --git a/src/Control/Effect/ParameterisedAsGraded.hs b/src/Control/Effect/ParameterisedAsGraded.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/ParameterisedAsGraded.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE KindSignatures, TypeFamilies, ConstraintKinds, PolyKinds, DataKinds #-}
+
+module Control.Effect.ParameterisedAsGraded 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