diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Fumiaki Kinoshita
+
+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 Fumiaki Kinoshita 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/extensible-skeleton.cabal b/extensible-skeleton.cabal
new file mode 100644
--- /dev/null
+++ b/extensible-skeleton.cabal
@@ -0,0 +1,49 @@
+cabal-version:       2.4
+name:                extensible-skeleton
+version:             0
+synopsis:            Operational-based extensible effect library
+homepage:            https://github.com/fumieval/extensible
+bug-reports:         http://github.com/fumieval/extensible/issues
+description:         See README.md
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Fumiaki Kinoshita
+maintainer:          Fumiaki Kinoshita <fumiexcel@gmail.com>
+copyright:           Copyright (c) 2019 Fumiaki Kinoshita
+category:            Monads
+build-type:          Simple
+stability:           experimental
+Tested-With:         GHC == 8.4.4, GHC == 8.6.3
+
+extra-source-files:
+
+source-repository head
+  type: git
+  location: https://github.com/fumieval/extensible.git
+
+library
+  build-depends: base >= 4.8 && <5
+    , extensible >= 0.6.2, monad-skeleton, resourcet, membership, transformers, mtl
+    , exceptions, profunctors, template-haskell
+  exposed-modules:
+    Data.Extensible.Effect
+    Data.Extensible.Effect.Default
+    Data.Extensible.Effect.TH
+  ghc-options: -Wall
+  hs-source-dirs: src
+  default-extensions:
+    TypeOperators
+    DataKinds
+    PolyKinds
+    GADTs
+    RankNTypes
+    FlexibleContexts
+    FlexibleInstances
+  default-language: Haskell2010
+
+test-suite effects
+  type: exitcode-stdio-1.0
+  main-is: effects.hs
+  build-depends: base, extensible
+  hs-source-dirs: tests
+  default-language:    Haskell2010
diff --git a/src/Data/Extensible/Effect.hs b/src/Data/Extensible/Effect.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Effect.hs
@@ -0,0 +1,481 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Effect
+-- Copyright   :  (c) Fumiaki Kinoshita 2018
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Name-based extensible effects
+-----------------------------------------------------------------------------
+module Data.Extensible.Effect (
+  -- * Base
+  Instruction(..)
+  , Eff
+  , liftEff
+  , liftsEff
+  , hoistEff
+  , castEff
+  -- * Step-wise handling
+  , Interpreter(..)
+  , handleEff
+  -- * Peeling
+  , peelEff
+  , Rebinder
+  , rebindEff0
+  , peelEff0
+  , rebindEff1
+  , peelEff1
+  , rebindEff2
+  , leaveEff
+  , retractEff
+  -- * Anonymous actions
+  , Action(..)
+  , Function
+  , runAction
+  , (@!?)
+  , peelAction
+  , peelAction0
+  -- * transformers-compatible actions and handlers
+  -- ** Reader
+  , ReaderEff
+  , askEff
+  , asksEff
+  , localEff
+  , runReaderEff
+  -- ** State
+  , State
+  , getEff
+  , getsEff
+  , putEff
+  , modifyEff
+  , stateEff
+  , runStateEff
+  , execStateEff
+  , evalStateEff
+  -- ** Writer
+  , WriterEff
+  , writerEff
+  , tellEff
+  , listenEff
+  , passEff
+  , runWriterEff
+  , execWriterEff
+  -- ** Maybe
+  , MaybeEff
+  , nothingEff
+  , runMaybeEff
+  -- ** Either
+  , EitherEff
+  , throwEff
+  , catchEff
+  , runEitherEff
+  , mapLeftEff
+  -- ** Iter
+  , Identity
+  , tickEff
+  , runIterEff
+  -- ** Cont
+  , ContT
+  , contEff
+  , runContEff
+  , callCCEff
+  ) where
+
+import Control.Applicative
+import Data.Bifunctor (first)
+import Control.Monad.Skeleton
+import Control.Monad.Trans.State.Strict
+import Control.Monad.Trans.Cont (ContT(..))
+import Data.Extensible.Field
+import Data.Extensible.Inclusion
+import Data.Extensible.Internal.Rig
+import Data.Extensible.Product
+import Data.Extensible.Class
+import Data.Kind (Type)
+import Data.Functor.Identity
+import Data.Profunctor.Unsafe -- Trustworthy since 7.8
+import Data.Type.Equality
+import Type.Membership
+
+-- | A unit of named effects. This is a variant of @(':|')@ specialised for
+-- 'Type -> Type'.
+data Instruction (xs :: [Assoc k (Type -> Type)]) a where
+  Instruction :: !(Membership xs kv) -> TargetOf kv a -> Instruction xs a
+
+-- | The extensible operational monad
+type Eff xs = Skeleton (Instruction xs)
+
+-- | Lift an instruction onto an 'Eff' action.
+liftEff :: forall s t xs a. Lookup xs s t => Proxy s -> t a -> Eff xs a
+liftEff p x = liftsEff p x id
+{-# INLINE liftEff #-}
+
+-- | Lift an instruction onto an 'Eff' action and apply a function to the result.
+liftsEff :: forall s t xs a r. Lookup xs s t
+  => Proxy s -> t a -> (a -> r) -> Eff xs r
+liftsEff _ x k = boned
+  $ Instruction (association :: Membership xs (s ':> t)) x :>>= return . k
+{-# INLINE liftsEff #-}
+
+-- | Censor a specific type of effects in an action.
+hoistEff :: forall s t xs a. Lookup xs s t => Proxy s -> (forall x. t x -> t x) -> Eff xs a -> Eff xs a
+hoistEff _ f = hoistSkeleton $ \(Instruction i t) -> case compareMembership (association :: Membership xs (s ':> t)) i of
+  Right Refl -> Instruction i (f t)
+  _ -> Instruction i t
+{-# INLINABLE hoistEff #-}
+
+-- | Upcast an action.
+castEff :: IncludeAssoc ys xs => Eff xs a -> Eff ys a
+castEff = hoistSkeleton
+  $ \(Instruction i t) -> Instruction (hlookup i inclusionAssoc) t
+
+-- | Build a relay-style handler from a triple of functions.
+--
+-- @
+-- runStateEff = peelEff1 (\a s -> return (a, s))
+--   (\m k s -> let (a, s') = runState m s in k a s')
+-- @
+--
+peelEff :: forall k t xs a r
+  . Rebinder xs r -- ^ Re-bind an unrelated action
+  -> (a -> r) -- ^ return the result
+  -> (forall x. t x -> (x -> r) -> r) -- ^ Handle the foremost type of an action
+  -> Eff (k >: t ': xs) a -> r
+peelEff pass ret wrap = go where
+  go m = case debone m of
+    Return a -> ret a
+    Instruction i t :>>= k -> testMembership i
+      (\Refl -> wrap t (go . k))
+      (\j -> pass (Instruction j t) (go . k))
+{-# INLINE peelEff #-}
+
+-- | 'peelEff' specialised for continuations with no argument
+peelEff0 :: forall k t xs a r. (a -> Eff xs r) -- ^ return the result
+  -> (forall x. t x -> (x -> Eff xs r) -> Eff xs r) -- ^ Handle the foremost type of an action
+  -> Eff (k >: t ': xs) a -> Eff xs r
+peelEff0 = peelEff rebindEff0
+{-# INLINE peelEff0 #-}
+
+-- | 'peelEff' specialised for 1-argument continuation
+peelEff1 :: forall k t xs a b r. (a -> b -> Eff xs r) -- ^ return the result
+  -> (forall x. t x -> (x -> b -> Eff xs r) -> b -> Eff xs r) -- ^ Handle the foremost type of an action
+  -> Eff (k >: t ': xs) a -> b -> Eff xs r
+peelEff1 = peelEff rebindEff1
+{-# INLINE peelEff1 #-}
+
+-- | A function to bind an 'Instruction' in 'peelEff'.
+type Rebinder xs r = forall x. Instruction xs x -> (x -> r) -> r
+
+-- | A common value for the second argument of 'peelEff'. Binds an instruction
+-- directly.
+rebindEff0 :: Rebinder xs (Eff xs r)
+rebindEff0 i k = boned $ i :>>= k
+
+-- | A pre-defined value for the second argument of 'peelEff'.
+-- Preserves the argument of the continuation.
+rebindEff1 :: Rebinder xs (a -> Eff xs r)
+rebindEff1 i k a = boned $ i :>>= flip k a
+
+-- | A pre-defined value for the second argument of 'peelEff'.
+-- Preserves two arguments of the continuation.
+rebindEff2 :: Rebinder xs (a -> b -> Eff xs r)
+rebindEff2 i k a b = boned $ i :>>= \x -> k x a b
+
+-- | Reveal the final result of 'Eff'.
+leaveEff :: Eff '[] a -> a
+leaveEff m = case debone m of
+  Return a -> a
+  _ -> error "Impossible"
+
+-- | Tear down an action using the 'Monad' instance of the instruction.
+retractEff :: forall k m a. Monad m => Eff '[k >: m] a -> m a
+retractEff m = case debone m of
+  Return a -> return a
+  Instruction i t :>>= k -> testMembership i
+    (\Refl -> t >>= retractEff . k)
+    $ error "Impossible"
+
+-- | Transformation between effects
+newtype Interpreter f g = Interpreter { runInterpreter :: forall a. g a -> f a }
+
+-- | Process an 'Eff' action using a record of 'Interpreter's.
+handleEff :: RecordOf (Interpreter m) xs -> Eff xs a -> MonadView m (Eff xs) a
+handleEff hs m = case debone m of
+  Instruction i t :>>= k -> views (pieceAt i) (runInterpreter .# getField) hs t :>>= k
+  Return a -> Return a
+
+-- | Anonymous representation of instructions.
+data Action (args :: [Type]) a r where
+  AResult :: Action '[] a a
+  AArgument :: x -> Action xs a r -> Action (x ': xs) a r
+
+-- | @'Function' [a, b, c] r@ is @a -> b -> c -> r@
+type family Function args r :: Type where
+  Function '[] r = r
+  Function (x ': xs) r = x -> Function xs r
+
+-- | Pass the arguments of 'Action' to the supplied function.
+runAction :: Function xs (f a) -> Action xs a r -> f r
+runAction r AResult = r
+runAction f (AArgument x a) = runAction (f x) a
+
+-- | Create a 'Field' of a 'Interpreter' for an 'Action'.
+(@!?) :: FieldName k -> Function xs (f a) -> Field (Interpreter f) (k ':> Action xs a)
+_ @!? f = Field $ Interpreter $ runAction f
+infix 1 @!?
+
+-- | Specialised version of 'peelEff' for 'Action's.
+-- You can pass a function @a -> b -> ... -> (q -> r) -> r@ as a handler for
+-- @'Action' '[a, b, ...] q@.
+peelAction :: forall k ps q xs a r
+  . (forall x. Instruction xs x -> (x -> r) -> r) -- ^ Re-bind an unrelated action
+  -> (a -> r) -- ^ return the result
+  -> Function ps ((q -> r) -> r) -- ^ Handle the foremost action
+  -> Eff (k >: Action ps q ': xs) a -> r
+peelAction pass ret wrap = go where
+  go m = case debone m of
+    Return a -> ret a
+    Instruction i t :>>= k -> testMembership i
+      (\Refl -> case t of
+        (_ :: Action ps q x) ->
+          let run :: forall t. Function t ((q -> r) -> r) -> Action t q x -> r
+              run f AResult = f (go . k)
+              run f (AArgument x a) = run (f x) a
+          in run wrap t)
+      $ \j -> pass (Instruction j t) (go . k)
+{-# INLINE peelAction #-}
+
+-- | Non continuation-passing variant of 'peelAction'.
+peelAction0 :: forall k ps q xs a. Function ps (Eff xs q) -- ^ Handle the foremost action
+  -> Eff (k >: Action ps q ': xs) a -> Eff xs a
+peelAction0 wrap = go where
+  go m = case debone m of
+    Return a -> return a
+    Instruction i t :>>= k -> testMembership i
+      (\Refl -> case t of
+        (_ :: Action ps q x) ->
+          let run :: forall t. Function t (Eff xs q) -> Action t q x -> Eff xs a
+              run f AResult = f >>= go . k
+              run f (AArgument x a) = run (f x) a
+          in run wrap t)
+      $ \j -> rebindEff0 (Instruction j t) (go . k)
+{-# INLINE peelAction0 #-}
+
+-- | The reader monad is characterised by a type equality between the result
+-- type and the enviroment type.
+type ReaderEff = (:~:)
+
+-- | Fetch the environment.
+askEff :: forall k r xs. Lookup xs k (ReaderEff r)
+  => Proxy k -> Eff xs r
+askEff p = liftEff p Refl
+{-# INLINE askEff #-}
+
+-- | Pass the environment to a function.
+asksEff :: forall k r xs a. Lookup xs k (ReaderEff r)
+  => Proxy k -> (r -> a) -> Eff xs a
+asksEff p = liftsEff p Refl
+{-# INLINE asksEff #-}
+
+-- | Modify the enviroment locally.
+localEff :: forall k r xs a. Lookup xs k (ReaderEff r)
+  => Proxy k -> (r -> r) -> Eff xs a -> Eff xs a
+localEff _ f = go where
+  go m = case debone m of
+    Return a -> return a
+    Instruction i t :>>= k -> case compareMembership
+      (association :: Membership xs (k >: ReaderEff r)) i of
+        Left _ -> boned $ Instruction i t :>>= go . k
+        Right Refl -> case t of
+          Refl -> boned $ Instruction i t :>>= go . k . f
+{-# INLINE localEff #-}
+
+-- | Run the frontal reader effect.
+runReaderEff :: forall k r xs a. Eff (k >: ReaderEff r ': xs) a -> r -> Eff xs a
+runReaderEff m r = peelEff0 return (\Refl k -> k r) m
+{-# INLINE runReaderEff #-}
+
+-- | Get the current state.
+getEff :: forall k s xs. Lookup xs k (State s)
+  => Proxy k -> Eff xs s
+getEff k = liftEff k get
+{-# INLINE getEff #-}
+
+-- | Pass the current state to a function.
+getsEff :: forall k s a xs. Lookup xs k (State s)
+  => Proxy k -> (s -> a) -> Eff xs a
+getsEff k = liftsEff k get
+{-# INLINE getsEff #-}
+
+-- | Replace the state with a new value.
+putEff :: forall k s xs. Lookup xs k (State s)
+  => Proxy k -> s -> Eff xs ()
+putEff k = liftEff k . put
+{-# INLINE putEff #-}
+
+-- | Modify the state.
+modifyEff :: forall k s xs. Lookup xs k (State s)
+  => Proxy k -> (s -> s) -> Eff xs ()
+modifyEff k f = liftEff k $ state $ \s -> ((), f s)
+{-# INLINE modifyEff #-}
+
+-- | Lift a state modification function.
+stateEff :: forall k s xs a. Lookup xs k (State s)
+  => Proxy k -> (s -> (a, s)) -> Eff xs a
+stateEff k = liftEff k . state
+{-# INLINE stateEff #-}
+
+contState :: State s a -> (a -> s -> r) -> s -> r
+contState m k s = let (a, s') = runState m s in k a $! s'
+
+-- | Run the frontal state effect.
+runStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs (a, s)
+runStateEff = peelEff1 (\a s -> return (a, s)) contState
+{-# INLINE runStateEff #-}
+
+-- | Run the frontal state effect and return the final state.
+execStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs s
+execStateEff = peelEff1 (const return) contState
+{-# INLINE execStateEff #-}
+
+-- | Run the frontal state effect and return the final result.
+evalStateEff :: forall k s xs a. Eff (k >: State s ': xs) a -> s -> Eff xs a
+evalStateEff = peelEff1 (const . return) contState
+{-# INLINE evalStateEff #-}
+
+-- | @(,)@ already is a writer monad.
+type WriterEff w = (,) w
+
+-- | Write the second element and return the first element.
+writerEff :: forall k w xs a. (Lookup xs k (WriterEff w))
+  => Proxy k -> (a, w) -> Eff xs a
+writerEff k (a, w) = liftEff k (w, a)
+{-# INLINE writerEff #-}
+
+-- | Write a value.
+tellEff :: forall k w xs. (Lookup xs k (WriterEff w))
+  => Proxy k -> w -> Eff xs ()
+tellEff k w = liftEff k (w, ())
+{-# INLINE tellEff #-}
+
+-- | Squash the outputs into one step and return it.
+listenEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w)
+  => Proxy k -> Eff xs a -> Eff xs (a, w)
+listenEff p = go mempty where
+  go w m = case debone m of
+    Return a -> writerEff p ((a, w), w)
+    Instruction i t :>>= k -> case compareMembership (association :: Membership xs (k ':> (,) w)) i of
+      Left _ -> boned $ Instruction i t :>>= go w . k
+      Right Refl -> let (w', a) = t
+                        !w'' = mappend w w' in go w'' (k a)
+{-# INLINE listenEff #-}
+
+-- | Modify the output using the function in the result.
+passEff :: forall k w xs a. (Lookup xs k (WriterEff w), Monoid w)
+  => Proxy k -> Eff xs (a, w -> w) -> Eff xs a
+passEff p = go mempty where
+  go w m = case debone m of
+    Return (a, f) -> writerEff p (a, f w)
+    Instruction i t :>>= k -> case compareMembership (association :: Membership xs (k ':> (,) w)) i of
+      Left _ -> boned $ Instruction i t :>>= go w . k
+      Right Refl -> let (w', a) = t
+                        !w'' = mappend w w' in go w'' (k a)
+{-# INLINE passEff #-}
+
+contWriter :: Monoid w => (w, a) -> (a -> w -> r) -> w -> r
+contWriter (w', a) k w = k a $! mappend w w'
+
+-- | Run the frontal writer effect.
+runWriterEff :: forall k w xs a. Monoid w => Eff (k >: WriterEff w ': xs) a -> Eff xs (a, w)
+runWriterEff = peelEff1 (\a w -> return (a, w)) contWriter `flip` mempty
+{-# INLINE runWriterEff #-}
+
+-- | Run the frontal state effect.
+execWriterEff :: forall k w xs a. Monoid w => Eff (k >: WriterEff w ': xs) a -> Eff xs w
+execWriterEff = peelEff1 (const return) contWriter `flip` mempty
+{-# INLINE execWriterEff #-}
+
+-- | An effect with no result
+type MaybeEff = Const ()
+
+-- | Break out of the computation. Similar to 'Nothing'.
+nothingEff :: Lookup xs k MaybeEff => Proxy k -> Eff xs a
+nothingEff = flip throwEff ()
+
+-- | Run an effect which may fail in the name of @k@.
+runMaybeEff :: forall k xs a. Eff (k >: MaybeEff ': xs) a -> Eff xs (Maybe a)
+runMaybeEff = peelEff0 (return . Just) $ \_ _ -> return Nothing
+{-# INLINE runMaybeEff #-}
+
+-- | Throwing an exception
+type EitherEff = Const
+
+-- | Throw an exception @e@, throwing the rest of the computation away.
+throwEff :: Lookup xs k (EitherEff e) => Proxy k -> e -> Eff xs a
+throwEff k = liftEff k . Const
+{-# INLINE throwEff #-}
+
+-- | Attach a handler for an exception.
+catchEff :: forall k e xs a. (Lookup xs k (EitherEff e))
+  => Proxy k -> Eff xs a -> (e -> Eff xs a) -> Eff xs a
+catchEff _ m0 handler = go m0 where
+  go m = case debone m of
+    Return a -> return a
+    Instruction i t :>>= k -> case compareMembership (association :: Membership xs (k ':> Const e)) i of
+      Left _ -> boned $ Instruction i t :>>= go . k
+      Right Refl -> handler (getConst t)
+{-# INLINE catchEff #-}
+
+-- | Run an action and abort on 'throwEff'.
+runEitherEff :: forall k e xs a. Eff (k >: EitherEff e ': xs) a -> Eff xs (Either e a)
+runEitherEff = peelEff0 (return . Right) $ \(Const e) _ -> return $ Left e
+{-# INLINE runEitherEff #-}
+
+-- | Put a milestone on a computation.
+tickEff :: Lookup xs k Identity => Proxy k -> Eff xs ()
+tickEff k = liftEff k $ Identity ()
+{-# INLINE tickEff #-}
+
+mapHeadEff :: (forall x. s x -> t x) -> Eff ((k >: s) ': xs) a -> Eff ((k' >: t) ': xs) a
+mapHeadEff f = hoistSkeleton $ \(Instruction i t) -> testMembership i
+  (\Refl -> Instruction leadership $ f t)
+  (\j -> Instruction (nextMembership j) t)
+
+-- | Take a function and applies it to an Either effect iff the effect takes the form Left _.
+mapLeftEff :: (e -> e') -> Eff ((k >: EitherEff e) ': xs) a -> Eff ((k >: EitherEff e') ': xs) a
+mapLeftEff f = mapHeadEff (first f)
+
+-- | Run a computation until the first call of 'tickEff'.
+runIterEff :: Eff (k >: Identity ': xs) a
+  -> Eff xs (Either a (Eff (k >: Identity ': xs) a))
+runIterEff m = case debone m of
+  Return a -> return (Left a)
+  Instruction i t :>>= k -> testMembership i
+    (\Refl -> return $ Right $ k $ runIdentity t)
+    $ \j -> boned $ Instruction j t :>>= runIterEff . k
+
+-- | Place a continuation-passing action.
+contEff :: Lookup xs k (ContT r m) => Proxy k
+  -> ((a -> m r) -> m r) -> Eff xs a
+contEff k = liftEff k . ContT
+
+-- | Unwrap a continuation.
+runContEff :: forall k r xs a. Eff (k >: ContT r (Eff xs) ': xs) a
+  -> (a -> Eff xs r)
+  -> Eff xs r
+runContEff m cont = case debone m of
+  Return a -> cont a
+  Instruction i t :>>= k -> testMembership i
+    (\Refl -> runContT t (flip runContEff cont . k))
+    $ \j -> boned $ Instruction j t :>>= flip runContEff cont . k
+
+-- | Call a function with the current continuation as its argument
+callCCEff :: Proxy k -> ((a -> Eff ((k >: ContT r (Eff xs)) : xs) b) -> Eff ((k >: ContT r (Eff xs)) : xs) a) -> Eff ((k >: ContT r (Eff xs)) : xs) a
+callCCEff k f = contHead k . ContT $ \c -> runContEff (f (\x -> contHead k . ContT $ \_ -> c x)) c
+  where
+    contHead :: Proxy k -> ContT r (Eff xs) a -> Eff ((k >: ContT r (Eff xs)) ': xs) a
+    contHead _ c = boned $ Instruction leadership c :>>= return
diff --git a/src/Data/Extensible/Effect/Default.hs b/src/Data/Extensible/Effect/Default.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Effect/Default.hs
@@ -0,0 +1,176 @@
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE CPP #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Effect.Default
+-- Copyright   :  (c) Fumiaki Kinoshita 2018
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+-- Default monad runners and 'MonadIO', 'MonadReader', 'MonadWriter',
+-- 'MonadState', 'MonadError' instances
+-----------------------------------------------------------------------------
+module Data.Extensible.Effect.Default (
+  ReaderDef
+  , runReaderDef
+  , StateDef
+  , runStateDef
+  , evalStateDef
+  , execStateDef
+  , WriterDef
+  , runWriterDef
+  , execWriterDef
+  , MaybeDef
+  , runMaybeDef
+  , EitherDef
+  , runEitherDef
+  , ContDef
+  , runContDef
+) where
+import Control.Applicative
+import Data.Extensible.Effect
+import Control.Monad.Except
+import Control.Monad.Catch
+import Control.Monad.Cont
+import Control.Monad.Reader.Class
+import Control.Monad.Skeleton
+import Control.Monad.State.Strict
+#if MIN_VERSION_resourcet(1,2,0)
+import Control.Monad.Trans.Resource
+#endif
+import Control.Monad.Writer.Class
+import Data.Type.Equality
+import Type.Membership
+
+instance (MonadIO m, Lookup xs "IO" m) => MonadIO (Eff xs) where
+  liftIO = liftEff (Proxy :: Proxy "IO") . liftIO
+
+#if MIN_VERSION_resourcet(1,2,0)
+instance (MonadResource m, Lookup xs "IO" m) => MonadResource (Eff xs) where
+  liftResourceT = liftEff (Proxy :: Proxy "IO") . liftResourceT
+#endif
+
+instance (MonadThrow m, Lookup xs "IO" m) => MonadThrow (Eff xs) where
+  throwM = liftEff (Proxy :: Proxy "IO") . throwM
+
+instance (MonadCatch m, Lookup xs "IO" m) => MonadCatch (Eff xs) where
+  catch m0 h = go m0 where
+    go m = case debone m of
+      Return a -> return a
+      Instruction i t :>>= k -> case compareMembership (association :: Membership xs ("IO" ':> m)) i of
+        Left _ -> boned $ Instruction i t :>>= go . k
+        Right Refl -> boned $ Instruction i (try t) :>>= go . either h k
+
+pReader :: Proxy "Reader"
+pReader = Proxy
+
+instance Lookup xs "Reader" ((:~:) r) => MonadReader r (Eff xs) where
+  ask = askEff pReader
+  local = localEff pReader
+  reader = asksEff pReader
+
+pState :: Proxy "State"
+pState = Proxy
+
+instance Lookup xs "State" (State s) => MonadState s (Eff xs) where
+  get = getEff pState
+  put = putEff pState
+  state = stateEff pState
+
+pWriter :: Proxy "Writer"
+pWriter = Proxy
+
+instance (Monoid w, Lookup xs "Writer" ((,) w)) => MonadWriter w (Eff xs) where
+  writer = writerEff pWriter
+  tell = tellEff pWriter
+  listen = listenEff pWriter
+  pass = passEff pWriter
+
+pEither :: Proxy "Either"
+pEither = Proxy
+
+instance (Lookup xs "Either" (Const e)) => MonadError e (Eff xs) where
+  throwError = throwEff pEither
+  catchError = catchEff pEither
+
+-- | A bit dubious
+instance (Monoid e, Lookup xs "Either" (Const e)) => Alternative (Eff xs) where
+  empty = throwError mempty
+  p <|> q = catchError p (const q)
+
+instance (Monoid e, Lookup xs "Either" (Const e)) => MonadPlus (Eff xs) where
+  mzero = empty
+  mplus = (<|>)
+
+pCont :: Proxy "Cont"
+pCont = Proxy
+
+instance MonadCont (Eff ((ContDef r (Eff xs)) ': xs)) where
+  callCC = callCCEff pCont
+
+-- | mtl-compatible reader
+type ReaderDef r = "Reader" >: ReaderEff r
+
+-- | Specialised version of 'runReaderEff' compatible with the 'MonadReader' instance.
+runReaderDef :: Eff (ReaderDef r ': xs) a -> r -> Eff xs a
+runReaderDef = runReaderEff
+{-# INLINE runReaderDef #-}
+
+-- | mtl-compatible state
+type StateDef s = "State" >: State s
+
+-- | 'runStateEff' specialised for the 'MonadState' instance.
+runStateDef :: Eff (StateDef s ': xs) a -> s -> Eff xs (a, s)
+runStateDef = runStateEff
+{-# INLINE runStateDef #-}
+
+-- | 'evalStateEff' specialised for the 'MonadState' instance.
+evalStateDef :: Eff (StateDef s ': xs) a -> s -> Eff xs a
+evalStateDef = evalStateEff
+{-# INLINE evalStateDef #-}
+
+-- | 'execStateEff' specialised for the 'MonadState' instance.
+execStateDef :: Eff (StateDef s ': xs) a -> s -> Eff xs s
+execStateDef = execStateEff
+{-# INLINE execStateDef #-}
+
+-- | mtl-compatible writer
+type WriterDef w = "Writer" >: WriterEff w
+
+-- | 'runWriterDef' specialised for the 'MonadWriter' instance.
+runWriterDef :: Monoid w => Eff (WriterDef w ': xs) a -> Eff xs (a, w)
+runWriterDef = runWriterEff
+{-# INLINE runWriterDef #-}
+
+-- | 'execWriterDef' specialised for the 'MonadWriter' instance.
+execWriterDef :: Monoid w => Eff (WriterDef w ': xs) a -> Eff xs w
+execWriterDef = execWriterEff
+{-# INLINE execWriterDef #-}
+
+-- | Same as @'EitherDef' ()@
+type MaybeDef = "Either" >: EitherEff ()
+
+-- | Similar to 'runMaybeT', but on 'Eff'
+runMaybeDef :: Eff (MaybeDef ': xs) a -> Eff xs (Maybe a)
+runMaybeDef = runMaybeEff
+{-# INLINE runMaybeDef #-}
+
+-- | mtl-compatible either effect
+type EitherDef e = "Either" >: EitherEff e
+
+-- | Similar to 'runExceptT', but on 'Eff'
+runEitherDef :: Eff (EitherDef e ': xs) a -> Eff xs (Either e a)
+runEitherDef = runEitherEff
+{-# INLINE runEitherDef #-}
+
+-- | mtl-compatible continuation
+type ContDef r m = "Cont" >: ContT r m
+
+-- | 'runContEff' specialised for the 'MonadCont' instance.
+runContDef :: Eff (ContDef r (Eff xs) ': xs) a -> (a -> Eff xs r) -> Eff xs r
+runContDef = runContEff
+{-# INLINE runContDef #-}
diff --git a/src/Data/Extensible/Effect/TH.hs b/src/Data/Extensible/Effect/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Effect/TH.hs
@@ -0,0 +1,166 @@
+{-# LANGUAGE Trustworthy, TemplateHaskell, LambdaCase, ViewPatterns #-}
+------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Effect.TH
+-- Copyright   :  (c) Fumiaki Kinoshita 2019
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+--
+------------------------------------------------------------------------
+module Data.Extensible.Effect.TH (decEffects
+  , decEffectSet
+  , decEffectSuite
+  , customDecEffects) where
+
+import Data.Extensible.Effect
+import Data.List (nub)
+import Language.Haskell.TH
+import Data.Char
+import Control.Monad
+import Type.Membership
+
+-- | Generate named effects from a GADT declaration.
+--
+-- @
+-- decEffects [d|
+--  data Blah a b x where
+--    Blah :: Int -> a -> Blah a b b
+--  |]
+-- @
+--
+-- generates
+--
+-- @
+-- type Blah a b = \"Blah\" >: Action '[Int, a] b
+-- blah :: forall xs a b
+--   . Associate \"Blah\" (Action '[Int, a] b) xs
+--   => Int -> a -> Eff xs b
+-- blah a0 a1
+--   = liftEff
+--     (Data.Proxy.Proxy :: Data.Proxy.Proxy \"Blah\")
+--     (AArgument a0 (AArgument a1 AResult))
+-- @
+decEffects :: DecsQ -> DecsQ
+decEffects = customDecEffects False True
+
+-- | Instead of making a type synonym for individual actions, it defines a list
+-- of actions.
+decEffectSet :: DecsQ -> DecsQ
+decEffectSet = customDecEffects True False
+
+-- | Generates type synonyms for the set of actions and also individual actions.
+decEffectSuite :: DecsQ -> DecsQ
+decEffectSuite = customDecEffects True True
+
+-- | Generate effect suite with custom settings.
+customDecEffects :: Bool -- ^ generate a synonym of the set of actions
+    -> Bool -- ^ generate synonyms for individual actions
+    -> DecsQ -> DecsQ
+customDecEffects synSet synActions decs = decs >>= \ds -> fmap concat $ forM ds $ \case
+  DataD _ dataName tparams _ cs _
+    -> do
+      (cxts, dcs) <- fmap unzip $ traverse (con2Eff tparams) cs
+
+      let vars = map PlainTV $ nub $ concatMap (varsT . snd) cxts
+      return $ [TySynD dataName vars (typeListT $ map snd cxts) | synSet]
+          ++ [ TySynD k (map PlainTV $ nub $ varsT t) t | synActions, (k, t) <- cxts]
+          ++ concat dcs
+  _ -> fail "mkEffects accepts GADT declaration"
+
+con2Eff :: [TyVarBndr] -> Con -> Q ((Name, Type), [Dec])
+con2Eff _ (GadtC [name] st (AppT _ resultT))
+  = return $ effectFunD name (map snd st) resultT
+con2Eff tparams (ForallC _ eqs (NormalC name st))
+  = return $ fromMangledGADT tparams eqs name st
+con2Eff tparams (ForallC _ _ c) = con2Eff tparams c
+con2Eff _ p = do
+  runIO (print p)
+  fail "Unsupported constructor"
+
+fromMangledGADT :: [TyVarBndr] -> [Type] -> Name -> [(Strict, Type)] -> ((Name, Type), [Dec])
+fromMangledGADT tyvars_ eqs con fieldTypes
+  = effectFunD con argumentsT result
+  where
+    getTV (PlainTV n) = n
+    getTV (KindedTV n _) = n
+
+    tyvars = map getTV tyvars_
+
+    dic_ = [(v, t) | AppT (AppT EqualityT (VarT v)) t <- eqs]
+    dic = dic_ ++ [(t, VarT v) | (v, VarT t) <- dic_]
+
+    params' = do
+      (t, v) <- zip tyvars uniqueNames
+      case lookup t dic of
+        Just (VarT p) -> return (t, p)
+        _ -> return (t, v)
+
+    argumentsT = map (\case
+      (_, VarT n) -> maybe (VarT n) VarT $ lookup n params'
+      (_, x) -> x) fieldTypes
+
+    result = case lookup (last tyvars) dic of
+      Just (VarT v) -> case lookup v params' of
+        Just p -> VarT p
+        Nothing -> VarT v
+      Just t -> t
+      Nothing -> VarT $ mkName "x"
+
+varsT :: Type -> [Name]
+varsT (VarT v) = [v]
+varsT (AppT s t) = varsT s ++ varsT t
+varsT _ = []
+
+effectFunD :: Name
+  -> [Type]
+  -> Type
+  -> ((Name, Type), [Dec])
+effectFunD key argumentsT resultT = ((key, PromotedT '(:>) `AppT` nameT `AppT` actionT)
+  , [SigD fName typ, FunD fName [effClause nameT (length argumentsT)]]) where
+
+    varList = mkName "xs"
+
+    fName = let (ch : rest) = nameBase key in mkName $ toLower ch : rest
+
+    typ = ForallT (map PlainTV $ varList : varsT resultT ++ concatMap varsT argumentsT)
+        [associateT nameT actionT varList]
+        $ effectFunT varList argumentsT resultT
+
+    -- Action [a, B, C] R
+    actionT = ConT ''Action `AppT` typeListT argumentsT `AppT` resultT
+
+    nameT = LitT $ StrTyLit $ nameBase key
+
+effectFunT :: Name
+  -> [Type]
+  -> Type
+  -> Type
+effectFunT varList argumentsT resultT
+  = foldr (\x y -> ArrowT `AppT` x `AppT` y) rt argumentsT where
+    rt = ConT ''Eff `AppT` VarT varList `AppT` resultT
+
+uniqueNames :: [Name]
+uniqueNames = map mkName $ concatMap (flip replicateM ['a'..'z']) [1..]
+
+typeListT :: [Type] -> Type
+typeListT = foldr (\x y -> PromotedConsT `AppT` x `AppT` y) PromotedNilT
+
+associateT :: Type -- key
+  -> Type -- type
+  -> Name -- variable
+  -> Type
+associateT nameT t xs = ConT ''Lookup `AppT` VarT xs `AppT` nameT `AppT` t
+
+effClause :: Type -- effect key
+  -> Int -- number of arguments
+  -> Clause
+effClause nameT n = Clause (map VarP argNames) (NormalB rhs) [] where
+  -- liftEff (Proxy :: Proxy "Foo")
+  lifter = VarE 'liftEff `AppE` (ConE 'Proxy `SigE` AppT (ConT ''Proxy) nameT)
+
+  argNames = map (mkName . ("a" ++) . show) [0..n-1]
+
+  rhs = lifter `AppE` foldr (\x y -> ConE 'AArgument `AppE` x `AppE` y)
+    (ConE 'AResult)
+    (map VarE argNames)
diff --git a/tests/effects.hs b/tests/effects.hs
new file mode 100644
--- /dev/null
+++ b/tests/effects.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs, DataKinds, FlexibleContexts, TemplateHaskell #-}
+{-# OPTIONS_GHC -ddump-splices #-}
+import Data.Extensible
+
+decEffects [d|
+  data Example a b x where
+    Concrete :: Int -> Example a b ()
+    PolyArg :: a -> Example a b ()
+    PolyRes :: Example a b b
+    PolyArgRes :: a -> Example a b b
+    UnboundArg :: x -> Example a b ()
+    UnboundRes :: Example a b x
+--    ExtArg :: Show s => s -> Example a b ()
+--    ExtRes :: Read s => Example a b s
+  |]
+
+decEffects [d|
+  data Simple x where
+    Simple :: Simple ()
+  |]
+
+main = return ()