diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,12 @@
 # Change log
 
+## 0.3
+
+* Add freer rigid selective functors: `Control.Selective.Rigid.Freer`.
+* Rename `Control.Selective.Free.Rigid` to `Control.Selective.Rigid.Free`.
+* Add free selective functors: `Control.Selective.Free`.
+* Switch to more conventional field names in `SelectA` and `SelectM`.
+
 ## 0.2
 
 * Make compatible with GHC >= 8.0.2.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -61,7 +61,7 @@
 
 ```haskell
 apS :: Selective f => f (a -> b) -> f a -> f b
-apS f x = select (Left <$> f) (flip ($) <$> x)
+apS f x = select (Left <$> f) ((&) <$> x)
 ```
 
 Here we wrap a given function `a -> b` into `Left` and turn the value `a`
@@ -133,7 +133,7 @@
 Instances of the `Selective` type class must satisfy a few laws to make
 it possible to refactor selective computations. These laws also allow us
 to establish a formal relation with the `Applicative` and `Monad` type
-classes. 
+classes.
 
 * Identity:
     ```haskell
@@ -171,7 +171,7 @@
 
 * Apply a pure function to the second argument:
     ```haskell
-    select x (f <$> y) = select (first (flip f) <$> x) (flip ($) <$> y)
+    select x (f <$> y) = select (first (flip f) <$> x) ((&) <$> y)
     ```
 
 * Generalised identity:
@@ -205,7 +205,7 @@
 analysis using instances like `Under` and `Over`.
 
 If `f` is also a `Monad`, we require that `select = selectM`, from which one
-can prove `apS = <*>`, and furthermore the above `Pure-Left` and `Pure-Right` 
+can prove `apS = <*>`, and furthermore the above `Pure-Left` and `Pure-Right`
 properties now hold.
 
 ## Static analysis of selective functors
diff --git a/examples/Build.hs b/examples/Build.hs
--- a/examples/Build.hs
+++ b/examples/Build.hs
@@ -2,7 +2,7 @@
 module Build where
 
 import Control.Selective
-import Control.Selective.Free.Rigid
+import Control.Selective.Rigid.Free
 
 -- See Section 3 of the paper:
 -- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf
@@ -105,7 +105,9 @@
 -- | Analyse a build task via free selective functors.
 --
 -- @
--- runBuild (fromJust $ cyclic "B1") == [Fetch "C1" (const ()),Fetch "B2",Fetch "A2"]
+-- runBuild (fromJust $ cyclic "B1") == [ Fetch "C1" (const ())
+--                                      , Fetch "B2" (const ())
+--                                      , Fetch "A2" (const ()) ]
 -- @
 runBuild :: Task k v -> [Fetch k v ()]
 runBuild task = getEffects (run task fetch)
diff --git a/examples/Processor.hs b/examples/Processor.hs
--- a/examples/Processor.hs
+++ b/examples/Processor.hs
@@ -1,10 +1,10 @@
-{-# LANGUAGE ConstraintKinds, DeriveFunctor
-             , LambdaCase, FlexibleContexts, FlexibleInstances, GADTs #-}
+{-# LANGUAGE ConstraintKinds, DeriveFunctor, GADTs, FlexibleContexts, LambdaCase #-}
 module Processor where
 
 import Control.Selective
-import Control.Selective.Free.Rigid
+import Control.Selective.Rigid.Free
 import Data.Functor
+import Data.Bool
 import Data.Int (Int16)
 import Data.Word (Word8)
 import Data.Map.Strict (Map)
@@ -33,16 +33,10 @@
 type Value = Int16
 
 -- | The processor has four registers.
-data Reg = R0 | R1 | R2 | R3 deriving (Show, Eq, Ord)
-
-r0, r1, r2, r3 :: Key
-r0 = Reg R0
-r1 = Reg R1
-r2 = Reg R2
-r3 = Reg R3
+data Register = R0 | R1 | R2 | R3 deriving (Show, Eq, Ord)
 
 -- | The register bank maps registers to values.
-type RegisterBank = Map Reg Value
+type RegisterBank = Map Register Value
 
 -- | The address space is indexed by one byte.
 type Address = Word8
@@ -56,7 +50,7 @@
     deriving (Show, Eq, Ord)
 
 -- | A flag assignment.
-type Flags = Map.Map Flag Value
+type Flags = Map Flag Value
 
 -- | Address in the program memory.
 type InstructionAddress = Value
@@ -78,7 +72,7 @@
                    , log       :: Log Key Value}
 
 -- | Various elements of the processor state.
-data Key = Reg Reg | Cell Address | Flag Flag | PC deriving Eq
+data Key = Reg Register | Cell Address | Flag Flag | PC deriving Eq
 
 instance Show Key where
     show (Reg r)  = show r
@@ -100,8 +94,7 @@
     show (Write k _        _) = "Write " ++ show k
 
 logEntry :: MonadState State m => LogEntry Key Value -> m ()
-logEntry item = S.modify $ \s ->
-    s {log = log s ++ [item] }
+logEntry item = S.modify $ \s -> s { log = log s ++ [item] }
 
 -- | Interpret the base functor in a 'MonadState'.
 toState :: MonadState State m => RW a -> m a
@@ -147,51 +140,31 @@
 write :: Key -> Program Value -> Program Value
 write k fv = liftSelect (Write k fv id)
 
--- --------------------------------------------------------------------------------
--- -------- Instructions ----------------------------------------------------------
--- --------------------------------------------------------------------------------
-
-------------
--- Add -----
-------------
-
--- | Read the values @x@ and @y@ and write the sum into @z@. If the sum is zero,
--- set the 'Zero' flag, otherwise reset it.
---
--- This implementation looks intuitive, but is incorrect, since the two write
--- operations are independent and the effects required for computing the sum,
--- i.e. @read x <*> read y@ will be executed twice. Consequently:
---   * the value written into @z@ is not guaranteed to be the same as the one
---     which was compared to zero,
---   * the static analysis of the computations would report more dependencies
---     than one might expect.
-addNaive :: Key -> Key -> Key -> Program Value
-addNaive x y z =
-    let sum    = (+)   <$> read x <*> read y
-        isZero = (==0) <$> sum
-    in write (Flag Zero) (ifS isZero (pure 1) (pure 0)) *> write z sum
+--------------------------------------------------------------------------------
+-------- Instructions ----------------------------------------------------------
+--------------------------------------------------------------------------------
 
--- | This implementation of addition executes the effects associated with 'sum'
--- only once and then reuses it without triggering the effects again.
-add :: Key -> Key -> Key -> Program Value
-add x y z =
-    let sum    = (+)   <$> read x <*> read y
-        isZero = (==0) <$> write z sum
-    in write (Flag Zero) (fromBool <$> isZero)
+-- | The addition instruction, which reads the summands from a 'Register' and a
+-- memory 'Address', adds them, writes the result back into the same register,
+-- and also updates the state of the 'Zero' flag to indicate whether the
+-- resulting 'Value' is zero.
+add :: Register -> Address -> Program Value
+add reg addr = let arg1   = read (Reg reg)
+                   arg2   = read (Cell addr)
+                   result = (+)   <$> arg1 <*> arg2
+                   isZero = (==0) <$> write (Reg reg) result
+               in write (Flag Zero) (bool 0 1 <$> isZero)
 
------------------
--- jumpZero -----
------------------
+-- | A conditional branching instruction that performs a jump if the result of
+-- the previous operation was zero.
 jumpZero :: Value -> Program ()
-jumpZero offset =
-    let pc       = read PC
-        zeroSet  = (==1) <$> read (Flag Zero)
-        modifyPC = void $ write PC ((+offset) <$> pc)
-    in whenS zeroSet modifyPC
+jumpZero offset = let zeroSet  = (==1) <$> read (Flag Zero)
+                      modifyPC = void $ write PC ((+offset) <$> read PC)
+                  in whenS zeroSet modifyPC
 
--- A block of instructions.
+-- | A simple block of instructions.
 addAndJump :: Program ()
-addAndJump = add (Reg R1) (Reg R2) (Reg R3) *> jumpZero 42
+addAndJump = add R0 1 *> jumpZero 42
 
 -----------------------------------
 -- Add with overflow tracking -----
@@ -242,9 +215,6 @@
 -- overflow detection, lift all the pure operations into 'Applicative'. This
 -- forces the semantics to read the input variables more times than
 -- 'addOverflow' does (@x@ is read 3x times, and @y@ is read 5x times).
---
--- It is not clear at the moment what to do with this. Should we just avoid this
--- style? Or could it sometimes be useful?
 addOverflowNaive :: Key -> Key -> Key -> Program Value
 addOverflowNaive x y z =
     let arg1   = read x
@@ -294,13 +264,10 @@
                  , pc = 0
                  , flags = emptyFlags
                  , memory = mem
-                 , log   = []
-                 }
+                 , log   = [] }
 
 twoAdds :: Program Value
-twoAdds = add r0 (Cell 0) r0
-          *>
-          add r0 (Cell 0) r0
+twoAdds = add R0 0 *> add R0 0
 
 addExample :: IO ()
 addExample = do
diff --git a/examples/Query.hs b/examples/Query.hs
new file mode 100644
--- /dev/null
+++ b/examples/Query.hs
@@ -0,0 +1,71 @@
+{-# LANGUAGE GADTs #-}
+module Query where
+
+import Control.Selective
+import Data.List
+
+type Prompt = String
+
+data Query a where
+    Terminal :: Prompt   -> Query String
+    File     :: FilePath -> Query String
+    Pure     :: a -> Query a
+    Apply    :: Query (a -> b) -> Query a -> Query b
+    Select   :: Query (Either a b) -> Query (a -> b) -> Query b
+
+instance Functor Query where
+    fmap f x = Apply (Pure f) x
+
+instance Applicative Query where
+    pure  = Pure
+    (<*>) = Apply
+
+instance Selective Query where
+    select = Select
+
+pureQuery :: Query String
+pureQuery = (++) <$> pure "Hello " <*> pure "World!"
+
+replace :: String -> String -> String -> String
+replace [] _ xs = xs
+replace from to xs | Just xs <- stripPrefix from xs = to ++ replace from to xs
+replace from to (x:xs) = x : replace from to xs
+replace _ _ [] = []
+
+welcomeQuery :: Query String
+welcomeQuery = replace "[NAME]" <$> Terminal "Name" <*> File "welcome.txt"
+
+welcomeBackQuery :: Query String
+welcomeBackQuery = (++) <$> welcomeQuery <*> pure "It's great to have you back!\n"
+
+welcomeQuery2 :: Query String
+welcomeQuery2 =
+    ifS (isInfixOf <$> Terminal "Name" <*> File "past-participants.txt")
+        welcomeBackQuery
+        welcomeQuery
+
+getPure :: Query a -> Maybe a
+getPure (Terminal _) = Nothing
+getPure (File _) = Nothing
+getPure (Pure a) = Just a
+getPure (Apply f x) = do
+    pf <- getPure f
+    px <- getPure x
+    return (pf px)
+getPure (Select x y) = do
+    px <- getPure x
+    py <- getPure y
+    return (either py id px)
+
+getEffects :: Query a -> ([Prompt], [FilePath])
+getEffects (Terminal p) = ([p], [] )
+getEffects (File f) = ([] , [f])
+getEffects (Pure _) = ([] , [] )
+getEffects (Apply f x) = (p1 ++ p2, f1 ++ f2)
+  where
+    (p1, f1) = getEffects f
+    (p2, f2) = getEffects x
+getEffects (Select x y) = (px ++ py, fx ++ fy)
+  where
+    (px, fx) = getEffects x
+    (py, fy) = getEffects y
diff --git a/examples/Teletype.hs b/examples/Teletype.hs
--- a/examples/Teletype.hs
+++ b/examples/Teletype.hs
@@ -4,7 +4,7 @@
 import Prelude hiding (getLine, putStrLn)
 import qualified Prelude as IO
 import Control.Selective
-import Control.Selective.Free.Rigid
+import Control.Selective.Free
 
 -- See Section 5.2 of the paper:
 -- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf
@@ -38,7 +38,9 @@
 putStrLn :: String -> Teletype ()
 putStrLn s = liftSelect (Write s ())
 
--- | The example from the paper's intro implemented using the free selective.
+-- | The ping-pong example from the introduction section of the paper
+-- implemented using free selective functors.
+--
 -- It can be statically analysed for effects:
 --
 -- @
@@ -46,6 +48,11 @@
 -- [Read,Write "pong"]
 -- @
 --
+-- @
+-- > getNecessaryEffects pingPongS
+-- [Read]
+-- @
+--
 -- If can also be executed in IO:
 --
 -- @
@@ -59,11 +66,13 @@
 pingPongS = whenS (fmap ("ping"==) getLine) (putStrLn "pong")
 
 ------------------------------- Ping-pong example ------------------------------
--- | Monadic ping-pong. Can be executed, but cannot be statically analysed.
+-- | Monadic ping-pong, which has the desired behaviour, but cannot be
+-- statically analysed.
 pingPongM :: IO ()
 pingPongM = IO.getLine >>= \s -> if s == "ping" then IO.putStrLn "pong" else pure ()
 
--- | Applicative ping-pong. Cannot be executed, but can be statically analysed.
+-- | Applicative ping-pong, which always executes both effect, but can be
+-- statically analysed.
 pingPongA :: IO ()
 pingPongA = fmap (\_ -> id) IO.getLine <*> IO.putStrLn "pong"
 
diff --git a/examples/Teletype/Rigid.hs b/examples/Teletype/Rigid.hs
new file mode 100644
--- /dev/null
+++ b/examples/Teletype/Rigid.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE DeriveFunctor, FlexibleInstances, GADTs #-}
+module Teletype.Rigid where
+
+import Prelude hiding (getLine, putStrLn)
+import qualified Prelude as IO
+import Control.Selective
+import Control.Selective.Rigid.Free
+
+-- See Section 5.2 of the paper:
+-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf
+
+-- | The classic @Teletype@ base functor.
+data TeletypeF a = Read (String -> a) | Write String a deriving Functor
+
+instance Eq (TeletypeF ()) where
+    Read  _    == Read  _    = True
+    Write x () == Write y () = (x == y)
+    _ == _ = False
+
+instance Show (TeletypeF a) where
+    show (Read _)    = "Read"
+    show (Write s _) = "Write " ++ show s
+
+-- | Interpret 'TeletypeF' commands as 'IO' actions.
+toIO :: TeletypeF a -> IO a
+toIO (Read f)    = f <$> IO.getLine
+toIO (Write s a) = a <$  IO.putStrLn s
+
+-- | A Teletype program is a free selective functor on top of the base functor
+-- 'TeletypeF'.
+type Teletype a = Select TeletypeF a
+
+-- | A convenient alias for reading a string.
+getLine :: Teletype String
+getLine = liftSelect (Read id)
+
+-- | A convenient alias for writing a string.
+putStrLn :: String -> Teletype ()
+putStrLn s = liftSelect (Write s ())
+
+-- | The ping-pong example from the introduction section of the paper
+-- implemented using free selective functors.
+--
+-- @
+-- > getEffects pingPongS
+-- [Read,Write "pong"]
+-- @
+--
+-- If can also be executed in IO:
+--
+-- @
+-- > runSelect toIO pingPongS
+-- hello
+-- > runSelect toIO pingPongS
+-- ping
+-- pong
+-- @
+pingPongS :: Teletype ()
+pingPongS = whenS (fmap ("ping"==) getLine) (putStrLn "pong")
+
+------------------------------- Ping-pong example ------------------------------
+-- | Monadic ping-pong, which has the desired behaviour, but cannot be
+-- statically analysed.
+pingPongM :: IO ()
+pingPongM = IO.getLine >>= \s -> if s == "ping" then IO.putStrLn "pong" else pure ()
+
+-- | Applicative ping-pong, which always executes both effect, but can be
+-- statically analysed.
+pingPongA :: IO ()
+pingPongA = fmap (\_ -> id) IO.getLine <*> IO.putStrLn "pong"
+
+-- | A monadic greeting. Cannot be implemented using selective functors.
+greeting :: IO ()
+greeting = IO.getLine >>= \name -> IO.putStrLn ("Hello, " ++ name)
diff --git a/selective.cabal b/selective.cabal
--- a/selective.cabal
+++ b/selective.cabal
@@ -1,5 +1,5 @@
 name:          selective
-version:       0.2
+version:       0.3
 synopsis:      Selective applicative functors
 license:       MIT
 license-file:  LICENSE
@@ -36,7 +36,8 @@
     hs-source-dirs:     src
     exposed-modules:    Control.Selective,
                         Control.Selective.Free,
-                        Control.Selective.Free.Rigid
+                        Control.Selective.Rigid.Free,
+                        Control.Selective.Rigid.Freer
     build-depends:      base         >= 4.7     && < 5,
                         containers   >= 0.5.5.1 && < 0.7,
                         transformers >= 0.4.2.0 && < 0.6
@@ -62,8 +63,10 @@
                         Laws,
                         Parser,
                         Processor,
+                        Query,
                         Sketch,
                         Teletype,
+                        Teletype.Rigid,
                         Validation
     type:               exitcode-stdio-1.0
     main-is:            Main.hs
@@ -74,7 +77,8 @@
                         selective,
                         tasty                  >= 0.11,
                         tasty-expected-failure >= 0.11,
-                        tasty-quickcheck       >= 0.8.4
+                        tasty-quickcheck       >= 0.8.4,
+                        transformers           >= 0.4.2.0 && < 0.6
     default-language:   Haskell2010
     GHC-options:        -Wall
                         -fno-warn-name-shadowing
diff --git a/src/Control/Selective.hs b/src/Control/Selective.hs
--- a/src/Control/Selective.hs
+++ b/src/Control/Selective.hs
@@ -1,5 +1,4 @@
-{-# LANGUAGE CPP, TupleSections, DeriveFunctor #-}
-{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE CPP, TupleSections, DeriveFunctor, GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module     : Control.Selective
@@ -39,6 +38,7 @@
 import Control.Monad.Trans.State
 import Control.Monad.Trans.Writer
 import Data.Bool
+import Data.Function
 import Data.Functor.Compose
 import Data.Functor.Identity
 import Data.Functor.Product
@@ -52,9 +52,9 @@
 import qualified Control.Monad.Trans.Writer.Strict as S
 
 -- | Selective applicative functors. You can think of 'select' as a selective
--- function application: when given a value of type @Left a@, you __must apply__
--- the given function, but when given a @Right b@, you __may skip__ the function
--- and associated effects, and simply return the @b@.
+-- function application: when given a value of type 'Left' @a@, you __must apply__
+-- the given function, but when given a 'Right' @b@, you __may skip__ the
+-- function and associated effects, and simply return the @b@.
 --
 -- Note that it is not a requirement for selective functors to skip unnecessary
 -- effects. It may be counterintuitive, but this makes them more useful. Why?
@@ -92,7 +92,7 @@
 --     h z = uncurry z
 -- @
 --
--- * Monadic @select@ (for selective functors that are also monads):
+-- * Monadic 'select' (for selective functors that are also monads):
 --
 -- @
 -- select = selectM
@@ -115,7 +115,7 @@
 -- * Apply a pure function to the second argument:
 --
 -- @
--- select x (f \<$\> y) = select (first (flip f) \<$\> x) (flip ($) \<$\> y)
+-- select x (f \<$\> y) = select (first (flip f) \<$\> x) ((&) \<$\> y)
 -- @
 --
 -- * Generalised identity:
@@ -124,30 +124,18 @@
 -- x \<*? pure y = either y id \<$\> x
 -- @
 --
--- * A selective functor is /rigid/ if it satisfies @\<*\> = apS@. The following
--- /interchange/ law holds for rigid selective functors:
+-- * A selective functor is /rigid/ if it satisfies '<*>' @=@ 'apS'. The
+-- following /interchange/ law holds for rigid selective functors:
 --
 -- @
 -- x *\> (y \<*? z) = (x *\> y) \<*? z
 -- @
 --
 -- If f is also a 'Monad', we require that 'select' = 'selectM', from which one
--- can prove @\<*\> = apS@.
+-- can prove '<*>' @=@ 'apS'.
 class Applicative f => Selective f where
     select :: f (Either a b) -> f (a -> b) -> f b
 
--- | A list of values, equipped with a fast membership test.
-data Cases a = Cases [a] (a -> Bool)
-
--- | The list of all possible values of an enumerable data type.
-casesEnum :: (Bounded a, Enum a) => Cases a
-casesEnum = Cases [minBound..maxBound] (const True)
-
--- | Embed a list of values into 'Cases' using the trivial but slow membership
--- test based on 'elem'.
-cases :: Eq a => [a] -> Cases a
-cases as = Cases as (`elem` as)
-
 -- | An operator alias for 'select', which is sometimes convenient. It tries to
 -- follow the notational convention for 'Applicative' operators. The angle
 -- bracket pointing to the left means we always use the corresponding value.
@@ -162,12 +150,16 @@
 -- functions to apply to a given argument; the other effect is unnecessary. It
 -- is possible to implement 'branch' in terms of 'select', which is a good
 -- puzzle (give it a try!).
-branch :: Selective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
-branch x l r = fmap (fmap Left) x <*? fmap (fmap Right) l <*? r
-
--- Implementing select via branch:
+--
+-- We can also implement 'select' via 'branch':
+--
+-- @
 -- selectB :: Selective f => f (Either a b) -> f (a -> b) -> f b
 -- selectB x y = branch x y (pure id)
+-- @
+--
+branch :: Selective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
+branch x l r = fmap (fmap Left) x <*? fmap (fmap Right) l <*? r
 
 -- | We can write a function with the type signature of 'select' using the
 -- 'Applicative' type class, but it will always execute the effects associated
@@ -175,8 +167,8 @@
 selectA :: Applicative f => f (Either a b) -> f (a -> b) -> f b
 selectA x y = (\e f -> either f id e) <$> x <*> y
 
-{-| Recover the application operator @\<*\>@ from 'select'. /Rigid/ selective
-functors satisfy the law @(\<*\>) = apS@ and furthermore, the resulting
+{-| Recover the application operator '<*>' from 'select'. /Rigid/ selective
+functors satisfy the law '<*>' @=@ 'apS' and furthermore, the resulting
 applicative functor satisfies all laws of 'Applicative':
 
 * Identity:
@@ -196,7 +188,7 @@
     > (.) <$> u <*> v <*> w = u <*> (v <*> w)
 -}
 apS :: Selective f => f (a -> b) -> f a -> f b
-apS f x = select (Left <$> f) (flip ($) <$> x)
+apS f x = select (Left <$> f) ((&) <$> x)
 
 -- | One can easily implement a monadic 'selectM' that satisfies the laws,
 -- hence any 'Monad' is 'Selective'.
@@ -223,6 +215,18 @@
     match _ (Right y) = Right (Right y)
     match x (Left  y) = if x == y then Left () else Right (Left y)
 
+-- | A list of values, equipped with a fast membership test.
+data Cases a = Cases [a] (a -> Bool)
+
+-- | The list of all possible values of an enumerable data type.
+casesEnum :: (Bounded a, Enum a) => Cases a
+casesEnum = Cases [minBound..maxBound] (const True)
+
+-- | Embed a list of values into 'Cases' using the trivial but slow membership
+-- test based on 'elem'.
+cases :: Eq a => [a] -> Cases a
+cases as = Cases as (`elem` as)
+
 -- | Eliminate all specified values @a@ from @f (Either a b)@ by replacing each
 -- of them with a given @f a@.
 matchS :: (Eq a, Selective f) => Cases a -> f a -> (a -> f b) -> f (Either a b)
@@ -316,8 +320,15 @@
 -- Instances
 
 -- | Any applicative functor can be given a 'Selective' instance by defining
--- @select = selectA@.
-newtype SelectA f a = SelectA { fromSelectA :: f a }
+-- 'select' @=@ 'selectA'. This data type captures this pattern, so you can use
+-- it in combination with the @DerivingVia@ extension as follows:
+--
+-- @
+-- newtype Over m a = Over m
+--     deriving (Functor, Applicative, Selective) via SelectA (Const m)
+-- @
+--
+newtype SelectA f a = SelectA { getSelectA :: f a }
     deriving (Functor, Applicative)
 
 instance Applicative f => Selective (SelectA f) where
@@ -331,8 +342,15 @@
     select (Other       x ) (Other y) = Other $   x  <*? y
 
 -- | Any monad can be given a 'Selective' instance by defining
--- @select = selectM@.
-newtype SelectM f a = SelectM { fromSelectM :: f a }
+-- 'select' @=@ 'selectM'. This data type captures this pattern, so you can use
+-- it in combination with the @DerivingVia@ extension as follows:
+--
+-- @
+-- newtype V1 a = V1 a
+--     deriving (Functor, Applicative, Selective, Monad) via SelectM Identity
+-- @
+--
+newtype SelectM f a = SelectM { getSelectM :: f a }
     deriving (Functor, Applicative, Monad)
 
 instance Monad f => Selective (SelectM f) where
@@ -369,8 +387,8 @@
 -- and enable the various threads as appropriate..."
 instance Selective ZipList where select = selectA
 
--- | Selective instance for the standard applicative functor Validation.
--- This is a good example of a selective functor which is not a monad.
+-- | Selective instance for the standard applicative functor Validation. This is
+-- a good example of a non-trivial selective functor which is not a monad.
 data Validation e a = Failure e | Success a deriving (Functor, Show)
 
 instance Semigroup e => Applicative (Validation e) where
@@ -381,8 +399,8 @@
     Success f  <*> Success a  = Success (f a)
 
 instance Semigroup e => Selective (Validation e) where
-    select (Success (Right b)) _ = Success b
     select (Success (Left  a)) f = ($a) <$> f
+    select (Success (Right b)) _ = Success b
     select (Failure e        ) _ = Failure e
 
 instance (Selective f, Selective g) => Selective (Product f g) where
@@ -397,6 +415,22 @@
 instance (Applicative f, Selective g) => Selective (Compose f g) where
     select (Compose x) (Compose y) = Compose (select <$> x <*> y)
 
+{- Here is why composing selective functors is tricky.
+
+Consider @Compose Maybe IO@. The only sensible implementation is:
+
+> select :: Maybe (IO (Either a b)) -> Maybe (IO (a -> b)) -> Maybe (IO b)
+> select Nothing  _        = Nothing
+> select (Just x) (Just y) = Just (select x y)
+> select (Just x) Nothing  = Nothing -- Can't use Just: we don't have @a -> b@!
+
+In other words, we have to be 'Applicative' on the outside functor 'Maybe',
+because there is no way to peek inside 'IO', which forces us to statically
+choose between 'Just', which doesn't work since we have no function @a -> b@,
+and 'Nothing' which corresponds to the behaviour of 'selectA'.
+
+-}
+
 -- Monad instances
 
 -- As a quick experiment, try: ifS (pure True) (print 1) (print 2)
@@ -428,14 +462,14 @@
 
 ------------------------------------ Arrows ------------------------------------
 -- See the following standard definitions in "Control.Arrow".
--- newtype ArrowMonad a b = ArrowMonad (a () b)
+-- newtype ArrowMonad a o = ArrowMonad (a () o)
 -- instance Arrow a => Functor (ArrowMonad a)
 -- instance Arrow a => Applicative (ArrowMonad a)
 
 instance ArrowChoice a => Selective (ArrowMonad a) where
     select (ArrowMonad x) y = ArrowMonad $ x >>> (toArrow y ||| returnA)
 
-toArrow :: Arrow a => ArrowMonad a (b -> c) -> a b c
+toArrow :: Arrow a => ArrowMonad a (i -> o) -> a i o
 toArrow (ArrowMonad f) = arr (\x -> ((), x)) >>> first f >>> arr (uncurry ($))
 
 ---------------------------------- Alternative ---------------------------------
diff --git a/src/Control/Selective/Free/Rigid.hs b/src/Control/Selective/Free/Rigid.hs
deleted file mode 100644
--- a/src/Control/Selective/Free/Rigid.hs
+++ /dev/null
@@ -1,121 +0,0 @@
-{-# LANGUAGE FlexibleInstances, GADTs, RankNTypes, TupleSections #-}
------------------------------------------------------------------------------
--- |
--- Module     : Control.Selective.Free.Rigid
--- Copyright  : (c) Andrey Mokhov 2018-2019
--- License    : MIT (see the file LICENSE)
--- Maintainer : andrey.mokhov@gmail.com
--- Stability  : experimental
---
--- This is a library for /selective applicative functors/, or just
--- /selective functors/ for short, an abstraction between applicative functors
--- and monads, introduced in this paper:
--- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf.
---
--- This module defines /free rigid selective functors/, i.e. for selective
--- functors satisfying the property @\<*\> = apS@.
---
------------------------------------------------------------------------------
-module Control.Selective.Free.Rigid (
-    -- * Free rigid selective functors
-    Select (..), liftSelect,
-
-    -- * Static analysis
-    getPure, getEffects, getNecessaryEffect, runSelect, foldSelect
-    ) where
-
-import Control.Monad.Trans.Except
-import Data.Bifunctor
-import Data.Functor
-import Control.Selective
-
--- Inspired by free applicative functors by Capriotti and Kaposi.
--- See: https://arxiv.org/pdf/1403.0749.pdf
-
--- TODO: The current approach is simple but very slow: 'fmap' costs O(N), where
--- N is the number of effects, and 'select' is even worse -- O(N^2). It is
--- possible to improve both bounds to O(1) by using the idea developed for free
--- applicative functors by Dave Menendez. See this blog post:
--- https://www.eyrie.org/~zednenem/2013/05/27/freeapp
--- An example implementation can be found here:
--- http://hackage.haskell.org/package/free/docs/Control-Applicative-Free-Fast.html
-
--- | Free rigid selective functors.
-data Select f a where
-    Pure   :: a -> Select f a
-    Select :: Select f (Either a b) -> f (a -> b) -> Select f b
-
--- TODO: Prove that this is a lawful 'Functor'.
-instance Functor f => Functor (Select f) where
-    fmap f (Pure a)     = Pure (f a)
-    fmap f (Select x y) = Select (fmap f <$> x) (fmap f <$> y)
-
--- TODO: Prove that this is a lawful 'Applicative'.
-instance Functor f => Applicative (Select f) where
-    pure  = Pure
-    (<*>) = apS -- Rigid selective functors
-
--- TODO: Prove that this is a lawful 'Selective'.
-instance Functor f => Selective (Select f) where
-    -- Identity law
-    select x (Pure y) = either y id <$> x
-
-    -- Associativity law
-    select x (Select y z) = Select (select (f <$> x) (g <$> y)) (h <$> z)
-      where
-        f x = Right <$> x
-        g y = \a -> bimap (,a) ($a) y
-        h z = uncurry z
-
-{- The following can be used in the above implementation as select = selectOpt.
-
--- An optimised implementation of select for the free instance. It accumulates
--- the calls to fmap on the @y@ parameter to avoid traversing the list on every
--- recursive step.
-selectOpt :: Functor f => Select f (Either a b) -> Select f (a -> b) -> Select f b
-selectOpt x y = go x y id
-
--- We turn @Select f (a -> b)@ to @(Select f c, c -> (a -> b))@. Hey, co-Yoneda!
-go :: Functor f => Select f (Either a b) -> Select f c -> (c -> (a -> b)) -> Select f b
-go x (Pure y)     k = either (k y) id <$> x
-go x (Select y z) k = Select (go (f <$> x) y (g . second k)) ((h . (k.)) <$> z)
-  where
-    f x = Right <$> x
-    g y = \a -> bimap (,a) ($a) y
-    h z = uncurry z
--}
-
--- | Lift a functor into a free selective computation.
-liftSelect :: Functor f => f a -> Select f a
-liftSelect f = Select (Pure (Left ())) (const <$> f)
-
--- | Given a natural transformation from @f@ to @g@, this gives a canonical
--- natural transformation from @Select f@ to @g@.
-runSelect :: Selective g => (forall x. f x -> g x) -> Select f a -> g a
-runSelect _ (Pure a)     = pure a
-runSelect t (Select x y) = select (runSelect t x) (t y)
-
--- | Concatenate all effects of a free selective computation.
-foldSelect :: Monoid m => (forall x. f x -> m) -> Select f a -> m
-foldSelect f = getOver . runSelect (Over . f)
-
--- | Extract the resulting value if there are no necessary effects.
-getPure :: Select f a -> Maybe a
-getPure = runSelect (const Nothing)
-
--- | Collect all possible effects in the order they appear in a free selective
--- computation.
-getEffects :: Functor f => Select f a -> [f ()]
-getEffects = foldSelect (pure . void)
-
--- Implementation used in the paper:
--- getEffects = getOver . runSelect (Over . pure . void)
-
--- | Extract the necessary effect from a free selective computation. Note: there
--- can be at most one effect that is statically guaranteed to be necessary.
-getNecessaryEffect :: Functor f => Select f a -> Maybe (f ())
-getNecessaryEffect = leftToMaybe . runExcept . runSelect (throwE . void)
-
-leftToMaybe :: Either a b -> Maybe a
-leftToMaybe (Left a) = Just a
-leftToMaybe _        = Nothing
diff --git a/src/Control/Selective/Rigid/Free.hs b/src/Control/Selective/Rigid/Free.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Selective/Rigid/Free.hs
@@ -0,0 +1,121 @@
+{-# LANGUAGE GADTs, RankNTypes, TupleSections #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module     : Control.Selective.Rigid.Free
+-- Copyright  : (c) Andrey Mokhov 2018-2019
+-- License    : MIT (see the file LICENSE)
+-- Maintainer : andrey.mokhov@gmail.com
+-- Stability  : experimental
+--
+-- This is a library for /selective applicative functors/, or just
+-- /selective functors/ for short, an abstraction between applicative functors
+-- and monads, introduced in this paper:
+-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf.
+--
+-- This module defines /free rigid selective functors/. Rigid selective functors
+-- are those that satisfy the property @\<*\> = apS@.
+--
+-----------------------------------------------------------------------------
+module Control.Selective.Rigid.Free (
+    -- * Free rigid selective functors
+    Select (..), liftSelect,
+
+    -- * Static analysis
+    getPure, getEffects, getNecessaryEffect, runSelect, foldSelect
+    ) where
+
+import Control.Monad.Trans.Except
+import Control.Selective
+import Data.Bifunctor
+import Data.Functor
+
+-- Inspired by free applicative functors by Capriotti and Kaposi.
+-- See: https://arxiv.org/pdf/1403.0749.pdf
+
+-- TODO: The current approach is simple but very slow: 'fmap' costs O(N), where
+-- N is the number of effects, and 'select' is even worse -- O(N^2). It is
+-- possible to improve both bounds to O(1) by using the idea developed for free
+-- applicative functors by Dave Menendez. See this blog post:
+-- https://www.eyrie.org/~zednenem/2013/05/27/freeapp
+-- An example implementation can be found here:
+-- http://hackage.haskell.org/package/free/docs/Control-Applicative-Free-Fast.html
+
+-- | Free rigid selective functors.
+data Select f a where
+    Pure   :: a -> Select f a
+    Select :: Select f (Either a b) -> f (a -> b) -> Select f b
+
+-- TODO: Prove that this is a lawful 'Functor'.
+instance Functor f => Functor (Select f) where
+    fmap f (Pure a)     = Pure (f a)
+    fmap f (Select x y) = Select (fmap f <$> x) (fmap f <$> y)
+
+-- TODO: Prove that this is a lawful 'Applicative'.
+instance Functor f => Applicative (Select f) where
+    pure  = Pure
+    (<*>) = apS -- Rigid selective functors
+
+-- TODO: Prove that this is a lawful 'Selective'.
+instance Functor f => Selective (Select f) where
+    -- Identity law
+    select x (Pure y) = either y id <$> x
+
+    -- Associativity law
+    select x (Select y z) = Select (select (f <$> x) (g <$> y)) (h <$> z)
+      where
+        f x = Right <$> x
+        g y = \a -> bimap (,a) ($a) y
+        h z = uncurry z
+
+{- The following can be used in the above implementation as select = selectOpt.
+
+-- An optimised implementation of select for the free instance. It accumulates
+-- the calls to fmap on the @y@ parameter to avoid traversing the list on every
+-- recursive step.
+selectOpt :: Functor f => Select f (Either a b) -> Select f (a -> b) -> Select f b
+selectOpt x y = go x y id
+
+-- We turn @Select f (a -> b)@ to @(Select f c, c -> (a -> b))@. Hey, co-Yoneda!
+go :: Functor f => Select f (Either a b) -> Select f c -> (c -> (a -> b)) -> Select f b
+go x (Pure y)     k = either (k y) id <$> x
+go x (Select y z) k = Select (go (f <$> x) y (g . second k)) ((h . (k.)) <$> z)
+  where
+    f x = Right <$> x
+    g y = \a -> bimap (,a) ($a) y
+    h z = uncurry z
+-}
+
+-- | Lift a functor into a free selective computation.
+liftSelect :: Functor f => f a -> Select f a
+liftSelect f = Select (Pure (Left ())) (const <$> f)
+
+-- | Given a natural transformation from @f@ to @g@, this gives a canonical
+-- natural transformation from @Select f@ to @g@.
+runSelect :: Selective g => (forall x. f x -> g x) -> Select f a -> g a
+runSelect _ (Pure a)     = pure a
+runSelect t (Select x y) = select (runSelect t x) (t y)
+
+-- | Concatenate all effects of a free selective computation.
+foldSelect :: Monoid m => (forall x. f x -> m) -> Select f a -> m
+foldSelect f = getOver . runSelect (Over . f)
+
+-- | Extract the resulting value if there are no necessary effects.
+getPure :: Select f a -> Maybe a
+getPure = runSelect (const Nothing)
+
+-- | Collect all possible effects in the order they appear in a free selective
+-- computation.
+getEffects :: Functor f => Select f a -> [f ()]
+getEffects = foldSelect (pure . void)
+
+-- Implementation used in the paper:
+-- getEffects = getOver . runSelect (Over . pure . void)
+
+-- | Extract the necessary effect from a free selective computation. Note: there
+-- can be at most one effect that is statically guaranteed to be necessary.
+getNecessaryEffect :: Functor f => Select f a -> Maybe (f ())
+getNecessaryEffect = leftToMaybe . runExcept . runSelect (throwE . void)
+
+leftToMaybe :: Either a b -> Maybe a
+leftToMaybe (Left a) = Just a
+leftToMaybe _        = Nothing
diff --git a/src/Control/Selective/Rigid/Freer.hs b/src/Control/Selective/Rigid/Freer.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Selective/Rigid/Freer.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE DeriveFunctor, GADTs, RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module     : Control.Selective.Rigid.Freer
+-- Copyright  : (c) Andrey Mokhov 2018-2019
+-- License    : MIT (see the file LICENSE)
+-- Maintainer : andrey.mokhov@gmail.com
+-- Stability  : experimental
+--
+-- This is a library for /selective applicative functors/, or just
+-- /selective functors/ for short, an abstraction between applicative functors
+-- and monads, introduced in this paper:
+-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf.
+--
+-- This module defines /freer rigid selective functors/. Rigid selective
+-- functors are those that satisfy the property @\<*\> = apS@. Compared to the
+-- "free" construction from "Control.Selective.Rigid.Free", this "freer"
+-- construction does not require the underlying base data type to be a functor.
+--
+-----------------------------------------------------------------------------
+module Control.Selective.Rigid.Freer (
+    -- * Free rigid selective functors
+    Select (..), liftSelect,
+
+    -- * Static analysis
+    getPure, getEffects, getNecessaryEffect, runSelect, foldSelect
+    ) where
+
+import Control.Monad.Trans.Except
+import Control.Selective
+import Data.Bifunctor
+import Data.Function
+import Data.Functor
+
+-- Inspired by free applicative functors by Capriotti and Kaposi.
+-- See: https://arxiv.org/pdf/1403.0749.pdf
+
+-- Note: In the current implementation, 'fmap' and 'select' cost O(N), where N
+-- is the number of effects. It is possible to improve this to O(1) by using the
+-- idea developed for free applicative functors by Dave Menendez, see this blog
+-- post: https://www.eyrie.org/~zednenem/2013/05/27/freeapp.
+-- An example implementation can be found here:
+-- http://hackage.haskell.org/package/free/docs/Control-Applicative-Free-Fast.html
+
+-- | Free rigid selective functors.
+data Select f a where
+    Pure   :: a -> Select f a
+    Select :: Select f (Either (x -> a) a) -> f x -> Select f a
+
+-- TODO: Prove that this is a lawful 'Functor'.
+instance Functor (Select f) where
+    fmap f (Pure a)     = Pure (f a)
+    fmap f (Select x y) = Select (bimap (f.) f <$> x) y -- O(N)
+
+-- TODO: Prove that this is a lawful 'Applicative'.
+instance Applicative (Select f) where
+    pure  = Pure
+    (<*>) = apS -- Rigid selective functors
+
+-- TODO: Prove that this is a lawful 'Selective'.
+instance Selective (Select f) where
+    select = selectBy (first (&))
+      where
+        selectBy :: (a -> Either (b -> c) c) -> Select f a -> Select f b -> Select f c
+        selectBy f x (Pure y)     = either ($y) id . f <$> x
+        selectBy f x (Select y z) = Select (selectBy g x y) z -- O(N)
+          where
+            g a = case f a of Right c -> Right (Right c)
+                              Left bc -> Left  (bimap (bc.) bc)
+
+-- | Lift a functor into a free selective computation.
+liftSelect :: f a -> Select f a
+liftSelect f = Select (Pure (Left id)) f
+
+-- | Given a natural transformation from @f@ to @g@, this gives a canonical
+-- natural transformation from @Select f@ to @g@.
+runSelect :: Selective g => (forall x. f x -> g x) -> Select f a -> g a
+runSelect _ (Pure a)     = pure a
+runSelect t (Select x y) = select (runSelect t x) ((&) <$> t y)
+
+-- | Concatenate all effects of a free selective computation.
+foldSelect :: Monoid m => (forall x. f x -> m) -> Select f a -> m
+foldSelect f = getOver . runSelect (Over . f)
+
+-- | Extract the resulting value if there are no necessary effects.
+getPure :: Select f a -> Maybe a
+getPure = runSelect (const Nothing)
+
+-- | Collect all possible effects in the order they appear in a free selective
+-- computation.
+getEffects :: Functor f => Select f a -> [f ()]
+getEffects = foldSelect (pure . void)
+
+-- | Extract the necessary effect from a free selective computation. Note: there
+-- can be at most one effect that is statically guaranteed to be necessary.
+getNecessaryEffect :: Functor f => Select f a -> Maybe (f ())
+getNecessaryEffect = leftToMaybe . runExcept . runSelect (throwE . void)
+
+leftToMaybe :: Either a b -> Maybe a
+leftToMaybe (Left a) = Just a
+leftToMaybe _        = Nothing
diff --git a/test/Laws.hs b/test/Laws.hs
--- a/test/Laws.hs
+++ b/test/Laws.hs
@@ -7,6 +7,7 @@
 import Data.Bifunctor (bimap, first, second)
 import Control.Arrow hiding (first, second)
 import Control.Selective
+import Data.Function
 import Data.Functor.Identity
 import Control.Monad.State
 import Text.Show.Functions()
@@ -64,7 +65,7 @@
 -- | Apply a pure function to the second argument:
 theorem3 :: (Selective f, Eq (f c)) =>
             (a -> b -> c) -> f (Either b c) -> f a -> Bool
-theorem3 f x y = (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))
+theorem3 f x y = (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))
 
 -- | Generalised identity:
 theorem4 :: (Selective f, Eq (f b)) => f (Either a b) -> (a -> b) -> Bool
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -1,20 +1,23 @@
 {-# LANGUAGE TypeApplications #-}
 
-import Data.Maybe hiding (maybe)
+import Control.Arrow (ArrowMonad)
+import Control.Selective
 import Data.Functor.Identity
+import Data.Maybe hiding (maybe)
 import Prelude hiding (maybe)
 import Test.Tasty
 import Test.Tasty.QuickCheck hiding (Success, Failure)
 import Test.Tasty.ExpectedFailure
-import Control.Selective
-import Control.Selective.Free.Rigid
-import Control.Arrow (ArrowMonad)
 
 import Build
 import Laws
-import Teletype
 import Validation
 
+import qualified Control.Selective.Free       as F
+import qualified Control.Selective.Rigid.Free as FR
+import qualified Teletype                     as F
+import qualified Teletype.Rigid               as FR
+
 main :: IO ()
 main = defaultMain $ testGroup "Tests"
     [pingPong, build, over, under, validation, arrowMonad, maybe, identity]
@@ -24,9 +27,13 @@
 --------------------------------------------------------------------------------
 pingPong :: TestTree
 pingPong = testGroup "pingPong"
-    [ testProperty "getEffects pingPongS == [Read,Write \"pong\"]" $
-       getEffects pingPongS == [Read (const ()),Write "pong" ()]
-    ]
+    [ testProperty "Free.getEffects pingPongS == [Read,Write \"pong\"]" $
+       F.getEffects F.pingPongS == [F.Read (const ()),F.Write "pong" ()]
+    , testProperty "Free.getNecessaryEffects pingPongS == [Read]" $
+       F.getNecessaryEffects F.pingPongS == [F.Read (const ())]
+    , testProperty "Free.Rigid.getEffects pingPongS == [Read,Write \"pong\"]" $
+       FR.getEffects FR.pingPongS == [FR.Read (const ()),FR.Write "pong" ()] ]
+
 --------------------------------------------------------------------------------
 ------------------------ Build -------------------------------------------------
 --------------------------------------------------------------------------------
@@ -42,22 +49,19 @@
     , testProperty "dependenciesUnder (fromJust $ cyclic \"B1\") == [\"C1\"]" $
        dependenciesUnder (fromJust $ cyclic "B1") == ["C1"]
     , testProperty "dependenciesUnder cyclic \"B2\") == [\"C1\"]" $
-        dependenciesUnder (fromJust $ cyclic "B2") == ["C1"]
-    ]
+        dependenciesUnder (fromJust $ cyclic "B2") == ["C1"] ]
 
 taskBindDeps :: TestTree
 taskBindDeps = testGroup "taskBindDeps"
     [ testProperty "dependenciesOver taskBind == [\"A1\",\"A2\",\"C5\",\"C6\",\"A2\",\"D5\",\"D6\"]" $
        dependenciesOver taskBind == ["A1","A2","C5","C6","A2","D5","D6"]
     , testProperty "dependenciesUnder taskBind == [\"A1\"]" $
-       dependenciesUnder taskBind == ["A1"]
-    ]
+       dependenciesUnder taskBind == ["A1"] ]
 
 runBuildDeps :: TestTree
 runBuildDeps = testGroup "runBuildDeps"
     [ testProperty "runBuild (fromJust $ cyclic \"B1\") == [Fetch \"C1\",Fetch \"B2\",Fetch \"A2\"]" $
-       runBuild (fromJust $ cyclic "B1") == [Fetch "C1" (const ()),Fetch "B2" (const ()),Fetch "A2" (const ())]
-    ]
+       runBuild (fromJust $ cyclic "B1") == [Fetch "C1" (const ()),Fetch "B2" (const ()),Fetch "A2" (const ())] ]
 
 --------------------------------------------------------------------------------
 ------------------------ Over --------------------------------------------------
@@ -72,8 +76,7 @@
     , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $
         \x -> lawDistributivity @(Over String) @Int @Int x
     , testProperty "Associativity: take a look at tests/Laws.hs" $
-        \x -> lawAssociativity @(Over String) @Int @Int x
-    ]
+        \x -> lawAssociativity @(Over String) @Int @Int x ]
 
 overTheorems :: TestTree
 overTheorems = testGroup "Theorems"
@@ -81,15 +84,14 @@
         \x -> theorem1 @(Over String) @Int @Int x
     , testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $
         \x -> theorem2 @(Over String) @Int @Int @Int x
-    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $
+    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))" $
         \x -> theorem3 @(Over String) @Int @Int @Int x
     , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $
         \x -> theorem4 @(Over String) @Int @Int x
     , testProperty "(f <*> g) == (f `apS` g)" $
         \x -> theorem5 @(Over String) @Int @Int x
     , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
-        \x -> theorem6 @(Over String) @Int @Int x
-    ]
+        \x -> theorem6 @(Over String) @Int @Int x ]
 
 overProperties :: TestTree
 overProperties = testGroup "Properties"
@@ -97,8 +99,7 @@
       testProperty "pure-right: pure (Right x) <*? y = pure x" $
         \x -> propertyPureRight @(Over String) @Int @Int x
     , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $
-        \x -> propertyPureLeft @(Over String) @Int @Int x
-    ]
+        \x -> propertyPureLeft @(Over String) @Int @Int x ]
 
 --------------------------------------------------------------------------------
 ------------------------ Under -------------------------------------------------
@@ -113,8 +114,7 @@
     , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $
         \x -> lawDistributivity @(Under String) @Int @Int x
     , testProperty "Associativity: take a look at tests/Laws.hs" $
-        \x -> lawAssociativity @(Under String) @Int @Int x
-    ]
+        \x -> lawAssociativity @(Under String) @Int @Int x ]
 
 underTheorems :: TestTree
 underTheorems = testGroup "Theorems"
@@ -122,7 +122,7 @@
         \x -> theorem1 @(Under String) @Int @Int x
     , testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $
         \x -> theorem2 @(Under String) @Int @Int @Int x
-    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $
+    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))" $
         \x -> theorem3 @(Under String) @Int @Int @Int x
     , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $
         \x -> theorem4 @(Under String) @Int @Int x
@@ -130,8 +130,7 @@
     , expectFail $ testProperty "(f <*> g) == (f `apS` g)" $
         \x -> theorem5 @(Under String) @Int @Int x
     , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
-        \x -> theorem6 @(Under String) @Int @Int x
-    ]
+        \x -> theorem6 @(Under String) @Int @Int x ]
 
 underProperties :: TestTree
 underProperties = testGroup "Properties"
@@ -139,8 +138,8 @@
         \x -> propertyPureRight @(Under String) @Int @Int x
     , expectFail $
       testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $
-        \x -> propertyPureLeft @(Under String) @Int @Int x
-    ]
+        \x -> propertyPureLeft @(Under String) @Int @Int x ]
+
 --------------------------------------------------------------------------------
 ------------------------ Validation --------------------------------------------
 --------------------------------------------------------------------------------
@@ -156,8 +155,7 @@
     , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $
         \x -> lawDistributivity @(Validation String) @Int @Int x
     , testProperty "Associativity: take a look at tests/Laws.hs" $
-        \x -> lawAssociativity @(Validation String) @Int @Int @Int x
-    ]
+        \x -> lawAssociativity @(Validation String) @Int @Int @Int x ]
 
 validationTheorems :: TestTree
 validationTheorems = testGroup "Theorems"
@@ -165,7 +163,7 @@
         \x -> theorem1 @(Validation String) @Int @Int @Int x
     , testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $
         \x -> theorem2 @(Validation String) @Int @Int @Int x
-    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $
+    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))" $
         \x -> theorem3 @(Validation String) @Int @Int @Int x
     , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $
         \x -> theorem4 @(Validation String) @Int @Int x
@@ -174,16 +172,14 @@
         \x -> theorem5 @(Validation String) @Int @Int x
     -- 'Validation' is a non-rigid selective functor
     , expectFail $ testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
-        \x -> theorem6 @(Validation String) @Int @Int @Int x
-    ]
+        \x -> theorem6 @(Validation String) @Int @Int @Int x ]
 
 validationProperties :: TestTree
 validationProperties = testGroup "Properties"
     [ testProperty "pure-right: pure (Right x) <*? y = pure x" $
         \x -> propertyPureRight @(Validation String) @Int @Int x
     , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $
-        \x -> propertyPureLeft @(Validation String) @Int @Int x
-    ]
+        \x -> propertyPureLeft @(Validation String) @Int @Int x ]
 
 validationExample :: TestTree
 validationExample = testGroup "validationExample"
@@ -198,13 +194,11 @@
     , testProperty "shape (Failure [\"choice?\"]) (Failure [\"radius?\"]) (Success 2) (Failure [\"height?\"])" $
         shape (Failure ["choice?"]) (Failure ["radius?"]) (Success 2) (Failure ["height?"]) == Failure ["choice?"]
     , testProperty "twoShapes s1 s2" $
-        twoShapes (shape (Failure ["choice 1?"]) (Success 1) (Failure ["width 1?"]) (Success 3)) (shape (Success False) (Success 1) (Success 2) (Failure ["height 2?"])) == Failure ["choice 1?","height 2?"]
-    ]
+        twoShapes (shape (Failure ["choice 1?"]) (Success 1) (Failure ["width 1?"]) (Success 3)) (shape (Success False) (Success 1) (Success 2) (Failure ["height 2?"])) == Failure ["choice 1?","height 2?"] ]
 
 --------------------------------------------------------------------------------
 ------------------------ ArrowMonad --------------------------------------------
 --------------------------------------------------------------------------------
-
 arrowMonad :: TestTree
 arrowMonad = testGroup "ArrowMonad (->)"
     [arrowMonadLaws, arrowMonadTheorems, arrowMonadProperties]
@@ -220,8 +214,7 @@
     , testProperty "select == selectM" $
         \x -> lawMonad @(ArrowMonad (->)) @Int @Int x
     , testProperty "select == selectA" $
-        \x -> selectALaw @(ArrowMonad (->)) @Int @Int x
-    ]
+        \x -> selectALaw @(ArrowMonad (->)) @Int @Int x ]
 
 arrowMonadTheorems :: TestTree
 arrowMonadTheorems = testGroup "Theorems"
@@ -229,23 +222,22 @@
         \x -> theorem1 @(ArrowMonad (->)) @Int @Int @Int x
     , testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $
         \x -> theorem2 @(ArrowMonad (->)) @Int @Int @Int x
-    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $
+    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))" $
         \x -> theorem3 @(ArrowMonad (->)) @Int @Int @Int x
     , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $
         \x -> theorem4 @(ArrowMonad (->)) @Int @Int x
     , testProperty "(f <*> g) == (f `apS` g)" $
         \x -> theorem5 @(ArrowMonad (->)) @Int @Int x
     , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
-        \x -> theorem6 @(ArrowMonad (->)) @Int @Int @Int x
-    ]
+        \x -> theorem6 @(ArrowMonad (->)) @Int @Int @Int x ]
 
 arrowMonadProperties :: TestTree
 arrowMonadProperties = testGroup "Properties"
     [ testProperty "pure-right: pure (Right x) <*? y = pure x" $
         \x -> propertyPureRight @(ArrowMonad (->)) @Int @Int x
     , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $
-        \x -> propertyPureLeft @(ArrowMonad (->)) @Int @Int x
-    ]
+        \x -> propertyPureLeft @(ArrowMonad (->)) @Int @Int x ]
+
 --------------------------------------------------------------------------------
 ------------------------ Maybe -------------------------------------------------
 --------------------------------------------------------------------------------
@@ -261,8 +253,7 @@
     , testProperty "Associativity: take a look at tests/Laws.hs" $
         \x -> lawAssociativity @Maybe @Int @Int @Int x
     , testProperty "select == selectM" $
-        \x -> lawMonad @Maybe @Int @Int x
-    ]
+        \x -> lawMonad @Maybe @Int @Int x ]
 
 maybeTheorems :: TestTree
 maybeTheorems = testGroup "Theorems"
@@ -270,23 +261,22 @@
         \x -> theorem1 @Maybe @Int @Int @Int x
     , testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $
         \x -> theorem2 @Maybe @Int @Int @Int x
-    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $
+    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))" $
         \x -> theorem3 @Maybe @Int @Int @Int x
     , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $
         \x -> theorem4 @Maybe @Int @Int x
     , testProperty "(f <*> g) == (f `apS` g)" $
         \x -> theorem5 @Maybe @Int @Int x
     , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
-        \x -> theorem6 @Maybe @Int @Int @Int x
-    ]
+        \x -> theorem6 @Maybe @Int @Int @Int x ]
 
 maybeProperties :: TestTree
 maybeProperties = testGroup "Properties"
     [ testProperty "pure-right: pure (Right x) <*? y = pure x" $
         \x -> propertyPureRight @Maybe @Int @Int x
     , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $
-        \x -> propertyPureLeft @Maybe @Int @Int x
-    ]
+        \x -> propertyPureLeft @Maybe @Int @Int x ]
+
 --------------------------------------------------------------------------------
 ------------------------ Identity ----------------------------------------------
 --------------------------------------------------------------------------------
@@ -303,8 +293,7 @@
     , testProperty "Associativity: take a look at tests/Laws.hs" $
         \x -> lawAssociativity @Identity @Int @Int @Int x
     , testProperty "select == selectM" $
-        \x -> lawMonad @Identity @Int @Int x
-    ]
+        \x -> lawMonad @Identity @Int @Int x ]
 
 identityTheorems :: TestTree
 identityTheorems = testGroup "Theorems"
@@ -312,20 +301,18 @@
         \x -> theorem1 @Identity @Int @Int @Int x
     , testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $
         \x -> theorem2 @Identity @Int @Int @Int x
-    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $
+    , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) ((&) <$> y))" $
         \x -> theorem3 @Identity @Int @Int @Int x
     , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $
         \x -> theorem4 @Identity @Int @Int x
     , testProperty "(f <*> g) == (f `apS` g)" $
         \x -> theorem5 @Identity @Int @Int x
     , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
-        \x -> theorem6 @Identity @Int @Int @Int x
-    ]
+        \x -> theorem6 @Identity @Int @Int @Int x ]
 
 identityProperties :: TestTree
 identityProperties = testGroup "Properties"
     [ testProperty "pure-right: pure (Right x) <*? y = pure x" $
         \x -> propertyPureRight @Identity @Int @Int x
     , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $
-        \x -> propertyPureLeft @Identity @Int @Int x
-    ]
+        \x -> propertyPureLeft @Identity @Int @Int x ]
diff --git a/test/Sketch.hs b/test/Sketch.hs
--- a/test/Sketch.hs
+++ b/test/Sketch.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE FlexibleInstances, GADTs, RankNTypes, ScopedTypeVariables, TupleSections #-}
+{-# LANGUAGE DeriveFunctor, EmptyCase, GADTs, RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables, TupleSections #-}
 module Sketch where
 
 import Control.Arrow hiding (first, second)
@@ -6,6 +7,9 @@
 import Control.Monad
 import Control.Selective
 import Data.Bifunctor
+import Data.Bool
+import Data.Function
+import Data.Semigroup (Semigroup (..))
 import Data.Void
 
 import qualified Control.Arrow    as A
@@ -50,9 +54,9 @@
 f2 :: Selective f => (a -> c) -> f (Either a b) -> f (c -> b) -> f b
 f2 f x y = select (first f <$> x) y === select x ((. f) <$> y)
 
--- F3 (Free): select x (f <$> y) = select (first (flip f) <$> x) (flip ($) <$> y)
+-- F3 (Free): select x (f <$> y) = select (first (flip f) <$> x) ((&) <$> y)
 f3 :: Selective f => (c -> a -> b) -> f (Either a b) -> f c -> f b
-f3 f x y = select x (f <$> y) === select (first (flip f) <$> x) (flip ($) <$> y)
+f3 f x y = select x (f <$> y) === select (first (flip f) <$> x) ((&) <$> y)
 
 -- P1 (Generalised identity): select x (pure y) == either y id <$> x
 p1 :: Selective f => f (Either a b) -> (a -> b) -> f b
@@ -140,11 +144,11 @@
     -- Express the lefthand side using 'apS'
     apS (pure id) v
     === -- Definition of 'apS'
-    select (Left <$> pure id) (flip ($) <$> v)
+    select (Left <$> pure id) ((&) <$> v)
     === -- Push 'Left' inside 'pure'
-    select (pure (Left id)) (flip ($) <$> v)
+    select (pure (Left id)) ((&) <$> v)
     === -- Apply P2
-    ($id) <$> (flip ($) <$> v)
+    ($id) <$> ((&) <$> v)
     === -- Simplify
     id <$> v
     === -- Functor identity: -- Functor identity: fmap id = id
@@ -156,15 +160,15 @@
     -- Express the lefthand side using 'apS'
     apS (pure f) (pure x)
     === -- Definition of 'apS'
-    select (Left <$> pure f) (flip ($) <$> pure x)
+    select (Left <$> pure f) ((&) <$> pure x)
     === -- Push 'Left' inside 'pure'
-    select (pure (Left f)) (flip ($) <$> pure x)
+    select (pure (Left f)) ((&) <$> pure x)
     === -- Applicative's fmap-pure law
-    select (pure (Left f)) (pure (flip ($) x))
+    select (pure (Left f)) (pure ((&) x))
     === -- Apply P1
-    either ((flip ($) x)) id <$> pure (Left f)
+    either (((&) x)) id <$> pure (Left f)
     === -- Applicative's fmap-pure law
-    pure ((flip ($) x) f)
+    pure (((&) x) f)
     === -- Simplify
     pure (f x)
 
@@ -175,7 +179,7 @@
     -- Express the lefthand side using 'apS'
     apS u (pure y)
     === -- Definition of 'apS'
-    select (Left <$> u) (flip ($) <$> pure y)
+    select (Left <$> u) ((&) <$> pure y)
     === -- Rewrite to have a pure second argument
     select (Left <$> u) (pure ($y))
     === -- Apply P1
@@ -186,11 +190,11 @@
     === -- Express right-hand side of the theorem using 'apS'
     apS (pure ($y)) u
     === -- Definition of 'apS'
-    select (Left <$> pure ($y)) (flip ($) <$> u)
+    select (Left <$> pure ($y)) ((&) <$> u)
     === -- Push 'Left' inside 'pure'
-    select (pure (Left ($y))) (flip ($) <$> u)
+    select (pure (Left ($y))) ((&) <$> u)
     === -- Apply P2
-    ($($y)) <$> (flip ($) <$> u)
+    ($($y)) <$> ((&) <$> u)
     === -- Simplify, obtaining (#)
     ($y) <$> u
 
@@ -200,36 +204,36 @@
     -- Express the lefthand side using 'apS'
     apS (apS ((.) <$> u) v) w
     === -- Definition of 'apS'
-    select (Left <$> select (Left <$> (.) <$> u) (flip ($) <$> v)) (flip ($) <$> w)
+    select (Left <$> select (Left <$> (.) <$> u) ((&) <$> v)) ((&) <$> w)
     === -- Apply F1 to push the leftmost 'Left' inside 'select'
-    select (select (second Left <$> Left <$> (.) <$> u) ((Left .) <$> flip ($) <$> v)) (flip ($) <$> w)
+    select (select (second Left <$> Left <$> (.) <$> u) ((Left .) <$> (&) <$> v)) ((&) <$> w)
     === -- Simplify
-    select (select (Left <$> (.) <$> u) ((Left .) <$> flip ($) <$> v)) (flip ($) <$> w)
+    select (select (Left <$> (.) <$> u) ((Left .) <$> (&) <$> v)) ((&) <$> w)
     === -- Pull (.) outside 'Left'
-    select (select (first (.) <$> Left <$> u) ((Left .) <$> flip ($) <$> v)) (flip ($) <$> w)
+    select (select (first (.) <$> Left <$> u) ((Left .) <$> (&) <$> v)) ((&) <$> w)
     === -- Apply F2 to push @(.)@ to the function
-    select (select (Left <$> u) ((. (.)) <$> (Left .) <$> flip ($) <$> v)) (flip ($) <$> w)
+    select (select (Left <$> u) ((. (.)) <$> (Left .) <$> (&) <$> v)) ((&) <$> w)
     === -- Simplify, obtaining (#)
-    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) (flip ($) <$> w)
+    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) ((&) <$> w)
 
     === -- Express the righthand side using 'apS'
     apS u (apS v w)
     === -- Definition of 'apS'
-    select (Left <$> u) (flip ($) <$> select (Left <$> v) (flip ($) <$> w))
-    === -- Apply F1 to push @flip ($)@ inside 'select'
-    select (Left <$> u) (select (Left <$> v) ((flip ($) .) <$> flip ($) <$> w))
+    select (Left <$> u) ((&) <$> select (Left <$> v) ((&) <$> w))
+    === -- Apply F1 to push @(&)@ inside 'select'
+    select (Left <$> u) (select (Left <$> v) (((&) .) <$> (&) <$> w))
     === -- Apply A1 to reassociate to the left
-    select (select (Left <$> u) ((\y a -> bimap (,a) ($a) y) <$> Left <$> v)) (uncurry . (flip ($) .) <$> flip ($) <$> w)
+    select (select (Left <$> u) ((\y a -> bimap (,a) ($a) y) <$> Left <$> v)) (uncurry . ((&) .) <$> (&) <$> w)
     === -- Simplify
     select (select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) ((\x (f, g) -> g (f x)) <$> w)
     === -- Apply F3 to pull the rightmost pure function inside 'select'
-    select (first (flip ((\x (f, g) -> g (f x)))) <$> select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) (flip ($) <$> w)
+    select (first (flip ((\x (f, g) -> g (f x)))) <$> select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) ((&) <$> w)
     === -- Simplify
-    select (first (\(f, g) -> g . f) <$> select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) (flip ($) <$> w)
+    select (first (\(f, g) -> g . f) <$> select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) ((&) <$> w)
     === -- Apply F1 to push the leftmost pure function inside 'select'
-    select (select (Left <$> u) (((first (\(f, g) -> g . f)).) <$> (\y a -> Left (y, a)) <$> v)) (flip ($) <$> w)
+    select (select (Left <$> u) (((first (\(f, g) -> g . f)).) <$> (\y a -> Left (y, a)) <$> v)) ((&) <$> w)
     === -- Simplify, obtaining (#)
-    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) (flip ($) <$> w)
+    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) ((&) <$> w)
 
 --------------------------------- End of proofs --------------------------------
 
@@ -259,11 +263,37 @@
   where
     f x = Right <$> x
     g y = \a -> bimap (\c f -> f c a) ($a) y
-    h z = ($z) -- h = flip ($)
+    h z = ($z) -- h = (&)
 
--- Alternative type classes for selective functors. They all come with an
--- additional requirement that we run effects from left to right.
+-- Alternative formulations of selective functors.
 
+-- Factoring out the selection logic into a pure argument
+class Applicative f => SelectiveBy f where
+    selectBy :: (a -> Either (b -> c) c) -> f a -> f b -> f c
+
+fromSelectBy :: SelectiveBy f => f (Either a b) -> f (a -> b) -> f b
+fromSelectBy = selectBy (first ((&)))
+
+toSelectBy :: Selective f => (a -> Either (b -> c) c) -> f a -> f b -> f c
+toSelectBy f x y = select (f <$> x) ((&) <$> y)
+
+whenBy :: SelectiveBy f => f Bool -> f () -> f ()
+whenBy = selectBy (bool (Right ()) (Left id))
+
+-- A first-order version of selective functors.
+class Applicative f => SelectiveF f where
+    selectF :: f (Either a b) -> f c -> f (Either a (b, c))
+
+toF :: Selective f => f (Either a b) -> f c -> f (Either a (b, c))
+toF x y = branch x (pure Left) ((\c b -> Right (b, c)) <$> y)
+
+fromF :: SelectiveF f => f (Either a b) -> f (a -> b) -> f b
+fromF x y = either id (uncurry ((&))) <$> selectF (swapEither <$> x) y
+
+-- A few variants that have a sum type in both arguments. They are not
+-- equivalent to 'Selective' of 'SelectiveF' unless we require that effects are
+-- executed from left to right.
+
 -- Composition of Applicative and Either monad
 class Applicative f => SelectiveA f where
     (|*|) :: f (Either e (a -> b)) -> f (Either e a) -> f (Either e b)
@@ -273,7 +303,6 @@
 class Applicative f => SelectiveS f where
     (|.|) :: f (Either e (b -> c)) -> f (Either e (a -> b)) -> f (Either e (a -> c))
 
-
 -- Composition of Monoidal and Either monad
 -- See: http://blog.ezyang.com/2012/08/applicative-functors/
 class Applicative f => SelectiveM f where
@@ -290,7 +319,7 @@
 a1M x y z =
     x ?*? (y ?*? z)
     ===
-    second assoc <$> ((x ?*? y) ?*? z)
+    fmap assoc <$> ((x ?*? y) ?*? z)
   where
     assoc ((a, b), c) = (a, (b, c))
 
@@ -314,9 +343,9 @@
     === -- Law: <*> = ap
     ap fab fa
     === -- Free theorem (?)
-    selectM (Left <$> fab) (flip ($) <$> fa)
+    selectM (Left <$> fab) ((&) <$> fa)
     === -- Law: selectM = select
-    select (Left <$> fab) (flip ($) <$> fa)
+    select (Left <$> fab) ((&) <$> fa)
     === -- Definition of apS
     apS fab fa
 
@@ -378,19 +407,19 @@
     === -- Apply F3 to move the rightmost pure function into the outer 'select'
     select (first (flip $ (\ab bc -> (bc .) <$> ab)) <$> maybe (Right Nothing) Left <$> (select (maybe (Right Nothing) Left <$> x)
         ((\ab bc -> (bc .) <$> ab) <$> y)))
-        (flip ($) <$> z)
+        ((&) <$> z)
     === -- Simplify
     select (maybe (Right Nothing) (\bc -> Left $ fmap $ (bc .)) <$> (select (maybe (Right Nothing) Left <$> x)
         ((\ab bc -> (bc .) <$> ab) <$> y)))
-        (flip ($) <$> z)
+        ((&) <$> z)
     === -- Apply F1 to move the pure function into the inner 'select'
     select (select (second (maybe (Right Nothing) (\bc -> Left $ fmap $ (bc .))) <$> maybe (Right Nothing) Left <$> x)
         (((maybe (Right Nothing) (\bc -> Left $ fmap $ (bc .))).) <$> (\ab bc -> (bc .) <$> ab) <$> y))
-        (flip ($) <$> z)
+        ((&) <$> z)
     === -- Simplify, obtaining (#)
     select (select (maybe (Right (Right Nothing)) Left <$> x)
         ((\mbc cd -> maybe (Right Nothing) (\bc -> Left $ fmap ((cd . bc) .)) mbc) <$> y))
-        (flip ($) <$> z)
+        ((&) <$> z)
 
     === -- Righthand side
     x .? (y .? z)
@@ -413,12 +442,11 @@
     === -- Apply F3 to move the rightmost pure function into the outer 'select'
     select (first (flip $ \ab (bc, cd) -> ((cd . bc) .) <$> ab) <$> select (maybe (Right (Right Nothing)) Left <$> x)
         ((\m a -> maybe (Right Nothing) (Left . (,a)) m) <$> y))
-        (flip ($) <$> z)
+        ((&) <$> z)
     === -- Apply F1 to move the pure function into the inner 'select', obtaining (#)
     select (select (maybe (Right (Right Nothing)) Left <$> x)
         ((\mbc cd -> maybe (Right Nothing) (\bc -> Left $ fmap ((cd . bc) .)) mbc) <$> y))
-        (flip ($) <$> z)
-
+        ((&) <$> z)
 
 ------------------------ Carter Schonwald's copatterns -------------------------
 -- See: https://github.com/cartazio/symmetric-monoidal/blob/15b209953b7d4a47651f615b02dbb0171de8af40/src/Control/Monoidal.hs#L93
@@ -480,3 +508,56 @@
 -- Execute a 'FreeArrowChoice' in an arbitrary monad.
 runArrowChoice :: Monad m => (forall i o. f i o -> (i -> m o)) -> FreeArrowChoice f a b -> (a -> m b)
 runArrowChoice f arr = runKleisli $ runFreeArrowChoice arr (Kleisli . f)
+
+-------------------------------- Simplified Haxl -------------------------------
+
+data BlockedRequests
+instance Semigroup BlockedRequests where (<>) x _ = case x of {}
+
+-- A Haxl computation is either completed (Done) or Blocked on pending data requests
+data Result a = Done a | Blocked BlockedRequests (Haxl a) deriving Functor
+newtype Haxl a = Haxl { runHaxl :: IO (Result a) } deriving Functor
+
+instance Applicative Haxl where
+    pure = return
+
+    Haxl iof <*> Haxl iox = Haxl $ do
+        rf <- iof
+        rx <- iox
+        return $ case (rf, rx) of
+            (Done f      , _           ) -> f    <$> rx
+            (_           , Done x      ) -> ($x) <$> rf
+            (Blocked bf f, Blocked bx x) -> Blocked (bf <> bx) (f <*> x) -- parallelism
+
+instance Selective Haxl where
+    select (Haxl iox) (Haxl iof) = Haxl $ do
+        rx <- iox
+        rf <- iof
+        return $ case (rx, rf) of
+            (Done (Right b), _           ) -> Done b -- abandon the second computation
+            (Done (Left  a), _           ) -> ($a) <$> rf
+            (_             , Done       f) -> either f id <$> rx
+            (Blocked bx x  , Blocked bf f) -> Blocked (bx <> bf) (select x f) -- speculative
+                                                                              -- execution
+instance Monad Haxl where
+    return = Haxl . return . Done
+
+    Haxl iox >>= f = Haxl $ do
+        rx <- iox
+        case rx of Done       x -> runHaxl (f x) -- dynamic dependency on runtime value 'x'
+                   Blocked bx x -> return (Blocked bx (x >>= f))
+
+
+
+data C f g a where
+    C :: f x -> g y -> (x -> Either (y -> a) a) -> C f g a
+
+instance Functor (C f g) where
+    fmap f (C p q k) = C p q (fmap (bimap (f.) f) k)
+
+instance (Applicative f, Applicative g) => Applicative (C f g) where
+    pure a = C (pure ()) (pure ()) (const (Left (const a)))
+    C p1 q1 k1 <*> C p2 q2 k2 = C ((,) <$> p1 <*> p2) ((,) <$> q1 <*> q2) $
+        \(x1, x2) -> Left (\(y1, y2) ->
+            (either ($y1) id (k1 x1)) (either ($y2) id (k2 x2)))
+