diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,19 @@
+Copyright Li-yao Xia (c) 2020
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the “Software”), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,74 @@
+# Self-normalizing applicative expressions [![Hackage](https://img.shields.io/hackage/v/ap-normalize.svg)](https://hackage.haskell.org/package/ap-normalize) [![pipeline status](https://gitlab.com/lysxia/ap-normalize/badges/main/pipeline.svg)](https://gitlab.com/lysxia/ap-normalize/-/commits/main)
+
+Normalize applicative expressions
+by simplifying intermediate `pure` and `(<$>)` and reassociating `(<*>)`.
+
+This works by transforming the underlying applicative functor into one whose
+operations (`pure`, `(<$>)`, `(<*>)`) reassociate themselves by inlining
+and beta-reduction.
+
+It relies entirely on GHC's simplifier. No rewrite rules, no Template
+Haskell, no plugins.
+Only Haskell code with two common extensions: `GADTs` and `RankNTypes`.
+
+## Example
+
+In the following traversal, one of the actions is `pure b`, which
+can be simplified in principle, but only assuming the applicative functor
+laws. As far as GHC is concerned, `pure`, `(<$>)`, and `(<*>)` are
+completely opaque because `f` is abstract, so it cannot simplify this
+expression.
+
+```haskell
+data Example a = Example a Bool [a] (Example a)
+
+traverseE :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+traverseE go (Example a b c d) =
+  Example
+    <$> go a
+    <*> pure b
+    <*> traverse go c
+    <*> traverseE go d
+  -- Total: 1 <$>, 3 <*>
+```
+
+Using this library, we can compose actions in a specialized applicative
+functor `Aps f`, keeping the code in roughly the same structure.
+
+```haskell
+traverseE :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+traverseE go (Example a b c d) =
+  Example
+    <$>^ go a
+    <*>  pure b
+    <*>^ traverse go c
+    <*>^ traverseE go d
+    & lowerAps
+  -- Total: 1 <$>, 3 <*>
+```
+
+GHC simplifies that traversal to the following, using only two
+combinators in total.
+
+```haskell
+traverseE :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+traverseE go (Example a b c d) =
+  liftA2 (\a' -> Example a' b)
+    (go a)
+    (traverse go c)
+    <*> traverseE go d
+  -- Total: 1 liftA2, 1 <*>
+```
+
+For more details see the `ApNormalize` module.
+
+## Related links
+
+The same idea can be applied to monoids and monads.
+They are all applications of Cayley's representation theorem.
+
+- [`Endo`][endo] to normalize `(<>)` and `mempty`, in *base*
+- [`Codensity`][codensity] to normalize `pure` and `(>>=)`, in *kan-extensions*
+
+[endo]: https://hackage.haskell.org/package/base-4.14.0.0/docs/Data-Monoid.html#t:Endo
+[codensity]: https://hackage.haskell.org/package/kan-extensions-5.2/docs/Control-Monad-Codensity.html
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/ap-normalize.cabal b/ap-normalize.cabal
new file mode 100644
--- /dev/null
+++ b/ap-normalize.cabal
@@ -0,0 +1,51 @@
+cabal-version: >=1.10
+
+name:    ap-normalize
+version: 0.1.0.0
+synopsis: Self-normalizing applicative expressions
+description:
+  An applicative functor transformer to normalize expressions using @(\<$>)@,
+  @(\<*>)@, and @pure@ into a linear list of actions.
+
+  See "ApNormalize" to get started.
+
+bug-reports: https://gitlab.com/lysxia/ap-normalize/-/issues
+license: MIT
+license-file: LICENSE
+author:       Li-yao Xia
+maintainer:   lysxia@gmail.com
+copyright:    Li-yao Xia 2020
+category:     Control
+build-type:   Simple
+extra-source-files:  README.md
+
+library
+  hs-source-dirs: src
+  exposed-modules:
+    ApNormalize
+    ApNormalize.Aps
+    ApNormalize.DList
+  build-depends:       base >=4.8 && <5
+  ghc-options: -Wall
+  default-language:    Haskell2010
+
+test-suite example-test
+  main-is: example.hs
+  type:    exitcode-stdio-1.0
+  hs-source-dirs:   test
+  default-language: Haskell2010
+  build-depends:
+    base,
+    inspection-testing,
+    ap-normalize
+
+test-suite assoc-test
+  main-is: assoc.hs
+  type:    exitcode-stdio-1.0
+  hs-source-dirs:   test
+  default-language: Haskell2010
+  build-depends:
+    base,
+    inspection-testing,
+    transformers,
+    ap-normalize
diff --git a/src/ApNormalize.hs b/src/ApNormalize.hs
new file mode 100644
--- /dev/null
+++ b/src/ApNormalize.hs
@@ -0,0 +1,122 @@
+-- |
+-- Description: Public interface
+--
+-- = Normalizing applicative functors
+--
+-- Normalize applicative expressions
+-- by simplifying intermediate 'pure' and @('<$>')@ and reassociating @('<*>')@.
+--
+-- This works by transforming the underlying applicative functor into one whose
+-- operations ('pure', @('<$>')@, @('<*>')@) reassociate themselves by inlining
+-- and beta-reduction.
+--
+-- It relies entirely on GHC's simplifier. No rewrite rules, no Template
+-- Haskell, no plugins.
+--
+-- == Example
+--
+-- In the following traversal, one of the actions is @pure b@, which
+-- can be simplified in principle, but only assuming the applicative functor
+-- laws. As far as GHC is concerned, 'pure', @('<$>')@, and @('<*>')@ are
+-- completely opaque because @f@ is abstract, so it cannot simplify this
+-- expression.
+--
+-- @
+-- data Example a = Example a Bool [a] (Example a)
+--
+-- traverseE :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+-- traverseE go (Example a b c d) =
+--   Example
+--     \<$\> go a
+--     \<*\> pure b
+--     \<*\> traverse go c
+--     \<*\> traverseE go d
+--   -- 1 \<$\>, 3 \<*\>
+-- @
+--
+-- Using this library, we can compose actions in a specialized applicative
+-- functor @'Aps' f@, keeping the code in roughly the same structure.
+-- In the following snippet, identifiers exported by the library are highlighted.
+--
+-- @
+-- traverseE :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+-- traverseE go (Example a b c d) =
+--   Example
+--     '<$>^' go a
+--     \<*\>  pure b
+--     '<*>^' traverse go c
+--     '<*>^' traverseE go d
+--     '&' 'lowerAps'
+--   -- 1 \<$\>, 3 \<*\>
+-- @
+--
+-- GHC simplifies that traversal to the following, using only two
+-- combinators in total.
+--
+-- @
+-- traverseE :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+-- traverseE go (Example a b c d) =
+--   liftA2 (\\a' -> Example a' b)
+--     (go a)
+--     (traverse go c)
+--     \<*\> traverseE go d
+--   -- 1 liftA2, 1 \<*\>
+-- @
+--
+-- The following example with a tree-shaped structure also reduces to the same
+-- list-shaped expression above.
+--
+-- @
+-- traverseE :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+-- traverseE go (Example a b c d) =
+--   (\\((a', b'), (c', d')) -> Example a' b' c' d')
+--     \<$\> ((,) \<$\> ((,) '<$>^' go a
+--                       \<*\>  pure b)
+--              \<*\> ((,) '<$>^' traverse go c
+--                       '<*>^' traverseE go d))
+--     '&' 'lowerAps'
+--   -- 4 \<$\>, 3 \<*\>
+-- @
+--
+-- Such structure occurs when using an intermediate definition (which itself
+-- uses the applicative operators) as the right operand of @('<$>')@ or
+-- @('<*>')@.
+-- This could also be found in a naive generic implementation of 'traverse'
+-- using "GHC.Generics".
+--
+-- == Usage
+--
+-- The main idea is to compose applicative actions not directly in your applicative
+-- functor @f@, but in a transformed one @'Aps' f@.
+--
+-- - Send actions from @f@ into @'Aps' f@ using 'liftAps'.
+-- - 'pure' actions lift themselves already:
+--   @pure x@ can be specialized to both @f@ and @Aps f@.
+-- - Compose actions in @'Aps' f@ using applicative combinators such as
+--   @('<$>')@, @('<*>')@, and 'Control.Applicative.liftA2'.
+-- - Move back from @'Aps' f@ to @f@ using 'lowerAps'.
+--
+-- The shorthands @('<$>^')@ and @('<*>^')@ can be used instead of
+-- @('<$>')@ and @('<*>')@ with a neighboring 'liftAps'.
+--
+-- Definitions in @'Aps' f@ should not be recursive,
+-- since this relies on inlining,
+-- and recursive functions are not inlined by GHC.
+
+module ApNormalize
+  ( -- * Interface
+    Aps
+  , (<$>^)
+  , (<*>^)
+  , liftAps
+  , lowerAps
+
+    -- * Reexported from @Data.Function@
+    --
+    -- | For convenience, to append @... '&' 'lowerAps'@ to the
+    -- end of an applicative expression.
+  , (&)
+  ) where
+
+import Data.Function ((&))
+import ApNormalize.Aps
diff --git a/src/ApNormalize/Aps.hs b/src/ApNormalize/Aps.hs
new file mode 100644
--- /dev/null
+++ b/src/ApNormalize/Aps.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE
+  GADTs #-}
+
+-- |
+-- The definition of 'Aps'.
+-- Most of this is reexported by "ApNormalize".
+
+module ApNormalize.Aps
+  ( -- * Normalizing applicative functors
+    Aps(..)
+  , (<$>^)
+  , (<*>^)
+  , liftAps
+  , lowerAps
+  , liftA2Aps
+  , apsToApDList
+  ) where
+
+import Control.Applicative (liftA2, liftA3)
+import ApNormalize.DList
+
+-- | An applicative functor transformer which accumulates @f@-actions (things of type @f x@)
+-- in a normal form.
+--
+-- It constructs a value of type @f a@ with the following syntactic invariant.
+-- It depends on the number of @f@-actions @a1 ... an@ composing it,
+-- which are delimited using 'liftAps':
+--
+-- - Zero action: @pure x@
+-- - One action: @f \<$> a1@
+-- - Two or more actions: @liftA2 f a1 a2 \<*> a3 \<*> ... \<*> an@
+data Aps f a where
+  Pure :: a -> Aps f a
+  FmapLift :: (x -> a) -> f x -> Aps f a
+  LiftA2Aps :: (x -> y -> z -> a) -> f x -> f y -> ApDList f z -> Aps f a
+
+infixl 4 <$>^, <*>^
+
+-- | @f \<$>^ u :: Aps f b@ is a delayed representation of @f \<$> u :: f b@,
+-- so that it can be fused with other applicative operations.
+--
+-- @f \<$>^ u@ is a shorthand for @f \<$> 'liftAps' u@.
+(<$>^) :: (a -> b) -> f a -> Aps f b
+(<$>^) = FmapLift
+{-# INLINE (<$>^) #-}
+
+-- | @u \<*>^ v@ appends an @f@-action @v@ to the right of an @('Aps' f)@-action @u@.
+--
+-- @u \<*>^ v@ is a shorthand for @u \<*> 'liftAps' v@.
+(<*>^) :: Applicative f => Aps f (a -> b) -> f a -> Aps f b
+u <*>^ v = u <*> liftAps v
+{-# INLINE (<*>^) #-}
+
+-- | Lift an @f@-action into @'Aps' f@.
+liftAps :: f a -> Aps f a
+liftAps = FmapLift id
+{-# INLINE liftAps #-}
+
+-- | Lower an @f@-action from @'Aps' f@.
+lowerAps :: Applicative f => Aps f a -> f a
+lowerAps (Pure x) = pure x
+lowerAps (FmapLift f u) = fmap f u
+lowerAps (LiftA2Aps f u v w) =
+   lowerApDList (Yoneda (\k -> liftA2 (\x y -> k (f x y)) u v)) w
+{-# INLINE lowerAps #-}
+
+instance Functor (Aps f) where
+  fmap f (Pure x) = Pure (f x)
+  fmap f (FmapLift g u) = FmapLift (f . g) u
+  fmap f (LiftA2Aps g u v w) = LiftA2Aps ((fmap . fmap . fmap) f g) u v w
+  {-# INLINE fmap #-}
+
+instance Applicative f => Applicative (Aps f) where
+  pure = Pure
+  Pure f <*> uy = fmap f uy
+  FmapLift f ux <*> uy = liftA2Aps f ux uy
+  LiftA2Aps f u v w <*> ww =
+    LiftA2Aps (\x y (z, zz) -> f x y z zz) u v (liftA2 (,) w (apsToApDList ww))
+  {-# INLINE pure #-}
+  {-# INLINE (<*>) #-}
+
+-- | Append an action to the left of an 'Aps'.
+liftA2Aps :: Applicative f => (a -> b -> c) -> f a -> Aps f b -> Aps f c
+liftA2Aps f ux (Pure y) = FmapLift (\x -> f x y) ux
+liftA2Aps f ux (FmapLift g uy) = LiftA2Aps (\x y _ -> f x (g y)) ux uy (pure ())
+liftA2Aps f ux (LiftA2Aps g u v w) =
+  LiftA2Aps (\x y (z, zz) -> f x (g y z zz)) ux u (liftA2 (,) (liftApDList v) w)
+{-# INLINE liftA2Aps #-}
+
+-- | Conversion from 'Aps' to 'ApDList'.
+apsToApDList :: Applicative f => Aps f a -> ApDList f a
+apsToApDList (Pure x) = pure x
+apsToApDList (FmapLift f u) = fmap f (liftApDList u)
+apsToApDList (LiftA2Aps f u v w) = liftA3 f (liftApDList u) (liftApDList v) w
+{-# INLINE apsToApDList #-}
diff --git a/src/ApNormalize/DList.hs b/src/ApNormalize/DList.hs
new file mode 100644
--- /dev/null
+++ b/src/ApNormalize/DList.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE
+  RankNTypes #-}
+
+-- | This structure is part of the definition of 'ApNormalize.Aps'.
+
+module ApNormalize.DList
+  ( -- * Applicative difference lists
+    ApDList(..)
+  , liftApDList
+  , lowerApDList
+  , Yoneda(..)
+  ) where
+
+-- | Type of applicative difference lists.
+--
+-- An applicative transformer which accumulates @f@-actions in
+-- a left-nested composition using @('<*>')@.
+--
+-- 'ApDList' represents a sequence of @f@-actions
+-- @u1 :: f x1@, ... @un :: f xn@ as "term with a hole"
+-- @(_ \<*> u1 \<*> ... \<*> un) :: f r@.
+--
+-- That hole must have type  @_ :: f (x1 -> ... -> un -> r)@;
+-- the variable number of arrows is hidden by existential quantification
+-- and continuation passing.
+--
+-- To help ensure that syntactic invariant,
+-- the 'Functor' and 'Applicative' instances for 'ApDList' have no constraints.
+-- 'liftApDList' is the only function whose signature requires an
+-- @'Applicative' f@ constraint, wrapping each action @u@ inside one @('<*>')@.
+newtype ApDList f a = ApDList (forall r. Yoneda f (a -> r) -> f r)
+
+-- | A difference list with one element @u@, denoted @_ \<*> u@.
+liftApDList :: Applicative f => f a -> ApDList f a
+liftApDList u = ApDList (\(Yoneda t) -> t id <*> u)
+{-# INLINE liftApDList #-}
+
+-- | Complete a difference list, filling the hole with the first argument.
+lowerApDList :: Yoneda f (b -> c) -> ApDList f b -> f c
+lowerApDList u (ApDList v) = v u
+{-# INLINE lowerApDList #-}
+
+instance Functor (ApDList f) where
+  fmap f (ApDList u) = ApDList (\t -> u (fmap (. f) t))
+  {-# INLINE fmap #-}
+
+instance Applicative (ApDList f) where
+  pure x = ApDList (\(Yoneda t) -> t (\k -> k x))
+  ApDList uf <*> ApDList ux = ApDList (\t -> ux (Yoneda (\c -> uf (fmap (\d e -> c (d . e)) t))))
+  {-# INLINE pure #-}
+  {-# INLINE (<*>) #-}
+
+-- | A delayed application of 'fmap' which can be fused with an inner 'fmap' or
+-- 'Control.Applicative.liftA2'.
+--
+-- This is the same definition as in the kan-extensions library, but we
+-- redefine it to not pay for all the dependencies.
+newtype Yoneda f a = Yoneda (forall x. (a -> x) -> f x)
+
+instance Functor (Yoneda f) where
+  fmap f (Yoneda u) = Yoneda (\g -> u (g . f))
diff --git a/test/assoc.hs b/test/assoc.hs
new file mode 100644
--- /dev/null
+++ b/test/assoc.hs
@@ -0,0 +1,85 @@
+{-# OPTIONS_GHC -dsuppress-all #-}
+{-# LANGUAGE CPP, TemplateHaskell #-}
+
+-- This module tests the "definitional associativity" of applicative functors
+-- from:
+-- - ap-normalize
+-- - base
+-- - transformers
+--
+-- An operation (here (<*>)) is definitionally associative if it is
+-- associative only by unfolding its definition and by simplification
+-- (beta-reduction, and sometimes eta-conversion for data types, to commute
+-- "case" expressions).
+
+import Control.Applicative (liftA2, ZipList)
+import Data.Monoid (Endo)
+
+import Control.Monad.ST (ST)
+import Data.Functor.Product (Product)
+import GHC.Conc (STM)
+
+import Control.Monad.Trans.Accum (Accum)
+import Control.Monad.Trans.Cont (ContT)
+import qualified Control.Monad.Trans.State.Lazy as Lazy
+import qualified Control.Monad.Trans.State.Strict as Strict
+import Control.Monad.Trans.RWS (RWS)
+import Control.Monad.Trans.Reader (Reader)
+import Control.Monad.Trans.Select (Select)
+import Control.Monad.Trans.Writer (Writer)
+
+import Test.Inspection
+
+import ApNormalize (Aps)
+import ApNormalize.DList (ApDList)
+
+assoc1, assoc2 :: Applicative f => f a -> f b -> f c -> f (a, b, c)
+assoc1 x y z = liftA2 (,,) x y <*> z
+assoc2 x y z = liftA2 (\x (y, z) -> (x, y, z)) x (liftA2 (,) y z)
+
+#define TEST_ASSOC_(NAME,M,FFF,CSTR) \
+assoc1'NAME, assoc2'NAME :: CSTR M a -> M b -> M c -> M (a, b, c) ; \
+assoc1'NAME = assoc1 ; \
+assoc2'NAME = assoc2 ; \
+inspect $ 'assoc1'NAME FFF 'assoc2'NAME
+
+#define TEST_ASSOC(NAME,M,FFF) TEST_ASSOC_(NAME,M,FFF,)
+
+
+-- Aps is actually not definitionally associative (it needs to know
+-- that computations were wrapped with 'liftAps' to do its work).
+TEST_ASSOC_(Aps,Aps f,=/=,Applicative f =>)
+
+-- Applicative difference lists are definitionally associative.
+TEST_ASSOC(ApDList,ApDList f,==-)
+
+
+-- Most of the fully concrete monads are definitionally associative.
+-- Unlike monad transformers with an abstract monad.
+TEST_ASSOC(IO,IO,===)
+TEST_ASSOC(ST,ST s,===)
+TEST_ASSOC(STM,STM,===)
+TEST_ASSOC(Maybe,Maybe,===)
+TEST_ASSOC(ProductMaybe,Product Maybe Maybe,===)
+TEST_ASSOC(Either,Either e,===)
+TEST_ASSOC(Reader,Reader r,===)
+TEST_ASSOC(State,Lazy.State s,==-)
+TEST_ASSOC(SState,Strict.State s,==-)
+TEST_ASSOC(Cont,ContT r m,===)
+
+-- Writer-like monads are only definitionally associative when the
+-- monoid is also definitionally associative.
+TEST_ASSOC(AccumEndo,Accum (Endo w),===)
+TEST_ASSOC(WriterEndo,Writer (Endo w),===)
+TEST_ASSOC(RWSEndo,RWS r (Endo w) s,==-)
+TEST_ASSOC_(Accum,Accum w,=/=,Monoid w =>)
+TEST_ASSOC_(Writer,Writer w,=/=,Monoid w =>)
+TEST_ASSOC_(RWS,RWS r w s,=/=,Monoid w =>)
+
+-- These are NOT definitionally associative
+TEST_ASSOC(List,[],=/=)
+TEST_ASSOC(ZipList,ZipList,=/=)
+TEST_ASSOC(Select,Select r,=/=)
+
+main :: IO ()
+main = pure ()
diff --git a/test/example.hs b/test/example.hs
new file mode 100644
--- /dev/null
+++ b/test/example.hs
@@ -0,0 +1,55 @@
+{-# OPTIONS_GHC -dsuppress-all #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+-- Testing example from the documentation
+
+import Control.Applicative (liftA2)
+import Test.Inspection
+import ApNormalize
+
+data Example a = Example a Bool [a] (Example a)
+
+traverseNaive :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+traverseNaive go (Example a b c d) =
+  Example
+    <$> go a
+    <*> pure b
+    <*> traverse go c
+    <*> traverseNaive go d
+  -- Total: 1 <$>, 3 <*>
+
+traverseAN :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+traverseAN go (Example a b c d) =
+  Example
+    <$>^ go a
+    <*>  pure b
+    <*>^ traverse go c
+    <*>^ traverseAN go d
+    & lowerAps
+  -- Total: 1 <$>, 3 <*>
+
+traverseNormal :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+traverseNormal go (Example a b c d) =
+  liftA2 (\a' -> Example a' b)
+    (go a)
+    (traverse go c)
+    <*> traverseNormal go d
+  -- Total: 1 liftA2, 1 <*>
+
+traverseTree :: Applicative f => (a -> f b) -> Example a -> f (Example b)
+traverseTree go (Example a b c d) =
+  (\((a', b'), (c', d')) -> Example a' b' c' d')
+    <$> ((,) <$> ((,) <$>^ go a
+                      <*>  pure b)
+             <*> ((,) <$>^ traverse go c
+                      <*>^ traverseTree go d))
+    & lowerAps
+  -- 4 \<$\>, 3 \<*\>
+
+inspect $ 'traverseNormal =/= 'traverseNaive
+inspect $ 'traverseNormal === 'traverseAN
+inspect $ 'traverseNormal === 'traverseTree
+
+-- dummy
+main :: IO ()
+main = pure ()