diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,15 @@
+0.3.5
+-----------------------------------------------------
+* Added `Data.Extensible.Effect`
+* Added `decEffects`
+
+0.3.4
+-----------------------------------------------------
+* Added `Data.Extensible.Wrapper`
+* Added `itemAt`, `item`, `itemAssoc`
+* Safe Haskell
+* Generalized `Field`
+
 0.3.3
 -----------------------------------------------------
 * Renamed `sectorAt`, `sector`, `sectorAssoc` to `pieceAt`, `piece`, `pieceAssoc`, respectively
diff --git a/examples/effect.hs b/examples/effect.hs
new file mode 100644
--- /dev/null
+++ b/examples/effect.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TemplateHaskell, DataKinds, FlexibleContexts #-}
+import Data.Extensible
+
+decEffects [d|
+  data Example x where
+    Foo :: Int -> Example ()
+    Bar :: Example String
+    Baz :: Bool -> Bool -> Example Int
+    |]
+
+mkField "Foo Bar Baz"
diff --git a/examples/state.hs b/examples/state.hs
new file mode 100644
--- /dev/null
+++ b/examples/state.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeOperators, DataKinds, TemplateHaskell, FlexibleContexts #-}
+import Data.Extensible
+import Control.Lens
+import Control.Monad.State
+
+mkField "foo bar baz"
+
+statefulStuff :: State (Record '["foo" :> Int, "bar" :> Int, "baz" :> Float]) ()
+statefulStuff = do
+    v <- use foo
+    bar += v
+    baz .= 42
+
+main = print $ execState statefulStuff
+  $ foo @= 10 <: bar @= 0 <: baz @= 0 <: Nil
diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.3.4
+version:             0.3.5
 synopsis:            Extensible, efficient, lens-friendly data types
 homepage:            https://github.com/fumieval/extensible
 bug-reports:         http://github.com/fumieval/extensible/issues
@@ -32,6 +32,7 @@
     Data.Extensible.Class
     Data.Extensible.Dictionary
     Data.Extensible.Field
+    Data.Extensible.Effect
     Data.Extensible.Inclusion
     Data.Extensible.Internal
     Data.Extensible.Internal.Rig
@@ -54,7 +55,7 @@
     , FlexibleInstances
     , PolyKinds
     , CPP
-  build-depends:       base >= 4.7 && <5, template-haskell, constraints, profunctors, tagged, transformers
+  build-depends:       base >= 4.7 && <5, template-haskell, constraints, profunctors, tagged, transformers, monad-skeleton
   hs-source-dirs:      src
   ghc-options: -Wall
   default-language:    Haskell2010
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -1,5 +1,4 @@
-{-# LANGUAGE Safe #-}
------------------------------------------------------------------------------
+----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible
 -- Copyright   :  (c) Fumiaki Kinoshita 2015
@@ -14,6 +13,7 @@
 module Data.Extensible (
   module Data.Extensible.Class
   , module Data.Extensible.Dictionary
+  , module Data.Extensible.Effect
   , module Data.Extensible.Field
   , module Data.Extensible.Inclusion
   , module Data.Extensible.Match
@@ -29,6 +29,7 @@
 import Data.Extensible.Class
 import Data.Extensible.Dictionary
 import Data.Extensible.Field
+import Data.Extensible.Effect
 import Data.Extensible.Inclusion
 import Data.Extensible.Match
 import Data.Extensible.Nullable
@@ -38,4 +39,3 @@
 import Data.Extensible.TH
 import Data.Extensible.Union
 import Data.Extensible.Wrapper
-
diff --git a/src/Data/Extensible/Class.hs b/src/Data/Extensible/Class.hs
--- a/src/Data/Extensible/Class.hs
+++ b/src/Data/Extensible/Class.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 -----------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Extensible/Dictionary.hs b/src/Data/Extensible/Dictionary.hs
--- a/src/Data/Extensible/Dictionary.hs
+++ b/src/Data/Extensible/Dictionary.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
 {-# LANGUAGE UndecidableInstances, MultiParamTypeClasses #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
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,64 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
+module Data.Extensible.Effect (Instruction(..)
+  , Eff
+  , liftEff
+  , hoistEff
+  , handleWith
+  , Handler(..)
+  -- * Unnamed actions
+  , Action(..)
+  , Function
+  , receive) where
+
+import Control.Monad.Skeleton
+import Data.Extensible.Field
+import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
+import Data.Extensible.Class
+import Data.Profunctor.Unsafe -- Trustworthy since 7.8
+
+-- | Unnamed action
+data Action (args :: [*]) a r where
+  AResult :: Action '[] a a
+  AArgument :: x -> Action xs a r -> Action (x ': xs) a r
+
+type family Function args r :: * where
+  Function '[] r = r
+  Function (x ': xs) r = x -> Function xs r
+
+-- | Transformation between effects
+newtype Handler f g = Handler { runHandler :: forall a. g a -> f a }
+
+receive :: Functor f => Function xs (f a) -> Handler f (Action xs a)
+receive f0 = Handler (go f0) where
+  go :: Functor f => Function xs (f a) -> Action xs a r -> f r
+  go r AResult = r
+  go f (AArgument x a) = go (f x) a
+
+----------------------------------------------
+
+-- | A unit of effects
+data Instruction (xs :: [Assoc k (* -> *)]) a where
+  Instruction :: !(Membership xs kv) -> AssocValue kv a -> Instruction xs a
+
+-- | The extensible operational monad
+type Eff xs = Skeleton (Instruction xs)
+
+-- | Lift some effect to 'Eff'
+liftEff :: forall proxy s t xs a. Associate s t xs => proxy s -> t a -> Eff xs a
+liftEff _ x = bone (Instruction (association :: Membership xs (s ':> t)) x)
+{-# INLINE liftEff #-}
+
+hoistEff :: forall proxy s t xs a. Associate s t xs => 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 #-}
+
+handleWith :: RecordOf (Handler m) xs -> Eff xs a -> MonadView m (Eff xs) a
+handleWith hs m = case unbone m of
+  Instruction i t :>>= k -> views (pieceAt i) (runHandler .# getField) hs t :>>= k
+  Return a -> Return a
+{-# INLINABLE handleWith #-}
diff --git a/src/Data/Extensible/Field.hs b/src/Data/Extensible/Field.hs
--- a/src/Data/Extensible/Field.hs
+++ b/src/Data/Extensible/Field.hs
@@ -1,8 +1,3 @@
-#if MIN_VERSION_base(4,8,0)
-{-# LANGUAGE Safe #-}
-#else
-{-# LANGUAGE Trustworthy #-}
-#endif
 {-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
 {-# LANGUAGE ScopedTypeVariables, TypeFamilies #-}
 -----------------------------------------------------------------------------
@@ -30,6 +25,9 @@
   , emptyRecord
   , VariantOf
   , Variant
+  -- * Matching
+  , matchWithField
+  , matchField
   -- * Constraint
   , AssocKey
   , AssocValue
@@ -41,6 +39,7 @@
   ) where
 import Data.Extensible.Class
 import Data.Extensible.Sum
+import Data.Extensible.Match
 import Data.Extensible.Product
 import Data.Extensible.Internal
 import Data.Extensible.Internal.Rig
@@ -64,11 +63,11 @@
 --
 -- @'Field' :: (v -> *) -> Assoc k v -> *@
 --
-newtype Field (h :: v -> *) (kv :: Assoc k v) = Field (h (AssocValue kv))
+newtype Field (h :: v -> *) (kv :: Assoc k v) = Field { getField :: h (AssocValue kv) }
 
 instance Wrapper h => Wrapper (Field h) where
   type Repr (Field h) kv = Repr h (AssocValue kv)
-  _Wrapper = dimap (\(Field v) -> v) (fmap Field) . _Wrapper
+  _Wrapper = dimap getField (fmap Field) . _Wrapper
   {-# INLINE _Wrapper #-}
 
 -- | Shows in @field \@= value@ style instead of the derived one.
@@ -100,6 +99,14 @@
 emptyRecord = Nil
 {-# INLINE emptyRecord #-}
 
+matchWithField :: (forall x. f x -> g x -> r) -> RecordOf f xs -> VariantOf g xs -> r
+matchWithField h = matchWith (\(Field x) (Field y) -> h x y)
+{-# INLINE matchWithField #-}
+
+matchField :: RecordOf (Match h r) xs -> VariantOf h xs -> r
+matchField = matchWithField runMatch
+{-# INLINE matchField #-}
+
 -- | @FieldOptic s@ is a type of optics that points a field/constructor named @s@.
 --
 -- The yielding fields can be
@@ -119,18 +126,17 @@
   , Associate k v xs
   , Labelling k p
   , Wrapper h)
-  => p (Repr h v) (f (Repr h v)) -> p (t (Field h) xs) (f (t (Field h) xs))
+  => Optic' p f (t (Field h) xs) (Repr h v)
 
 -- | The trivial inextensible data type
 data Inextensible (h :: k -> *) (xs :: [k])
 
-instance Functor f => Extensible f (LabelPhantom s) Inextensible where
+instance (Functor f, Profunctor p) => Extensible f p Inextensible where
   pieceAt _ _ = error "Impossible"
 
 -- | When you see this type as an argument, it expects a 'FieldLens'.
 -- This type is used to resolve the name of the field internally.
-type FieldName k = forall v. LabelPhantom k () (Proxy ())
-  -> LabelPhantom k (Inextensible (Field Proxy) '[k ':> v]) (Proxy (Inextensible (Field Proxy) '[k ':> v]))
+type FieldName k = Optic' (LabelPhantom k) Proxy (Inextensible (Field Proxy) '[k ':> ()]) ()
 
 type family Labelling s p :: Constraint where
   Labelling s (LabelPhantom t) = s ~ t
diff --git a/src/Data/Extensible/Inclusion.hs b/src/Data/Extensible/Inclusion.hs
--- a/src/Data/Extensible/Inclusion.hs
+++ b/src/Data/Extensible/Inclusion.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 ------------------------------------------------------------------------
diff --git a/src/Data/Extensible/Match.hs b/src/Data/Extensible/Match.hs
--- a/src/Data/Extensible/Match.hs
+++ b/src/Data/Extensible/Match.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
@@ -34,7 +33,7 @@
 
 -- | Applies a function to the result of 'Match'.
 mapMatch :: (a -> b) -> Match h a x -> Match h b x
-mapMatch f (Match g) = Match (f . g)
+mapMatch f = Match #. (f.) .# runMatch
 {-# INLINE mapMatch #-}
 
 -- | /O(log n)/ Perform pattern matching.
diff --git a/src/Data/Extensible/Nullable.hs b/src/Data/Extensible/Nullable.hs
--- a/src/Data/Extensible/Nullable.hs
+++ b/src/Data/Extensible/Nullable.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE LambdaCase, TypeFamilies #-}
 ------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Extensible/Product.hs b/src/Data/Extensible/Product.hs
--- a/src/Data/Extensible/Product.hs
+++ b/src/Data/Extensible/Product.hs
@@ -1,267 +1,267 @@
-{-# LANGUAGE Trustworthy #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Extensible.Product
--- Copyright   :  (c) Fumiaki Kinoshita 2015
--- License     :  BSD3
---
--- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable
---
-------------------------------------------------------------------------
-module Data.Extensible.Product (
-  -- * Basic operations
-  (:*)(..)
-  , (<:)
-  , (<:*)
-  , (*++*)
-  , hhead
-  , htail
-  , huncons
-  , hmap
-  , hmapWithIndex
-  , htrans
-  , hzipWith
-  , hzipWith3
-  , hfoldMap
-  , htraverse
-  , htraverseWithIndex
-  , hsequence
-  , hcollect
-  , hdistribute
-  -- * Lookup
-  , hlookup
-  , hindex
-  , sectorAt
-  , sector
-  -- * Generation
-  , Generate(..)
-  , htabulate
-  , Forall(..)
-  , htabulateFor) where
-
-import Data.Extensible.Internal
-import Data.Extensible.Internal.Rig
-import Unsafe.Coerce
-#if !MIN_VERSION_base(4,8,0)
-import Control.Applicative
-#endif
-import Data.Monoid
-import Data.Typeable (Typeable)
-import Data.Extensible.Class
-import Data.Functor.Identity
-import Data.Extensible.Wrapper
-import Data.Profunctor.Unsafe
-
--- | The type of extensible products.
---
--- @(:*) :: (k -> *) -> [k] -> *@
---
-data (h :: k -> *) :* (s :: [k]) where
-  Nil :: h :* '[]
-  Tree :: !(h x)
-    -> h :* Half xs
-    -> h :* Half (Tail xs)
-    -> h :* (x ': xs)
-
-deriving instance Typeable (:*)
-
--- | /O(1)/ Extract the head element.
-hhead :: h :* (x ': xs) -> h x
-hhead (Tree a _ _) = a
-{-# INLINE hhead #-}
-
--- | /O(log n)/ Extract the tail of the product.
-htail :: h :* (x ': xs) -> h :* xs
-htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
-htail (Tree _ Nil _) = unsafeCoerce Nil
-
--- | Split a product to the head and the tail.
-huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
-huncons t@(Tree a _ _) = (a, htail t)
-{-# INLINE huncons #-}
-
--- | An alias for ('<:').
-(<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs)
-a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $ b <: d) c
-a <:* Nil = Tree a Nil Nil
-infixr 0 <:*
-
--- | /O(log n)/ Add an element to a product.
-(<:) :: h x -> h :* xs -> h :* (x ': xs)
-(<:) = (<:*)
-{-# INLINE (<:) #-}
-infixr 0 <:
-
--- | Transform every elements in a product, preserving the order.
---
--- @
--- 'hmap' 'id' ≡ 'id'
--- 'hmap' (f . g) ≡ 'hmap' f . 'hmap' g
--- @
-hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
-hmap t (Tree h a b) = Tree (t h) (hmap t a) (hmap t b)
-hmap _ Nil = Nil
-
--- | Transform every elements in a product, preserving the order.
-htrans :: (forall x. g x -> h (t x)) -> g :* xs -> h :* Map t xs
-htrans t (Tree h a b) = unsafeCoerce (Tree (t h)) (htrans t a) (htrans t b)
-htrans _ Nil = Nil
-
--- | Combine products.
-(*++*) :: h :* xs -> h :* ys -> h :* (xs ++ ys)
-(*++*) Nil ys = ys
-(*++*) xs'@(Tree x _ _) ys = let xs = htail xs' in x <:* (xs *++* ys)
-infixr 0 *++*
-
--- | 'zipWith' for heterogeneous product
-hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
-hzipWith t (Tree f a b) (Tree g c d) = Tree (t f g) (hzipWith t a c) (hzipWith t b d)
-hzipWith _ Nil _ = Nil
-hzipWith _ _ Nil = Nil
-
--- | 'zipWith3' for heterogeneous product
-hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
-hzipWith3 t (Tree f a b) (Tree g c d) (Tree h e f') = Tree (t f g h) (hzipWith3 t a c e) (hzipWith3 t b d f')
-hzipWith3 _ Nil _ _ = Nil
-hzipWith3 _ _ Nil _ = Nil
-hzipWith3 _ _ _ Nil = Nil
-
--- | Map elements to a monoid and combine the results.
---
--- @'hfoldMap' f . 'hmap' g ≡ 'hfoldMap' (f . g)@
-hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
-hfoldMap f (Tree h a b) = f h <> hfoldMap f a <> hfoldMap f b
-hfoldMap _ Nil = mempty
-
--- | Traverse all elements and combine the result sequentially.
--- @
--- htraverse (fmap f . g) ≡ fmap (hmap f) . htraverse g
--- htraverse pure ≡ pure
--- htraverse (Comp . fmap g . f) ≡ Comp . fmap (htraverse g) . htraverse f
--- @
-htraverse :: Applicative f => (forall x. g x -> f (h x)) -> g :* xs -> f (h :* xs)
-htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b
-htraverse _ Nil = pure Nil
-
--- | 'sequence' analog for extensible products
-hsequence :: Applicative f => Comp f h :* xs -> f (h :* xs)
-hsequence = htraverse getComp
-{-# INLINE hsequence #-}
-
--- | The dual of 'htraverse'
-hcollect :: (Functor f, Generate xs) => (a -> h :* xs) -> f a -> Comp f h :* xs
-hcollect f m = htabulate $ \i -> Comp $ fmap (hlookup i . f) m
-{-# INLINABLE hcollect #-}
-
--- | The dual of 'hsequence'
-hdistribute :: (Functor f, Generate xs) => f (h :* xs) -> Comp f h :* xs
-hdistribute = hcollect id
-{-# INLINE hdistribute #-}
-
--- | /O(log n)/ Pick up an elemtnt.
-hlookup :: Membership xs x -> h :* xs -> h x
-hlookup = view . pieceAt
-{-# INLINABLE hlookup #-}
-
--- | Flipped 'hlookup'
-hindex :: h :* xs -> Membership xs x -> h x
-hindex = flip hlookup
-{-# INLINE hindex #-}
-
--- | 'hmap' with 'Membership's.
-hmapWithIndex :: forall g h xs. (forall x. Membership xs x -> g x -> h x) -> g :* xs -> h :* xs
-hmapWithIndex f = go id where
-  go :: (forall x. Membership t x -> Membership xs x) -> g :* t -> h :* t
-  go k (Tree g a b) = Tree (f (k here) g) (go (k . navL) a) (go (k . navR) b)
-  go _ Nil = Nil
-{-# INLINE hmapWithIndex #-}
-
--- | 'htraverse' with 'Membership's.
-htraverseWithIndex :: forall f g h xs. Applicative f
-  => (forall x. Membership xs x -> g x -> f (h x)) -> g :* xs -> f (h :* xs)
-htraverseWithIndex f = go id where
-  go :: (forall x. Membership t x -> Membership xs x) -> g :* t -> f (h :* t)
-  go k (Tree g a b) = Tree <$> f (k here) g <*> go (k . navL) a <*> go (k . navR) b
-  go _ Nil = pure Nil
-{-# INLINE htraverseWithIndex #-}
-
-instance Functor f => Extensible f (->) (:*) where
-  -- | /O(log n)/ A lens for a value in a known position.
-  pieceAt = pieceAt_
-  {-# INLINE pieceAt #-}
-
-pieceAt_ :: forall (xs :: [k]) (x :: k) (h :: k -> *) (f :: * -> *). Functor f
-  => Membership xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-pieceAt_ i f = flip go i where
-  go :: forall t. h :* t -> Membership t x -> f (h :* t)
-  go (Tree h a b) = navigate
-    (\Here -> fmap (\h' -> Tree h' a b) (f h))
-    (fmap (\a' -> Tree h a' b) . go a)
-    (fmap (\b' -> Tree h a b') . go b)
-  go Nil = error "Impossible"
-{-# INLINE pieceAt_ #-}
-
-{-# DEPRECATED sectorAt "Use pieceAt" #-}
--- | The legacy name for 'pieceAt'
-sectorAt :: Functor f => Membership xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-sectorAt = pieceAt
-
-{-# DEPRECATED sector "Use piece" #-}
--- | The legacy name for 'piece'
-sector :: (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-sector = piece
-
--- | Given a function that maps types to values, we can "collect" entities all you want.
-class Generate (xs :: [k]) where
-  -- | /O(n)/ Generate a product with the given function.
-  hgenerate :: Applicative f => (forall x. Membership xs x -> f (h x)) -> f (h :* xs)
-
-instance Generate '[] where
-  hgenerate _ = pure Nil
-  {-# INLINE hgenerate #-}
-
-instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
-  hgenerate f = Tree <$> f here <*> hgenerate (f . navL) <*> hgenerate (f . navR)
-  {-# INLINE hgenerate #-}
-
--- | Pure version of 'hgenerate'.
---
--- @
--- 'hmap' f ('htabulate' g) ≡ 'htabulate' (f . g)
--- 'htabulate' ('hindex' m) ≡ m
--- 'hindex' ('htabulate' k) ≡ k
--- @
-htabulate :: Generate xs => (forall x. Membership xs x -> h x) -> h :* xs
-htabulate f = runIdentity (hgenerate (Identity #. f))
-{-# INLINE htabulate #-}
-
--- | Guarantees the all elements satisfies the predicate.
-class Forall c (xs :: [k]) where
-  -- | /O(n)/ Analogous to 'hgenerate', but it also supplies a context @c x@ for every elements in @xs@.
-  hgenerateFor :: Applicative f => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (h :* xs)
-
-instance Forall c '[] where
-  hgenerateFor _ _ = pure Nil
-  {-# INLINE hgenerateFor #-}
-
-instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where
-  hgenerateFor proxy f = Tree
-    <$> f here
-    <*> hgenerateFor proxy (f . navL)
-    <*> hgenerateFor proxy (f . navR)
-  {-# INLINE hgenerateFor #-}
-
--- | Pure version of 'hgenerateFor'.
-htabulateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> h :* xs
-htabulateFor p f = runIdentity (hgenerateFor p (Identity #. f))
-{-# INLINE htabulateFor #-}
-
--- | GHC can't prove this
-lemmaHalfTail :: proxy xs -> h :* (x ': Half (Tail xs)) -> h :* (Half (x ': xs))
-lemmaHalfTail _ = unsafeCoerce
-{-# INLINE lemmaHalfTail #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses, UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Product
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.Product (
+  -- * Basic operations
+  (:*)(..)
+  , (<:)
+  , (<:*)
+  , (*++*)
+  , hhead
+  , htail
+  , huncons
+  , hmap
+  , hmapWithIndex
+  , htrans
+  , hzipWith
+  , hzipWith3
+  , hfoldMap
+  , htraverse
+  , htraverseWithIndex
+  , hsequence
+  , hcollect
+  , hdistribute
+  -- * Lookup
+  , hlookup
+  , hindex
+  , sectorAt
+  , sector
+  -- * Generation
+  , Generate(..)
+  , htabulate
+  , Forall(..)
+  , htabulateFor) where
+
+import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig
+import Unsafe.Coerce
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative
+#endif
+import Data.Monoid
+import Data.Typeable (Typeable)
+import Data.Extensible.Class
+import Data.Functor.Identity
+import Data.Extensible.Wrapper
+import Data.Profunctor.Unsafe
+
+-- | The type of extensible products.
+--
+-- @(:*) :: (k -> *) -> [k] -> *@
+--
+data (h :: k -> *) :* (s :: [k]) where
+  Nil :: h :* '[]
+  Tree :: !(h x)
+    -> h :* Half xs
+    -> h :* Half (Tail xs)
+    -> h :* (x ': xs)
+
+deriving instance Typeable (:*)
+
+-- | /O(1)/ Extract the head element.
+hhead :: h :* (x ': xs) -> h x
+hhead (Tree a _ _) = a
+{-# INLINE hhead #-}
+
+-- | /O(log n)/ Extract the tail of the product.
+htail :: h :* (x ': xs) -> h :* xs
+htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
+htail (Tree _ Nil _) = unsafeCoerce Nil
+
+-- | Split a product to the head and the tail.
+huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
+huncons t@(Tree a _ _) = (a, htail t)
+{-# INLINE huncons #-}
+
+-- | An alias for ('<:').
+(<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs)
+a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $ b <: d) c
+a <:* Nil = Tree a Nil Nil
+infixr 0 <:*
+
+-- | /O(log n)/ Add an element to a product.
+(<:) :: h x -> h :* xs -> h :* (x ': xs)
+(<:) = (<:*)
+{-# INLINE (<:) #-}
+infixr 0 <:
+
+-- | Transform every elements in a product, preserving the order.
+--
+-- @
+-- 'hmap' 'id' ≡ 'id'
+-- 'hmap' (f . g) ≡ 'hmap' f . 'hmap' g
+-- @
+hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
+hmap t (Tree h a b) = Tree (t h) (hmap t a) (hmap t b)
+hmap _ Nil = Nil
+
+-- | Transform every elements in a product, preserving the order.
+htrans :: (forall x. g x -> h (t x)) -> g :* xs -> h :* Map t xs
+htrans t (Tree h a b) = unsafeCoerce (Tree (t h)) (htrans t a) (htrans t b)
+htrans _ Nil = Nil
+
+-- | Combine products.
+(*++*) :: h :* xs -> h :* ys -> h :* (xs ++ ys)
+(*++*) Nil ys = ys
+(*++*) xs'@(Tree x _ _) ys = let xs = htail xs' in x <:* (xs *++* ys)
+infixr 0 *++*
+
+-- | 'zipWith' for heterogeneous product
+hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
+hzipWith t (Tree f a b) (Tree g c d) = Tree (t f g) (hzipWith t a c) (hzipWith t b d)
+hzipWith _ Nil _ = Nil
+hzipWith _ _ Nil = Nil
+
+-- | 'zipWith3' for heterogeneous product
+hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
+hzipWith3 t (Tree f a b) (Tree g c d) (Tree h e f') = Tree (t f g h) (hzipWith3 t a c e) (hzipWith3 t b d f')
+hzipWith3 _ Nil _ _ = Nil
+hzipWith3 _ _ Nil _ = Nil
+hzipWith3 _ _ _ Nil = Nil
+
+-- | Map elements to a monoid and combine the results.
+--
+-- @'hfoldMap' f . 'hmap' g ≡ 'hfoldMap' (f . g)@
+hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
+hfoldMap f (Tree h a b) = f h <> hfoldMap f a <> hfoldMap f b
+hfoldMap _ Nil = mempty
+
+-- | Traverse all elements and combine the result sequentially.
+-- @
+-- htraverse (fmap f . g) ≡ fmap (hmap f) . htraverse g
+-- htraverse pure ≡ pure
+-- htraverse (Comp . fmap g . f) ≡ Comp . fmap (htraverse g) . htraverse f
+-- @
+htraverse :: Applicative f => (forall x. g x -> f (h x)) -> g :* xs -> f (h :* xs)
+htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b
+htraverse _ Nil = pure Nil
+
+-- | 'sequence' analog for extensible products
+hsequence :: Applicative f => Comp f h :* xs -> f (h :* xs)
+hsequence = htraverse getComp
+{-# INLINE hsequence #-}
+
+-- | The dual of 'htraverse'
+hcollect :: (Functor f, Generate xs) => (a -> h :* xs) -> f a -> Comp f h :* xs
+hcollect f m = htabulate $ \i -> Comp $ fmap (hlookup i . f) m
+{-# INLINABLE hcollect #-}
+
+-- | The dual of 'hsequence'
+hdistribute :: (Functor f, Generate xs) => f (h :* xs) -> Comp f h :* xs
+hdistribute = hcollect id
+{-# INLINE hdistribute #-}
+
+-- | /O(log n)/ Pick up an elemtnt.
+hlookup :: Membership xs x -> h :* xs -> h x
+hlookup = view . pieceAt
+{-# INLINABLE hlookup #-}
+
+-- | Flipped 'hlookup'
+hindex :: h :* xs -> Membership xs x -> h x
+hindex = flip hlookup
+{-# INLINE hindex #-}
+
+-- | 'hmap' with 'Membership's.
+hmapWithIndex :: forall g h xs. (forall x. Membership xs x -> g x -> h x) -> g :* xs -> h :* xs
+hmapWithIndex f = go id where
+  go :: (forall x. Membership t x -> Membership xs x) -> g :* t -> h :* t
+  go k (Tree g a b) = Tree (f (k here) g) (go (k . navL) a) (go (k . navR) b)
+  go _ Nil = Nil
+{-# INLINE hmapWithIndex #-}
+
+-- | 'htraverse' with 'Membership's.
+htraverseWithIndex :: forall f g h xs. Applicative f
+  => (forall x. Membership xs x -> g x -> f (h x)) -> g :* xs -> f (h :* xs)
+htraverseWithIndex f = go id where
+  go :: (forall x. Membership t x -> Membership xs x) -> g :* t -> f (h :* t)
+  go k (Tree g a b) = Tree <$> f (k here) g <*> go (k . navL) a <*> go (k . navR) b
+  go _ Nil = pure Nil
+{-# INLINE htraverseWithIndex #-}
+
+instance Functor f => Extensible f (->) (:*) where
+  -- | /O(log n)/ A lens for a value in a known position.
+  pieceAt = pieceAt_
+  {-# INLINE pieceAt #-}
+
+pieceAt_ :: forall (xs :: [k]) (x :: k) (h :: k -> *) (f :: * -> *). Functor f
+  => Membership xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+pieceAt_ i f = flip go i where
+  go :: forall t. h :* t -> Membership t x -> f (h :* t)
+  go (Tree h a b) = navigate
+    (\Here -> fmap (\h' -> Tree h' a b) (f h))
+    (fmap (\a' -> Tree h a' b) . go a)
+    (fmap (\b' -> Tree h a b') . go b)
+  go Nil = error "Impossible"
+{-# INLINE pieceAt_ #-}
+
+{-# DEPRECATED sectorAt "Use pieceAt" #-}
+-- | The legacy name for 'pieceAt'
+sectorAt :: Functor f => Membership xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+sectorAt = pieceAt
+
+{-# DEPRECATED sector "Use piece" #-}
+-- | The legacy name for 'piece'
+sector :: (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+sector = piece
+
+-- | Given a function that maps types to values, we can "collect" entities all you want.
+class Generate (xs :: [k]) where
+  -- | /O(n)/ Generate a product with the given function.
+  hgenerate :: Applicative f => (forall x. Membership xs x -> f (h x)) -> f (h :* xs)
+
+instance Generate '[] where
+  hgenerate _ = pure Nil
+  {-# INLINE hgenerate #-}
+
+instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
+  hgenerate f = Tree <$> f here <*> hgenerate (f . navL) <*> hgenerate (f . navR)
+  {-# INLINE hgenerate #-}
+
+-- | Pure version of 'hgenerate'.
+--
+-- @
+-- 'hmap' f ('htabulate' g) ≡ 'htabulate' (f . g)
+-- 'htabulate' ('hindex' m) ≡ m
+-- 'hindex' ('htabulate' k) ≡ k
+-- @
+htabulate :: Generate xs => (forall x. Membership xs x -> h x) -> h :* xs
+htabulate f = runIdentity (hgenerate (Identity #. f))
+{-# INLINE htabulate #-}
+
+-- | Guarantees the all elements satisfies the predicate.
+class Forall c (xs :: [k]) where
+  -- | /O(n)/ Analogous to 'hgenerate', but it also supplies a context @c x@ for every elements in @xs@.
+  hgenerateFor :: Applicative f => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (h :* xs)
+
+instance Forall c '[] where
+  hgenerateFor _ _ = pure Nil
+  {-# INLINE hgenerateFor #-}
+
+instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where
+  hgenerateFor proxy f = Tree
+    <$> f here
+    <*> hgenerateFor proxy (f . navL)
+    <*> hgenerateFor proxy (f . navR)
+  {-# INLINE hgenerateFor #-}
+
+-- | Pure version of 'hgenerateFor'.
+htabulateFor :: Forall c xs => proxy c -> (forall x. c x => Membership xs x -> h x) -> h :* xs
+htabulateFor p f = runIdentity (hgenerateFor p (Identity #. f))
+{-# INLINE htabulateFor #-}
+
+-- | GHC can't prove this
+lemmaHalfTail :: proxy xs -> h :* (x ': Half (Tail xs)) -> h :* (Half (x ': xs))
+lemmaHalfTail _ = unsafeCoerce
+{-# INLINE lemmaHalfTail #-}
diff --git a/src/Data/Extensible/Sum.hs b/src/Data/Extensible/Sum.hs
--- a/src/Data/Extensible/Sum.hs
+++ b/src/Data/Extensible/Sum.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
diff --git a/src/Data/Extensible/TH.hs b/src/Data/Extensible/TH.hs
--- a/src/Data/Extensible/TH.hs
+++ b/src/Data/Extensible/TH.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE Trustworthy, TemplateHaskell #-}
+{-# LANGUAGE Trustworthy, TemplateHaskell, LambdaCase, ViewPatterns #-}
 ------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible.TH
@@ -10,34 +10,42 @@
 -- Portability :  non-portable
 --
 ------------------------------------------------------------------------
-module Data.Extensible.TH (mkField, decFields, decFieldsDeriving) where
+module Data.Extensible.TH (mkField, decFields, decFieldsDeriving, decEffects) where
 
 import Data.Proxy
-import Data.Extensible.Class (Member, Extensible, itemAssoc)
-import Data.Extensible.Field (FieldOptic)
+import Data.Extensible.Internal
+import Data.Extensible.Internal.Rig (Optic')
+import Data.Extensible.Class (Extensible, itemAssoc)
+import Data.Extensible.Effect
+import Data.Extensible.Field
 import Data.Extensible.Plain (accessing)
 import Language.Haskell.TH
-import Control.Monad (forM)
-import Data.Char (toLower)
+import Data.Char
 import Data.Functor.Identity
+import Control.Monad
 
+#if !MIN_VERSION_base(4,8,0)
+import Data.Foldable (foldMap)
+#endif
+
 -- | Generate fields using 'itemAssoc'.
--- @'mkField' "foo bar"@ defines:
+-- @'mkField' "foo Bar"@ defines:
 --
 -- @
 -- foo :: FieldOptic "foo"
 -- foo = itemAssoc (Proxy :: Proxy "foo")
--- bar :: FieldOptic "bar"
--- bar = itemAssoc (Proxy :: Proxy "bar")
+-- _Bar :: FieldOptic "Bar"
+-- _Bar = itemAssoc (Proxy :: Proxy "Bar")
 -- @
 --
 mkField :: String -> DecsQ
-mkField str = fmap concat $ forM (words str) $ \s -> do
+mkField str = fmap concat $ forM (words str) $ \s@(x:xs) -> do
   let st = litT (strTyLit s)
+  let name = mkName $ if isLower x then x : xs else '_' : x : xs
   let lbl = conE 'Proxy `sigE` (conT ''Proxy `appT` st)
-  sequence [sigD (mkName s) $ conT ''FieldOptic `appT` st
-    , valD (varP (mkName s)) (normalB $ varE 'itemAssoc `appE` lbl) []
-    , return $ PragmaD $ InlineP (mkName s) Inline FunLike AllPhases
+  sequence [sigD name $ conT ''FieldOptic `appT` st
+    , valD (varP name) (normalB $ varE 'itemAssoc `appE` lbl) []
+    , return $ PragmaD $ InlineP name Inline FunLike AllPhases
     ]
 
 -- | Generate newtype wrappers and lenses from type synonyms.
@@ -62,30 +70,113 @@
 decFieldsDeriving drv' ds = ds >>= fmap concat . mapM mkBody
   where
     mkBody (NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) drv) = do
-      let name = let (x:xs) = nameBase name_ in mkName (toLower x : xs)
+      let name = let (x:xs) = nameBase name_ in mkName $ toLower x : xs
           xs_ = mkName "xs"
           f_ = mkName "f"
           p_ = mkName "p"
-          q_ = mkName "q"
           t_ = mkName "t"
           ext = varT t_ `appT` conT ''Identity `appT` varT xs_
-          tvs' = PlainTV xs_ : PlainTV f_ : PlainTV p_ : PlainTV q_ : PlainTV t_ : tvs
+          tvs' = PlainTV xs_ : PlainTV f_ : PlainTV p_ : PlainTV t_ : tvs
       sequence [return $ NewtypeD cx name_ tvs (NormalC nc [(st, ty)]) (drv' ++ drv)
 
         ,sigD name
 #if MIN_VERSION_template_haskell(2,10,0)
           $ forallT tvs' (sequence [conT ''Member `appT` varT xs_ `appT` conT name_
-            , conT ''Extensible `appT` varT f_ `appT` varT p_ `appT` varT q_ `appT` varT t_])
+            , conT ''Extensible `appT` varT f_ `appT` varT p_ `appT` varT t_])
 #else
           $ forallT tvs' (sequence [classP ''Member [varT xs_, conT name_]
-            , classP ''Extensible [varT f_, varT p_, varT q_, varT t_]])
+            , classP ''Extensible [varT f_, varT p_, varT t_]])
 #endif
-          $ arrowT
-            `appT` (varT p_ `appT` return ty `appT` (varT f_ `appT` return ty))
-            `appT` (varT q_ `appT` ext `appT` (varT f_ `appT` ext))
+          $ conT ''Optic' `appT` varT p_ `appT` varT f_ `appT` ext `appT` return ty
 
         , valD (varP name) (normalB $ varE 'accessing `appE` conE nc) []
         , return $ PragmaD $ InlineP name Inline FunLike AllPhases
         ]
     mkBody (TySynD name_ tvs ty) = mkBody (NewtypeD [] name_ tvs (NormalC (mkName (nameBase name_)) [(NotStrict, ty)]) [])
     mkBody _ = fail "Unsupported declaration: genField handles newtype declarations or type synonyms"
+
+-- | Generate named effects from a GADT declaration.
+decEffects :: DecsQ -> DecsQ
+decEffects decs = decs >>= \ds -> fmap concat $ forM ds $ \case
+  DataD _ _ (fmap getTV -> tyvars) cs _
+    | not (null tyvars) -> fmap concat $ forM cs $ \case
+      NormalC con st -> mk tyvars [] con st
+      ForallC _ eqs (NormalC con st) -> mk tyvars eqs con st
+      p -> do
+        runIO (print p)
+        fail "Unsupported constructor"
+  _ -> fail "mkEffects accepts GADT declaration"
+  where
+    mk tyvars eqs con (fmap snd -> argTypes) = do
+#if MIN_VERSION_template_haskell(2,10,0)
+      let dic_ = [(v, t) | AppT (AppT EqualityT (VarT v)) t <- eqs]
+#else
+      let dic_ = [(v, t) | EqualP (VarT v) t <- eqs]
+#endif
+      let dic = dic_ ++ [(t, VarT v) | (v, VarT t) <- dic_]
+
+      let tvs = map mkName $ concatMap (flip replicateM ['a'..'z']) [1..]
+
+      let params' = do
+            (t, v) <- zip tyvars tvs
+            case lookup t dic of
+              Just (VarT p) -> return (t, p)
+              _ -> return (t, v)
+
+      let (_, fts) = foldMap (\(p, t) -> maybe ([VarT t], [t]) (\case
+              VarT _ -> ([VarT t], [t])
+              x -> ([x], [])) (lookup p dic)) (init params')
+
+      let argTypes' = map (\case
+            VarT n -> maybe (VarT n) VarT $ lookup n params'
+            x -> x) argTypes
+
+      let (extra, result) = case lookup (last tyvars) dic of
+            Just (VarT v) -> (id, case lookup v params' of
+              Just p -> VarT p
+              Nothing -> VarT v)
+            Just t -> (id, t)
+            Nothing -> ((PlainTV (mkName "x"):), VarT $ mkName "x")
+
+      -- Eff xs R
+      let rt = ConT ''Eff `AppT` VarT (mkName "xs") `AppT` result
+
+      -- a -> B -> C -> Eff xs R
+      let fun = foldr (\x y -> ArrowT `AppT` x `AppT` y) rt argTypes'
+
+      -- Action [a, B, C] R
+      let eff = ConT ''Action
+            `AppT` foldr (\x y -> PromotedConsT `AppT` x `AppT` y) PromotedNilT argTypes'
+            `AppT` result
+
+      -- "Foo"
+      let nameT = LitT $ StrTyLit $ nameBase con
+
+      -- Associate "Foo" (Foo a B C) xs
+#if MIN_VERSION_template_haskell(2,10,0)
+      let cx = ConT ''Associate
+            `AppT` nameT
+            `AppT` eff
+            `AppT` VarT (mkName "xs")
+#else
+      let cx = ClassP ''Associate [nameT, eff, VarT (mkName "xs")]
+#endif
+
+      let typ = ForallT (PlainTV (mkName "xs") : extra (map PlainTV fts)) [cx] fun
+
+      -- liftEff (Proxy :: Proxy "Foo")
+      let lifter = VarE 'liftEff `AppE` (ConE 'Proxy `SigE` AppT (ConT ''Proxy) nameT)
+
+      let argNames = map (mkName . ("a" ++) . show) [0..length argTypes-1]
+
+      let ex = lifter
+            `AppE` foldr (\x y -> ConE 'AArgument `AppE` x `AppE` y)
+                         (ConE 'AResult)
+                         (map VarE argNames)
+
+      let fName = let (ch : rest) = nameBase con in mkName $ toLower ch : rest
+      return [SigD fName typ
+        , FunD fName [Clause (map VarP argNames) (NormalB ex) []]]
+
+    getTV (PlainTV n) = n
+    getTV (KindedTV n _) = n
diff --git a/src/Data/Extensible/Union.hs b/src/Data/Extensible/Union.hs
--- a/src/Data/Extensible/Union.hs
+++ b/src/Data/Extensible/Union.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Extensible/Wrapper.hs b/src/Data/Extensible/Wrapper.hs
--- a/src/Data/Extensible/Wrapper.hs
+++ b/src/Data/Extensible/Wrapper.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE Safe #-}
 {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
 {-# LANGUAGE TypeFamilies #-}
 -----------------------------------------------------------------------------
@@ -25,12 +24,6 @@
 import Data.Profunctor.Unsafe (Profunctor(..))
 import Data.Functor.Identity (Identity(..))
 import Data.Extensible.Internal.Rig (Optic', withIso)
-
-#if !MIN_VERSION_base(4,8,0)
-import Data.Monoid
-import Data.Foldable (Foldable)
-import Data.Traversable (Traversable)
-#endif
 
 -- | The extensible data types should take @k -> *@ as a parameter.
 -- This class allows us to take a shortcut for direct representation.