diff --git a/extensible-effects.cabal b/extensible-effects.cabal
--- a/extensible-effects.cabal
+++ b/extensible-effects.cabal
@@ -6,7 +6,7 @@
 -- PVP summary:      +-+------- breaking API changes
 --                   | | +----- non-breaking API additions
 --                   | | | +--- code changes with no API change
-version:             1.8.1.0
+version:             1.9.0.0
 
 -- A short (one-line) description of the package.
 synopsis:            An Alternative to Monad Transformers
@@ -72,6 +72,7 @@
                        Control.Eff.Writer.Lazy
                        Control.Eff.Writer.Strict
                        Control.Eff.Trace
+                       Control.Monad.Free.Reflection
                        Data.OpenUnion
 
   -- Modules included in this library but not exported.
@@ -110,10 +111,12 @@
   build-depends:       base >= 4.6 && < 5
                        , free >= 4.0 && < 5.0
                        , kan-extensions >= 4.0 && < 5.0
+                       , type-aligned >= 0.9.3
                        -- For MonadIO instance
                        , transformers >= 0.3 && < 0.5
                        -- For MonadBase instance
                        , transformers-base == 0.4.*
+                       , void >= 0.6 && < 0.8
 
   -- Directories containing source files.
   hs-source-dirs:      src
@@ -129,13 +132,14 @@
   ghc-options: -Wall
 
   build-depends:
-    base >= 4.6 && < 5,
-    QuickCheck == 2.*,
-    HUnit == 1.2.*,
-    test-framework == 0.8.*,
-    test-framework-hunit == 0.3.*,
-    test-framework-quickcheck2 == 0.3.*,
-    extensible-effects
+    base >= 4.6 && < 5
+    , QuickCheck == 2.*
+    , HUnit == 1.2.*
+    , test-framework == 0.8.*
+    , test-framework-hunit == 0.3.*
+    , test-framework-quickcheck2 == 0.3.*
+    , extensible-effects
+    , void >= 0.6 && < 0.8
 
   default-language:    Haskell2010
 
diff --git a/src/Control/Eff.hs b/src/Control/Eff.hs
--- a/src/Control/Eff.hs
+++ b/src/Control/Eff.hs
@@ -1,22 +1,14 @@
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE DeriveDataTypeable, GeneralizedNewtypeDeriving, DeriveFunctor #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
 {-# LANGUAGE CPP #-}
-#if __GLASGOW_HASKELL__ >= 708
--- needed for the orphan Typeable instance for Codensity below
-{-# OPTIONS -fno-warn-orphans #-}
-#endif
 
 -- | Original work available at <http://okmij.org/ftp/Haskell/extensible/Eff.hs>.
 -- This module implements extensible effects as an alternative to monad transformers,
@@ -69,8 +61,7 @@
 -- >                in (lst, total)
 module Control.Eff(
                     Eff
-                  , VE
-                  , Free (..)
+                  , module Reflection
                   , Member
                   , SetMember
                   , Union
@@ -80,77 +71,49 @@
                   , prjForce
                   , decomp
                   , send
-                  , admin
                   , run
                   , interpose
                   , handleRelay
                   , unsafeReUnion
                   ) where
 
-import Control.Applicative ((<$>))
-import Control.Monad.Codensity (Codensity (..))
-import Control.Monad.Free (Free (..))
+import Control.Monad.Free.Reflection as Reflection
 import Data.OpenUnion
 import Data.Typeable
+import Data.Void
 
 #if MIN_VERSION_base(4,7,0)
 #define Typeable1 Typeable
 #endif
 
--- | A `VE` is either a value, or an effect of type @`Union` r@ producing another `VE`.
--- The result is that a `VE` can produce an arbitrarily long chain of @`Union` r@
--- effects, terminated with a pure value.
---
--- As is made explicit here, `VE` is simply the Free monad resulting from the
--- @`Union` r@ functor.
-type VE r = Free (Union r)
-
-fromVal :: VE r w -> w
-fromVal (Pure w) = w
-fromVal _ = error "extensible-effects: fromVal was called on a non-terminal effect."
-{-# INLINE fromVal #-}
-
--- | Basic datatype returned by all computations with extensible effects. The
--- @`Eff` r@ type is a type synonym where the type @r@ is the type of effects
--- that can be handled, and the missing type @a@ (from the type application) is
--- the type of value that is returned.
+-- | Basic type returned by all computations with extensible effects. The @`Eff`
+-- r@ type is a type synonym where the type @r@ is the type of effects that can
+-- be handled, and the missing type @a@ (from the type application) is the type
+-- of value that is returned.
 --
--- As is made explicit below, the `Eff` type is simply the application of the
--- Codensity transformer to `VE`:
+-- Expressed another way: an `Eff` can either be a value (i.e., 'Pure' case), or
+-- an effect of type @`Union` r@ producing another `Eff` (i.e., 'Impure'
+-- case). The result is that an `Eff` can produce an arbitrarily long chain of
+-- @`Union` r@ effects, terminated with a pure value.
 --
---     @type `Eff` r a = `Codensity` (`VE` r) a@
+-- As is made explicit below, the `Eff` type is simply the Free monad resulting from the
+-- @`Union` r@ functor.
 --
--- This is done to gain the asymptotic speedups for scenarios where there is a
--- single 'execution' stage where the built up monadic computation gets
--- executed. For scenarios where the computation execution and building stages
--- are interspersed, the reflection without remorse techniques would be a
--- better fit. See <https://github.com/atzeus/reflectionwithoutremorse>.
-type Eff r = Codensity (VE r)
-#if __GLASGOW_HASKELL__ >= 708
--- as of version 4.1.0.1 Codensity in kan-extensions does not have a a Typeable
--- instance. it doesn't seem possible to be able to define an orphan Typeable
--- instance for Codensity in ghc-7.6
-deriving instance Typeable Codensity
-#endif
+--     @type `Eff` r a = `Free` (`Union` r) a@
+type Eff r = Free (Union r)
 
 -- | Given a method of turning requests into results,
 -- we produce an effectful computation.
-send :: (forall w. (a -> VE r w) -> Union r (VE r w)) -> Eff r a
-send f = Codensity (Free . f)
+send :: Union r a -> Eff r a
+send = freeImpure . (fmap freePure)
 {-# INLINE send #-}
 
--- | Tell an effectful computation that you're ready to start running effects
--- and return a value.
-admin :: Eff r w -> VE r w
-admin (Codensity m) = m Pure
-{-# INLINE admin #-}
-
 -- | Get the result from a pure computation.
-run :: Eff () w -> w
-run = fromVal . admin
+run :: Eff Void w -> w
+run = freeMap id
+      (\_ -> error "extensible-effects: the impossible happened!")
 {-# INLINE run #-}
-
--- the other case is unreachable since () has no constructors
+-- the other case is unreachable since Void has no constructors
 -- Therefore, run is a total function if m Val terminates.
 
 -- | Given a request, either handle it or relay it.
@@ -160,9 +123,7 @@
             -> (t v -> Eff r a) -- ^ Handle the request of type t
             -> Eff r a
 handleRelay u loop h = either passOn h $ decomp u
-  where passOn u' = send (<$> u') >>= loop
-  -- perhaps more efficient:
-  -- passOn u' = send (\k -> fmap (\w -> runCodensity (loop w) k) u')
+  where passOn u' = send u' >>= loop
 {-# INLINE handleRelay #-}
 
 -- | Given a request, either handle it or relay it. Both the handler
@@ -172,5 +133,5 @@
           -> (v -> Eff r a)
           -> (t v -> Eff r a)
           -> Eff r a
-interpose u loop h = maybe (send (<$> u) >>= loop) h $ prj u
+interpose u loop h = maybe (send u >>= loop) h $ prj u
 {-# INLINE interpose #-}
diff --git a/src/Control/Eff/Choose.hs b/src/Control/Eff/Choose.hs
--- a/src/Control/Eff/Choose.hs
+++ b/src/Control/Eff/Choose.hs
@@ -26,7 +26,7 @@
 -- | choose lst non-deterministically chooses one value from the lst
 -- choose [] thus corresponds to failure
 choose :: Member Choose r => [a] -> Eff r a
-choose lst = send (inj . Choose lst)
+choose lst = send . inj $ Choose lst id
 
 -- | MonadPlus-like operators are expressible via choose
 mzero' :: Member Choose r => Eff r a
@@ -38,12 +38,13 @@
 
 -- | Run a nondeterministic effect, returning all values.
 runChoice :: forall a r. Eff (Choose :> r) a -> Eff r [a]
-runChoice m = loop (admin m)
+runChoice = loop
  where
-  loop (Pure x)  = return [x]
-  loop (Free u)    = handleRelay u loop (\(Choose lst k) -> handle lst k)
+  loop = freeMap
+         (\x -> return [x])
+         (\u -> handleRelay u loop (\(Choose lst k) -> handle lst k))
 
-  handle :: [t] -> (t -> VE (Choose :> r) a) -> Eff r [a]
+  handle :: [t] -> (t -> Eff (Choose :> r) a) -> Eff r [a]
   handle [] _  = return []
   handle [x] k = loop (k x)
   handle lst k = concat <$> mapM (loop . k) lst
diff --git a/src/Control/Eff/Coroutine.hs b/src/Control/Eff/Coroutine.hs
--- a/src/Control/Eff/Coroutine.hs
+++ b/src/Control/Eff/Coroutine.hs
@@ -21,7 +21,7 @@
 
 -- | Yield a value of type a and suspend the coroutine.
 yield :: (Typeable a, Member (Yield a) r) => a -> Eff r ()
-yield x = send (inj . Yield x)
+yield x = send . inj $ Yield x id
 
 -- | Status of a thread: done or reporting the value of the type a
 --   (For simplicity, a co-routine reports a value but accepts unit)
@@ -37,8 +37,9 @@
 
 -- | Launch a thread and report its status.
 runC :: Typeable a => Eff (Yield a :> r) w -> Eff r (Y r a w)
-runC m = loop (admin m)
+runC = loop
   where
-    loop (Pure x) = return (Done x)
-    loop (Free u)   = handleRelay u loop $
-                    \(Yield x k) -> return (Y x (loop . k))
+    loop = freeMap
+           (return . Done)
+           (\u -> handleRelay u loop $
+                  \(Yield x k) -> return (Y x (loop . k)))
diff --git a/src/Control/Eff/Cut.hs b/src/Control/Eff/Cut.hs
--- a/src/Control/Eff/Cut.hs
+++ b/src/Control/Eff/Cut.hs
@@ -45,7 +45,6 @@
                       , cutfalse
                       ) where
 
-import Control.Applicative ((<$>))
 import Data.Typeable
 
 import Control.Eff
@@ -67,16 +66,24 @@
 -- it discards the remaining choicepoints.
 -- It completely handles CutFalse effects but not non-determinism.
 call :: Member Choose r => Eff (Exc CutFalse :> r) a -> Eff r a
-call m = loop [] (admin m) where
- loop jq (Pure x) = return x `mplus'` next jq          -- (C2)
- loop jq (Free u) = case decomp u of
-    Right (Exc CutFalse) -> mzero'  -- drop jq (F2)
-    Left u' -> check jq u'
+call = loop [] where
+ loop jq = freeMap
+           (\x -> return x `mplus'` next jq)          -- (C2)
+           (\u -> case decomp u of
+               Right (Exc CutFalse) -> mzero'  -- drop jq (F2)
+               Left u' -> check jq u')
 
+ check :: Member Choose r
+          => [Eff (Exc CutFalse :> r) a]
+          -> Union r (Eff (Exc CutFalse :> r) a)
+          -> Eff r a
  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 (<$> u) >>= loop jq      -- (C4)
+ check jq u = send u >>= loop jq      -- (C4)
 
+ next :: Member Choose r
+         => [Eff (Exc CutFalse :> r) a]
+         -> Eff r a
  next []    = mzero'
  next (h:t) = loop t h
diff --git a/src/Control/Eff/Exception.hs b/src/Control/Eff/Exception.hs
--- a/src/Control/Eff/Exception.hs
+++ b/src/Control/Eff/Exception.hs
@@ -37,7 +37,7 @@
 
 -- | Throw an exception in an effectful computation.
 throwExc :: (Typeable e, Member (Exc e) r) => e -> Eff r a
-throwExc e = send (\_ -> inj $ Exc e)
+throwExc e = send . inj $ Exc e
 {-# INLINE throwExc #-}
 
 -- | Makes an effect fail, preventing future effects from happening.
@@ -47,15 +47,16 @@
 
 -- | Run a computation that might produce an exception.
 runExc :: Typeable e => Eff (Exc e :> r) a -> Eff r (Either e a)
-runExc = loop . admin
+runExc = loop
  where
-  loop (Pure x)  = return (Right x)
-  loop (Free u)    = handleRelay u loop (\(Exc e) -> return (Left e))
+  loop = freeMap
+         (return . Right)
+         (\u -> handleRelay u loop (\(Exc e) -> return (Left e)))
 
 -- | Runs a failable effect, such that failed computation return 'Nothing', and
 --   'Just' the return value on success.
 runFail :: Eff (Fail :> r) a -> Eff r (Maybe a)
-runFail = fmap (either (\_-> Nothing) Just) . runExc
+runFail = fmap (either (const Nothing) Just) . runExc
 {-# INLINE runFail #-}
 
 -- | Run a computation that might produce exceptions,
@@ -64,10 +65,11 @@
          => Eff r a
          -> (e -> Eff r a)
          -> Eff r a
-catchExc m handle = loop (admin m)
+catchExc m handle = loop m
  where
-  loop (Pure x)  = return x
-  loop (Free u)    = interpose u loop (\(Exc e) -> handle e)
+  loop = freeMap
+         return
+         (\u -> interpose u loop (\(Exc e) -> handle e))
 
 -- | Add a default value (i.e. failure handler) to a fallible computation.
 -- This hides the fact that a failure happened.
diff --git a/src/Control/Eff/Fresh.hs b/src/Control/Eff/Fresh.hs
--- a/src/Control/Eff/Fresh.hs
+++ b/src/Control/Eff/Fresh.hs
@@ -19,12 +19,13 @@
 
 -- | Produce a value that has not been previously produced.
 fresh :: (Typeable i, Enum i, Member (Fresh i) r) => Eff r i
-fresh = send (inj . Fresh)
+fresh = send . inj $ Fresh id
 
 -- | Run an effect requiring unique values.
 runFresh :: (Typeable i, Enum i) => Eff (Fresh i :> r) w -> i -> Eff r w
-runFresh m s0 = loop s0 (admin m)
+runFresh m s0 = loop s0 m
   where
-    loop _ (Pure x) = return x
-    loop s (Free u)   = handleRelay u (loop s) $
-                          \(Fresh k) -> (loop $! succ s) (k s)
+    loop s = freeMap
+             return
+             (\u -> handleRelay u (loop s) $
+                    \(Fresh k) -> (loop $! succ s) (k s))
diff --git a/src/Control/Eff/Lift.hs b/src/Control/Eff/Lift.hs
--- a/src/Control/Eff/Lift.hs
+++ b/src/Control/Eff/Lift.hs
@@ -50,11 +50,13 @@
 
 -- | Lift a Monad to an Effect.
 lift :: (Typeable1 m, SetMember Lift (Lift m) r) => m a -> Eff r a
-lift m = send (inj . Lift m)
+lift m = send . inj $ Lift m id
 
 -- | The handler of Lift requests. It is meant to be terminal:
 -- we only allow a single Lifted Monad.
 runLift :: (Monad m, Typeable1 m) => Eff (Lift m :> ()) w -> m w
-runLift m = loop (admin m) where
- loop (Pure x) = return x
- loop (Free u) = prjForce u $ \(Lift m' k) -> m' >>= loop . k
+runLift = loop
+  where
+    loop = freeMap
+           return
+           (\u -> prjForce u $ \(Lift m' k) -> m' >>= loop . k)
diff --git a/src/Control/Eff/Reader/Lazy.hs b/src/Control/Eff/Reader/Lazy.hs
--- a/src/Control/Eff/Reader/Lazy.hs
+++ b/src/Control/Eff/Reader/Lazy.hs
@@ -23,19 +23,20 @@
 
 -- | Get the current value from a Reader.
 ask :: (Typeable e, Member (Reader e) r) => Eff r e
-ask = send (inj . Reader)
+ask = send . inj $ Reader id
 
 -- | Locally rebind the value in the dynamic environment.
--- This function both requests and admins Reader requests.
+-- This function both requests and handles Reader requests.
 local :: (Typeable e, Member (Reader e) r)
       => (e -> e)
       -> Eff r a
       -> Eff r a
 local f m = do
   e <- f <$> ask
-  let loop (Pure x) = return x
-      loop (Free u) = interpose u loop (\(Reader k) -> loop (k e))
-  loop (admin m)
+  let loop = freeMap
+             return
+             (\u -> interpose u loop (\(Reader k) -> loop (k e)))
+  loop m
 
 -- | Request the environment value using a transformation function.
 reader :: (Typeable e, Member (Reader e) r) => (e -> a) -> Eff r a
@@ -44,7 +45,8 @@
 -- | The handler of Reader requests. The return type shows that
 -- all Reader requests are fully handled.
 runReader :: Typeable e => Eff (Reader e :> r) w -> e -> Eff r w
-runReader m e = loop (admin m)
+runReader m e = loop m
   where
-    loop (Pure x) = return x
-    loop (Free u) = handleRelay u loop (\(Reader k) -> loop (k e))
+    loop = freeMap
+           return
+           (\u -> handleRelay u loop (\(Reader k) -> loop (k e)))
diff --git a/src/Control/Eff/Reader/Strict.hs b/src/Control/Eff/Reader/Strict.hs
--- a/src/Control/Eff/Reader/Strict.hs
+++ b/src/Control/Eff/Reader/Strict.hs
@@ -24,7 +24,7 @@
 
 -- | Get the current value from a Reader.
 ask :: (Typeable e, Member (Reader e) r) => Eff r e
-ask = send (inj . Reader)
+ask = send . inj $ Reader id
 
 -- | Locally rebind the value in the dynamic environment.
 -- This function both requests and admins Reader requests.
@@ -34,9 +34,10 @@
       -> Eff r a
 local f m = do
   e <- f <$> ask
-  let loop (Pure x) = return x
-      loop (Free u) = interpose u loop (\(Reader k) -> loop (k e))
-  loop (admin m)
+  let loop = freeMap
+             return
+             (\u -> interpose u loop (\(Reader k) -> loop (k e)))
+  loop m
 
 -- | Request the environment value using a transformation function.
 reader :: (Typeable e, Member (Reader e) r) => (e -> a) -> Eff r a
@@ -45,6 +46,7 @@
 -- | The handler of Reader requests. The return type shows that
 -- all Reader requests are fully handled.
 runReader :: Typeable e => Eff (Reader e :> r) w -> e -> Eff r w
-runReader m !e = loop (admin m) where
- loop (Pure x) = return x
- loop (Free u) = handleRelay u loop (\(Reader k) -> loop (k e))
+runReader m !e = loop m where
+  loop = freeMap
+         return
+         (\u -> handleRelay u loop (\(Reader k) -> loop (k e)))
diff --git a/src/Control/Eff/State/Lazy.hs b/src/Control/Eff/State/Lazy.hs
--- a/src/Control/Eff/State/Lazy.hs
+++ b/src/Control/Eff/State/Lazy.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -28,22 +27,24 @@
 
 -- | Return the current value of the state.
 get :: (Typeable e, Member (State e) r) => Eff r e
-get = send (inj . State id)
+get = send . inj $ State id id
 
 -- | Transform the state with a function.
 modify :: (Typeable s, Member (State s) r) => (s -> s) -> Eff r ()
-modify f = send $ \k -> inj $ State f $ \_ -> k ()
+modify f = send . inj $ State f $ const ()
 
 -- | Run a State effect.
 runState :: Typeable s
          => s                     -- ^ Initial state
          -> Eff (State s :> r) w  -- ^ Effect incorporating State
          -> Eff r (s, w)          -- ^ Effect containing final state and a return value
-runState s0 = loop s0 . admin where
- loop s (Pure x) = return (s, x)
- loop s (Free u)   = handleRelay u (loop s) $
-                       \(State t k) -> let s' = t s
-                                       in loop s' (k s')
+runState = loop
+  where
+    loop s = freeMap
+             (\x -> return (s, x))
+             (\u -> handleRelay u (loop s) $
+                    \(State t k) -> let s' = t s
+                                    in loop s' (k s'))
 
 -- | Run a State effect, discarding the final state.
 evalState :: Typeable s => s -> Eff (State s :> r) w -> Eff r w
diff --git a/src/Control/Eff/State/Strict.hs b/src/Control/Eff/State/Strict.hs
--- a/src/Control/Eff/State/Strict.hs
+++ b/src/Control/Eff/State/Strict.hs
@@ -41,22 +41,24 @@
 
 -- | Return the current value of the state.
 get :: (Typeable e, Member (State e) r) => Eff r e
-get = send (inj . State id)
+get = send . inj $ State id id
 
 -- | Transform the state with a function.
 modify :: (Typeable s, Member (State s) r) => (s -> s) -> Eff r ()
-modify f = send $ \k -> inj $ State f $ \_ -> k ()
+modify f = send . inj $ State f $ const ()
 
 -- | Run a State effect.
 runState :: Typeable s
          => s                     -- ^ Initial state
          -> Eff (State s :> r) w  -- ^ Effect incorporating State
          -> Eff r (s, w)          -- ^ Effect containing final state and a return value
-runState s0 = loop s0 . admin where
- loop !s (Pure x) = return (s, x)
- loop !s (Free u)   = handleRelay u (loop s) $
-                       \(State t k) -> let s' = t s
-                                       in loop s' (k s')
+runState = loop
+  where
+    loop !s = freeMap
+              (\x -> return (s, x))
+              (\u -> handleRelay u (loop s) $
+                     \(State t k) -> let s' = t s
+                                     in loop s' (k s'))
 
 -- | Run a State effect, discarding the final state.
 evalState :: Typeable s => s -> Eff (State s :> r) w -> Eff r w
diff --git a/src/Control/Eff/Trace.hs b/src/Control/Eff/Trace.hs
--- a/src/Control/Eff/Trace.hs
+++ b/src/Control/Eff/Trace.hs
@@ -18,11 +18,12 @@
 
 -- | Print a string as a trace.
 trace :: Member Trace r => String -> Eff r ()
-trace x = send (inj . Trace x)
+trace x = send . inj $ Trace x id
 
 -- | Run a computation producing Traces.
 runTrace :: Eff (Trace :> ()) w -> IO w
-runTrace m = loop (admin m)
+runTrace = loop
   where
-    loop (Pure x) = return x
-    loop (Free u)   = prjForce u $ \(Trace s k) -> putStrLn s >> loop (k ())
+    loop = freeMap
+           return
+           (\u -> prjForce u $ \(Trace s k) -> putStrLn s >> loop (k ()))
diff --git a/src/Control/Eff/Writer/Lazy.hs b/src/Control/Eff/Writer/Lazy.hs
--- a/src/Control/Eff/Writer/Lazy.hs
+++ b/src/Control/Eff/Writer/Lazy.hs
@@ -25,25 +25,27 @@
 
 -- | Write a new value.
 tell :: (Typeable w, Member (Writer w) r) => w -> Eff r ()
-tell w = send $ \f -> inj $ Writer w $ f ()
+tell w = send . inj $ Writer w ()
 
 -- | Transform the state being produced.
 censor :: (Typeable w, Member (Writer w) r) => (w -> w) -> Eff r a -> Eff r a
-censor f = loop . admin
+censor f = loop
   where
-    loop (Pure x) = return x
-    loop (Free u) = interpose u loop
-               $ \(Writer w v) -> tell (f w) >> loop v
+    loop = freeMap
+           return
+           (\u -> interpose u loop
+                  $ \(Writer w v) -> tell (f w) >> loop v)
 
 -- | Handle Writer requests, using a user-provided function to accumulate values.
 runWriter :: Typeable w => (w -> b -> b) -> b -> Eff (Writer w :> r) a -> Eff r (b, a)
-runWriter accum b = loop . admin
+runWriter accum b = loop
   where
     first f (x, y) = (f x, y)
 
-    loop (Pure x) = return (b, x)
-    loop (Free u) = handleRelay u loop
-                 $ \(Writer w v) -> first (accum w) <$> loop v
+    loop = freeMap
+           (\x -> return (b, x))
+           (\u -> handleRelay u loop
+                  $ \(Writer w v) -> first (accum w) <$> loop v)
 
 -- | Handle Writer requests by taking the first value provided.
 runFirstWriter :: Typeable w => Eff (Writer w :> r) a -> Eff r (Maybe w, a)
diff --git a/src/Control/Eff/Writer/Strict.hs b/src/Control/Eff/Writer/Strict.hs
--- a/src/Control/Eff/Writer/Strict.hs
+++ b/src/Control/Eff/Writer/Strict.hs
@@ -26,25 +26,27 @@
 
 -- | Write a new value.
 tell :: (Typeable w, Member (Writer w) r) => w -> Eff r ()
-tell !w = send $ \f -> inj $ Writer w $ f ()
+tell !w = send . inj $ Writer w ()
 
 -- | Transform the state being produced.
 censor :: (Typeable w, Member (Writer w) r) => (w -> w) -> Eff r a -> Eff r a
-censor f = loop . admin
+censor f = loop
   where
-    loop (Pure x) = return x
-    loop (Free u) = interpose u loop
-               $ \(Writer w v) -> tell (f w) >> loop v
+    loop = freeMap
+           return
+           (\u -> interpose u loop
+                  $ \(Writer w v) -> tell (f w) >> loop v)
 
 -- | Handle Writer requests, using a user-provided function to accumulate values.
 runWriter :: Typeable w => (w -> b -> b) -> b -> Eff (Writer w :> r) a -> Eff r (b, a)
-runWriter accum !b = loop . admin
+runWriter accum !b = loop
   where
     first f (x, y) = (f x, y)
 
-    loop (Pure x) = return (b, x)
-    loop (Free u) = handleRelay u loop
-                 $ \(Writer w v) -> first (accum w) <$> loop v
+    loop = freeMap
+           (\x -> return (b, x))
+           (\u -> handleRelay u loop
+                  $ \(Writer w v) -> first (accum w) <$> loop v)
 
 -- | Handle Writer requests by taking the first value provided.
 runFirstWriter :: Typeable w => Eff (Writer w :> r) a -> Eff r (Maybe w, a)
diff --git a/src/Control/Monad/Free/Reflection.hs b/src/Control/Monad/Free/Reflection.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Free/Reflection.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+#if __GLASGOW_HASKELL__ >= 708
+{-# LANGUAGE AutoDeriveTypeable #-}
+#endif
+
+module Control.Monad.Free.Reflection(
+  Free
+  , freePure
+  , freeImpure
+  , freeMap
+  , FreeView (..)
+  , fromView
+  , toView
+  ) where
+
+import Control.Arrow (Kleisli (..))
+import Control.Applicative
+import Control.Monad
+import Data.TASequence
+import Data.TASequence.FastCatQueue (FastTCQueue)
+
+-- | Specific type-aligned sequence used to store chain of monadic binds.
+type TCQ = FastTCQueue
+
+-- | Type used to denote monadic chain of binds. As expected this builds on the
+-- Kleisli representation.
+type FreeExp f a b = TCQ (Kleisli (Free f)) a b
+
+-- | The abstract Free datatype. Original work available at
+-- <http://okmij.org/ftp/Haskell/AlgorithmsH1.html#reflection-without-remorse>.
+data Free f a =
+  forall x. Free (FreeView f x) (FreeExp f x a)
+
+-- | Inject a pure value into Free
+freePure :: a -> Free f a
+freePure = fromView . Pure
+
+-- | Inject an impure value into Free
+freeImpure :: f (Free f a) -> Free f a
+freeImpure = fromView . Impure
+
+-- | Case analysis for the 'Free' construction. Similar in spirit to 'either'
+-- and 'maybe'.
+freeMap :: Functor f
+           => (a -> t) -- ^ function to be applied if value is Pure
+           -> (f (Free f a) -> t) -- ^ function to be applied on Impure value
+           -> Free f a -- ^ Free value to be mapped over
+           -> t -- ^ result
+freeMap f g mx = case toView mx of
+  Pure x -> f x
+  Impure u -> g u
+
+instance Functor f => Functor (Free f) where
+  fmap = liftM
+instance Functor f => Applicative (Free f) where
+  pure = return
+  (<*>) = ap
+instance Functor f => Monad (Free f) where
+  return = freePure
+  mx >>= f = mx ^>>= tsingleton (Kleisli f)
+
+-- | The traditional 'view' of Free constructions
+data FreeView f a = Pure a -- ^ case embedding pure values
+                  | Impure (f (Free f a)) -- ^ case embedding impure values
+                                          -- nested in @f@. Traditionally this
+                                          -- is the @Control.Monad.Free.Free@
+                                          -- constructor, but that's confusing.
+
+-- | A way to get a 'Free' construction from the view by constructing an
+-- explicit expression with one element.
+fromView :: FreeView f a -> Free f a
+fromView x = Free x tempty
+
+-- | A way to evaluate the 'Free' construction to its view (i.e., head normal
+-- form). This includes the logic to perform one level of monadic bind as needed
+-- from the 'FreeExp' representation.
+toView :: Functor f => Free f a -> FreeView f a
+toView (Free h t) = case h of
+  Pure x -> case tviewl t of
+    TAEmptyL -> Pure x
+    hc :< tc -> toView (runKleisli hc x ^>>= tc)
+  Impure f -> Impure (fmap (^>>= t) f)
+
+-- | The essence of monadic '>>=', i.e., append/concatenation (of sorts)
+(^>>=) :: Free f a -> FreeExp f a b -> Free f b
+(Free x ys) ^>>= r = Free x (ys >< r)
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -21,6 +21,7 @@
 import Control.Eff.Reader.Strict as StrictR
 import Control.Eff.State.Strict as StrictS
 import Control.Eff.Writer.Strict as StrictW
+import Data.Void
 
 withError :: a -> ErrorCall -> a
 withError a _ = a
@@ -75,7 +76,7 @@
     inc :: Integer -> Integer
     inc = (+1)
 
-    listE :: Eff (LazyW.Writer Integer :> ()) () -> [Integer]
+    listE :: Eff (LazyW.Writer Integer :> Void) () -> [Integer]
     listE = fst . run . LazyW.runWriter (:) []
 
 testReaderLaziness :: Assertion
@@ -83,7 +84,7 @@
                      in assertNoUndefined (e :: ())
   where
     voidReader = do
-        _ <- (LazyR.ask :: Eff (LazyR.Reader () :> ()) ())
+        _ <- (LazyR.ask :: Eff (LazyR.Reader () :> Void) ())
         return ()
 
 testReaderStrictness :: Assertion
@@ -91,7 +92,7 @@
                        in assertUndefined (e :: ())
   where
     voidReader = do
-        _ <- (StrictR.ask :: Eff (StrictR.Reader () :> ()) ())
+        _ <- (StrictR.ask :: Eff (StrictR.Reader () :> Void) ())
         return ()
 
 testStateLaziness :: Assertion
@@ -102,10 +103,10 @@
                                >> putVoid ()
                     in assertNoUndefined r
   where
-    getVoid :: Eff (LazyS.State () :> ()) ()
+    getVoid :: Eff (LazyS.State () :> Void) ()
     getVoid = LazyS.get
 
-    putVoid :: () -> Eff (LazyS.State () :> ()) ()
+    putVoid :: () -> Eff (LazyS.State () :> Void) ()
     putVoid = LazyS.put
 
 testStateStrictness :: Assertion
@@ -116,10 +117,10 @@
                                  >> putVoid ()
                       in assertUndefined r
   where
-    getVoid :: Eff (StrictS.State () :> ()) ()
+    getVoid :: Eff (StrictS.State () :> Void) ()
     getVoid = StrictS.get
 
-    putVoid :: () -> Eff (StrictS.State () :> ()) ()
+    putVoid :: () -> Eff (StrictS.State () :> Void) ()
     putVoid = StrictS.put
 
 testLastWriterLaziness :: Assertion
@@ -136,7 +137,7 @@
 
 testFailure :: Assertion
 testFailure =
-  let go :: Eff (Exc () :> StrictW.Writer Int :> ()) Int
+  let go :: Eff (Exc () :> StrictW.Writer Int :> Void) Int
          -> Int
       go = fst . run . StrictW.runWriter (+) 0 . ignoreFail
       ret = go $ do
@@ -166,12 +167,12 @@
     qu :: Bool -> Bool
     qu x = run $ StrictR.runReader (readerAp x) readerId
 
-    readerAp :: Bool -> Eff (StrictR.Reader (Eff (StrictR.Reader Bool :> ()) Bool) :> ()) Bool
+    readerAp :: Bool -> Eff (StrictR.Reader (Eff (StrictR.Reader Bool :> Void) Bool) :> Void) Bool
     readerAp x = do
       f <- StrictR.ask
       return . run $ StrictR.runReader f x
 
-    readerId :: Eff (StrictR.Reader Bool :> ()) Bool
+    readerId :: Eff (StrictR.Reader Bool :> Void) Bool
     readerId = do
       x <- StrictR.ask
       return x