diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
new file mode 100644
--- /dev/null
+++ b/CODE_OF_CONDUCT.md
@@ -0,0 +1,45 @@
+# Contributor Code of Conduct
+
+As contributors and maintainers of this project, and in the interest
+of fostering an open and welcoming community, we pledge to respect all
+people who contribute through reporting issues, posting feature
+requests, updating documentation, submitting pull requests or patches,
+and other activities.
+
+We are committed to making participation in this project a
+harassment-free experience for everyone, regardless of level of
+experience, gender, gender identity and expression, sexual
+orientation, disability, personal appearance, body size, race,
+ethnicity, age, religion, or nationality.
+
+Examples of unacceptable behavior by participants include:
+
+* The use of sexualized language or imagery
+* Personal attacks
+* Trolling or insulting/derogatory comments
+* Public or private harassment
+* Publishing other's private information, such as physical or
+  electronic addresses, without explicit permission
+* Other unethical or unprofessional conduct.
+
+Project maintainers have the right and responsibility to remove, edit,
+or reject comments, commits, code, wiki edits, issues, and other
+contributions that are not aligned to this Code of Conduct. By
+adopting this Code of Conduct, project maintainers commit themselves
+to fairly and consistently applying these principles to every aspect
+of managing this project. Project maintainers who do not follow or
+enforce the Code of Conduct may be permanently removed from the
+project team.
+
+This code of conduct applies both within project spaces and in public
+spaces when an individual is representing the project or its
+community.
+
+Instances of abusive, harassing, or otherwise unacceptable behavior
+may be reported by opening an issue or contacting one or more of the
+project maintainers.
+
+This Code of Conduct is adapted from the
+[Contributor Covenant](http://contributor-covenant.org), version
+1.2.0, available at
+[http://contributor-covenant.org/version/1/2/0/](http://contributor-covenant.org/version/1/2/0/)
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Alej Cabrera
+
+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.
+
+    * Neither the name of Alej Cabrera nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,120 @@
+# Freer: Extensible Effects with Freer Monads
+
+Freer is an implementation of
+["Freer Monads, More Extensible Effects"](http://okmij.org/ftp/Haskell/extensible/more.pdf). Much
+of the implementation is a repackaging and cleaning up of the
+reference materials provided
+[here](http://okmij.org/ftp/Haskell/extensible/).
+
+# Features
+
+The key features of Freer are:
+
+* An efficient effect system for Haskell as a library
+* Implementations for several common Haskell monad instances:
+  * Reader
+  * Writer
+  * State
+  * StateRW: State in terms of Reader/Writer
+  * Trace
+  * Exception
+* Core components for defining your own Effects
+
+# Example: Teletype DSL
+
+Here's what using Freer looks like:
+
+```haskell
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+module Teletype where
+
+import Control.Monad.Freer
+import Control.Monad.Freer.Internal
+import System.Exit hiding (ExitSuccess)
+
+--------------------------------------------------------------------------------
+                          -- Effect Model --
+--------------------------------------------------------------------------------
+data Teletype s where
+  PutStrLn    :: String -> Teletype ()
+  GetLine     :: Teletype String
+  ExitSuccess :: Teletype ()
+
+putStrLn' :: Member Teletype r => String -> Eff r ()
+putStrLn' = send . PutStrLn
+
+getLine'  :: Member Teletype r => Eff r String
+getLine' = send GetLine
+
+exitSuccess' :: Member Teletype r => Eff r ()
+exitSuccess' = send ExitSuccess
+
+--------------------------------------------------------------------------------
+                     -- Effectful Interpreter --
+--------------------------------------------------------------------------------
+runTeletype :: Eff '[Teletype] w -> IO w
+runTeletype (Val x) = return x
+runTeletype (E u q) = case decomp u of
+              Right (PutStrLn msg) -> putStrLn msg  >> runTeletype (qApp q ())
+              Right GetLine        -> getLine      >>= \s -> runTeletype (qApp q s)
+              Right ExitSuccess    -> exitSuccess
+              Left  _              -> error "This cannot happen"
+
+--------------------------------------------------------------------------------
+                        -- Pure Interpreter --
+--------------------------------------------------------------------------------
+runTeletypePure :: [String] -> Eff '[Teletype] w -> [String]
+runTeletypePure inputs req = reverse (go inputs req [])
+  where go :: [String] -> Eff '[Teletype] w -> [String] -> [String]
+        go _      (Val _) acc = acc
+        go []     _       acc = acc
+        go (x:xs) (E u q) acc = case decomp u of
+          Right (PutStrLn msg) -> go (x:xs) (qApp q ()) (msg:acc)
+          Right GetLine        -> go xs     (qApp q x) acc
+          Right ExitSuccess    -> go xs     (Val ())   acc
+          Left _               -> go xs     (Val ())   acc
+```
+
+# Contributing
+
+Contributions are welcome! Documentation, examples, code, and
+feedback - they all help.
+
+Be sure to review the included code of conduct. This project adheres
+to the [Contributor's Covenant](http://contributor-covenant.org/). By
+participating in this project you agree to abide by its terms.
+
+## Developer Setup
+
+The easiest way to start contributing is to install
+[stack](https://github.com/commercialhaskell/stack). stack can install
+GHC/Haskell for you, and automates common developer tasks.
+
+The key commands are:
+
+* stack setup : install GHC
+* stack build
+* stack clean
+* stack haddock : builds documentation
+* stack test
+* stack bench
+* stack ghci : start a REPL instance
+
+# Licensing
+
+This project is distrubted under a BSD3 license. See the included
+LICENSE file for more details.
+
+# Acknowledgements
+
+This package would not be possible without the paper and the reference
+implementation. In particular:
+
+* Data.Open.Union maps to [OpenUnion41.hs](http://okmij.org/ftp/Haskell/extensible/OpenUnion41.hs)
+* Data.FTCQueue maps to [FTCQueue1](http://okmij.org/ftp/Haskell/extensible/FTCQueue1.hs)
+* Control.Monad.Freer* maps to [Union1.hs](http://okmij.org/ftp/Haskell/extensible/Eff1.hs)
+
+There will be deviations from the source.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/bench/Core.hs b/bench/Core.hs
new file mode 100644
--- /dev/null
+++ b/bench/Core.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DeriveFunctor #-}
+module Main where
+
+import Control.Monad
+import Control.Monad.Freer
+import Control.Monad.Freer.Internal
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.State
+import Control.Monad.Freer.StateRW
+
+import Criterion
+import Criterion.Main
+import qualified Control.Monad.State as MTL
+import qualified Control.Monad.Except as MTL
+import qualified Control.Monad.Free as Free
+
+--------------------------------------------------------------------------------
+                        -- State Benchmarks --
+--------------------------------------------------------------------------------
+oneGet :: Int -> (Int, Int)
+oneGet n = run (runState get n)
+
+countDown :: Int -> (Int,Int)
+countDown start = run (runState go start)
+  where go = get >>= (\n -> if n <= 0 then return n else put (n-1) >> go)
+
+countDownRW :: Int -> (Int,Int)
+countDownRW start = run (runStateR go start)
+  where go = ask >>= (\n -> if n <= 0 then return n else tell (n-1) >> go)
+
+countDownMTL :: Int -> (Int,Int)
+countDownMTL = MTL.runState go
+  where go = MTL.get >>= (\n -> if n <= 0 then return n else MTL.put (n-1) >> go)
+
+--------------------------------------------------------------------------------
+                       -- Exception + State --
+--------------------------------------------------------------------------------
+countDownExc :: Int -> Either String (Int,Int)
+countDownExc start = run $ runError (runState go start)
+  where go = get >>= (\n -> if n <= (0 :: Int) then throwError "wat" else put (n-1) >> go)
+
+countDownExcMTL :: Int -> Either String (Int,Int)
+countDownExcMTL = MTL.runStateT go
+  where go = MTL.get >>= (\n -> if n <= (0 :: Int) then MTL.throwError "wat" else MTL.put (n-1) >> go)
+
+--------------------------------------------------------------------------------
+                          -- Freer: Interpreter --
+--------------------------------------------------------------------------------
+data Http out where
+  Open :: String -> Http ()
+  Close :: Http ()
+  Post  :: String -> Http String
+  Get   :: Http String
+
+open' :: Member Http r => String -> Eff r ()
+open'  = send . Open
+
+close' :: Member Http r => Eff r ()
+close' = send Close
+
+post' :: Member Http r => String -> Eff r String
+post' = send . Post
+
+get' :: Member Http r => Eff r String
+get' = send Get
+
+runHttp :: Eff (Http ': r) w -> Eff r w
+runHttp (Val x) = return x
+runHttp (E u q) = case decomp u of
+  Right (Open _) -> runHttp (qApp q ())
+  Right Close    -> runHttp (qApp q ())
+  Right (Post d) -> runHttp (qApp q d)
+  Right Get      -> runHttp (qApp q "")
+  Left u'        -> E u' (tsingleton (runHttp . qApp q ))
+
+--------------------------------------------------------------------------------
+                          -- Free: Interpreter --
+--------------------------------------------------------------------------------
+data FHttpT x
+  = FOpen String x
+  | FClose x
+  | FPost String (String -> x)
+  | FGet (String -> x)
+    deriving Functor
+
+type FHttp = Free.Free FHttpT
+
+fopen' :: String -> FHttp ()
+fopen' s = Free.liftF $ FOpen s ()
+
+fclose' :: FHttp ()
+fclose' = Free.liftF $ FClose ()
+
+fpost' :: String -> FHttp String
+fpost' s = Free.liftF $ FPost s id
+
+fget' :: FHttp String
+fget' = Free.liftF $ FGet id
+
+runFHttp :: FHttp a -> Maybe a
+runFHttp (Free.Pure x) = return x
+runFHttp (Free.Free (FOpen _ n)) = runFHttp n
+runFHttp (Free.Free (FClose n))  = runFHttp n
+runFHttp (Free.Free (FPost s n)) = pure s  >>= runFHttp . n
+runFHttp (Free.Free (FGet n))    = pure "" >>= runFHttp . n
+
+--------------------------------------------------------------------------------
+                        -- Benchmark Suite --
+--------------------------------------------------------------------------------
+prog :: Member Http r => Eff r ()
+prog = open' "cats" >> get' >> post' "cats" >> close'
+
+prog' :: FHttp ()
+prog' = fopen' "cats" >> fget' >> fpost' "cats" >> fclose'
+
+p :: Member Http r => Int -> Eff r ()
+p count   =  open' "cats" >> replicateM_ count (get' >> post' "cats") >>  close'
+
+p' :: Int -> FHttp ()
+p' count  = fopen' "cats" >> replicateM_ count (fget' >> fpost' "cats") >> fclose'
+
+main :: IO ()
+main =
+  defaultMain [
+    bgroup "State" [
+        bench "get"          $ whnf oneGet 0
+    ],
+    bgroup "Countdown Bench" [
+        bench "freer.State"    $ whnf countDown 10000
+      , bench "freer.StateRW"  $ whnf countDownRW 10000
+      , bench "mtl.State"      $ whnf countDownMTL 10000
+    ],
+    bgroup "Countdown+Except Bench" [
+        bench "freer.ExcState"  $ whnf countDownExc 10000
+      , bench "mtl.ExceptState" $ whnf countDownExcMTL 10000
+    ],
+    bgroup "HTTP Simple DSL" [
+        bench "freer" $ whnf (run . runHttp) prog
+      , bench "free" $ whnf runFHttp prog'
+
+      , bench "freerN"      $ whnf (run . runHttp . p) 1000000
+      , bench "freeN"       $ whnf (runFHttp . p')     1000000
+    ]
+  ]
diff --git a/changelog.md b/changelog.md
new file mode 100644
--- /dev/null
+++ b/changelog.md
@@ -0,0 +1,38 @@
+# 0.2.2.1 (Sep. 14, 2015)
+
+* Document ALL THE THINGS
+
+# 0.2.2.0 (Sep. 13, 2015)
+
+* Add bench suite
+
+# 0.2.1.0 (Sep. 13, 2015)
+
+* Add test suite
+
+# 0.2.0.2 (Sep. 12, 2015)
+
+* Clean up language extensions per file
+* Add Teletype DSL to the README
+
+# 0.2.0.1 (Sep. 12, 2015)
+
+* Add Teletype DSL example
+* Expose `send` in public interface
+
+# 0.2.0.0 (Sep. 12, 2015)
+
+* Implement NonDetEff
+* Separate Cut/Coroutine out from Internals
+  * Partial implementation: won't compile yet
+* Extract remaining examples from Internal comments
+
+# 0.1.1.0 (Sep. 12, 2015)
+
+* Warnings clean up
+* Examples separated from primary implementation
+* Initial project documentation added
+
+# 0.1.0.0 (Sep. 12, 2015)
+
+* Initial release
diff --git a/examples/src/Common.hs b/examples/src/Common.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/Common.hs
@@ -0,0 +1,6 @@
+module Common where
+
+import Control.Applicative
+
+add :: Applicative f => f Int -> f Int -> f Int
+add = liftA2 (+)
diff --git a/examples/src/Coroutine.hs b/examples/src/Coroutine.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/Coroutine.hs
@@ -0,0 +1,215 @@
+module Coroutine where
+
+-- import Control.Monad.Freer.Coroutine
+
+{-
+
+-- First example of coroutines
+yieldInt :: Member (Yield Int ()) r => Int -> Eff r ()
+yieldInt = yield
+
+th1 :: Member (Yield Int ()) r => Eff r ()
+th1 = yieldInt 1 >> yieldInt 2
+
+
+c1 = runTrace (loop =<< runC th1)
+ where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+       loop Done    = trace "Done"
+{-
+1
+2
+Done
+-}
+
+-- Add dynamic variables
+-- The code is essentially the same as that in transf.hs (only added
+-- a type specializtion on yield). The inferred signature is different though.
+-- Before it was
+--    th2 :: MonadReader Int m => CoT Int m ()
+-- Now it is more general:
+th2 :: (Member (Yield Int ()) r, Member (Reader Int) r) => Eff r ()
+th2 = ask >>= yieldInt >> (ask >>= yieldInt)
+
+
+-- Code is essentially the same as in transf.hs; no liftIO though
+c2 = runTrace $ runReader (loop =<< runC th2) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+       loop Done    = trace "Done"
+{-
+10
+10
+Done
+-}
+
+-- locally changing the dynamic environment for the suspension
+c21 = runTrace $ runReader (loop =<< runC th2) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+       loop Done    = trace "Done"
+{-
+10
+11
+Done
+-}
+
+-- Real example, with two sorts of local rebinding
+th3 :: (Member (Yield Int ()) r, Member (Reader Int) r) => Eff r ()
+th3 = ay >> ay >> local (+(10::Int)) (ay >> ay)
+ where ay = ask >>= yieldInt
+
+c3 = runTrace $ runReader (loop =<< runC th3) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> k () >>= loop
+       loop Done    = trace "Done"
+{-
+10
+10
+20
+20
+Done
+-}
+
+-- locally changing the dynamic environment for the suspension
+c31 = runTrace $ runReader (loop =<< runC th3) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+       loop Done    = trace "Done"
+{-
+10
+11
+21
+21
+Done
+-}
+-- The result is exactly as expected and desired: the coroutine shares the
+-- dynamic environment with its parent; however, when the environment
+-- is locally rebound, it becomes private to coroutine.
+
+-- We now make explicit that the client computation, run by th4,
+-- is abstract. We abstract it out of th4
+c4 = runTrace $ runReader (loop =<< runC (th4 client)) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (+(1::Int)) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       th4 cl = cl >> local (+(10::Int)) cl
+       client = ay >> ay
+       ay     = ask >>= yieldInt
+
+{-
+10
+11
+21
+21
+Done
+-}
+
+-- Even more dynamic example
+c5 = runTrace $ runReader (loop =<< runC (th client)) (10::Int)
+ where loop (Y x k) = trace (show (x::Int)) >> local (\y->x+1) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       client = ay >> ay >> ay
+       ay     = ask >>= yieldInt
+
+       -- There is no polymorphic recursion here
+       th cl = do
+         cl
+         v <- ask
+         (if v > (20::Int) then id else local (+(5::Int))) cl
+         if v > (20::Int) then return () else local (+(10::Int)) (th cl)
+{-
+10
+11
+12
+18
+18
+18
+29
+29
+29
+29
+29
+29
+Done
+-}
+
+-- And even more
+c7 = runTrace $
+      runReader (runReader (loop =<< runC (th client)) (10::Int)) (1000::Double)
+ where loop (Y x k) = trace (show (x::Int)) >>
+                      local (\y->fromIntegral (x+1)::Double) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       client = ay >> ay >> ay
+       ay     = ask >>= \x -> ask >>=
+                 \y -> yieldInt (x + round (y::Double))
+
+       -- There is no polymorphic recursion here
+       th cl = do
+         cl
+         v <- ask
+         (if v > (20::Int) then id else local (+(5::Int))) cl
+         if v > (20::Int) then return () else local (+(10::Int)) (th cl)
+
+{-
+1010
+1021
+1032
+1048
+1064
+1080
+1101
+1122
+1143
+1169
+1195
+1221
+1252
+1283
+1314
+1345
+1376
+1407
+Done
+-}
+
+c7' = runTrace $
+      runReader (runReader (loop =<< runC (th client)) (10::Int)) (1000::Double)
+ where loop (Y x k) = trace (show (x::Int)) >>
+                      local (\y->fromIntegral (x+1)::Double) (k ()) >>= loop
+       loop Done    = trace "Done"
+
+       -- cl, client, ay are monomorphic bindings
+       client = ay >> ay >> ay
+       ay     = ask >>= \x -> ask >>=
+                 \y -> yieldInt (x + round (y::Double))
+
+       -- There is no polymorphic recursion here
+       th cl = do
+         cl
+         v <- ask
+         (if v > (20::Int) then id else local (+(5::Double))) cl
+         if v > (20::Int) then return () else local (+(10::Int)) (th cl)
+{-
+1010
+1021
+1032
+1048
+1048
+1048
+1069
+1090
+1111
+1137
+1137
+1137
+1168
+1199
+1230
+1261
+1292
+1323
+Done
+-}
+
+-}
diff --git a/examples/src/Cut.hs b/examples/src/Cut.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/Cut.hs
@@ -0,0 +1,33 @@
+module Cut where
+
+-- import Control.Monad.Freer.Cut
+
+
+{-
+-- The signature is inferred
+tcut1 :: (Member Choose r, Member (Exc CutFalse) r) => Eff r Int
+tcut1 = (return (1::Int) `mplus'` return 2) `mplus'`
+         ((cutfalse `mplus'` return 4) `mplus'`
+          return 5)
+
+tcut1r = run . makeChoice $ call tcut1
+-- [1,2]
+
+tcut2 = return (1::Int) `mplus'`
+         call (return 2 `mplus'` (cutfalse `mplus'` return 3) `mplus'`
+               return 4)
+       `mplus'` return 5
+
+-- Here we see nested call. It poses no problems...
+tcut2r = run . makeChoice $ call tcut2
+-- [1,2,5]
+
+-- More nested calls
+tcut3 = call tcut1 `mplus'` call (tcut2 `mplus'` cutfalse)
+tcut3r = run . makeChoice $ call tcut3
+-- [1,2,1,2,5]
+
+tcut4 = call tcut1 `mplus'`  (tcut2 `mplus'` cutfalse)
+tcut4r = run . makeChoice $ call tcut4
+-- [1,2,1,2,5]
+-}
diff --git a/examples/src/Fresh.hs b/examples/src/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/Fresh.hs
@@ -0,0 +1,15 @@
+module Fresh where
+
+import Control.Monad.Freer.Fresh
+import Control.Monad.Freer.Trace
+
+traceFresh :: IO ()
+traceFresh = runTrace $ flip runFresh' 0 $ do
+  n <- fresh
+  trace $ "Fresh " ++ show n
+  n' <- fresh
+  trace $ "Fresh " ++ show n'
+{-
+Fresh 0
+Fresh 1
+-}
diff --git a/examples/src/Main.hs b/examples/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/Main.hs
@@ -0,0 +1,4 @@
+module Main where
+
+main :: IO ()
+main = print "placeholder"
diff --git a/examples/src/NonDetEff.hs b/examples/src/NonDetEff.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/NonDetEff.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE FlexibleContexts #-}
+module NonDetEff where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Freer
+
+ifte :: Member NonDetEff r
+     => Eff r a -> (a -> Eff r b) -> Eff r b -> Eff r b
+ifte t th el = (t >>= th) <|> el
+
+testIfte :: Member NonDetEff r => Eff r Int
+testIfte = do
+  n <- gen
+  ifte (do d <- gen
+           guard $ d < n && n `mod` d == 0)
+       (const mzero)
+       (return n)
+  where gen = msum . fmap return $ [2..30]
+
+testIfteRun :: [Int]
+testIfteRun = run . makeChoiceA $ testIfte
diff --git a/examples/src/Teletype.hs b/examples/src/Teletype.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/Teletype.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+module Teletype where
+
+import Control.Monad.Freer
+import Control.Monad.Freer.Internal
+import System.Exit hiding (ExitSuccess)
+
+--------------------------------------------------------------------------------
+                          -- Effect Model --
+--------------------------------------------------------------------------------
+data Teletype s where
+  PutStrLn    :: String -> Teletype ()
+  GetLine     :: Teletype String
+  ExitSuccess :: Teletype ()
+
+putStrLn' :: Member Teletype r => String -> Eff r ()
+putStrLn' = send . PutStrLn
+
+getLine'  :: Member Teletype r => Eff r String
+getLine' = send GetLine
+
+exitSuccess' :: Member Teletype r => Eff r ()
+exitSuccess' = send ExitSuccess
+
+--------------------------------------------------------------------------------
+                     -- Effectful Interpreter --
+--------------------------------------------------------------------------------
+runTeletype :: Eff '[Teletype] w -> IO w
+runTeletype (Val x) = return x
+runTeletype (E u q) = case decomp u of
+              Right (PutStrLn msg) -> putStrLn msg  >> runTeletype (qApp q ())
+              Right GetLine        -> getLine      >>= \s -> runTeletype (qApp q s)
+              Right ExitSuccess    -> exitSuccess
+              Left  _              -> error "This cannot happen"
+
+--------------------------------------------------------------------------------
+                        -- Pure Interpreter --
+--------------------------------------------------------------------------------
+runTeletypePure :: [String] -> Eff '[Teletype] w -> [String]
+runTeletypePure inputs req = reverse (go inputs req [])
+  where go :: [String] -> Eff '[Teletype] w -> [String] -> [String]
+        go _      (Val _) acc = acc
+        go []     _       acc = acc
+        go (x:xs) (E u q) acc = case decomp u of
+          Right (PutStrLn msg) -> go (x:xs) (qApp q ()) (msg:acc)
+          Right GetLine        -> go xs     (qApp q x) acc
+          Right ExitSuccess    -> go xs     (Val ())   acc
+          Left _               -> go xs     (Val ())   acc
diff --git a/examples/src/Trace.hs b/examples/src/Trace.hs
new file mode 100644
--- /dev/null
+++ b/examples/src/Trace.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+module Trace where
+
+import Control.Monad.Freer
+import Control.Monad.Freer.Reader
+import Control.Monad.Freer.Trace
+
+import Common
+
+-- Higher-order effectful function
+-- The inferred type shows that the Trace affect is added to the effects
+-- of r
+mapMdebug:: (Show a, Member Trace r) =>
+     (a -> Eff r b) -> [a] -> Eff r [b]
+mapMdebug _ [] = return []
+mapMdebug f (h:t) = do
+  trace $ "mapMdebug: " ++ show h
+  h' <- f h
+  t' <- mapMdebug f t
+  return (h':t')
+
+tMd :: IO [Int]
+tMd = runTrace $ runReader (mapMdebug f [1..5]) (10::Int)
+ where f x = ask `add` return x
+{-
+mapMdebug: 1
+mapMdebug: 2
+mapMdebug: 3
+mapMdebug: 4
+mapMdebug: 5
+[11,12,13,14,15]
+-}
+
+-- duplicate layers
+tdup :: IO ()
+tdup = runTrace $ runReader m (10::Int)
+ where
+ m = do
+     runReader tr (20::Int)
+     tr
+ tr = do
+      v <- ask
+      trace $ "Asked: " ++ show (v::Int)
+{-
+Asked: 20
+Asked: 10
+-}
diff --git a/freer.cabal b/freer.cabal
new file mode 100644
--- /dev/null
+++ b/freer.cabal
@@ -0,0 +1,104 @@
+name:                freer
+version:             0.2.2.1
+synopsis:            Implementation of the Freer Monad
+license:             BSD3
+license-file:        LICENSE
+author:              Alej Cabrera
+maintainer:          cpp.cabrera@gmail.com
+copyright:           Alej Cabrera 2015
+homepage:            https://gitlab.com/cpp.cabrera/freer
+bug-reports:         https://gitlab.com/cpp.cabrera/freer/issues
+category:            Control
+build-type:          Simple
+cabal-version:       >=1.18
+tested-with:         GHC==7.10.2
+description:
+
+    Freer is an implementation of "Freer Monads, More Extensible
+    Effects"
+    .
+    The key features of Freer are:
+    .
+    * An efficient effect system for Haskell - as a library!
+    .
+    * Implementations for several common Haskell monad instances:
+    .
+    * Core components for defining your own Effects
+
+extra-source-files:
+    README.md
+    changelog.md
+    CODE_OF_CONDUCT.md
+
+source-repository head
+    type: git
+    location: git clone https://gitlab.com/cpp.cabrera/freer.git
+
+library
+  exposed-modules:     Control.Monad.Freer
+                     , Control.Monad.Freer.Coroutine
+                     , Control.Monad.Freer.Cut
+                     , Control.Monad.Freer.Exception
+                     , Control.Monad.Freer.Fresh
+                     , Control.Monad.Freer.Internal
+                     , Control.Monad.Freer.Reader
+                     , Control.Monad.Freer.State
+                     , Control.Monad.Freer.StateRW
+                     , Control.Monad.Freer.Trace
+                     , Control.Monad.Freer.Writer
+                     , Data.FTCQueue
+                     , Data.Open.Union
+
+  build-depends:       base >=4.7 && <4.9
+  hs-source-dirs:      src
+  ghc-options:         -Wall
+  default-language:    Haskell2010
+
+executable examples
+  main-is:             Main.hs
+  other-modules:       Common
+                     , Coroutine
+                     , Cut
+                     , Fresh
+                     , NonDetEff
+                     , Teletype
+                     , Trace
+  build-depends:       base >=4.7 && <4.9
+                     , freer
+  hs-source-dirs:      examples/src
+  ghc-options:         -Wall
+  default-language:    Haskell2010
+
+test-suite test
+  default-language: Haskell2010
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   tests
+  main-is:          Tests.hs
+  other-modules:       Tests.Common
+                     , Tests.Exception
+                     , Tests.Fresh
+                     , Tests.NonDetEff
+                     , Tests.Reader
+                     , Tests.State
+                     , Tests.StateRW
+  build-depends:    base
+                  , freer
+                  , tasty
+                  , tasty-hunit
+                  , tasty-quickcheck
+                  , QuickCheck
+
+  ghc-options: -Wall
+
+benchmark core
+  default-language: Haskell2010
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   bench
+  main-is:          Core.hs
+  build-depends:    base
+                  , freer
+                  , criterion
+                  , mtl
+                  , free
+
+  ghc-options: -Wall -O2
diff --git a/src/Control/Monad/Freer.hs b/src/Control/Monad/Freer.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer.hs
@@ -0,0 +1,22 @@
+{-|
+Module      : Control.Monad.Freer
+Description : Freer - an extensible effects library
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+-}
+module Control.Monad.Freer (
+  Member,
+  Eff,
+  run,
+  send,
+
+  NonDetEff(..),
+  makeChoiceA,
+  msplit
+) where
+
+import Control.Monad.Freer.Internal
diff --git a/src/Control/Monad/Freer/Coroutine.hs b/src/Control/Monad/Freer/Coroutine.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Coroutine.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+{-|
+Module      : Control.Monad.Freer.Coroutine
+Description : Composable coroutine effects layer.
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : broken
+Portability : POSIX
+
+An effect to compose functions with the ability to yield.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Coroutine (
+  Yield,
+  yield,
+  Status(..)
+) where
+
+import Control.Monad.Freer.Internal
+
+-- | A type representing a yielding of control
+-- a: The current type
+-- b: The input to the continuation function
+-- v: The output of the continuation
+data Yield a b v = Yield a (b -> v)
+    deriving (Functor)
+
+-- | Lifts a value and a function into the Coroutine effect
+yield :: (Member (Yield a b) r) => a -> (b -> c) -> Eff r c
+yield x f = send (Yield x f)
+
+-- |
+-- Status of a thread: done or reporting the value of the type a and
+-- resuming with the value of type b
+data Status r a b = Done | Continue a (b -> Eff r (Status r a b))
+
+{- FIXME: this does not compile
+-- Launch a thread and report its status
+runC :: Eff (Yield a b ': r) w -> Eff r (Y r a b)
+runC m = loop m
+  where loop :: Monad m => Eff a b -> m (Y r c d)
+        loop (Val _)  = return Done
+        loop (E u u') = handleRelay u loop $
+                          \(Yield x k) -> return (Y x (loop . k))
+-}
diff --git a/src/Control/Monad/Freer/Cut.hs b/src/Control/Monad/Freer/Cut.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Cut.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+
+{-|
+Module      : Control.Monad.Freer.Cut
+Description : An implementation of logical Cut
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : broken
+Portability : POSIX
+
+Composable handler for logical Cut effects. Implemented in terms of
+Exc effect.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Cut (
+  CutFalse,
+  cutFalse,
+  -- call
+) where
+
+-- import Control.Monad
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Internal
+
+data CutFalse = CutFalse
+-- data Choose a b = Choose [a] b
+
+-- | Implementation of logical Cut using Exc effects.
+cutFalse :: Member (Exc CutFalse) r => Eff r a
+cutFalse = throwError CutFalse
+
+{-
+call :: Member (Exc CutFalse) r => Eff (Exc CutFalse ': r) a -> Eff r a
+call m = loop [] m where
+ loop jq (Val x) = return x `mplus` next jq          -- (C2)
+ loop jq (E u q) = case decomp u of
+    Right (Exc CutFalse) -> mzero  -- drop jq (F2)
+    Left u -> check jq u
+
+ check jq u | Just (Choose [] _) <- prj u  = next jq  -- (C1)
+ check jq u | Just (Choose [x] k) <- prj u = loop jq (k x)  -- (C3), optim
+ check jq u | Just (Choose lst k) <- prj u = next $ map k lst ++ jq -- (C3)
+ check jq u = send (\k -> fmap k u) >>= loop jq      -- (C4)
+
+ next []    = mzero
+ next (h:t) = loop t h
+-}
diff --git a/src/Control/Monad/Freer/Exception.hs b/src/Control/Monad/Freer/Exception.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Exception.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+{-|
+Module      : Control.Monad.Freer.Exception
+Description : An Exception effect and handler.
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+Composable handler for Exception effects. Communicates success/failure
+via an Either type.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Exception (
+  Exc(..),
+  throwError,
+  runError,
+  catchError
+) where
+
+import Control.Monad.Freer.Internal
+
+--------------------------------------------------------------------------------
+                           -- Exceptions --
+--------------------------------------------------------------------------------
+-- | Exceptions of the type e; no resumption
+newtype Exc e v = Exc e
+
+-- | Throws an error carrying information of type e
+throwError :: (Member (Exc e) r) => e -> Eff r a
+throwError e = send (Exc e)
+
+-- | Handler for exception effects
+-- If there are no exceptions thrown, returns Right If exceptions are
+-- thrown and not handled, returns Left, interrupting the execution of
+-- any other effect handlers.
+runError :: Eff (Exc e ': r) a -> Eff r (Either e a)
+runError =
+   handleRelay (return . Right) (\ (Exc e) _k -> return (Left e))
+
+-- | A catcher for Exceptions. Handlers are allowed to rethrow
+-- exceptions.
+catchError :: Member (Exc e) r =>
+        Eff r a -> (e -> Eff r a) -> Eff r a
+catchError m handle = interpose return (\(Exc e) _k -> handle e) m
diff --git a/src/Control/Monad/Freer/Fresh.hs b/src/Control/Monad/Freer/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Fresh.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+
+{-|
+Module      : Control.Monad.Freer.Fresh
+Description : Generation of fresh integers as an effect.
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : broken
+Portability : POSIX
+
+Composable handler for Fresh effects. This is likely to be of use when
+implementing De Bruijn naming/scopes.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Fresh (
+  Fresh,
+  fresh,
+  runFresh'
+) where
+
+import Control.Monad.Freer.Internal
+
+--------------------------------------------------------------------------------
+                             -- Fresh --
+--------------------------------------------------------------------------------
+-- | Fresh effect model
+data Fresh v where
+  Fresh :: Fresh Int
+
+-- | Request a fresh effect
+fresh :: Member Fresh r => Eff r Int
+fresh = send Fresh
+
+-- | Handler for Fresh effects, with an Int for a starting value
+runFresh' :: Eff (Fresh ': r) w -> Int -> Eff r w
+runFresh' m s =
+  handleRelayS s (\_s x -> return x)
+                 (\s' Fresh k -> (k $! s'+1) s')
+                 m
diff --git a/src/Control/Monad/Freer/Internal.hs b/src/Control/Monad/Freer/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Internal.hs
@@ -0,0 +1,213 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+-- The following is needed to define MonadPlus instance. It is decidable
+-- (there is no recursion!), but GHC cannot see that.
+-- TODO: remove once GHC can deduce the decidability of this instance
+{-# LANGUAGE UndecidableInstances #-}
+
+{-|
+Module      : Control.Monad.Freer.Internal
+Description : Mechanisms to make effects work
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+Internal machinery for this effects library. This includes:
+
+* Eff data type, for expressing effects
+* NonDetEff data type, for nondeterministic effects
+* Functions for facilitating the construction of effects and their handlers
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Internal (
+  Eff(..),
+  Member(..),
+  Arr,
+  Arrs,
+  Union,
+
+  NonDetEff(..),
+  makeChoiceA,
+  msplit,
+
+  decomp,
+  tsingleton,
+
+  qApp,
+  qComp,
+  send,
+  run,
+  handleRelay,
+  handleRelayS,
+  interpose,
+) where
+
+import Control.Monad
+import Control.Applicative
+import Data.Open.Union
+import Data.FTCQueue
+
+
+-- |
+-- Effectful arrow type: a function from a to b that also does effects
+-- denoted by r
+type Arr r a b = a -> Eff r b
+
+-- |
+-- An effectful function from 'a' to 'b' that is a composition of
+-- several effectful functions. The paremeter r describes the overall
+-- effect. The composition members are accumulated in a type-aligned
+-- queue.
+type Arrs r a b = FTCQueue (Eff r) a b
+
+-- |
+-- The Eff representation.
+--
+-- Status of a coroutine (client):
+-- * Val: Done with the value of type a
+-- * E  : Sending a request of type Union r with the continuation Arrs r b a
+data Eff r a = Val a
+             | forall b. E (Union r b) (Arrs r b a)
+
+-- | Function application in the context of an array of effects, Arrs r b w
+qApp :: Arrs r b w -> b -> Eff r w
+qApp q' x =
+   case tviewl q' of
+   TOne k  -> k x
+   k :| t -> case k x of
+     Val y -> qApp t y
+     E u q -> E u (q >< t)
+
+-- | Composition of effectful arrows
+-- Allows for the caller to change the effect environment, as well
+qComp :: Arrs r a b -> (Eff r b -> Eff r' c) -> Arr r' a c
+qComp g h a = h $ qApp g a
+
+instance Functor (Eff r) where
+  {-# INLINE fmap #-}
+  fmap f (Val x) = Val (f x)
+  fmap f (E u q) = E u (q |> (Val . f))
+
+instance Applicative (Eff r) where
+  {-# INLINE pure #-}
+  {-# INLINE (<*>) #-}
+  pure = Val
+  Val f <*> Val x = Val $ f x
+  Val f <*> E u q = E u (q |> (Val . f))
+  E u q <*> Val x = E u (q |> (Val . ($ x)))
+  E u q <*> m     = E u (q |> (`fmap` m))
+
+instance Monad (Eff r) where
+  {-# INLINE return #-}
+  {-# INLINE (>>=) #-}
+  return = Val
+  Val x >>= k = k x
+  E u q >>= k = E u (q |> k)
+
+-- | send a request and wait for a reply
+send :: Member t r => t v -> Eff r v
+send t = E (inj t) (tsingleton Val)
+
+--------------------------------------------------------------------------------
+                       -- Base Effect Runner --
+--------------------------------------------------------------------------------
+-- | Runs a set of Effects. Requires that all effects are consumed.
+-- Typically composed as follows:
+-- > run . runEff1 eff1Arg . runEff2 eff2Arg1 eff2Arg2 (program)
+run :: Eff '[] w -> w
+run (Val x) = x
+run _       = error "Internal:run - This (E) should never happen"
+
+-- the other case is unreachable since Union [] a cannot be
+-- constructed. Therefore, run is a total function if its argument
+-- terminates.
+
+-- | Given a request, either handle it or relay it.
+handleRelay :: (a -> Eff r w) ->
+               (forall v. t v -> Arr r v w -> Eff r w) ->
+               Eff (t ': r) a -> Eff r w
+handleRelay ret h = loop
+ where
+  loop (Val x)  = ret x
+  loop (E u' q)  = case decomp u' of
+    Right x -> h x k
+    Left  u -> E u (tsingleton k)
+   where k = qComp q loop
+
+-- | Parameterized 'handleRelay'
+-- Allows sending along some state to be handled for the target
+-- effect, or relayed to a handler that can handle the target effect.
+handleRelayS :: s ->
+                (s -> a -> Eff r w) ->
+                (forall v. s -> t v -> (s -> Arr r v w) -> Eff r w) ->
+                Eff (t ': r) a -> Eff r w
+handleRelayS s' ret h = loop s'
+  where
+    loop s (Val x)  = ret s x
+    loop s (E u' q)  = case decomp u' of
+      Right x -> h s x k
+      Left  u -> E u (tsingleton (k s))
+     where k s'' x = loop s'' $ qApp q x
+
+-- | Intercept the request and possibly reply to it, but leave it
+-- unhandled
+interpose :: Member t r =>
+             (a -> Eff r w) -> (forall v. t v -> Arr r v w -> Eff r w) ->
+             Eff r a -> Eff r w
+interpose ret h = loop
+ where
+   loop (Val x)  = ret x
+   loop (E u q)  = case prj u of
+     Just x -> h x k
+     _      -> E u (tsingleton k)
+    where k = qComp q loop
+
+--------------------------------------------------------------------------------
+                    -- Nondeterministic Choice --
+--------------------------------------------------------------------------------
+-- | A data type for representing nondeterminstic choice
+data NonDetEff a where
+  MZero :: NonDetEff a
+  MPlus :: NonDetEff Bool
+
+instance Member NonDetEff r => Alternative (Eff r) where
+  empty = mzero
+  (<|>) = mplus
+
+instance Member NonDetEff r => MonadPlus (Eff r) where
+  mzero       = send MZero
+  mplus m1 m2 = send MPlus >>= \x -> if x then m1 else m2
+
+-- | A handler for nondeterminstic effects
+makeChoiceA :: Alternative f
+            => Eff (NonDetEff ': r) a -> Eff r (f a)
+makeChoiceA =
+  handleRelay (return . pure) $ \m k ->
+    case m of
+      MZero -> return empty
+      MPlus -> liftM2 (<|>) (k True) (k False)
+
+msplit :: Member NonDetEff r
+       => Eff r a -> Eff r (Maybe (a, Eff r a))
+msplit = loop []
+  where loop jq (Val x)     = return (Just (x, msum jq))
+        loop jq (E u q) =
+          case prj u of
+            Just MZero ->
+              case jq of
+                []     -> return Nothing
+                (j:jq') -> loop jq' j
+            Just MPlus -> loop (qApp q False : jq) (qApp q True)
+            Nothing    -> E u (tsingleton k)
+              where k = qComp q (loop jq)
diff --git a/src/Control/Monad/Freer/Reader.hs b/src/Control/Monad/Freer/Reader.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Reader.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+{-|
+Module      : Control.Monad.Freer.Reader
+Description : Reader effects, for encapsulating an environment
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+Composable handler for Reader effects. Handy for encapsulating an
+environment with immutable state for interpreters.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Reader (
+  Reader(..),
+
+  ask,
+  runReader,
+  local
+) where
+
+import Control.Monad.Freer.Internal
+
+-- |
+data Reader e v where
+  Reader :: Reader e e
+
+-- | Request a value for the environment
+ask :: (Member (Reader e) r) => Eff r e
+ask = send Reader
+
+-- | Handler for reader effects
+runReader :: Eff (Reader e ': r) w -> e -> Eff r w
+runReader m e = handleRelay return (\Reader k -> k e) m
+
+-- |
+-- Locally rebind the value in the dynamic environment
+-- This function is like a relay; it is both an admin for Reader requests,
+-- and a requestor of them
+local :: forall e a r. Member (Reader e) r =>
+         (e -> e) -> Eff r a -> Eff r a
+local f m = do
+  e0 <- ask
+  let e = f e0
+  let h :: Reader e v -> Arr r v a -> Eff r a
+      h Reader g = g e
+  interpose return h m
diff --git a/src/Control/Monad/Freer/State.hs b/src/Control/Monad/Freer/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/State.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+{-|
+Module      : Control.Monad.Freer.State
+Description : State effects, for state-carrying computations.
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+Composable handler for State effects.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.State (
+  State,
+  get,
+  put,
+  runState,
+
+  ProxyState(..),
+  transactionState
+) where
+
+import Control.Monad.Freer.Internal
+
+--------------------------------------------------------------------------------
+                         -- State, strict --
+--------------------------------------------------------------------------------
+
+-- | Strict State effects: one can either Get values or Put them
+data State s v where
+  Get :: State s s
+  Put :: !s -> State s ()
+
+-- | Retrieve state
+get :: Member (State s) r => Eff r s
+get = send Get
+
+-- | Modify state
+put :: Member (State s) r => s -> Eff r ()
+put s = send (Put s)
+
+-- | Handler for State effects
+runState :: Eff (State s ': r) w -> s -> Eff r (w,s)
+runState (Val x) s = return (x,s)
+runState (E u q) s = case decomp u of
+  Right Get      -> runState (qApp q s) s
+  Right (Put s') -> runState (qApp q ()) s'
+  Left  u'       -> E u' (tsingleton (\x -> runState (qApp q x) s))
+
+
+data ProxyState s = ProxyState
+
+-- |
+-- An encapsulated State handler, for transactional semantics
+-- The global state is updated only if the transactionState finished
+-- successfully
+transactionState :: forall s r w. Member (State s) r =>
+                    ProxyState s -> Eff r w -> Eff r w
+transactionState _ m = do s <- get; loop s m
+ where
+   loop :: s -> Eff r w -> Eff r w
+   loop s (Val x) = put s >> return x
+   loop s (E (u :: Union r b) q) = case prj u :: Maybe (State s b) of
+     Just Get      -> loop s (qApp q s)
+     Just (Put s') -> loop s'(qApp q ())
+     _             -> E u (tsingleton k) where k = qComp q (loop s)
diff --git a/src/Control/Monad/Freer/StateRW.hs b/src/Control/Monad/Freer/StateRW.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/StateRW.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+
+{-|
+Module      : Control.Monad.Freer.StateRW
+Description : State effects in terms of Reader/Writer
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+Composable handler for State effects in terms of Reader/Writer
+effects. This module is more a tutorial on how to compose handlers. It
+is slightly slower than a dedicated State handler.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.StateRW (
+  runStateR,
+  Reader,
+  Writer,
+  tell,
+  ask
+) where
+
+import Control.Monad.Freer.Reader
+import Control.Monad.Freer.Writer
+import Control.Monad.Freer.Internal
+
+-- | State handler, using Reader/Writer effects
+runStateR :: Eff (Writer s ': Reader s ': r) w -> s -> Eff r (w,s)
+runStateR m s = loop s m
+ where
+   loop :: s -> Eff (Writer s ': Reader s ': r) w -> Eff r (w,s)
+   loop s' (Val x) = return (x,s')
+   loop s' (E u q) = case decomp u of
+     Right (Writer o) -> k o ()
+     Left  u'  -> case decomp u' of
+       Right Reader -> k s' s'
+       Left u'' -> E u'' (tsingleton (k s'))
+    where k s'' = qComp q (loop s'')
diff --git a/src/Control/Monad/Freer/Trace.hs b/src/Control/Monad/Freer/Trace.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Trace.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+
+{-|
+Module      : Control.Monad.Freer.Trace
+Description : Composable Trace effects
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+Composable handler for Trace effects. Trace allows one to debug the
+operation of sequences of effects by outputing to the console.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Trace (
+  Trace,
+  trace,
+  runTrace
+) where
+
+import Control.Monad.Freer.Internal
+
+-- | A Trace effect; takes a String and performs output
+data Trace v where
+  Trace :: String -> Trace ()
+
+-- | Printing a string in a trace
+trace :: Member Trace r => String -> Eff r ()
+trace = send . Trace
+
+-- | An IO handler for Trace effects
+runTrace :: Eff '[Trace] w -> IO w
+runTrace (Val x) = return x
+runTrace (E u q) = case decomp u of
+     Right (Trace s) -> putStrLn s >> runTrace (qApp q ())
+     Left _          -> error "runTrace:Left - This should never happen"
diff --git a/src/Control/Monad/Freer/Writer.hs b/src/Control/Monad/Freer/Writer.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Freer/Writer.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE DataKinds #-}
+
+{-|
+Module      : Control.Monad.Freer.Writer
+Description : Composable Writer effects -
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+Writer effects, for writing changes to an attached environment.
+
+Using <http://okmij.org/ftp/Haskell/extensible/Eff1.hs> as a
+starting point.
+
+-}
+module Control.Monad.Freer.Writer (
+  Writer(..),
+  tell,
+  runWriter
+) where
+
+import Control.Monad.Freer.Internal
+
+-- | Writer effects - send outputs to an effect environment
+data Writer o x where
+  Writer :: o -> Writer o ()
+
+-- | Send a change to the attached environment
+tell :: Member (Writer o) r => o -> Eff r ()
+tell o = send $ Writer o
+
+-- | Simple handler for Writer effects
+runWriter :: Eff (Writer o ': r) a -> Eff r (a,[o])
+runWriter = handleRelay (\x -> return (x,[]))
+                  (\ (Writer o) k -> k () >>= \ (x,l) -> return (x,o:l))
diff --git a/src/Data/FTCQueue.hs b/src/Data/FTCQueue.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/FTCQueue.hs
@@ -0,0 +1,79 @@
+{-# LANGUAGE GADTs #-}
+
+{-|
+Module      : Data.FTCQueue
+Description : Fast type-aligned queue optimized to effectful functions.
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+* Constant-time append/(><) and snoc/(|>)
+* Average constant-time viewL (left-edge deconstruction)
+
+Using <http://okmij.org/ftp/Haskell/extensible/FTCQueue1.hs> as a
+starting point.
+
+A minimal version of FTCQueue from "Reflection w/o Remorse":
+
+* research: http://okmij.org/ftp/Haskell/Reflection.html
+* type-aligned(FTCQueue): https://hackage.haskell.org/package/type-aligned
+
+-}
+module Data.FTCQueue (
+  FTCQueue,
+  tsingleton,
+  (|>),
+  snoc,
+  (><),
+  append,
+  ViewL(..),
+  tviewl
+) where
+
+-- |
+-- Non-empty tree. Deconstruction operations make it more and more
+-- left-leaning
+data FTCQueue m a b where
+  Leaf :: (a -> m b) -> FTCQueue m a b
+  Node :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
+
+{-# INLINE tsingleton #-}
+-- | Build a leaf from a single operation [O(1)]
+tsingleton :: (a -> m b) -> FTCQueue m a b
+tsingleton = Leaf
+
+{-# INLINE (|>) #-}
+-- | Append an operation to the right of the tree [O(1)]
+(|>) :: FTCQueue m a x -> (x -> m b) -> FTCQueue m a b
+t |> r = Node t (Leaf r)
+
+{-# INLINE snoc #-}
+-- | An alias for '(|>)'
+snoc :: FTCQueue m a x -> (x -> m b) -> FTCQueue m a b
+snoc = (|>)
+
+{-# INLINE (><) #-}
+-- | Append two trees of operations [O(1)]
+(><)   :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
+t1 >< t2 = Node t1 t2
+
+{-# INLINE append #-}
+-- | An alias for '(><)'
+append :: FTCQueue m a x -> FTCQueue m x b -> FTCQueue m a b
+append = (><)
+
+-- | Left view deconstruction data structure
+data ViewL m a b where
+  TOne  :: (a -> m b) -> ViewL m a b
+  (:|)  :: (a -> m x) -> FTCQueue m x b -> ViewL m a b
+
+-- | Left view deconstruction [average O(1)]
+tviewl :: FTCQueue m a b -> ViewL m a b
+tviewl (Leaf r) = TOne r
+tviewl (Node t1 t2) = go t1 t2
+ where
+   go :: FTCQueue m a x -> FTCQueue m x b -> ViewL m a b
+   go (Leaf r) tr = r :| tr
+   go (Node tl1 tl2) tr = go tl1 (Node tl2 tr)
diff --git a/src/Data/Open/Union.hs b/src/Data/Open/Union.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Open/Union.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-|
+Module      : Data.Open.Union
+Description : Open unions (type-indexed co-products) for extensible effects.
+Copyright   : Alej Cabrera 2015
+License     : BSD-3
+Maintainer  : cpp.cabrera@gmail.com
+Stability   : experimental
+Portability : POSIX
+
+This implementation relies on _closed_ type families added to GHC
+7.8. It has NO overlapping instances and NO Typeable. Alas, the
+absence of Typeable means the projections and injections generally
+take linear time.  The code illustrate how to use closed type families
+to disambiguate otherwise overlapping instances.
+
+The data constructors of Union are not exported. Essentially, the
+nested Either data type.
+
+Using <http://okmij.org/ftp/Haskell/extensible/OpenUnion41.hs> as a
+starting point.
+
+-}
+
+module Data.Open.Union (
+  Union,
+  decomp,
+  weaken,
+  Member(..)
+) where
+
+import GHC.TypeLits (Nat)
+
+--------------------------------------------------------------------------------
+                           -- Interface --
+--------------------------------------------------------------------------------
+data Union (r :: [ * -> * ]) v where
+  UNow  :: t v -> Union (t ': r) v
+  UNext :: Union r v -> Union (any ': r) v
+
+{-# INLINE decomp #-}
+decomp :: Union (t ': r) v -> Either (Union r v) (t v)
+decomp (UNow x)  = Right x
+decomp (UNext v) = Left v
+
+{-# INLINE weaken #-}
+weaken :: Union r w -> Union (any ': r) w
+weaken = UNext
+
+class (Member' t r (FindElem t r)) => Member t r where
+  inj :: t v -> Union r v
+  prj :: Union r v -> Maybe (t v)
+
+instance (Member' t r (FindElem t r)) => Member t r where
+  inj = inj' (P :: P (FindElem t r))
+  prj = prj' (P :: P (FindElem t r))
+
+--------------------------------------------------------------------------------
+                         -- Implementation --
+--------------------------------------------------------------------------------
+data P (n :: Nat) = P
+
+-- injecting/projecting at a specified position P n
+class Member' t r (n :: Nat) where
+  inj' :: P n -> t v -> Union r v
+  prj' :: P n -> Union r v -> Maybe (t v)
+
+instance (r ~ (t ': r')) => Member' t r 0 where
+  inj' _ = UNow
+  prj' _ (UNow x) = Just x
+  prj' _ _        = Nothing
+
+instance (r ~ (t' ': r'), Member' t r' n) => Member' t r n where
+  inj' _ = UNext . inj' (P::P n)
+  prj' _ (UNow _)  = Nothing
+  prj' _ (UNext x) = prj' (P::P n) x
+
+-- Find an index of an element in a `list'
+-- The element must exist
+-- This closed type family disambiguates otherwise overlapping
+-- instances
+type family FindElem (t :: * -> *) r :: Nat where
+  FindElem t (t ': r)    = 0
+  FindElem t (any ': r)  = FindElem t r
+
+type family EQU (a :: k) (b :: k) :: Bool where
+  EQU a a = 'True
+  EQU a b = 'False
diff --git a/tests/Tests.hs b/tests/Tests.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests.hs
@@ -0,0 +1,108 @@
+module Main where
+
+import Control.Monad.Freer
+
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+
+import Tests.Exception
+import Tests.Fresh
+import Tests.NonDetEff
+import Tests.Reader
+import Tests.State
+import Tests.StateRW
+
+--------------------------------------------------------------------------------
+                           -- Pure Tests --
+--------------------------------------------------------------------------------
+addInEff :: Int -> Int -> Int
+addInEff x y = run ((+) <$> pure x <*> pure y)
+
+pureTests :: TestTree
+pureTests = testGroup "Pure Eff tests"
+  [ testProperty "Pure run just works: (+)"
+      (\x y -> addInEff x y == x + y)
+  ]
+
+--------------------------------------------------------------------------------
+                        -- Exception Tests --
+--------------------------------------------------------------------------------
+exceptionTests :: TestTree
+exceptionTests = testGroup "Exception Eff tests"
+  [ testProperty "Exc takes precedence" (\x y -> testExceptionTakesPriority x y == Left y)
+  , testCase "uncaught: runState (runError t)" $
+      ter1 @?= (Left "exc", 2)
+  , testCase "uncaught: runError (runState t)" $
+      ter2 @?= Left "exc"
+  , testCase "caught: runState (runError t)" $
+      ter3 @?= (Right "exc", 2)
+  , testCase "caught: runError (runState t)" $
+      ter4 @?= Right ("exc", 2)
+  , testCase "success: runReader (runErrBig t)" (ex2rr @?= Right 5)
+  , testCase "uncaught: runReader (runErrBig t)" $
+      ex2rr1 @?= Left (TooBig 7)
+  , testCase "uncaught: runErrBig (runReader t)" $
+      ex2rr2 @?= Left (TooBig 7)
+  ]
+
+--------------------------------------------------------------------------------
+                       -- Fresh Effect Tests --
+--------------------------------------------------------------------------------
+freshTests :: TestTree
+freshTests = testGroup "Fresh tests"
+  [ testCase "Start at 0, refresh twice, yields 1" (testFresh 10 @?= 9)
+  , testProperty "Freshening n times yields (n-1)" (\n -> n > 0 ==> testFresh n == (n-1))
+  ]
+
+--------------------------------------------------------------------------------
+                 -- Nondeterministic Effect Tests --
+--------------------------------------------------------------------------------
+nonDetEffTests :: TestTree
+nonDetEffTests = testGroup "NonDetEff tests"
+  [ testCase "[2,3,5] are primes generated by ifte" (testIfte [2..6] @?= [2,3,5])
+  ]
+
+--------------------------------------------------------------------------------
+                      -- Reader Effect Tests --
+--------------------------------------------------------------------------------
+readerTests :: TestTree
+readerTests = testGroup "Reader tests"
+  [ testProperty "Reader passes along environment: n + x"
+    (\n x -> testReader n x == n + x)
+  , testProperty "Multiple readers work"
+    (\f n -> testMultiReader f n == ((f + 2.0) + fromIntegral (n + 1)))
+  , testProperty "Local injects into env"
+    (\env inc -> testLocal env inc == 2*(env+1) + inc)
+  ]
+
+--------------------------------------------------------------------------------
+                     -- State[RW] Effect Tests --
+--------------------------------------------------------------------------------
+stateTests :: TestTree
+stateTests = testGroup "State tests"
+  [ testProperty "get after put n yields (n,n)" (\n -> testPutGet n 0 == (n,n))
+  , testProperty "Final put determines stored state" $
+    \p1 p2 start -> testPutGetPutGetPlus p1 p2 start == (p1+p2, p2)
+  , testProperty "If only getting, start state determines outcome" $
+    \start -> testGetStart start == (start,start)
+  , testProperty "testPutGet: State == StateRW" $
+    \n -> testPutGet n 0 == testPutGetRW n 0
+  , testProperty "testPutGetPutGetPlus: State == StateRW" $
+    \p1 p2 start -> testPutGetPutGetPlus p1 p2 start == testPutGetPutGetPlusRW p1 p2 start
+  , testProperty "testGetStart: State == StateRW" $
+    \n -> testGetStart n == testGetStartRW n
+  ]
+
+--------------------------------------------------------------------------------
+                             -- Runner --
+--------------------------------------------------------------------------------
+main :: IO ()
+main = defaultMain $ testGroup "Tests"
+  [ pureTests
+  , exceptionTests
+  , freshTests
+  -- , nonDetEffTests -- FIXME: failing
+  , readerTests
+  , stateTests
+  ]
diff --git a/tests/Tests/Common.hs b/tests/Tests/Common.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/Common.hs
@@ -0,0 +1,6 @@
+module Tests.Common where
+
+import Control.Applicative
+
+add :: Applicative f => f Int -> f Int -> f Int
+add = liftA2 (+)
diff --git a/tests/Tests/Exception.hs b/tests/Tests/Exception.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/Exception.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Tests.Exception (
+  TooBig(..),
+
+  testExceptionTakesPriority,
+
+  ter1,
+  ter2,
+  ter3,
+  ter4,
+
+  ex2rr,
+  ex2rr1,
+  ex2rr2,
+) where
+
+import Control.Monad.Freer
+import Control.Monad.Freer.Exception
+import Control.Monad.Freer.Reader
+import Control.Monad.Freer.State
+
+import Tests.Common
+
+testExceptionTakesPriority :: Int -> Int -> Either Int Int
+testExceptionTakesPriority x y = run $ runError (go x y)
+  where go a b = return a `add` throwError b
+
+-- The following won't type: unhandled exception!
+-- ex2rw = run et2
+{-
+    No instance for (Member (Exc Int) Void)
+      arising from a use of `et2'
+-}
+
+-- exceptions and state
+incr :: Member (State Int) r => Eff r ()
+incr = get >>= put . (+ (1::Int))
+
+tes1 :: (Member (State Int) r, Member (Exc String) r) => Eff r b
+tes1 = do
+ incr
+ throwError "exc"
+
+ter1 :: (Either String Int, Int)
+ter1 = run $ runState (runError tes1) (1::Int)
+
+ter2 :: Either String (String, Int)
+ter2 = run $ runError (runState tes1 (1::Int))
+
+teCatch :: Member (Exc String) r => Eff r a -> Eff r String
+teCatch m = catchError (m >> return "done") (\e -> return (e::String))
+
+ter3 :: (Either String String, Int)
+ter3 = run $ runState (runError (teCatch tes1)) (1::Int)
+
+ter4 :: Either String (String, Int)
+ter4 = run $ runError (runState (teCatch tes1) (1::Int))
+
+-- The example from the paper
+newtype TooBig = TooBig Int deriving (Eq, Show)
+
+ex2 :: Member (Exc TooBig) r => Eff r Int -> Eff r Int
+ex2 m = do
+  v <- m
+  if v > 5 then throwError (TooBig v)
+     else return v
+
+-- specialization to tell the type of the exception
+runErrBig :: Eff (Exc TooBig ': r) a -> Eff r (Either TooBig a)
+runErrBig = runError
+
+ex2rr :: Either TooBig Int
+ex2rr = run go
+  where go = runReader (runErrBig (ex2 ask)) (5::Int)
+
+ex2rr1 :: Either TooBig Int
+ex2rr1 = run $ runReader (runErrBig (ex2 ask)) (7::Int)
+
+-- Different order of handlers (layers)
+ex2rr2 :: Either TooBig Int
+ex2rr2 = run $ runErrBig (runReader (ex2 ask) (7::Int))
diff --git a/tests/Tests/Fresh.hs b/tests/Tests/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/Fresh.hs
@@ -0,0 +1,11 @@
+module Tests.Fresh where
+
+import Control.Monad
+import Control.Monad.Freer
+import Control.Monad.Freer.Fresh
+
+makeFresh :: Int -> Eff r Int
+makeFresh n = runFresh' (liftM last (replicateM n fresh)) 0
+
+testFresh :: Int -> Int
+testFresh = run . makeFresh
diff --git a/tests/Tests/NonDetEff.hs b/tests/Tests/NonDetEff.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/NonDetEff.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Tests.NonDetEff where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Freer
+
+ifte :: Member NonDetEff r
+     => Eff r a -> (a -> Eff r b) -> Eff r b -> Eff r b
+ifte t th el = (t >>= th) <|> el
+
+generatePrimes :: Member NonDetEff r => [Int] -> Eff r Int
+generatePrimes xs = do
+  n <- gen
+  ifte (do d <- gen
+           guard $ d < n && n `mod` d == 0)
+       (const mzero)
+       (return n)
+  where gen = msum . fmap return $ xs
+
+testIfte :: [Int] -> [Int]
+testIfte = run . makeChoiceA . generatePrimes
diff --git a/tests/Tests/Reader.hs b/tests/Tests/Reader.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/Reader.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Tests.Reader (
+  testReader,
+  testMultiReader,
+  testLocal
+) where
+
+import Control.Monad.Freer
+import Control.Monad.Freer.Reader
+
+import Tests.Common
+
+--------------------------------------------------------------------------------
+                            -- Examples --
+--------------------------------------------------------------------------------
+testReader :: Int -> Int -> Int
+testReader n x = run . flip runReader n $ ask `add` pure x
+
+{-
+t1rr' = run t1
+    No instance for (Member (Reader Int) Void)
+      arising from a use of `t1'
+-}
+
+testMultiReader :: Float -> Int -> Float
+testMultiReader f n = run . flip runReader f . flip runReader n $ t2
+  where t2 = do
+          v1 <- ask
+          v2 <- ask
+          return $ fromIntegral (v1 + (1::Int)) + (v2 + (2::Float))
+
+-- The opposite order of layers
+{- If we mess up, we get an error
+t2rrr1' = run $ runReader (runReader t2 (20::Float)) (10::Float)
+    No instance for (Member (Reader Int) [])
+      arising from a use of `t2'
+-}
+
+testLocal :: Int -> Int -> Int
+testLocal env inc = run $ runReader t3 env
+  where t3 = t1 `add` local (+ inc) t1
+        t1 = ask `add` return (1 :: Int)
diff --git a/tests/Tests/State.hs b/tests/Tests/State.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/State.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Tests.State (
+  testPutGet,
+  testPutGetPutGetPlus,
+  testGetStart
+) where
+
+import Control.Monad.Freer
+import Control.Monad.Freer.State
+
+testPutGet :: Int -> Int -> (Int,Int)
+testPutGet n start = run (runState go start)
+  where go = put n >> get
+
+testPutGetPutGetPlus :: Int -> Int -> Int -> (Int,Int)
+testPutGetPutGetPlus p1 p2 start = run (runState go start)
+  where go = do
+          put p1
+          x <- get
+          put p2
+          y <- get
+          return (x+y)
+
+testGetStart :: Int -> (Int,Int)
+testGetStart = run . runState get
diff --git a/tests/Tests/StateRW.hs b/tests/Tests/StateRW.hs
new file mode 100644
--- /dev/null
+++ b/tests/Tests/StateRW.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Tests.StateRW (
+  testPutGetRW,
+  testPutGetPutGetPlusRW,
+  testGetStartRW
+) where
+
+import Control.Monad.Freer
+import Control.Monad.Freer.StateRW
+
+testPutGetRW :: Int -> Int -> (Int,Int)
+testPutGetRW n start = run (runStateR go start)
+  where go = tell n >> ask
+
+testPutGetPutGetPlusRW :: Int -> Int -> Int -> (Int,Int)
+testPutGetPutGetPlusRW p1 p2 start = run (runStateR go start)
+  where go = do
+          tell p1
+          x <- ask
+          tell p2
+          y <- ask
+          return (x+y)
+
+testGetStartRW :: Int -> (Int,Int)
+testGetStartRW = run . runStateR go
+  where go = ask