diff --git a/CHANGES.md b/CHANGES.md
new file mode 100644
--- /dev/null
+++ b/CHANGES.md
@@ -0,0 +1,7 @@
+# Change log
+
+## 0.2
+
+* Make compatible with GHC >= 8.0.2.
+* Add another free construction `Control.Selective.Free`.
+* Add several new `Selective` instances.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,5 +1,8 @@
 # Selective applicative functors
 
+[![Hackage version](https://img.shields.io/hackage/v/selective.svg?label=Hackage)](https://hackage.haskell.org/package/selective) [![Linux & OS X status](https://img.shields.io/travis/snowleopard/selective/master.svg?label=Linux%20%26%20OS%20X)](https://travis-ci.org/snowleopard/selective) [![Windows status](https://img.shields.io/appveyor/ci/snowleopard/selective/master.svg?label=Windows)](https://ci.appveyor.com/project/snowleopard/selective)
+
+
 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).
diff --git a/examples/Processor.hs b/examples/Processor.hs
--- a/examples/Processor.hs
+++ b/examples/Processor.hs
@@ -1,4 +1,5 @@
-{-# LANGUAGE ConstraintKinds, DeriveFunctor, FlexibleContexts, GADTs #-}
+{-# LANGUAGE ConstraintKinds, DeriveFunctor
+             , LambdaCase, FlexibleContexts, FlexibleInstances, GADTs #-}
 module Processor where
 
 import Control.Selective
@@ -7,7 +8,7 @@
 import Data.Int (Int16)
 import Data.Word (Word8)
 import Data.Map.Strict (Map)
-import Prelude hiding (read)
+import Prelude hiding (read, log)
 
 import qualified Control.Monad.State as S
 import qualified Data.Map.Strict     as Map
@@ -32,13 +33,13 @@
 type Value = Int16
 
 -- | The processor has four registers.
-data Reg = R1 | R2 | R3 | R4 deriving (Show, Eq, Ord)
+data Reg = R0 | R1 | R2 | R3 deriving (Show, Eq, Ord)
 
 r0, r1, r2, r3 :: Key
-r0 = Reg R1
-r1 = Reg R2
-r2 = Reg R3
-r3 = Reg R4
+r0 = Reg R0
+r1 = Reg R1
+r2 = Reg R2
+r3 = Reg R3
 
 -- | The register bank maps registers to values.
 type RegisterBank = Map Reg Value
@@ -60,55 +61,79 @@
 -- | Address in the program memory.
 type InstructionAddress = Value
 
+-- | A program execution log entry, recording either a read from a key and the
+-- obtained value, or a write to a key, along with the written value.
+data LogEntry k v where
+    ReadEntry  :: k -> v -> LogEntry k v
+    WriteEntry :: k -> v -> LogEntry k v
+
+-- | A log is a sequence of log entries, in the execution order.
+type Log k v = [LogEntry k v]
+
 -- | The complete processor state.
 data State = State { registers :: RegisterBank
                    , memory    :: Memory
                    , pc        :: InstructionAddress
-                   , flags     :: Flags }
+                   , flags     :: Flags
+                   , log       :: Log Key Value}
 
 -- | Various elements of the processor state.
-data Key = Reg Reg | Cell Address | Flag Flag | PC deriving (Eq, Show)
+data Key = Reg Reg | Cell Address | Flag Flag | PC deriving Eq
 
+instance Show Key where
+    show (Reg r)  = show r
+    show (Cell a) = show a
+    show (Flag f) = show f
+    show PC       = "PC"
+
 -- | The base functor for mutable processor state.
-data RW a = R Key                 (Value -> a)
-          | W Key (Program Value) (Value -> a)
+data RW a = Read  Key                 (Value -> a)
+          | Write Key (Program Value) (Value -> a)
     deriving Functor
 
 -- | A program is a free selective on top of the 'RW' base functor.
 type Program a = Select RW a
 
-instance Show a => Show (RW a) where
-    show (R k          _) = "Read "  ++ show k
-    show (W k (Pure v) _) = "Write " ++ show k ++ " " ++ show v
-    show (W k _        _) = "Write " ++ show k
+instance Show (RW a) where
+    show (Read  k          _) = "Read "  ++ show k
+    show (Write k (Pure v) _) = "Write " ++ show k ++ " " ++ show v
+    show (Write k _        _) = "Write " ++ show k
 
+logEntry :: MonadState State m => LogEntry Key Value -> m ()
+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
-toState (R k t) = t <$> case k of
-    Reg  r    -> (Map.! r   ) <$> S.gets registers
-    Cell addr -> (Map.! addr) <$> S.gets memory
-    Flag f    -> (Map.! f   ) <$> S.gets flags
-    PC        -> pc <$> S.get
-toState (W k p t) = case k of
-    Reg r     -> do v <- runSelect toState p
-                    let regs' s = Map.insert r v (registers s)
-                    S.state (\s -> (t v, s {registers = regs' s}))
-    Cell addr -> do v <- runSelect toState p
-                    let mem' s = Map.insert addr v (memory s)
-                    S.state (\s -> (t v, s {memory = mem' s}))
-    Flag f    -> do v <- runSelect toState p
-                    let flags' s = Map.insert f v (flags s)
-                    S.state (\s -> (t v, s {flags = flags' s}))
-    PC          -> error "toState: Can't write the Program Counter (PC)"
+toState = \case
+    (Read k t) -> do
+        v <- case k of
+                   Reg  r    -> (Map.! r   ) <$> S.gets registers
+                   Cell addr -> (Map.! addr) <$> S.gets memory
+                   Flag f    -> (Map.! f   ) <$> S.gets flags
+                   PC        -> pc <$> S.get
+        logEntry (ReadEntry k v)
+        pure (t v)
+    (Write k p t) -> do
+        v <- runSelect toState p
+        logEntry (WriteEntry k v)
+        case k of
+            Reg r     -> let regs' s = Map.insert r v (registers s)
+                         in  S.state (\s -> (t v, s {registers = regs' s}))
+            Cell addr -> let mem' s = Map.insert addr v (memory s)
+                         in S.state (\s -> (t v, s {memory = mem' s}))
+            Flag f    -> let flags' s = Map.insert f v (flags s)
+                         in S.state (\s -> (t v, s {flags = flags' s}))
+            PC        -> S.state (\s -> (t v, s {pc = v}))
 
 -- | Interpret a program as a state trasformer.
 runProgramState :: Program a -> State -> (a, State)
 runProgramState f = S.runState (runSelect toState f)
 
 -- | Interpret the base functor in the selective functor 'Over'.
-toOver :: RW a -> Over [RW ()] b
-toOver (R k _   ) = Over [void $ R k (const ())]
-toOver (W k fv _) = void (runSelect toOver fv) *> Over [W k fv (const ())]
+toOver :: RW a -> Over [RW ()] a
+toOver (Read  k _   ) = Over [Read k (const ())]
+toOver (Write k fv _) = runSelect toOver fv *> Over [Write k fv (const ())]
 
 -- | Get all possible program effects.
 getProgramEffects :: Program a -> [RW ()]
@@ -116,11 +141,11 @@
 
 -- | A convenient alias for reading an element of the processor state.
 read :: Key -> Program Value
-read k = liftSelect (R k id)
+read k = liftSelect (Read k id)
 
 -- | A convenient alias for writing into an element of the processor state.
 write :: Key -> Program Value -> Program Value
-write k fv = fv *> liftSelect (W k fv id)
+write k fv = liftSelect (Write k fv id)
 
 -- --------------------------------------------------------------------------------
 -- -------- Instructions ----------------------------------------------------------
@@ -164,6 +189,10 @@
         modifyPC = void $ write PC ((+offset) <$> pc)
     in whenS zeroSet modifyPC
 
+-- A block of instructions.
+addAndJump :: Program ()
+addAndJump = add (Reg R1) (Reg R2) (Reg R3) *> jumpZero 42
+
 -----------------------------------
 -- Add with overflow tracking -----
 -----------------------------------
@@ -235,3 +264,51 @@
         o4 = (<) <$> arg1 <*> ((-) <$> pure minBound <*> arg2)
     in  (||) <$> ((&&) <$> o1 <*> o2)
              <*> ((&&) <$> o3 <*> o4)
+
+-----------------------------------
+-- Example simulations ------------
+-----------------------------------
+
+renderState :: State -> String
+renderState state =
+  "Registers: " ++ show (registers state)          ++ "\n" ++
+  "Flags: "     ++ show (Map.toList $ flags state) ++ "\n" ++
+  "Log: "       ++ show (log state)
+
+instance Show State where
+    show = renderState
+
+emptyRegisters :: RegisterBank
+emptyRegisters = Map.fromList [(R0, 0), (R1, 0), (R2, 0), (R3, 0)]
+
+emptyFlags :: Flags
+emptyFlags = Map.fromList $ zip [Zero, Overflow] [0, 0..]
+
+initialiseMemory :: [(Address, Value)] -> Memory
+initialiseMemory m =
+    let blankMemory = Map.fromList $ zip [0..maxBound] [0, 0..]
+    in foldr (\(addr, value) acc -> Map.adjust (const value) addr acc) blankMemory m
+
+boot :: Memory -> State
+boot mem = State { registers = emptyRegisters
+                 , pc = 0
+                 , flags = emptyFlags
+                 , memory = mem
+                 , log   = []
+                 }
+
+twoAdds :: Program Value
+twoAdds = add r0 (Cell 0) r0
+          *>
+          add r0 (Cell 0) r0
+
+addExample :: IO ()
+addExample = do
+    let initState = boot (initialiseMemory [(0, 2)])
+    print . snd $ runProgramState twoAdds initState
+
+---------------------------- Some boilerplate code -----------------------------
+
+instance (Show k, Show v) => Show (LogEntry  k v) where
+    show (ReadEntry k v)  = "Read (" ++ show k ++ ", " ++ show v ++ ")"
+    show (WriteEntry k v) = "Write (" ++ show k ++ ", " ++ show v ++ ")"
diff --git a/selective.cabal b/selective.cabal
--- a/selective.cabal
+++ b/selective.cabal
@@ -1,5 +1,5 @@
 name:          selective
-version:       0.1.0
+version:       0.2
 synopsis:      Selective applicative functors
 license:       MIT
 license-file:  LICENSE
@@ -10,6 +10,11 @@
 category:      Control
 build-type:    Simple
 cabal-version: 1.18
+tested-with:   GHC == 8.0.2,
+               GHC == 8.2.2,
+               GHC == 8.4.3,
+               GHC == 8.6.5,
+               GHC == 8.8.1
 stability:     experimental
 description:   Selective applicative functors: declare your effects statically,
                select which to execute dynamically.
@@ -20,6 +25,7 @@
                <https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf this paper>.
 
 extra-doc-files:
+    CHANGES.md
     README.md
 
 source-repository head
@@ -29,12 +35,20 @@
 library
     hs-source-dirs:     src
     exposed-modules:    Control.Selective,
+                        Control.Selective.Free,
                         Control.Selective.Free.Rigid
     build-depends:      base         >= 4.7     && < 5,
-                        containers   >= 0.5.7.1 && < 7,
-                        mtl          >= 2.2.1   && < 2.3,
-                        transformers >= 0.5.2.0 && < 0.6
+                        containers   >= 0.5.5.1 && < 0.7,
+                        transformers >= 0.4.2.0 && < 0.6
     default-language:   Haskell2010
+    other-extensions:   DeriveFunctor,
+                        FlexibleInstances,
+                        GADTs,
+                        GeneralizedNewtypeDeriving,
+                        RankNTypes,
+                        StandaloneDeriving,
+                        TupleSections,
+                        TypeApplications
     GHC-options:        -Wall
                         -fno-warn-name-shadowing
                         -Wcompat
@@ -44,8 +58,7 @@
 
 test-suite test
     hs-source-dirs:     test, examples
-    other-modules:      ArrowLaws,
-                        Build,
+    other-modules:      Build,
                         Laws,
                         Parser,
                         Processor,
@@ -55,14 +68,13 @@
     type:               exitcode-stdio-1.0
     main-is:            Main.hs
     build-depends:      base                   >= 4.7     && < 5,
-                        checkers,
-                        containers             >= 0.5.7.1 && < 7,
+                        containers             >= 0.5.5.1 && < 0.7,
                         mtl                    >= 2.2.1   && < 2.3,
-                        QuickCheck             >= 2.9     && < 2.13,
+                        QuickCheck             >= 2.8     && < 2.14,
                         selective,
-                        tasty                  >= 1.2,
-                        tasty-expected-failure >= 0.11.1.1,
-                        tasty-quickcheck       >= 0.10
+                        tasty                  >= 0.11,
+                        tasty-expected-failure >= 0.11,
+                        tasty-quickcheck       >= 0.8.4
     default-language:   Haskell2010
     GHC-options:        -Wall
                         -fno-warn-name-shadowing
@@ -70,5 +82,3 @@
                         -Wincomplete-record-updates
                         -Wincomplete-uni-patterns
                         -Wredundant-constraints
-                        -fno-warn-orphans
-                        -fno-warn-missing-signatures
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,5 @@
-{-# LANGUAGE DeriveFunctor, RankNTypes, ScopedTypeVariables, TupleSections #-}
-{-# LANGUAGE DerivingVia, FlexibleInstances, GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE CPP, TupleSections, DeriveFunctor #-}
+{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module     : Control.Selective
@@ -23,19 +23,34 @@
     foldS, anyS, allS, bindS, Cases, casesEnum, cases, matchS, matchM,
 
     -- * Selective functors
-    ViaSelectA (..), Over (..), getOver, Under (..), getUnder, Validation (..),
+    SelectA (..), SelectM (..), Over (..), Under (..), Validation (..)
     ) where
 
 import Control.Applicative
+import Control.Applicative.Lift
 import Control.Arrow
+import Control.Monad.ST
+import Control.Monad.Trans.Cont
 import Control.Monad.Trans.Except
+import Control.Monad.Trans.Identity
+import Control.Monad.Trans.Maybe
 import Control.Monad.Trans.Reader
+import Control.Monad.Trans.RWS
 import Control.Monad.Trans.State
 import Control.Monad.Trans.Writer
 import Data.Bool
+import Data.Functor.Compose
 import Data.Functor.Identity
+import Data.Functor.Product
+import Data.List.NonEmpty
 import Data.Proxy
+import Data.Semigroup (Semigroup (..))
+import GHC.Conc (STM)
 
+import qualified Control.Monad.Trans.RWS.Strict    as S
+import qualified Control.Monad.Trans.State.Strict  as S
+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
@@ -291,35 +306,69 @@
 allS p = foldr ((<&&>) . p) (pure True)
 
 -- | Generalised folding with the short-circuiting behaviour.
-foldS :: (Selective f, Foldable t, Monoid a) => t (f (Either e a)) -> f (Either e a)
+foldS :: (Selective f, Foldable t, Monoid a
+#if !MIN_VERSION_base(4,11,0)
+  , Semigroup a
+#endif
+    ) => t (f (Either e a)) -> f (Either e a)
 foldS = foldr andAlso (pure (Right mempty))
 
 -- Instances
 
--- As a quick experiment, try: ifS (pure True) (print 1) (print 2)
-instance Selective IO where select = selectM
+-- | Any applicative functor can be given a 'Selective' instance by defining
+-- @select = selectA@.
+newtype SelectA f a = SelectA { fromSelectA :: f a }
+    deriving (Functor, Applicative)
 
--- And... we need to write a lot more instances
-instance Selective [] where select = selectM
-instance Selective ((->) a) where select = selectM
-instance Monoid a => Selective ((,) a) where select = selectM
-instance Selective Identity where select = selectM
-instance Selective Maybe where select = selectM
-instance Selective Proxy where select = selectM
+instance Applicative f => Selective (SelectA f) where
+    select = selectA
 
-instance Monad m => Selective (ExceptT s m) where select = selectM
-instance Monad m => Selective (ReaderT s m) where select = selectM
-instance Monad m => Selective (StateT s m) where select = selectM
-instance (Monoid s, Monad m) => Selective (WriterT s m) where select = selectM
+-- Note: Validation e a ~ Lift (Under e) a
+instance Selective f => Selective (Lift f) where
+    select              x   (Pure  y) = either y id <$> x
+    select (Pure (Right x)) _         = Pure x
+    select (Pure (Left  x)) (Other y) = Other $ ($x) <$> y
+    select (Other       x ) (Other y) = Other $   x  <*? y
 
--- | Any applicative functor can be given an instnce of 'Selective' by
--- defining @select = selectA@.
-newtype ViaSelectA f a = ViaSelectA { fromViaSelectA :: f a }
-    deriving (Functor, Applicative)
+-- | Any monad can be given a 'Selective' instance by defining
+-- @select = selectM@.
+newtype SelectM f a = SelectM { fromSelectM :: f a }
+    deriving (Functor, Applicative, Monad)
 
-instance Applicative f => Selective (ViaSelectA f) where
-    select = selectA
+instance Monad f => Selective (SelectM f) where
+    select = selectM
 
+-- | Static analysis of selective functors with over-approximation.
+newtype Over m a = Over { getOver :: m }
+    deriving (Eq, Functor, Ord, Show)
+
+instance Monoid m => Applicative (Over m) where
+    pure _            = Over mempty
+    Over x <*> Over y = Over (mappend x y)
+
+instance Monoid m => Selective (Over m) where
+    select (Over x) (Over y) = Over (mappend x y)
+
+-- | Static analysis of selective functors with under-approximation.
+newtype Under m a = Under { getUnder :: m }
+    deriving (Eq, Functor, Ord, Show)
+
+instance Monoid m => Applicative (Under m) where
+    pure _              = Under mempty
+    Under x <*> Under y = Under (mappend x y)
+
+instance Monoid m => Selective (Under m) where
+    select (Under m) _ = Under m
+
+-- The 'Selective' 'ZipList' instance corresponds to the SIMT execution model.
+-- Quoting https://en.wikipedia.org/wiki/Single_instruction,_multiple_threads:
+--
+-- "...to handle an IF-ELSE block where various threads of a processor execute
+-- different paths, all threads must actually process both paths (as all threads
+-- of a processor always execute in lock-step), but masking is used to disable
+-- 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.
 data Validation e a = Failure e | Success a deriving (Functor, Show)
@@ -336,32 +385,48 @@
     select (Success (Left  a)) f = ($a) <$> f
     select (Failure e        ) _ = Failure e
 
--- | Static analysis of selective functors with over-approximation.
-newtype Over m a = Over m
-    deriving
-        (Functor, Applicative, Selective)
-    via
-        ViaSelectA (Const m)
-    deriving Show
+instance (Selective f, Selective g) => Selective (Product f g) where
+    select (Pair fx gx) (Pair fy gy) = Pair (select fx fy) (select gx gy)
 
--- | Extract the contents of 'Over'.
-getOver :: Over m a -> m
-getOver (Over x) = x
+-- TODO: Is this a useful instance? Note that composition of 'Alternative'
+-- requires @f@ to be 'Alternative', and @g@ to be 'Applicative', which is
+-- opposite to what we have here:
+--
+-- instance (Alternative f, Applicative g) => Alternative (Compose f g) ...
+--
+instance (Applicative f, Selective g) => Selective (Compose f g) where
+    select (Compose x) (Compose y) = Compose (select <$> x <*> y)
 
--- | Static analysis of selective functors with under-approximation.
-newtype Under m a = Under m
-    deriving (Functor, Applicative) via Const m
-    deriving Show
+-- Monad instances
 
-instance Monoid m => Selective (Under m) where
-    select (Under m) _ = Under m
+-- As a quick experiment, try: ifS (pure True) (print 1) (print 2)
+instance Selective IO where select = selectM
 
--- | Extract the contents of 'Under'.
-getUnder :: Under m a -> m
-getUnder (Under x) = x
+-- And... we need to write a lot more instances
+instance             Selective []         where select = selectM
+instance Monoid a => Selective ((,) a)    where select = selectM
+instance             Selective ((->) a)   where select = selectM
+instance             Selective (Either e) where select = selectM
+instance             Selective Identity   where select = selectM
+instance             Selective Maybe      where select = selectM
+instance             Selective NonEmpty   where select = selectM
+instance             Selective Proxy      where select = selectM
+instance             Selective (ST s)     where select = selectM
+instance             Selective STM        where select = selectM
 
------------------------------------- Arrows ------------------------------------
+instance                        Selective (ContT      r m) where select = selectM
+instance            Monad m  => Selective (ExceptT    e m) where select = selectM
+instance            Monad m  => Selective (IdentityT    m) where select = selectM
+instance            Monad m  => Selective (MaybeT       m) where select = selectM
+instance            Monad m  => Selective (ReaderT    r m) where select = selectM
+instance (Monoid w, Monad m) => Selective (RWST   r w s m) where select = selectM
+instance (Monoid w, Monad m) => Selective (S.RWST r w s m) where select = selectM
+instance            Monad m  => Selective (StateT     s m) where select = selectM
+instance            Monad m  => Selective (S.StateT   s m) where select = selectM
+instance (Monoid w, Monad m) => Selective (WriterT    w m) where select = selectM
+instance (Monoid w, Monad m) => Selective (S.WriterT  w m) where select = selectM
 
+------------------------------------ Arrows ------------------------------------
 -- See the following standard definitions in "Control.Arrow".
 -- newtype ArrowMonad a b = ArrowMonad (a () b)
 -- instance Arrow a => Functor (ArrowMonad a)
@@ -372,3 +437,41 @@
 
 toArrow :: Arrow a => ArrowMonad a (b -> c) -> a b c
 toArrow (ArrowMonad f) = arr (\x -> ((), x)) >>> first f >>> arr (uncurry ($))
+
+---------------------------------- Alternative ---------------------------------
+newtype ComposeEither f e a = ComposeEither (f (Either e a))
+    deriving Functor
+
+instance Applicative f => Applicative (ComposeEither f e) where
+    pure a                              = ComposeEither (pure $ Right a)
+    ComposeEither x <*> ComposeEither y = ComposeEither ((<*>) <$> x <*> y)
+
+instance (Selective f, Monoid e
+#if !MIN_VERSION_base(4,11,0)
+  , Semigroup e
+#endif
+    ) => Alternative (ComposeEither f e) where
+    empty                               = ComposeEither (pure $ Left mempty)
+    ComposeEither x <|> ComposeEither y = ComposeEither (x `orElse` y)
+
+{- One could also try implementing 'select' via 'Alternative' as follows:
+
+selectAlt :: Alternative f => f (Either a b) -> f (a -> b) -> f b
+selectAlt x y = failIfLeft x <|> selectA x y
+  where
+    failIfLeft :: Alternative f => f (Either a b) -> f b
+    failIfLeft = undefined
+
+This has two issues:
+
+1) A generic 'failIfLeft' if not possible, although many actual instances should
+   be able to implement it.
+
+2) More importantly, this requires duplication of work: if we failed becauase we
+   happened to parse a 'Left' value in the first parser, then we need to rerun
+   it, obtain a 'Left' once again, and then execute the second parser. Again, a
+   specific instance may be able to cache the result and reuse it without
+   duplicating any work, but this does not seem to be possible to achieve
+   generically for any Alternative.
+
+-}
diff --git a/src/Control/Selective/Free.hs b/src/Control/Selective/Free.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Selective/Free.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE RankNTypes #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module     : Control.Selective.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 selective functors/ using the ideas from the
+-- Sjoerd Visscher's package 'free-functors':
+-- https://hackage.haskell.org/package/free-functors-1.0.1/docs/Data-Functor-HFree.html.
+--
+-----------------------------------------------------------------------------
+module Control.Selective.Free (
+    -- * Free selective functors
+    Select (..), liftSelect,
+
+    -- * Static analysis
+    getPure, getEffects, getNecessaryEffects, runSelect, foldSelect
+    ) where
+
+import Control.Selective
+import Data.Functor
+
+-- | Free selective functors.
+newtype Select f a = Select (forall g. Selective g => (forall x. f x -> g x) -> g a)
+
+instance Functor (Select f) where
+    fmap f (Select x) = Select $ \k -> f <$> x k
+
+instance Applicative (Select f) where
+    pure a                = Select $ \_ -> pure a
+    Select x <*> Select y = Select $ \k -> x k <*> y k
+
+instance Selective (Select f) where
+    select (Select x) (Select y) = Select $ \k -> x k <*? y k
+
+-- | Lift a functor into a free selective computation.
+liftSelect :: f a -> Select f a
+liftSelect x = Select ($x)
+
+-- | Given a natural transformation from @f@ to @g@, this gives a canonical
+-- natural transformation from @Select f@ to @g@. Note that here we rely on the
+-- fact that @g@ is a lawful selective functor.
+runSelect :: Selective g => (forall x. f x -> g x) -> Select f a -> g a
+runSelect k (Select x) = x k
+
+-- | 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 /all necessary effects/ in the order they appear in a free
+-- selective computation.
+getNecessaryEffects :: Functor f => Select f a -> [f ()]
+getNecessaryEffects = getUnder . runSelect (Under . pure . void)
diff --git a/test/ArrowLaws.hs b/test/ArrowLaws.hs
deleted file mode 100644
--- a/test/ArrowLaws.hs
+++ /dev/null
@@ -1,44 +0,0 @@
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE StandaloneDeriving, DerivingVia #-}
-{-# LANGUAGE FlexibleInstances, TupleSections, ExplicitForAll #-}
-
-module ArrowLaws where
-
-import Prelude hiding (maybe)
-import Test.Tasty
-import Test.Tasty.QuickCheck()
-import Test.QuickCheck.Checkers as Checkers
-import Test.QuickCheck.Checkers (EqProp)
-import Test.QuickCheck.Classes as Checkers
-import Control.Selective
-import Laws ()
-
-check :: IO ()
-check = defaultMain $ testGroup "Arrows instances"
-    []
-
------
--- Arrow laws as QuickCheck properties
------
--- | Most of the properties Checkers provide require triples as arguments for the reason that is yet
--- unclear to me. This dummy value is handy to use with -XTypeApplication, like this: labrat @Maybe.
--- Checkers.T is a type alias for Char.
-labrat :: f (Checkers.T, Checkers.T, Checkers.T)
-labrat = undefined
-
-functorLawsMaybe = Checkers.verboseBatch (Checkers.functor (labrat @Maybe))
-
-instance Eq m => EqProp (Over m a) where
-    (Over m1) =-= (Over m2) = Checkers.eq m1 m2
-
--- | Silly Monad instance for 'Over String', used for sanity check of
---   'Checkers.monad'.
-instance Monad (Over String) where
-    (Over _) >>= _ = Over "c"
-
--- | Will fail, since the the provided Monad instance in lawless.
-monadLawsOver = Checkers.verboseBatch (Checkers.monad (labrat @(Over String)))
-
-applicativeLawsOver = Checkers.verboseBatch (Checkers.applicative (labrat @(Over String)))
-
-arrowLawsArrow = Checkers.verboseBatch (Checkers.arrow (labrat @((->) Int)))
diff --git a/test/Laws.hs b/test/Laws.hs
--- a/test/Laws.hs
+++ b/test/Laws.hs
@@ -1,12 +1,11 @@
-{-# LANGUAGE StandaloneDeriving, DerivingVia #-}
-{-# LANGUAGE FlexibleInstances, TupleSections, ExplicitForAll, TypeApplications #-}
-
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances, TupleSections, TypeApplications #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
 module Laws where
 
 import Test.QuickCheck hiding (Failure, Success)
 import Data.Bifunctor (bimap, first, second)
 import Control.Arrow hiding (first, second)
-import Data.Functor.Const
 import Control.Selective
 import Data.Functor.Identity
 import Control.Monad.State
@@ -100,8 +99,9 @@
 --------------------------------------------------------------------------------
 ------------------------ Over --------------------------------------------------
 --------------------------------------------------------------------------------
-deriving instance Eq m => Eq (Over m a)
-deriving via (Const m a) instance Arbitrary m => Arbitrary (Over m a)
+instance Arbitrary a => Arbitrary (Over a b) where
+    arbitrary = Over <$> arbitrary
+    shrink    = map Over . shrink . getOver
 
 propertyPureRightOver :: IO ()
 propertyPureRightOver = quickCheck (propertyPureRight @(Over String) @Int)
@@ -109,8 +109,9 @@
 --------------------------------------------------------------------------------
 ------------------------ Under -------------------------------------------------
 --------------------------------------------------------------------------------
-deriving instance Eq m => Eq (Under m a)
-deriving via (Const m a) instance Arbitrary m => Arbitrary (Under m a)
+instance Arbitrary a => Arbitrary (Under a b) where
+    arbitrary = Under <$> arbitrary
+    shrink    = map Under . shrink . getUnder
 
 propertyPureRightUnder :: IO ()
 propertyPureRightUnder = quickCheck (propertyPureRight @(Under String) @Int)
@@ -120,18 +121,10 @@
 --------------------------------------------------------------------------------
 deriving instance (Eq e, Eq a) => Eq (Validation e a)
 
--- | This is a copy-paste of the 'Arbitrary2' instance for 'Either' defined in
---   the 'Test.QuickCheck.Arbitrary' module. 'Left' is renamed to 'Failure' and
---   'Right' to 'Success'.
-instance Arbitrary2 Validation where
-  liftArbitrary2 arbA arbB = oneof [liftM Failure arbA, liftM Success arbB]
-
-  liftShrink2 shrA _ (Failure x)  = [ Failure  x' | x' <- shrA x ]
-  liftShrink2 _ shrB (Success y) = [ Success y' | y' <- shrB y ]
-
 instance (Arbitrary e, Arbitrary a) => Arbitrary (Validation e a) where
-  arbitrary = arbitrary2
-  shrink = shrink2
+  arbitrary = oneof [liftM Failure arbitrary, liftM Success arbitrary]
+  shrink (Failure x) = [ Failure x' | x' <- shrink x ]
+  shrink (Success y) = [ Success y' | y' <- shrink y ]
 
 --------------------------------------------------------------------------------
 ------------------------ ArrowMonad --------------------------------------------
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -75,6 +75,7 @@
         \x -> lawAssociativity @(Over String) @Int @Int x
     ]
 
+overTheorems :: TestTree
 overTheorems = testGroup "Theorems"
     [ testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $
         \x -> theorem1 @(Over String) @Int @Int x
@@ -90,6 +91,7 @@
         \x -> theorem6 @(Over String) @Int @Int x
     ]
 
+overProperties :: TestTree
 overProperties = testGroup "Properties"
     [ expectFail $
       testProperty "pure-right: pure (Right x) <*? y = pure x" $
@@ -124,8 +126,8 @@
         \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
-    , expectFailBecause "'Under' is a non-rigid selective functor" $
-      testProperty "(f <*> g) == (f `apS` g)" $
+    -- 'Under' is a non-rigid selective functor
+    , 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
@@ -167,11 +169,11 @@
         \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
-    , expectFailBecause "'Validation' is a non-rigid selective functor" $
-      testProperty "(f <*> g) == (f `apS` g)" $
+    -- 'Validation' is a non-rigid selective functor
+    , expectFail $ testProperty "(f <*> g) == (f `apS` g)" $
         \x -> theorem5 @(Validation String) @Int @Int x
-    , expectFailBecause "'Validation' is a non-rigid selective functor" $
-      testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
+    -- 'Validation' is a non-rigid selective functor
+    , expectFail $ testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $
         \x -> theorem6 @(Validation String) @Int @Int @Int x
     ]
 
@@ -207,6 +209,7 @@
 arrowMonad = testGroup "ArrowMonad (->)"
     [arrowMonadLaws, arrowMonadTheorems, arrowMonadProperties]
 
+arrowMonadLaws :: TestTree
 arrowMonadLaws = testGroup "Laws"
     [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $
         \x -> lawIdentity @(ArrowMonad (->)) @Int x
@@ -220,6 +223,7 @@
         \x -> selectALaw @(ArrowMonad (->)) @Int @Int x
     ]
 
+arrowMonadTheorems :: TestTree
 arrowMonadTheorems = testGroup "Theorems"
     [ testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $
         \x -> theorem1 @(ArrowMonad (->)) @Int @Int @Int x
@@ -235,6 +239,7 @@
         \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
@@ -247,6 +252,7 @@
 maybe :: TestTree
 maybe = testGroup "Maybe" [maybeLaws, maybeTheorems, maybeProperties]
 
+maybeLaws :: TestTree
 maybeLaws = testGroup "Laws"
     [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $
         \x -> lawIdentity @Maybe @Int x
@@ -258,6 +264,7 @@
         \x -> lawMonad @Maybe @Int @Int x
     ]
 
+maybeTheorems :: TestTree
 maybeTheorems = testGroup "Theorems"
     [ testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $
         \x -> theorem1 @Maybe @Int @Int @Int x
@@ -273,6 +280,7 @@
         \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
@@ -286,6 +294,7 @@
 identity = testGroup "Identity"
     [identityLaws, identityTheorems, identityProperties]
 
+identityLaws :: TestTree
 identityLaws = testGroup "Laws"
     [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $
         \x -> lawIdentity @Identity @Int x
@@ -297,6 +306,7 @@
         \x -> lawMonad @Identity @Int @Int x
     ]
 
+identityTheorems :: TestTree
 identityTheorems = testGroup "Theorems"
     [ testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $
         \x -> theorem1 @Identity @Int @Int @Int x
@@ -312,6 +322,7 @@
         \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
diff --git a/test/Sketch.hs b/test/Sketch.hs
--- a/test/Sketch.hs
+++ b/test/Sketch.hs
@@ -1,11 +1,16 @@
-{-# LANGUAGE FlexibleInstances, ScopedTypeVariables, TupleSections #-}
+{-# LANGUAGE FlexibleInstances, GADTs, RankNTypes, ScopedTypeVariables, TupleSections #-}
 module Sketch where
 
+import Control.Arrow hiding (first, second)
+import Control.Category (Category)
 import Control.Monad
 import Control.Selective
 import Data.Bifunctor
 import Data.Void
 
+import qualified Control.Arrow    as A
+import qualified Control.Category as C
+
 -- This file contains various examples and proof sketches and we keep it here to
 -- make sure it still compiles.
 
@@ -413,3 +418,65 @@
     select (select (maybe (Right (Right Nothing)) Left <$> x)
         ((\mbc cd -> maybe (Right Nothing) (\bc -> Left $ fmap ((cd . bc) .)) mbc) <$> y))
         (flip ($) <$> z)
+
+
+------------------------ Carter Schonwald's copatterns -------------------------
+-- See: https://github.com/cartazio/symmetric-monoidal/blob/15b209953b7d4a47651f615b02dbb0171de8af40/src/Control/Monoidal.hs#L93
+-- And also: https://twitter.com/andreymokhov/status/1102648479841701888
+
+data Choose a b c where
+    CLeft  :: Choose a b a
+    CRight :: Choose a b b
+
+newtype Choice a b = Choice (forall r . Choose a b r -> r)
+
+class SelectiveC f where
+    choose :: f (Either a b) -> Choice (f (a -> c)) (f (b -> c)) -> f c
+
+-- Recover selective 'branch' from 'choose'.
+branchC :: SelectiveC f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
+branchC x l r = choose x $ Choice $ \c -> case c of { CLeft -> l; CRight -> r }
+
+-- Recover 'choose' from selective 'branch'.
+chooseS :: Selective f => f (Either a b) -> Choice (f (a -> c)) (f (b -> c)) -> f c
+chooseS x (Choice c) = branch x (c CLeft) (c CRight)
+
+------------------------------- Free ArrowChoice -------------------------------
+
+-- A free 'ArrowChoice' built on top of base components @f i o@.
+newtype FreeArrowChoice f a b = FreeArrowChoice {
+    runFreeArrowChoice :: forall arr. ArrowChoice arr =>
+        (forall i o. f i o -> arr i o) -> arr a b }
+
+instance Category (FreeArrowChoice f) where
+    id = FreeArrowChoice (\_ -> C.id)
+    FreeArrowChoice x . FreeArrowChoice y = FreeArrowChoice (\t -> x t C.. y t)
+
+instance Arrow (FreeArrowChoice f) where
+    arr x = FreeArrowChoice (\_ -> A.arr x)
+    first (FreeArrowChoice x) = FreeArrowChoice (\t -> A.first (x t))
+
+instance ArrowChoice (FreeArrowChoice f) where
+    left (FreeArrowChoice x) = FreeArrowChoice (\t -> A.left (x t))
+
+-- A constant arrow, similar to the 'Const' applicative functor.
+newtype ConstArrow m a b = ConstArrow { getConstArrow :: m }
+
+instance Monoid m => Category (ConstArrow m) where
+    id = ConstArrow mempty
+    ConstArrow x . ConstArrow y = ConstArrow (mappend x y)
+
+instance Monoid m => Arrow (ConstArrow m) where
+    arr _ = ConstArrow mempty
+    first (ConstArrow x) = ConstArrow x
+
+instance Monoid m => ArrowChoice (ConstArrow m) where
+    left (ConstArrow x) = ConstArrow x
+
+-- Collect all base arrows in a 'FreeArrowChoice'.
+foldArrowChoice :: Monoid m => (forall i o. f i o -> m) -> FreeArrowChoice f a b -> m
+foldArrowChoice f arr = getConstArrow $ runFreeArrowChoice arr (ConstArrow . f)
+
+-- 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)