diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Anthony Vandikas
+
+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 Anthony Vandikas 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/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/effin.cabal b/effin.cabal
new file mode 100644
--- /dev/null
+++ b/effin.cabal
@@ -0,0 +1,51 @@
+name:                effin
+version:             0.1.0.0
+synopsis:            A Typeable-free implementation of extensible effects
+description:         A Typeable-free implementation of extensible effects
+homepage:            https://github.com/YellPika/effin
+license:             BSD3
+license-file:        LICENSE
+author:              Anthony Vandikas
+maintainer:          yellpika@gmail.com
+copyright:           (c) 2014 Anthony Vandikas
+category:            Control
+build-type:          Simple
+-- extra-source-files:
+cabal-version:       >=1.10
+
+flag mtl
+  description: Enable MTL support
+  default: True
+  manual: True
+
+library
+  exposed-modules:
+    Control.Effect,
+    Control.Effect.Coroutine,
+    Control.Effect.Exception,
+    Control.Effect.Lift,
+    Control.Effect.List,
+    Control.Effect.Reader,
+    Control.Effect.State,
+    Control.Effect.Thread,
+    Control.Effect.Union,
+    Control.Effect.Writer,
+    Control.Monad.Effect
+
+  other-modules:
+    Data.Union
+
+  build-depends: base >= 4.7 && < 4.8
+  if flag(mtl)
+    build-depends: mtl >= 2.1 && < 3
+
+  hs-source-dirs: src
+  default-language: Haskell2010
+  ghc-options: -Wall
+
+  if flag(mtl)
+    cpp-options: -DMTL
+
+source-repository head
+  type:     git
+  location: git://github.com/YellPika/effin.git
diff --git a/src/Control/Effect.hs b/src/Control/Effect.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect.hs
@@ -0,0 +1,23 @@
+module Control.Effect (
+    module Control.Effect.Coroutine,
+    module Control.Effect.Exception,
+    module Control.Effect.Lift,
+    module Control.Effect.List,
+    module Control.Effect.Reader,
+    module Control.Effect.State,
+    module Control.Effect.Thread,
+    module Control.Effect.Union,
+    module Control.Effect.Writer,
+    module Control.Monad.Effect
+) where
+
+import Control.Effect.Coroutine
+import Control.Effect.Exception
+import Control.Effect.Lift
+import Control.Effect.List
+import Control.Effect.Reader
+import Control.Effect.State
+import Control.Effect.Thread
+import Control.Effect.Union
+import Control.Effect.Writer
+import Control.Monad.Effect
diff --git a/src/Control/Effect/Coroutine.hs b/src/Control/Effect/Coroutine.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Coroutine.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Effect.Coroutine (
+    EffectCoroutine, Coroutine, Iterator (..), runCoroutine, suspend
+) where
+
+import Control.Monad.Effect
+
+-- | An effect describing a suspendable computation.
+data Coroutine i o a = Coroutine (o -> a) i
+  deriving Functor
+
+-- | A suspended computation.
+data Iterator i o es a
+    = Done a -- ^ Describes a finished computation.
+    | Next (o -> Effect es (Iterator i o es a)) i
+    -- ^ Describes a computation that provided a value
+    -- of type `i` and awaits a value of type `o`.
+
+type EffectCoroutine i o es = (Member (Coroutine i o) es, '(i, o) ~ CoroutineType es)
+type family CoroutineType es where
+    CoroutineType (Coroutine i o ': es) = '(i, o)
+    CoroutineType (e ': es) = CoroutineType es
+
+-- | Suspends the current computation by providing a value
+-- of type `i` and then waiting for a value of type `o`.
+suspend :: EffectCoroutine i o es => i -> Effect es o
+suspend = send . Coroutine id
+
+-- | Converts a `Coroutine` effect into an `Iterator`.
+runCoroutine :: Effect (Coroutine i o ': es) a -> Effect es (Iterator i o es a)
+runCoroutine =
+    handle (return . Done)
+    $ eliminate (\(Coroutine f k) -> return (Next f k))
+    $ defaultRelay
diff --git a/src/Control/Effect/Exception.hs b/src/Control/Effect/Exception.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Exception.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+#if MTL
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Exception (
+    EffectException, Exception, runException,
+    raise, except, finally
+) where
+
+import Control.Monad.Effect
+
+#ifdef MTL
+import qualified Control.Monad.Error.Class as E
+
+instance EffectException e es => E.MonadError e (Effect es) where
+    throwError = raise
+    catchError = except
+#endif
+
+-- | An effect that describes the possibility of failure.
+newtype Exception e a = Exception { unException :: e }
+  deriving Functor
+
+type EffectException e es = (Member (Exception e) es, e ~ ExceptionType es)
+type family ExceptionType es where
+    ExceptionType (Exception e ': es) = e
+    ExceptionType (e ': es) = ExceptionType es
+
+-- | Raises an exception.
+raise :: EffectException e es => e -> Effect es a
+raise = send . Exception
+
+-- | Handles an exception. Intended to be used in infix form.
+--
+-- > myComputation `except` \ex -> doSomethingWith ex
+except :: EffectException e es => Effect es a -> (e -> Effect es a) -> Effect es a
+except = flip run
+  where
+    run handler =
+        handle return
+        $ intercept (handler . unException)
+        $ defaultRelay
+
+-- | Ensures that a computation is run after another one completes,
+-- regardless of whether an exception was raised. Intended to be
+-- used in infix form.
+--
+-- > do x <- loadSomeResource
+-- >    doSomethingWith x `finally` unload x
+finally :: EffectException e es => Effect es a -> Effect es () -> Effect es a
+finally effect finalizer = do
+    result <- effect `except` \e -> do
+        finalizer
+        raise e
+    finalizer
+    return result
+
+-- | Completely handles an exception effect.
+runException :: Effect (Exception e ': es) a -> Effect es (Either e a)
+runException =
+    handle (return . Right)
+    $ eliminate (return . Left . unException)
+    $ defaultRelay
diff --git a/src/Control/Effect/Lift.hs b/src/Control/Effect/Lift.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Lift.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+#ifdef MTL
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Lift (
+    Lift, runLift, lift
+) where
+
+import Control.Monad.Effect
+import Control.Monad (join, liftM)
+
+#ifdef MTL
+import Control.Monad.Trans (MonadIO (..))
+
+instance EffectLift IO es => MonadIO (Effect es) where
+    liftIO = lift
+#endif
+
+-- | An effect described by a monad.
+-- All monads are functors, but not all `Monad`s have `Functor` instances.
+-- By wrapping a monad in the `Lift` effect, all monads can be used without
+-- having to provide a `Functor` instance for each one.
+newtype Lift m a = Lift { unLift :: m a }
+
+instance Monad m => Functor (Lift m) where
+    fmap f = Lift . liftM f . unLift
+
+type EffectLift m es = (Member (Lift m) es, m ~ LiftType es, Monad m)
+type family LiftType es where
+    LiftType (Lift m ': es) = m
+    LiftType (e ': es) = LiftType es
+
+-- | Lifts a monadic value into an effect.
+lift :: EffectLift m es => m a -> Effect es a
+lift = send . Lift
+
+-- | Converts a computation containing only monadic
+-- effects into a monadic computation.
+runLift :: Monad m => Effect '[Lift m] a -> m a
+runLift =
+    handle return
+    $ eliminate (join . unLift)
+    $ emptyRelay
diff --git a/src/Control/Effect/List.hs b/src/Control/Effect/List.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/List.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module Control.Effect.List (
+    EffectList, List, runList,
+    choose, never, select,
+
+    EffectCut, Cut,
+    cut, runCut
+) where
+
+import Control.Monad.Effect
+import Control.Arrow (second)
+import Control.Applicative (Alternative (..), (<$>))
+import Control.Monad (MonadPlus (..), (<=<), join)
+
+-- | Describes a nondeterminism (backtracking) effect.
+newtype List a = List { unList :: [a] }
+  deriving Functor
+
+type EffectList = Member List
+
+-- | Nondeterministically chooses a value from the input list.
+choose :: EffectList es => [a] -> Effect es a
+choose = send . List
+
+-- | Describes a nondeterministic computation that never returns a value.
+never :: EffectList es => Effect es a
+never = choose []
+
+-- | Nondeterministically chooses a value from a list of computations.
+select :: EffectList es => [Effect es a] -> Effect es a
+select = join . choose
+
+-- | Obtains all possible values from a computation
+-- parameterized by a nondeterminism effect.
+runList :: Effect (List ': es) a -> Effect es [a]
+runList =
+    handle (\x -> return [x])
+    $ eliminate (fmap concat . sequence . unList)
+    $ defaultRelay
+
+instance EffectList es => Alternative (Effect es) where
+    empty = never
+    x <|> y = select [x, y]
+
+instance EffectList es => MonadPlus (Effect es) where
+    mzero = empty
+    mplus = (<|>)
+
+-- | Describes a Prolog-like cut effect.
+-- This effect must be used with the `List` effect.
+data Cut a = Cut
+  deriving Functor
+
+type EffectCut = Member Cut
+
+-- | Prevents backtracking past the point this value was invoked.
+-- Unlike Prolog's '!' operator, `cut` will cause the current
+-- computation to fail immediately, instead of when it backtracks.
+cut :: (EffectList es, EffectCut es) => Effect es a
+cut = send Cut
+
+-- | Handles the `Cut` effect. `cut`s have no effect beyond
+-- the scope of the computation passed to this function.
+runCut :: EffectList es => Effect (Cut ': es) a -> Effect es a
+runCut = choose . snd <=< reifyCut
+  where
+    -- Gather the results of a computation into a list (like in runList), but
+    -- also return a Bool indicating whether a cut was performed in the
+    -- computation. When we intercept the List effect, we get a continuation and
+    -- a list of values. If we map the continuation to the list of values, then
+    -- we get a list of computations. We can now execute each computation one by
+    -- one, and inspect the Bool after each computation to determine when we
+    -- should stop.
+    reifyCut :: EffectList es => Effect (Cut ': es) a -> Effect es (Bool, [a])
+    reifyCut =
+        handle (\x -> return (False, [x]))
+        $ eliminate (\Cut -> return (True, []))
+        $ intercept (\(List xs) -> runAll xs)
+        $ defaultRelay
+
+    runAll [] = return (False, [])
+    runAll (x:xs) = do
+        (cutRequested, x') <- x
+        if cutRequested
+        then return (True, x')
+        else second (x' ++) <$> runAll xs
diff --git a/src/Control/Effect/Reader.hs b/src/Control/Effect/Reader.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Reader.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+#if MTL
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Reader (
+	EffectReader, Reader, runReader,
+    ask, asks, local
+) where
+
+import Control.Monad.Effect
+
+#ifdef MTL
+import qualified Control.Monad.Reader.Class as R
+
+instance EffectReader r es => R.MonadReader r (Effect es) where
+    ask = ask
+    local = local
+    reader = asks
+#endif
+
+-- | An effect that describes an implicit environment.
+newtype Reader r a = Reader (r -> a)
+  deriving Functor
+
+type EffectReader r es = (Member (Reader r) es, r ~ ReaderType es)
+type family ReaderType es where
+    ReaderType (Reader r ': es) = r
+    ReaderType (e ': es) = ReaderType es
+
+-- | Retrieves the current environment.
+ask :: EffectReader r es => Effect es r
+ask = asks id
+
+-- | Retrieves a value that is a function of the current environment.
+asks :: EffectReader r es => (r -> a) -> Effect es a
+asks = send . Reader
+
+-- | Runs a computation with a modified environment.
+local :: EffectReader r es => (r -> r) -> Effect es a -> Effect es a
+local f effect = do
+    env <- asks f
+    run env effect
+  where
+    run env =
+        handle return
+        $ intercept (bind env)
+        $ defaultRelay
+
+-- | Completely handes a `Reader` effect by providing an
+-- environment value to be used throughout the computation.
+runReader :: r -> Effect (Reader r ': es) a -> Effect es a
+runReader env =
+    handle return
+    $ eliminate (bind env)
+    $ defaultRelay
+
+bind :: r -> Reader r (Effect es b) -> Effect es b
+bind env (Reader k) = k env
diff --git a/src/Control/Effect/State.hs b/src/Control/Effect/State.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/State.hs
@@ -0,0 +1,92 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+#if MTL
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.State (
+    EffectState, State, runState,
+    evalState, execState,
+    get, gets, put,
+    modify, modify',
+    state, withState
+) where
+
+import Control.Applicative ((<$>))
+import Control.Monad.Effect
+
+#ifdef MTL
+import qualified Control.Monad.State.Class as S
+
+instance EffectState s es => S.MonadState s (Effect es) where
+    get = get
+    put = put
+    state = state
+#endif
+
+-- | An effect where a state value is threaded throughout the computation.
+newtype State s a = State (s -> (a, s))
+  deriving Functor
+
+type EffectState s es = (Member (State s) es, s ~ StateType es)
+type family StateType es where
+    StateType (State s ': es) = s
+    StateType (e ': es) = StateType es
+
+-- | Gets the current state.
+get :: EffectState s es => Effect es s
+get = state $ \s -> (s, s)
+
+-- | Gets a value that is a function of the current state.
+gets :: EffectState s es => (s -> a) -> Effect es a
+gets f = f <$> get
+
+-- | Replaces the current state.
+put :: EffectState s es => s -> Effect es ()
+put x = state $ const ((), x)
+
+-- | Applies a pure modifier to the state value.
+modify :: EffectState s es => (s -> s) -> Effect es ()
+modify f = get >>= put . f
+
+-- | Applies a pure modifier to the state value.
+-- The modified value is converted to weak head normal form.
+modify' :: EffectState s es => (s -> s) -> Effect es ()
+modify' f = do
+    x <- get
+    put $! f x
+
+-- | Lifts a stateful computation to the `Effect` monad.
+state :: EffectState s es => (s -> (a, s)) -> Effect es a
+state = send . State
+
+-- | Runs a computation with a modified state value.
+--
+-- prop> withState f x = modify f >> x
+withState :: EffectState s es => (s -> s) -> Effect es a -> Effect es a
+withState f x = modify f >> x
+
+-- | Completely handles a `State` effect by providing an
+-- initial state, and making the final state explicit.
+runState :: s -> Effect (State s ': es) a -> Effect es (a, s)
+runState = flip $
+    handle (\x s -> return (x, s))
+    $ eliminate (\(State k) s -> let (k', s') = k s in k' s')
+    $ relay (\x s -> sendEffect $ fmap ($ s) x)
+
+-- | Completely handles a `State` effect, and discards the final state.
+evalState :: s -> Effect (State s ': es) a -> Effect es a
+evalState s = fmap fst . runState s
+
+-- | Completely handles a `State` effect, and discards the final value.
+execState :: s -> Effect (State s ': es) a -> Effect es s
+execState s = fmap snd . runState s
diff --git a/src/Control/Effect/Thread.hs b/src/Control/Effect/Thread.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Thread.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Effect.Thread (
+    EffectThread, Thread,
+    runMain, runSync, runAsync,
+    yield, fork, abort,
+) where
+
+import Control.Effect.Lift
+import Control.Monad.Effect
+import Control.Applicative ((<$>))
+import Control.Monad (void)
+import qualified Control.Concurrent as IO
+
+-- | An effect that describes concurrent computation.
+data Thread a = Yield a | Fork a a | Abort
+  deriving Functor
+
+type EffectThread = Member Thread
+
+-- | Yields to the next available thread.
+yield :: EffectThread es => Effect es ()
+yield = send (Yield ())
+
+-- | Forks a child thread.
+fork :: EffectThread es => Effect es () -> Effect es ()
+fork child = sendEffect $ Fork child (return ())
+
+-- | Immediately terminates the current thread.
+abort :: EffectThread es => Effect es ()
+abort = send Abort
+
+-- | Executes a threaded computation synchronously.
+-- Completes when the main thread exits.
+runMain :: Effect (Thread ': es) () -> Effect es ()
+runMain = run [] . toAST
+  where
+    run auxThreads thread = do
+        result <- thread
+        case result of
+            AbortAST -> return ()
+            YieldAST k -> do
+                auxThreads' <- runAll auxThreads
+                run auxThreads' k
+            ForkAST child parent -> do
+                auxThreads' <- runAll [child]
+                run (auxThreads ++ auxThreads') parent
+
+    runAll [] = return []
+    runAll (thread:xs) = do
+        result <- thread
+        case result of
+            AbortAST -> runAll xs
+            YieldAST k -> (k:) <$> runAll xs
+            ForkAST child parent -> (parent:) <$> runAll (child:xs)
+
+-- | Executes a threaded computation synchronously.
+-- Does not complete until all threads have exited.
+runSync :: Effect (Thread ': es) () -> Effect es ()
+runSync = run . (:[]) . toAST
+  where
+    run [] = return ()
+    run (thread:xs) = do
+        result <- thread
+        case result of
+            AbortAST -> run xs
+            YieldAST k -> run (xs ++ [k])
+            ForkAST child parent -> run (child:xs ++ [parent])
+
+-- | Executes a threaded computation asynchronously.
+runAsync :: Effect '[Thread, Lift IO] () -> IO ()
+runAsync = run . toAST
+  where
+    run thread = do
+        result <- runLift thread
+        case result of
+            AbortAST -> return ()
+            YieldAST k -> do
+                IO.yield
+                run k
+            ForkAST child parent -> do
+                void $ IO.forkIO $ run child
+                run parent
+
+data ThreadAST es
+    = YieldAST (Effect es (ThreadAST es))
+    | ForkAST (Effect es (ThreadAST es)) (Effect es (ThreadAST es))
+    | AbortAST
+
+-- Converts a threaded computation into its corresponding AST. This allows
+-- different backends to interpret calls to fork/yield/abort as they please. See
+-- the implementations of runAsync, runSync, and runMain.
+toAST :: Effect (Thread ': es) () -> Effect es (ThreadAST es)
+toAST =
+    handle (\() -> return AbortAST)
+    $ eliminate (\thread ->
+        case thread of
+            Abort -> return AbortAST
+            Yield k -> return (YieldAST k)
+            Fork child parent -> return (ForkAST child parent))
+    $ defaultRelay
diff --git a/src/Control/Effect/Union.hs b/src/Control/Effect/Union.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Union.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Control.Effect.Union (
+    EffectUnion, Union, runUnion, nest,
+    KnownList, type (++),
+) where
+
+import Control.Monad.Effect
+import Data.Union
+
+type EffectUnion es fs = (KnownList es, Member (Union es) fs, es ~ UnionType fs)
+type family UnionType fs where
+    UnionType (Union es ': fs) = es
+    UnionType (f ': fs) = UnionType fs
+
+-- | Nests an effect with another.
+nest :: EffectUnion es fs => Effect es a -> Effect fs a
+nest =
+    handle return
+    $ relayUnion sendEffect
+
+-- | Flattens a nested list of effects.
+runUnion :: KnownList es => Effect (Union es ': fs) a -> Effect (es ++ fs) a
+runUnion =
+    handle return
+    $ relayUnion (withUnion sendEffect . flatten)
+
+relayUnion :: (Union es b -> b) -> Handler es b
+relayUnion f = relay (f . inject)
diff --git a/src/Control/Effect/Writer.hs b/src/Control/Effect/Writer.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Effect/Writer.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+#if MTL
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+#endif
+
+module Control.Effect.Writer (
+    EffectWriter, Writer, runWriter,
+    tell, listen, listens, pass, censor
+) where
+
+import Control.Monad.Effect
+import Control.Applicative ((<$>))
+import Control.Arrow (second)
+import Data.Monoid (Monoid (..))
+
+#ifdef MTL
+import qualified Control.Monad.Writer.Class as W
+
+instance EffectWriter e es => W.MonadWriter e (Effect es) where
+    tell = tell
+    listen = listen
+    pass = pass
+#endif
+
+-- | An effect that allows accumulating output.
+data Writer w a = Writer w a
+  deriving Functor
+
+type EffectWriter w es = (Monoid w, Member (Writer w) es, w ~ WriterType es)
+type family WriterType es where
+    WriterType (Writer w ': es) = w
+    WriterType (t ': es) = WriterType es
+
+-- | Writes a value to the output.
+tell :: EffectWriter w es => w -> Effect es ()
+tell x = send (Writer x ())
+
+-- | Executes a computation, and obtains the writer output.
+-- The writer output of the inner computation is still
+-- written to the writer output of the outer computation.
+listen :: EffectWriter w es => Effect es a -> Effect es (a, w)
+listen effect = do
+    value@(_, output) <- run effect
+    tell output
+    return value
+  where
+    run =
+        handle point
+        $ intercept bind
+        $ defaultRelay
+
+-- | Like `listen`, but the writer output is run through a function.
+listens :: EffectWriter w es => (w -> b) -> Effect es a -> Effect es (a, b)
+listens f = fmap (second f) . listen
+
+-- | Runs a computation that returns a value and a function,
+-- applies the function to the writer output, and then returns the value.
+pass :: EffectWriter w es => Effect es (a, w -> w) -> Effect es a
+pass effect = do
+    ((x, f), l) <- listen effect
+    tell (f l)
+    return x
+
+-- | Applies a function to the writer output of a computation.
+censor :: EffectWriter w es => (w -> w) -> Effect es a -> Effect es a
+censor f effect = pass $ do
+    a <- effect
+    return (a, f)
+
+-- | Completely handles a writer effect. The writer value must be a `Monoid`.
+-- `mempty` is used as an initial value, and `mappend` is used to combine values.
+-- Returns the result of the computation and the final output value.
+runWriter :: Monoid w => Effect (Writer w ': es) a -> Effect es (a, w)
+runWriter =
+    handle point
+    $ eliminate bind
+    $ defaultRelay
+
+point :: Monoid w => a -> Effect es (a, w)
+point x = return (x, mempty)
+
+bind :: Monoid w => Writer w (Effect es (b, w)) -> Effect es (b, w)
+bind (Writer l k) = second (mappend l) <$> k
diff --git a/src/Control/Monad/Effect.hs b/src/Control/Monad/Effect.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Effect.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | This module provides three things:
+--
+-- 1. An `Effect` monad for representing effectful computations,
+-- 2. A DSL for effect handling that lets you cleanly handle an arbitrary number of effects, and
+-- 3. A type-level list membership constraint.
+module Control.Monad.Effect (
+    -- * The Effect Monad
+    Effect,
+    runEffect, send, sendEffect,
+
+    -- * Effect Handlers
+    -- | The following types and functions form a small DSL that allows users to
+    -- specify how to handle effects. A handler can be formed by a call to
+    -- `handle`, followed by a chain of calls to `eliminate`, `intercept`, and
+    -- ended by either a `defaultRelay`, `emptyRelay`, or a call to `relay`.
+    --
+    -- For example, a possible handler for the state effect would be:
+    --
+    -- > data State s a = State (s -> (s, a))
+    -- >
+    -- > runState :: Effect (State s ': es) a -> s -> Effect es (s, a)
+    -- > runState =
+    -- >     handle (\output state -> return (state, output))
+    -- >     $ eliminate (\(State transform) state ->
+    -- >         let (state', continue) = transform state
+    -- >         in continue state')
+    -- >     $ relay (\effect state -> do
+    -- >         continue <- sendEffect effect
+    -- >         return (continue state))
+    --
+    -- As an analogy to monads, `handle` lets you specify the return function,
+    -- while `eliminate`, `intercept`, and `relay`, let you specify the bind
+    -- function.
+    Handler, handle,
+    eliminate, intercept,
+    relay, defaultRelay, emptyRelay,
+
+    -- * Membership
+    Member
+) where
+
+import Data.Union
+import Control.Applicative (Applicative (..), (<$>))
+import Control.Monad (join)
+
+-- | An effectful computation. An @Effect es a@ may perform any of the effects
+-- specified by the list of effects @es@ before returning a result of type @a@.
+-- The definition is isomorphic to the following GADT:
+--
+-- > data Effect es a where
+-- >     Done :: a -> Effect es a
+-- >     Side :: `Union` es (Effect es a) -> Effect es a
+data Effect es a = Effect {
+    unEffect :: forall r. (a -> r) -> (Union es r -> r) -> r
+} deriving Functor
+
+instance Applicative (Effect es) where
+    pure x = Effect $ \p _ -> p x
+    Effect f <*> Effect x = Effect $ \p b ->
+        f (\f' -> x (p . f') b) b
+
+instance Monad (Effect es) where
+    return = pure
+    Effect x >>= f = Effect $ \p b ->
+        x (\x' -> unEffect (f x') p b) b
+
+-- | Converts an computation that produces no effects into a regular value.
+runEffect :: Effect '[] a -> a
+runEffect (Effect f) = f id absurdUnion
+
+-- | Executes an effect of type @e@ that produces a return value of type @a@.
+send :: Member e es => e a -> Effect es a
+send x = Effect $ \point bind -> bind $ inject $ point <$> x
+
+-- | Executes an effect of type @e@ that produces a return value of type @a@.
+sendEffect :: Member e es => e (Effect es a) -> Effect es a
+sendEffect = join . send
+
+-- | A handler for an effectful computation.
+-- Combined with 'handle', allows one to convert a computation
+-- parameterized by the effect list @es@ to a value of type @a@.
+data Handler es a = Handler (Union es a -> a)
+
+-- | @handle p h@ transforms an effect into a value of type @b@.
+--
+-- @p@ specifies how to convert pure values. That is,
+--
+-- prop> handle p h (return x) = p x
+--
+-- @h@ specifies how to handle effects.
+handle :: (a -> b) -> Handler es b -> Effect es a -> b
+handle point (Handler bind) (Effect f) = f point bind
+
+-- | Provides a way to completely handle an effect. The given function is passed
+-- an effect value parameterized by the output type (i.e. the return type of
+-- `handle`).
+eliminate :: (e b -> b) -> Handler es b -> Handler (e ': es) b
+eliminate bind (Handler pass) = Handler (either pass bind . reduce)
+
+-- | Provides a way to handle an effect without eliminating it. The given
+-- function is passed an effect value parameterized by the output type (i.e. the
+-- return type of `handle`).
+intercept :: Member e es => (e b -> b) -> Handler es b -> Handler es b
+intercept bind (Handler pass) = Handler $ \u ->
+    maybe (pass u) bind (project u)
+
+-- | Computes a basis handler. Provides a way to pass on effects of unknown
+-- types. In most cases, `defaultRelay` is sufficient.
+relay :: (forall e. Member e es => e b -> b) -> Handler es b
+relay f = Handler (withUnion f)
+
+-- | Relays all effects without examining them.
+--
+-- prop> handle id defaultRelay x = x
+defaultRelay :: Handler es (Effect es a)
+defaultRelay = relay sendEffect
+
+-- | A handler for when there are no effects. Since `Handler`s handle effects,
+-- they cannot be run on a computation that never produces an effect. By the
+-- principle of explosion, a handler that requires exactly zero effects can
+-- produce any value.
+emptyRelay :: Handler '[] a
+emptyRelay = Handler absurdUnion
diff --git a/src/Data/Union.hs b/src/Data/Union.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Union.hs
@@ -0,0 +1,119 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Union (
+    Union, Member,
+    inject, project,
+    reduce, flatten,
+    withUnion, absurdUnion,
+
+    KnownList, type (++)
+) where
+
+import Data.Proxy (Proxy (..))
+import Unsafe.Coerce (unsafeCoerce)
+
+-- Union -----------------------------------------------------------------------
+
+-- | Represents a union of the list of type constructors in @es@ parameterized
+-- by @a@. As an effect, it represents the union of each type constructor's
+-- corresponding effect.
+data Union es a where
+    Union :: Functor e => Index e es -> e a -> Union es a
+
+instance Functor (Union es) where
+    fmap f (Union i x) = Union i (fmap f x)
+
+inject :: Member e es => e a -> Union es a
+inject = Union index
+
+project :: forall a e es. Member e es => Union es a -> Maybe (e a)
+project (Union (Index i) x)
+    | i == j = Just (unsafeCoerce x)
+    | otherwise = Nothing
+  where
+    Index j = index :: Index e es
+
+reduce :: Union (e ': es) a -> Either (Union es a) (e a)
+reduce (Union (Index 0) x) = Right (unsafeCoerce x)
+reduce (Union (Index n) x) = Left (Union (Index (n - 1)) x)
+
+flatten :: KnownList es => Union (Union es ': fs) a -> Union (es ++ fs) a
+flatten = flatten' size . reduce
+  where
+    flatten' :: Size es -> Either (Union fs a) (Union es a) -> Union (es ++ fs) a
+    flatten' _ (Right (Union (Index i) x)) = Union (Index i) x
+    flatten' (Size n) (Left (Union (Index i) x)) = Union (Index (n + i)) x
+
+withUnion :: (forall e. Member e es => e a -> r) -> Union es a -> r
+withUnion f (Union i x) = withIndex (f x) (\Proxy -> i)
+
+absurdUnion :: Union '[] a -> b
+absurdUnion _ = error "absurdUnion"
+
+-- Membership ------------------------------------------------------------------
+
+-- | A constraint that requires that the type constructor @t :: * -> *@ is a
+-- member of the list of types @ts :: [* -> *]@.
+class (Functor t, Member' t ts (IndexOf t ts)) => Member t ts where
+    index :: Index t ts
+
+instance (Functor t, Member' t ts (IndexOf t ts)) => Member t ts where
+    index = index' (Proxy :: Proxy (IndexOf t ts))
+
+class Member' e es (n :: N) where
+    index' :: Proxy n -> Index e es
+
+instance Member' e (e ': es) Z where
+    index' _ = Index 0
+
+instance (Member' e es n, IndexOf e (f ': es) ~ S n) => Member' e (f ': es) (S n) where
+    index' p = incr (index' (decr p))
+      where
+        incr :: Index e es -> Index e (f ': es)
+        incr (Index i) = Index (i + 1)
+
+        decr :: Proxy (S n) -> Proxy n
+        decr Proxy = Proxy
+
+newtype Index (e :: * -> *) (es :: [* -> *]) = Index Integer
+
+withIndex :: (Member' e es (IndexOf e es) => r) -> (Proxy (IndexOf e es) -> Index e es) -> r
+withIndex = unsafeCoerce
+
+-- Type Level Indices ----------------------------------------------------------
+data N = Z | S N
+
+type family IndexOf (t :: * -> *) ts where
+    IndexOf t (t ': ts) = Z
+    IndexOf t (u ': ts) = S (IndexOf t ts)
+
+-- Type Level Lists ------------------------------------------------------------
+newtype Size (es :: [* -> *]) = Size Integer
+
+-- | A 'known list' is a type level list who's size is known at compile time.
+class KnownList es where
+    size :: Size es
+
+instance KnownList '[] where
+    size = Size 0
+
+instance KnownList es => KnownList (e ': es) where
+    size = incr size
+      where
+        incr :: Size es -> Size (e ': es)
+        incr (Size n) = Size (n + 1)
+
+-- | Type level list append.
+type family es ++ fs :: [* -> *] where
+    '[] ++ fs = fs
+    (e ': es) ++ fs = e ': (es ++ fs)