selective (empty) → 0.1.0

raw patch · 14 files changed

+2358/−0 lines, 14 filesdep +QuickCheckdep +basedep +checkers

Dependencies added: QuickCheck, base, checkers, containers, mtl, selective, tasty, tasty-expected-failure, tasty-quickcheck, transformers

Files

• LICENSE +21/−0
• README.md +305/−0
• examples/Build.hs +111/−0
• examples/Parser.hs +65/−0
• examples/Processor.hs +237/−0
• examples/Teletype.hs +72/−0
• examples/Validation.hs +40/−0
• selective.cabal +74/−0
• src/Control/Selective.hs +374/−0
• src/Control/Selective/Free/Rigid.hs +121/−0
• test/ArrowLaws.hs +44/−0
• test/Laws.hs +159/−0
• test/Main.hs +320/−0
• test/Sketch.hs +415/−0

@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2018 Andrey Mokhov++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.

@@ -0,0 +1,305 @@+# Selective applicative functors++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).++Abstract of the paper:++Applicative functors and monads have conquered the world of functional programming by+providing general and powerful ways of describing effectful computations using pure+functions. Applicative functors provide a way to compose *independent effects* that+cannot depend on values produced by earlier computations, and all of which are declared+statically. Monads extend the applicative interface by making it possible to compose+*dependent effects*, where the value computed by one effect determines all subsequent+effects, dynamically.++This paper introduces an intermediate abstraction called *selective applicative functors*+that requires all effects to be declared statically, but provides a way to select which+of the effects to execute dynamically. We demonstrate applications of the new+abstraction on several examples, including two real-life case studies.+++## What are selective functors?++While you're encouraged to read the paper, here is a brief description of+the main idea. Consider the following new type class introduced between+`Applicative` and `Monad`:++```haskell+class Applicative f => Selective f where+    select :: f (Either a b) -> f (a -> b) -> f b++-- | An operator alias for 'select'.+(<*?) :: Selective f => f (Either a b) -> f (a -> b) -> f b+(<*?) = select++infixl 4 <*?+```++Think of `select` as a *selective function application*: you **must apply** the function+of type `a -> b` when given a value of type `Left a`, but you **may skip** the+function and associated effects, and simply return `b` when given `Right b`.++Note that you can write a function with this type signature using+`Applicative` functors, but it will always execute the effects associated+with the second argument, hence being potentially less efficient:++```haskell+selectA :: Applicative f => f (Either a b) -> f (a -> b) -> f b+selectA x f = (\e f -> either f id e) <$> x <*> f+```++Any `Applicative` instance can thus be given a corresponding `Selective`+instance simply by defining `select = selectA`. The opposite is also true+in the sense that one can recover the operator `<*>` from `select` as+follows (I'll use the suffix `S` to denote `Selective` equivalents of+commonly known functions).++```haskell+apS :: Selective f => f (a -> b) -> f a -> f b+apS f x = select (Left <$> f) (flip ($) <$> x)+```++Here we wrap a given function `a -> b` into `Left` and turn the value `a`+into a function `($a)`, which simply feeds itself to the function `a -> b`+yielding `b` as desired. Note: `apS` is a perfectly legal+application operator `<*>`, i.e. it satisfies the laws dictated by the+`Applicative` type class as long as [the laws](#laws) of the `Selective`+type class hold.++The `branch` function is a natural generalisation of `select`: instead of+skipping an unnecessary effect, it chooses which of the two given effectful+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!).++```haskell+branch :: Selective f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c+branch = ... -- Try to figure out the implementation!+```++Finally, any `Monad` is `Selective`:++```haskell+selectM :: Monad f => f (Either a b) -> f (a -> b) -> f b+selectM mx mf = do+    x <- mx+    case x of+        Left  a -> fmap ($a) mf+        Right b -> pure b+```++Selective functors are sufficient for implementing many conditional constructs,+which traditionally require the (more powerful) `Monad` type class. For example:++```haskell+-- | Branch on a Boolean value, skipping unnecessary effects.+ifS :: Selective f => f Bool -> f a -> f a -> f a+ifS i t e = branch (bool (Right ()) (Left ()) <$> i) (const <$> t) (const <$> e)++-- | Conditionally perform an effect.+whenS :: Selective f => f Bool -> f () -> f ()+whenS x act = ifS x act (pure ())++-- | Keep checking an effectful condition while it holds.+whileS :: Selective f => f Bool -> f ()+whileS act = whenS act (whileS act)++-- | A lifted version of lazy Boolean OR.+(<||>) :: Selective f => f Bool -> f Bool -> f Bool+(<||>) a b = ifS a (pure True) b++-- | A lifted version of 'any'. Retains the short-circuiting behaviour.+anyS :: Selective f => (a -> f Bool) -> [a] -> f Bool+anyS p = foldr ((<||>) . p) (pure False)++-- | Return the first @Right@ value. If both are @Left@'s, accumulate errors.+orElse :: (Selective f, Semigroup e) => f (Either e a) -> f (Either e a) -> f (Either e a)+orElse x = select (Right <$> x) . fmap (\y e -> first (e <>) y)+```++See more examples in [src/Control/Selective.hs](src/Control/Selective.hs).++Code written using selective combinators can be both statically analysed+(by reporting all possible effects of a computation) and efficiently+executed (by skipping unnecessary effects).++## Laws++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. ++* Identity:+    ```haskell+    x <*? pure id = either id id <$> x+    ```++* Distributivity (note that `y` and `z` have the same type `f (a -> b)`):+    ```haskell+    pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z)+    ```+* Associativity:+    ```haskell+    x <*? (y <*? z) = (f <$> x) <*? (g <$> y) <*? (h <$> z)+      where+        f x = Right <$> x+        g y = \a -> bimap (,a) ($a) y+        h z = uncurry z+    ```+* Monadic select (for selective functors that are also monads):+    ```haskell+    select = selectM+    ```++There are also a few useful theorems:++* Apply a pure function to the result:+    ```haskell+    f <$> select x y = select (fmap f <$> x) (fmap f <$> y)+    ```++* Apply a pure function to the `Left` case of the first argument:+    ```haskell+    select (first f <$> x) y = select x ((. f) <$> y)+    ```++* Apply a pure function to the second argument:+    ```haskell+    select x (f <$> y) = select (first (flip f) <$> x) (flip ($) <$> y)+    ```++* Generalised identity:+    ```haskell+    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:+    ```haskell+    x *> (y <*? z) = (x *> y) <*? z+    ```++Note that there are no laws for selective application of a function to a pure+`Left` or `Right` value, i.e. we do not require that the following laws hold:++```haskell+select (pure (Left  x)) y = ($x) <$> y -- Pure-Left+select (pure (Right x)) y = pure x     -- Pure-Right+```++In particular, the following is allowed too:++```haskell+select (pure (Left  x)) y = pure ()       -- when y :: f (a -> ())+select (pure (Right x)) y = const x <$> y+```++We therefore allow `select` to be selective about effects in these cases, which+in practice allows to under- or over-approximate possible effects in static+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` +properties now hold.++## Static analysis of selective functors++Like applicative functors, selective functors can be analysed statically.+We can make the `Const` functor an instance of `Selective` as follows.++```haskell+instance Monoid m => Selective (Const m) where+    select = selectA+```++Although we don't need the function `Const m (a -> b)` (note that+`Const m (Either a b)` holds no values of type `a`), we choose to+accumulate the effects associated with it. This allows us to extract+the static structure of any selective computation very similarly+to how this is done with applicative computations.++The `Validation` instance is perhaps a bit more interesting.++```haskell+data Validation e a = Failure e | Success a deriving (Functor, Show)++instance Semigroup e => Applicative (Validation e) where+    pure = Success+    Failure e1 <*> Failure e2 = Failure (e1 <> e2)+    Failure e1 <*> Success _  = Failure e1+    Success _  <*> Failure e2 = Failure e2+    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 = Success ($a) <*> f+    select (Failure e        ) _ = Failure e+```++Here, the last line is particularly interesting: unlike the `Const`+instance, we choose to actually skip the function effect in case of+`Failure`. This allows us not to report any validation errors which+are hidden behind a failed conditional.++Let's clarify this with an example. Here we define a function to+construct a `Shape` (a circle or a rectangle) given a choice of the+shape `s` and the shape's parameters (`r`, `w`, `h`) in a selective+context `f`.++```haskell+type Radius = Int+type Width  = Int+type Height = Int++data Shape = Circle Radius | Rectangle Width Height deriving Show++shape :: Selective f => f Bool -> f Radius -> f Width -> f Height -> f Shape+shape s r w h = ifS s (Circle <$> r) (Rectangle <$> w <*> h)+```++We choose `f = Validation [String]` to report the errors that occurred+when parsing a value. Let's see how it works.++```haskell+> shape (Success True) (Success 10) (Failure ["no width"]) (Failure ["no height"])+Success (Circle 10)++> shape (Success False) (Failure ["no radius"]) (Success 20) (Success 30)+Success (Rectangle 20 30)++> shape (Success False) (Failure ["no radius"]) (Success 20) (Failure ["no height"])+Failure ["no height"]++> shape (Success False) (Failure ["no radius"]) (Failure ["no width"]) (Failure ["no height"])+Failure ["no width","no height"]++> shape (Failure ["no choice"]) (Failure ["no radius"]) (Success 20) (Failure ["no height"])+Failure ["no choice"]+```++In the last example, since we failed to parse which shape has been chosen,+we do not report any subsequent errors. But it doesn't mean we are short-circuiting+the validation. We will continue accumulating errors as soon as we get out of the+opaque conditional, as demonstrated below.++```haskell+twoShapes :: Selective f => f Shape -> f Shape -> f (Shape, Shape)+twoShapes s1 s2 = (,) <$> s1 <*> s2++> s1 = shape (Failure ["no choice 1"]) (Failure ["no radius 1"]) (Success 20) (Failure ["no height 1"])+> s2 = shape (Success False) (Failure ["no radius 2"]) (Success 20) (Failure ["no height 2"])+> twoShapes s1 s2+Failure ["no choice 1","no height 2"]+```++## Do we still need monads?++Yes! Here is what selective functors cannot do: `join :: Selective f => f (f a) -> f a`.++## Further reading++* A paper introducing selective functors: https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf.+* An older blog post introducing selective functors: https://blogs.ncl.ac.uk/andreymokhov/selective.

@@ -0,0 +1,111 @@+{-# LANGUAGE ConstraintKinds, DeriveFunctor, FlexibleInstances, GADTs, RankNTypes #-}+module Build where++import Control.Selective+import Control.Selective.Free.Rigid++-- See Section 3 of the paper:+-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf++-- | Selective build tasks.+-- See "Build Systems à la Carte": https://dl.acm.org/citation.cfm?id=3236774.+newtype Task k v = Task { run :: forall f. Selective f => (k -> f v) -> f v }++-- | Selective build scripts.+type Script k v = k -> Maybe (Task k v)++-- | Build dependencies with over-appriximation.+dependenciesOver :: Task k v -> [k]+dependenciesOver task = getOver $ run task (\k -> Over [k])++-- | Build dependencies with under-appriximation.+dependenciesUnder :: Task k v -> [k]+dependenciesUnder task = getUnder $ run task (\k -> Under [k])++-- | A build script with a static dependency cycle, which always resolves into+-- an acyclic dependency graph in runtime.+--+-- @+-- 'dependenciesOver'  ('fromJust' $ 'cyclic' "B1") == ["C1","B2","A2"]+-- 'dependenciesOver'  ('fromJust' $ 'cyclic' "B2") == ["C1","A1","B1"]+-- 'dependenciesUnder' ('fromJust' $ 'cyclic' "B1") == ["C1"]+-- 'dependenciesUnder' ('fromJust' $ 'cyclic' "B2") == ["C1"]+-- @+cyclic :: Script String Integer+cyclic "B1" = Just $ Task $ \fetch -> ifS ((1==) <$> fetch "C1") (fetch "B2") (fetch "A2")+cyclic "B2" = Just $ Task $ \fetch -> ifS ((1==) <$> fetch "C1") (fetch "A1") (fetch "B1")+cyclic _    = Nothing++-- | A build task demonstrating the use of 'bindS'.+--+-- @+-- 'dependenciesOver'  'taskBind' == ["A1","A2","C5","C6","D5","D6"]+-- 'dependenciesUnder' 'taskBind' == ["A1"]+-- @+taskBind :: Task String Integer+taskBind = Task $ \fetch -> (odd <$> fetch "A1") `bindS` \x ->+                            (odd <$> fetch "A2") `bindS` \y ->+                                let c = if x then "C" else "D"+                                    n = if y then "5" else "6"+                                in fetch (c ++ n)++data Key = A Int | B Int | C Int Int deriving (Eq, Show)++editDistance :: Script Key Int+editDistance (C i 0) = Just $ Task $ const $ pure i+editDistance (C 0 j) = Just $ Task $ const $ pure j+editDistance (C i j) = Just $ Task $ \fetch ->+    ((==) <$> fetch (A i) <*> fetch (B j)) `bindS` \equals ->+        if equals+            then fetch (C (i - 1) (j - 1))+            else (\insert delete replace -> 1 + minimum [insert, delete, replace])+                 <$> fetch (C  i      (j - 1))+                 <*> fetch (C (i - 1)  j     )+                 <*> fetch (C (i - 1) (j - 1))+editDistance _ = Nothing++-- | Example from the paper: a mock for the @tar@ archiving utility.+tar :: Applicative f => [f String] -> f String+tar xs = concat <$> sequenceA xs++-- | Example from the paper: a mock for the configuration parser.+parse :: Functor f => f String -> f Bool+parse = fmap null++-- | Example from the paper: a mock for the OCaml compiler parser.+compile :: Applicative f => [f String] -> f String+compile xs = concat <$> sequenceA xs++-- | Example from the paper.+script :: Script FilePath String+script "release.tar" = Just $ Task $ \fetch -> tar [fetch "LICENSE", fetch "exe"]+script "exe" = Just $ Task $ \fetch ->+    let src   = fetch "src.ml"+        cfg   = fetch "config"+        libc  = fetch "lib.c"+        libml = fetch "lib.ml"+    in compile [src, ifS (parse cfg) libc libml]+script _ = Nothing++--------------------------------- Free example ---------------------------------++-- | Base functor for a free build system.+data Fetch k v a = Fetch k (v -> a) deriving Functor++instance Eq k => Eq (Fetch k v ()) where+    Fetch x _ == Fetch y _ = (x == y)++instance Show k => Show (Fetch k v a) where+    show (Fetch k _) = "Fetch " ++ show k++-- | A convenient alias.+fetch :: k -> Select (Fetch k v) v+fetch key = liftSelect $ Fetch key id++-- | Analyse a build task via free selective functors.+--+-- @+-- runBuild (fromJust $ cyclic "B1") == [Fetch "C1" (const ()),Fetch "B2",Fetch "A2"]+-- @+runBuild :: Task k v -> [Fetch k v ()]+runBuild task = getEffects (run task fetch)

@@ -0,0 +1,65 @@+{-# LANGUAGE ConstraintKinds, DeriveFunctor, GADTs, RankNTypes #-}+module Parser where++import Control.Applicative+import Control.Monad+import Control.Selective++-- See Section 7.2 of the paper:+-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf++newtype Parser a = Parser { parse :: String -> [(a, String)] }++instance Functor Parser where+    fmap f p = Parser $ \x -> [ (f a, s) | (a, s) <- parse p x ]++instance Applicative Parser where+    pure a = Parser $ \s -> [(a, s)]+    (<*>)  = ap++instance Alternative Parser where+    empty   = Parser $ \_ -> []+    p <|> q = Parser $ \s -> parse p s ++ parse q s++instance Selective Parser where+    select = selectM++instance Monad Parser where+    return = pure+    p >>= f = Parser $ \x -> concat [ parse (f a) y | (a, y) <- parse p x ]++class MonadZero f where+    zero :: f a++instance MonadZero Parser where+    zero = Parser (\_ -> [])++item :: Parser Char+item = Parser $ \s -> case s of+    ""    -> []+    (c:cs) -> [(c,cs)]++sat :: (Char -> Bool) -> Parser Char+sat p = do { c <- item; if p c then return c else zero }++char :: Char -> Parser Char+char c = sat (==c)++string :: String -> Parser String+string []     = return ""+string (c:cs) = do+    _ <- char c+    _ <- string cs+    return (c:cs)++bin :: Parser Int+bin = undefined++hex :: Parser Int+hex = undefined++numberA :: Parser Int+numberA = (string "0b" *> bin) <|> (string "0x" *> hex)++numberS :: Parser Int+numberS = string "0" *> ifS (('b'==) <$> sat (`elem` "bx")) bin hex

@@ -0,0 +1,237 @@+{-# LANGUAGE ConstraintKinds, DeriveFunctor, FlexibleContexts, GADTs #-}+module Processor where++import Control.Selective+import Control.Selective.Free.Rigid+import Data.Functor+import Data.Int (Int16)+import Data.Word (Word8)+import Data.Map.Strict (Map)+import Prelude hiding (read)++import qualified Control.Monad.State as S+import qualified Data.Map.Strict     as Map++-- See Section 5.3 of the paper:+-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf+-- Note that we have changed the naming.++-- | Hijack @mtl@'s 'MonadState' constraint to include Selective.+type MonadState s m = (Selective m, S.MonadState s m)++-- | Convert a 'Bool' to @0@ or @1@.+fromBool :: Num a => Bool -> a+fromBool True  = 1+fromBool False = 0++--------------------------------------------------------------------------------+-------- Types -----------------------------------------------------------------+--------------------------------------------------------------------------------++-- | All values are signed 16-bit words.+type Value = Int16++-- | The processor has four registers.+data Reg = R1 | R2 | R3 | R4 deriving (Show, Eq, Ord)++r0, r1, r2, r3 :: Key+r0 = Reg R1+r1 = Reg R2+r2 = Reg R3+r3 = Reg R4++-- | The register bank maps registers to values.+type RegisterBank = Map Reg Value++-- | The address space is indexed by one byte.+type Address = Word8++-- | The memory maps addresses to signed 16-bit words.+type Memory = Map.Map Address Value++-- | The processor has two status flags.+data Flag = Zero     -- ^ tracks if the result of the last arithmetical operation was zero+          | Overflow -- ^ tracks integer overflow+    deriving (Show, Eq, Ord)++-- | A flag assignment.+type Flags = Map.Map Flag Value++-- | Address in the program memory.+type InstructionAddress = Value++-- | The complete processor state.+data State = State { registers :: RegisterBank+                   , memory    :: Memory+                   , pc        :: InstructionAddress+                   , flags     :: Flags }++-- | Various elements of the processor state.+data Key = Reg Reg | Cell Address | Flag Flag | PC deriving (Eq, Show)++-- | The base functor for mutable processor state.+data RW a = R Key                 (Value -> a)+          | W 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++-- | 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)"++-- | 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 ())]++-- | Get all possible program effects.+getProgramEffects :: Program a -> [RW ()]+getProgramEffects = getOver . runSelect toOver++-- | A convenient alias for reading an element of the processor state.+read :: Key -> Program Value+read k = liftSelect (R 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)++-- --------------------------------------------------------------------------------+-- -------- 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++-- | 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)++-----------------+-- jumpZero -----+-----------------+jumpZero :: Value -> Program ()+jumpZero offset =+    let pc       = read PC+        zeroSet  = (==1) <$> read (Flag Zero)+        modifyPC = void $ write PC ((+offset) <$> pc)+    in whenS zeroSet modifyPC++-----------------------------------+-- Add with overflow tracking -----+-----------------------------------++{-  The following example demonstrates how important it is to be aware of your+    effects.++    Problem: implement the semantics of the @add@ instruction which calculates+    the sum of two values and writes it to the specified destination, updates+    the 'Zero' flag if the result is zero, and also detects if integer overflow+    has occurred, updating the 'Overflow' flag accordingly.++    We'll take a look at two approaches that implement this semantics and see+    the crucial deference between them.+-}++-- | Add two values and detect integer overflow.+--+-- The interesting bit here is the call to the 'willOverflowPure' function.+-- Since the function is pure, the call @willOverflowPure <$> arg1 <*> arg2@+-- triggers only one 'read' of @arg1@ and @arg2@, even though we use the+-- variables many times in the 'willOverflowPure' implementation. Thus,+-- 'willOverflowPure' might be thought as an atomic processor microcommand.+addOverflow :: Key -> Key -> Key -> Program Value+addOverflow x y z =+    let arg1     = read x+        arg2     = read y+        result   = (+)   <$> arg1   <*> arg2+        isZero   = (==0) <$> write z result+        overflow = willOverflowPure <$> arg1 <*> arg2+    in write (Flag Zero)     (fromBool <$> isZero) *>+       write (Flag Overflow) (fromBool <$> overflow)++-- | A pure check for integer overflow during addition.+willOverflowPure :: Value -> Value -> Bool+willOverflowPure x y =+    let o1 = (>) y 0+        o2 = (>) x((-) maxBound y)+        o3 = (<) y 0+        o4 = (<) x((-) minBound y)+    in  (||) ((&&) o1 o2)+             ((&&) o3 o4)++-- | Add two values and detect integer overflow.+--+-- In this implementations we take a different approach and, when implementing+-- 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+        arg2   = read y+        result = (+)   <$> arg1 <*> arg2+        isZero = (==0) <$> write z result+        overflow = willOverflow arg1 arg2+    in write (Flag Zero)     (fromBool <$> isZero) *>+       write (Flag Overflow) (fromBool <$> overflow)++-- | An 'Applicative' check for integer overflow during addition.+willOverflow :: Program Value -> Program Value -> Program Bool+willOverflow arg1 arg2 =+    let o1 = (>) <$> arg2 <*> pure 0+        o2 = (>) <$> arg1 <*> ((-) <$> pure maxBound <*> arg2)+        o3 = (<) <$> arg2 <*> pure 0+        o4 = (<) <$> arg1 <*> ((-) <$> pure minBound <*> arg2)+    in  (||) <$> ((&&) <$> o1 <*> o2)+             <*> ((&&) <$> o3 <*> o4)

@@ -0,0 +1,72 @@+{-# LANGUAGE DeriveFunctor, FlexibleInstances, GADTs #-}+module Teletype where++import Prelude hiding (getLine, putStrLn)+import qualified Prelude as IO+import Control.Selective+import Control.Selective.Free.Rigid++-- 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 example from the paper's intro implemented using the free selective.+-- It can be statically analysed for effects:+--+-- @+-- > 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. Can be executed, 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.+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)

@@ -0,0 +1,40 @@+{-# LANGUAGE ConstraintKinds, DeriveFunctor, GADTs, RankNTypes #-}+module Validation where++import Control.Selective++-- See Section 2.2 of the paper:+-- https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf++type Radius = Word+type Width  = Word+type Height = Word++-- | A circle or rectangle.+data Shape = Circle Radius | Rectangle Width Height deriving (Eq, Show)++-- Some validation examples:+--+-- > shape (Success True) (Success 1) (Failure ["width?"]) (Failure ["height?"])+-- > Success (Circle 1)+--+-- > shape (Success False) (Failure ["radius?"]) (Success 2) (Success 3)+-- > Success (Rectangle 2 3)+--+-- > shape (Success False) (Failure ["radius?"]) (Success 2) (Failure ["height?"])+-- > Failure ["height?"]+--+-- > shape (Success False) (Success 1) (Failure ["width?"]) (Failure ["height?"])+-- > Failure ["width?", "height?"]+--+-- > shape (Failure ["choice?"]) (Failure ["radius?"]) (Success 2) (Failure ["height?"])+-- > Failure ["choice?"]+shape :: Selective f => f Bool -> f Radius -> f Width -> f Height -> f Shape+shape s r w h = ifS s (Circle <$> r) (Rectangle <$> w <*> h)++-- > s1 = shape (Failure ["choice 1?"]) (Success 1) (Failure ["width 1?"]) (Success 3)+-- > s2 = shape (Success False) (Success 1) (Success 2) (Failure ["height 2?"])+-- > twoShapes s1 s2+-- > Failure ["choice 1?","height 2?"]+twoShapes :: Selective f => f Shape -> f Shape -> f (Shape, Shape)+twoShapes s1 s2 = (,) <$> s1 <*> s2

@@ -0,0 +1,74 @@+name:          selective+version:       0.1.0+synopsis:      Selective applicative functors+license:       MIT+license-file:  LICENSE+author:        Andrey Mokhov <andrey.mokhov@gmail.com>, github: @snowleopard+maintainer:    Andrey Mokhov <andrey.mokhov@gmail.com>, github: @snowleopard+copyright:     Andrey Mokhov, 2018-2019+homepage:      https://github.com/snowleopard/selective+category:      Control+build-type:    Simple+cabal-version: 1.18+stability:     experimental+description:   Selective applicative functors: declare your effects statically,+               select which to execute dynamically.+               .+               This is a library for /selective applicative functors/, or just+               /selective functors/ for short, an abstraction between+               applicative functors and monads, introduced in+               <https://www.staff.ncl.ac.uk/andrey.mokhov/selective-functors.pdf this paper>.++extra-doc-files:+    README.md++source-repository head+    type:     git+    location: https://github.com/snowleopard/selective.git++library+    hs-source-dirs:     src+    exposed-modules:    Control.Selective,+                        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+    default-language:   Haskell2010+    GHC-options:        -Wall+                        -fno-warn-name-shadowing+                        -Wcompat+                        -Wincomplete-record-updates+                        -Wincomplete-uni-patterns+                        -Wredundant-constraints++test-suite test+    hs-source-dirs:     test, examples+    other-modules:      ArrowLaws,+                        Build,+                        Laws,+                        Parser,+                        Processor,+                        Sketch,+                        Teletype,+                        Validation+    type:               exitcode-stdio-1.0+    main-is:            Main.hs+    build-depends:      base                   >= 4.7     && < 5,+                        checkers,+                        containers             >= 0.5.7.1 && < 7,+                        mtl                    >= 2.2.1   && < 2.3,+                        QuickCheck             >= 2.9     && < 2.13,+                        selective,+                        tasty                  >= 1.2,+                        tasty-expected-failure >= 0.11.1.1,+                        tasty-quickcheck       >= 0.10+    default-language:   Haskell2010+    GHC-options:        -Wall+                        -fno-warn-name-shadowing+                        -Wcompat+                        -Wincomplete-record-updates+                        -Wincomplete-uni-patterns+                        -Wredundant-constraints+                        -fno-warn-orphans+                        -fno-warn-missing-signatures

@@ -0,0 +1,374 @@+{-# LANGUAGE DeriveFunctor, RankNTypes, ScopedTypeVariables, TupleSections #-}+{-# LANGUAGE DerivingVia, FlexibleInstances, GeneralizedNewtypeDeriving #-}+-----------------------------------------------------------------------------+-- |+-- Module     : Control.Selective+-- 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.+--+-----------------------------------------------------------------------------+module Control.Selective (+    -- * Type class+    Selective (..), (<*?), branch, selectA, apS, selectM,++    -- * Conditional combinators+    ifS, whenS, fromMaybeS, orElse, andAlso, untilRight, whileS, (<||>), (<&&>),+    foldS, anyS, allS, bindS, Cases, casesEnum, cases, matchS, matchM,++    -- * Selective functors+    ViaSelectA (..), Over (..), getOver, Under (..), getUnder, Validation (..),+    ) where++import Control.Applicative+import Control.Arrow+import Control.Monad.Trans.Except+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State+import Control.Monad.Trans.Writer+import Data.Bool+import Data.Functor.Identity+import Data.Proxy++-- | 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@.+--+-- 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?+-- Typically, when executing a selective computation, you would want to skip the+-- effects (saving work); but on the other hand, if your goal is to statically+-- analyse a given selective computation and extract the set of all possible+-- effects (without actually executing them), then you do not want to skip any+-- effects, because that defeats the purpose of static analysis.+--+-- The type signature of 'select' is reminiscent of both '<*>' and '>>=', and+-- indeed a selective functor is in some sense a composition of an applicative+-- functor and the 'Either' monad.+--+-- Laws:+--+-- * Identity:+--+-- @+-- x \<*? pure id = either id id \<$\> x+-- @+--+-- * Distributivity; note that @y@ and @z@ have the same type @f (a -> b)@:+--+-- @+-- pure x \<*? (y *\> z) = (pure x \<*? y) *\> (pure x \<*? z)+-- @+--+-- * Associativity:+--+-- @+-- x \<*? (y \<*? z) = (f \<$\> x) \<*? (g \<$\> y) \<*? (h \<$\> z)+--   where+--     f x = Right \<$\> x+--     g y = \a -\> bimap (,a) ($a) y+--     h z = uncurry z+-- @+--+-- * Monadic @select@ (for selective functors that are also monads):+--+-- @+-- select = selectM+-- @+--+-- There are also a few useful theorems:+--+-- * Apply a pure function to the result:+--+-- @+-- f \<$\> select x y = select (fmap f \<$\> x) (fmap f \<$\> y)+-- @+--+-- * Apply a pure function to the @Left@ case of the first argument:+--+-- @+-- select (first f \<$\> x) y = select x ((. f) \<$\> y)+-- @+--+-- * Apply a pure function to the second argument:+--+-- @+-- select x (f \<$\> y) = select (first (flip f) \<$\> x) (flip ($) \<$\> y)+-- @+--+-- * Generalised identity:+--+-- @+-- 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:+--+-- @+-- x *\> (y \<*? z) = (x *\> y) \<*? z+-- @+--+-- If f is also a 'Monad', we require that 'select' = 'selectM', from which one+-- 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.+-- The value on the right, however, may be skipped, hence the question mark.+(<*?) :: Selective f => f (Either a b) -> f (a -> b) -> f b+(<*?) = select++infixl 4 <*?++-- | The 'branch' function is a natural generalisation of 'select': instead of+-- skipping an unnecessary effect, it chooses which of the two given effectful+-- 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:+-- selectB :: Selective f => f (Either a b) -> f (a -> b) -> f b+-- selectB x y = branch x y (pure id)++-- | We can write a function with the type signature of 'select' using the+-- 'Applicative' type class, but it will always execute the effects associated+-- with the second argument, hence being potentially less efficient.+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+applicative functor satisfies all laws of 'Applicative':++* Identity:++    > pure id <*> v = v++* Homomorphism:++    > pure f <*> pure x = pure (f x)++* Interchange:++    > u <*> pure y = pure ($y) <*> u++* Composition:++    > (.) <$> u <*> v <*> w = u <*> (v <*> w)+-}+apS :: Selective f => f (a -> b) -> f a -> f b+apS f x = select (Left <$> f) (flip ($) <$> x)++-- | One can easily implement a monadic 'selectM' that satisfies the laws,+-- hence any 'Monad' is 'Selective'.+selectM :: Monad f => f (Either a b) -> f (a -> b) -> f b+selectM x y = x >>= \e -> case e of Left  a -> ($a) <$> y -- execute y+                                    Right b -> pure b     -- skip y++-- Many useful 'Monad' combinators can be implemented with 'Selective'++-- | Branch on a Boolean value, skipping unnecessary effects.+ifS :: Selective f => f Bool -> f a -> f a -> f a+ifS x t e = branch (bool (Right ()) (Left ()) <$> x) (const <$> t) (const <$> e)++-- Implementation used in the paper:+-- ifS x t e = branch selector (fmap const t) (fmap const e)+--   where+--     selector = bool (Right ()) (Left ()) <$> x -- NB: convert True to Left ()++-- | Eliminate a specified value @a@ from @f (Either a b)@ by replacing it+-- with a given @f b@.+eliminate :: (Eq a, Selective f) => a -> f b -> f (Either a b) -> f (Either a b)+eliminate x fb fa = select (match x <$> fa) (const . Right <$> fb)+  where+    match _ (Right y) = Right (Right y)+    match x (Left  y) = if x == y then Left () else Right (Left y)++-- | 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)+matchS (Cases cs _) x f = foldr (\c -> eliminate c (f c)) (Left <$> x) cs++-- | Eliminate all specified values @a@ from @f (Either a b)@ by replacing each+-- of them with a given @f a@.+matchM :: Monad m => Cases a -> m a -> (a -> m b) -> m (Either a b)+matchM (Cases _ p) mx f = do+    x <- mx+    if p x then Right <$> (f x) else return (Left x)++-- TODO: Add a type-safe version based on @KnownNat@.+-- | A restricted version of monadic bind. Fails with an error if the 'Bounded'+-- and 'Enum' instances for @a@ do not cover all values of @a@.+bindS :: (Bounded a, Enum a, Eq a, Selective f) => f a -> (a -> f b) -> f b+bindS x f = fromRight <$> matchS casesEnum x f+  where+    fromRight (Right b) = b+    fromRight _ = error "Selective.bindS: incorrect Bounded and/or Enum instance"++-- | Conditionally perform an effect.+whenS :: Selective f => f Bool -> f () -> f ()+whenS x y = select (bool (Right ()) (Left ()) <$> x) (const <$> y)++-- Implementation used in the paper:+-- whenS x y = selector <*? effect+--   where+--     selector = bool (Right ()) (Left ()) <$> x -- NB: maps True to Left ()+--     effect   = const                     <$> y++-- | A lifted version of 'Data.Maybe.fromMaybe'.+fromMaybeS :: Selective f => f a -> f (Maybe a) -> f a+fromMaybeS x mx = select (maybe (Left ()) Right <$> mx) (const <$> x)++-- | Return the first @Right@ value. If both are @Left@'s, accumulate errors.+orElse :: (Selective f, Semigroup e) => f (Either e a) -> f (Either e a) -> f (Either e a)+orElse x y = branch x (flip appendLeft <$> y) (pure Right)++-- | Accumulate the @Right@ values, or return the first @Left@.+andAlso :: (Selective f, Semigroup a) => f (Either e a) -> f (Either e a) -> f (Either e a)+andAlso x y = swapEither <$> orElse (swapEither <$> x) (swapEither <$> y)++-- | Swap @Left@ and @Right@.+swapEither :: Either a b -> Either b a+swapEither = either Right Left++-- | Append two semigroup values or return the @Right@ one.+appendLeft :: Semigroup a => a -> Either a b -> Either a b+appendLeft a1 (Left a2) = Left (a1 <> a2)+appendLeft _  (Right b) = Right b++-- | Keep checking an effectful condition while it holds.+whileS :: Selective f => f Bool -> f ()+whileS act = whenS act (whileS act)++-- | Keep running an effectful computation until it returns a @Right@ value,+-- collecting the @Left@'s using a supplied @Monoid@ instance.+untilRight :: (Monoid a, Selective f) => f (Either a b) -> f (a, b)+untilRight x = select y h+  where+    -- y :: f (Either a (a, b))+    y = fmap (mempty,) <$> x+    -- h :: f (a -> (a, b))+    h = (\(as, b) a -> (mappend a as, b)) <$> untilRight x++-- | A lifted version of lazy Boolean OR.+(<||>) :: Selective f => f Bool -> f Bool -> f Bool+a <||> b = ifS a (pure True) b++-- | A lifted version of lazy Boolean AND.+(<&&>) :: Selective f => f Bool -> f Bool -> f Bool+a <&&> b = ifS a b (pure False)++-- | A lifted version of 'any'. Retains the short-circuiting behaviour.+anyS :: Selective f => (a -> f Bool) -> [a] -> f Bool+anyS p = foldr ((<||>) . p) (pure False)++-- | A lifted version of 'all'. Retains the short-circuiting behaviour.+allS :: Selective f => (a -> f Bool) -> [a] -> f Bool+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 = foldr andAlso (pure (Right mempty))++-- Instances++-- As a quick experiment, try: ifS (pure True) (print 1) (print 2)+instance Selective IO where select = selectM++-- 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 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++-- | 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)++instance Applicative f => Selective (ViaSelectA f) 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)++instance Semigroup e => Applicative (Validation e) where+    pure = Success+    Failure e1 <*> Failure e2 = Failure (e1 <> e2)+    Failure e1 <*> Success _  = Failure e1+    Success _  <*> Failure e2 = Failure e2+    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 (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++-- | Extract the contents of 'Over'.+getOver :: Over m a -> m+getOver (Over x) = x++-- | Static analysis of selective functors with under-approximation.+newtype Under m a = Under m+    deriving (Functor, Applicative) via Const m+    deriving Show++instance Monoid m => Selective (Under m) where+    select (Under m) _ = Under m++-- | Extract the contents of 'Under'.+getUnder :: Under m a -> m+getUnder (Under x) = x++------------------------------------ Arrows ------------------------------------++-- See the following standard definitions in "Control.Arrow".+-- newtype ArrowMonad a b = ArrowMonad (a () b)+-- 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 (ArrowMonad f) = arr (\x -> ((), x)) >>> first f >>> arr (uncurry ($))

@@ -0,0 +1,121 @@+{-# 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

@@ -0,0 +1,44 @@+{-# 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)))

@@ -0,0 +1,159 @@+{-# LANGUAGE StandaloneDeriving, DerivingVia #-}+{-# LANGUAGE FlexibleInstances, TupleSections, ExplicitForAll, TypeApplications #-}++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+import Text.Show.Functions()++-- | TODO:+-- ifS (pure x) a1 b1 *> ifS (pure x) a2 b2 = ifS (pure x) (a1 *> a2) (b1 *> b2)++--------------------------------------------------------------------------------+------------------------ Laws --------------------------------------------------+--------------------------------------------------------------------------------+-- | Identity+lawIdentity :: (Selective f, Eq (f a)) => f (Either a a) -> Bool+lawIdentity x = (x <*? pure id) == (either id id <$> x)++-- | Distributivity+lawDistributivity :: (Selective f, Eq (f b)) => Either a b -> f (a -> b) -> f (a -> b) -> Bool+lawDistributivity x y z = (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))++-- | Associativity+lawAssociativity :: (Selective f, Eq (f c)) =>+        f (Either b c) -> f (Either a (b -> c)) -> f (a -> b -> c) -> Bool+lawAssociativity x y z = (x <*? (y <*? z)) == ((f <$> x) <*? (g <$> y) <*? (h <$> z))+        where+            f x = Right <$> x+            g y = \a -> bimap (,a) ($a) y+            h z = uncurry z++{- | If 'f' is a 'Monad' |-}++lawMonad :: (Selective f, Monad f, Eq (f b)) =>+            f (Either a b) -> f (a -> b) -> Bool+lawMonad x f = select x f == selectM x f++selectALaw :: (Selective f, Eq (f b)) =>+              f (Either a b) -> f (a -> b) -> Bool+selectALaw x f = select x f == selectA x f++--------------------------------------------------------------------------------+------------------------ Theorems ----------------------------------------------+--------------------------------------------------------------------------------+{-| Theorems about selective applicative functors,+    as presented in the Fig.4 of the paper+|-}++-- | Apply a pure function to the result:+theorem1 :: (Selective f, Eq (f c)) =>+            (a -> c) -> f (Either b a) -> f (b -> a) -> Bool+theorem1 f x y = (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))++-- | Apply a pure function to the Left case of the first argument:+theorem2 :: (Selective f, Eq (f c)) =>+            (a -> b) -> f (Either a c) -> f (b -> c) -> Bool+theorem2 f x y = (select (first f <$> x) y) == (select x ((. f) <$> y))++-- | 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))++-- | Generalised identity:+theorem4 :: (Selective f, Eq (f b)) => f (Either a b) -> (a -> b) -> Bool+theorem4 x y = (x <*? pure y) == (either y id <$> x)++{-| For rigid selective functors (in particular, for monads):+|-}++-- | Selective apply+theorem5 :: (Selective f, Eq (f b)) => f (a -> b) -> f a -> Bool+theorem5 f g = (f <*> g) == (f `apS` g)++-- | Interchange+theorem6 :: (Selective f, Eq (f c)) =>+            f a -> f (Either b c) -> f (b -> c) -> Bool+theorem6 x y z = (x *> (y <*? z)) == ((x *> y) <*? z)++--------------------------------------------------------------------------------+------------------------ Properties ----------------------------------------------+--------------------------------------------------------------------------------++-- | pure-right+--   pure (Right x) <*? y = pure x+propertyPureRight :: (Selective f, Eq (f a)) => a -> f (b -> a) -> Bool+propertyPureRight x y = (pure (Right x) <*? y) == pure x++-- | pure-left+--   pure (Left x) <*? y = ($x) <$> y+propertyPureLeft :: (Selective f, Eq (f b)) => a -> f (a -> b) -> Bool+propertyPureLeft x y = (pure (Left x) <*? y) == (($x) <$> y)++--------------------------------------------------------------------------------+------------------------ Over --------------------------------------------------+--------------------------------------------------------------------------------+deriving instance Eq m => Eq (Over m a)+deriving via (Const m a) instance Arbitrary m => Arbitrary (Over m a)++propertyPureRightOver :: IO ()+propertyPureRightOver = quickCheck (propertyPureRight @(Over String) @Int)++--------------------------------------------------------------------------------+------------------------ Under -------------------------------------------------+--------------------------------------------------------------------------------+deriving instance Eq m => Eq (Under m a)+deriving via (Const m a) instance Arbitrary m => Arbitrary (Under m a)++propertyPureRightUnder :: IO ()+propertyPureRightUnder = quickCheck (propertyPureRight @(Under String) @Int)++--------------------------------------------------------------------------------+------------------------ Validation --------------------------------------------+--------------------------------------------------------------------------------+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++--------------------------------------------------------------------------------+------------------------ ArrowMonad --------------------------------------------+--------------------------------------------------------------------------------+instance Eq a => Eq (ArrowMonad (->) a) where+  ArrowMonad f == ArrowMonad g = f () == g ()++instance Arbitrary a => Arbitrary (ArrowMonad (->) a) where+  arbitrary = ArrowMonad . const <$> arbitrary++instance Show a => Show (ArrowMonad (->) a) where+  show (ArrowMonad f) = show (f ())+--------------------------------------------------------------------------------+------------------------ Maybe -------------------------------------------------+--------------------------------------------------------------------------------++propertyPureRightMaybe :: IO ()+propertyPureRightMaybe = quickCheck (propertyPureRight @Maybe @Int @Int)++--------------------------------------------------------------------------------+------------------------ Identity ----------------------------------------------+--------------------------------------------------------------------------------++propertyPureRightIdentity :: IO ()+propertyPureRightIdentity = quickCheck (propertyPureRight @Identity @Int @Int)

@@ -0,0 +1,320 @@+{-# LANGUAGE TypeApplications #-}++import Data.Maybe hiding (maybe)+import Data.Functor.Identity+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++main :: IO ()+main = defaultMain $ testGroup "Tests"+    [pingPong, build, over, under, validation, arrowMonad, maybe, identity]++--------------------------------------------------------------------------------+------------------------ Ping-pong----------------------------------------------+--------------------------------------------------------------------------------+pingPong :: TestTree+pingPong = testGroup "pingPong"+    [ testProperty "getEffects pingPongS == [Read,Write \"pong\"]" $+       getEffects pingPongS == [Read (const ()),Write "pong" ()]+    ]+--------------------------------------------------------------------------------+------------------------ Build -------------------------------------------------+--------------------------------------------------------------------------------+build :: TestTree+build = testGroup "Build" [cyclicDeps, taskBindDeps, runBuildDeps]++cyclicDeps :: TestTree+cyclicDeps = testGroup "cyclicDeps"+    [ testProperty "dependenciesOver (fromJust $ cyclic \"B1\") == [\"C1\",\"B2\",\"A2\"]" $+       dependenciesOver (fromJust $ cyclic "B1") == ["C1","B2","A2"]+    , testProperty "dependenciesOver cyclic \"B2\") == [\"C1\",\"A1\",\"B1\"]" $+        dependenciesOver (fromJust $ cyclic "B2") == ["C1","A1","B1"]+    , testProperty "dependenciesUnder (fromJust $ cyclic \"B1\") == [\"C1\"]" $+       dependenciesUnder (fromJust $ cyclic "B1") == ["C1"]+    , testProperty "dependenciesUnder 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"]+    ]++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 ())]+    ]++--------------------------------------------------------------------------------+------------------------ Over --------------------------------------------------+--------------------------------------------------------------------------------+over :: TestTree+over = testGroup "Over" [overLaws, overTheorems, overProperties]++overLaws :: TestTree+overLaws = testGroup "Laws"+    [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $+        \x -> lawIdentity @(Over String) x+    , 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+    ]++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+    , 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))" $+        \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+    ]++overProperties = testGroup "Properties"+    [ expectFail $+      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+    ]++--------------------------------------------------------------------------------+------------------------ Under -------------------------------------------------+--------------------------------------------------------------------------------+under :: TestTree+under = testGroup "Under" [underLaws, underTheorems, underProperties]++underLaws :: TestTree+underLaws = testGroup "Laws"+    [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $+        \x -> lawIdentity @(Under String) x+    , 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+    ]++underTheorems :: TestTree+underTheorems = testGroup "Theorems"+    [ testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $+        \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))" $+        \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)" $+        \x -> theorem5 @(Under String) @Int @Int x+    , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $+        \x -> theorem6 @(Under String) @Int @Int x+    ]++underProperties :: TestTree+underProperties = testGroup "Properties"+    [ testProperty "pure-right: pure (Right x) <*? y = pure x" $+        \x -> propertyPureRight @(Under String) @Int @Int x+    , expectFail $+      testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $+        \x -> propertyPureLeft @(Under String) @Int @Int x+    ]+--------------------------------------------------------------------------------+------------------------ Validation --------------------------------------------+--------------------------------------------------------------------------------+--------------------------------------------------------------------------------+validation :: TestTree+validation = testGroup "Validation"+    [validationLaws, validationTheorems, validationProperties, validationExample]++validationLaws :: TestTree+validationLaws = testGroup "Laws"+    [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $+        \x -> lawIdentity @(Validation String) @Int x+    , 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+    ]++validationTheorems :: TestTree+validationTheorems = testGroup "Theorems"+    [ testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $+        \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))" $+        \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)" $+        \x -> theorem5 @(Validation String) @Int @Int x+    , expectFailBecause "'Validation' is a non-rigid selective functor" $+      testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $+        \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+    ]++validationExample :: TestTree+validationExample = testGroup "validationExample"+    [ testProperty "shape (Success True) (Success 1) (Failure [\"width?\"]) (Failure [\"height?\"])" $+        shape (Success True) (Success 1) (Failure ["width?"]) (Failure ["height?"]) == Success (Circle 1)+    , testProperty "shape (Success False) (Failure [\"radius?\"]) (Success 2) (Success 3)" $+        shape (Success False) (Failure ["radius?"]) (Success 2) (Success 3) == Success (Rectangle 2 3)+    , testProperty "shape (Success False) (Failure [\"radius?\"]) (Success 2) (Failure [\"height?\"])" $+        shape (Success False) (Failure ["radius?"]) (Success 2) (Failure ["height?"]) == Failure ["height?"]+    , testProperty "shape (Success False) (Success 1) (Failure [\"width?\"]) (Failure [\"height?\"])" $+        shape (Success False) (Success 1) (Failure ["width?"]) (Failure ["height?"]) == Failure ["width?", "height?"]+    , 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?"]+    ]++--------------------------------------------------------------------------------+------------------------ ArrowMonad --------------------------------------------+--------------------------------------------------------------------------------++arrowMonad :: TestTree+arrowMonad = testGroup "ArrowMonad (->)"+    [arrowMonadLaws, arrowMonadTheorems, arrowMonadProperties]++arrowMonadLaws = testGroup "Laws"+    [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $+        \x -> lawIdentity @(ArrowMonad (->)) @Int x+    , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $+        \x -> lawDistributivity @(ArrowMonad (->)) @Int @Int x+    , testProperty "Associativity: take a look at tests/Laws.hs" $+        \x -> lawAssociativity @(ArrowMonad (->)) @Int @Int @Int x+    , testProperty "select == selectM" $+        \x -> lawMonad @(ArrowMonad (->)) @Int @Int x+    , testProperty "select == selectA" $+        \x -> selectALaw @(ArrowMonad (->)) @Int @Int x+    ]++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+    , 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))" $+        \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+    ]++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+    ]+--------------------------------------------------------------------------------+------------------------ Maybe -------------------------------------------------+--------------------------------------------------------------------------------+maybe :: TestTree+maybe = testGroup "Maybe" [maybeLaws, maybeTheorems, maybeProperties]++maybeLaws = testGroup "Laws"+    [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $+        \x -> lawIdentity @Maybe @Int x+    , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $+        \x -> lawDistributivity @Maybe @Int @Int x+    , 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+    ]++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+    , 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))" $+        \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+    ]++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+    ]+--------------------------------------------------------------------------------+------------------------ Identity ----------------------------------------------+--------------------------------------------------------------------------------+identity :: TestTree+identity = testGroup "Identity"+    [identityLaws, identityTheorems, identityProperties]++identityLaws = testGroup "Laws"+    [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $+        \x -> lawIdentity @Identity @Int x+    , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $+        \x -> lawDistributivity @Identity @Int @Int x+    , 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+    ]++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+    , 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))" $+        \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+    ]++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+    ]

@@ -0,0 +1,415 @@+{-# LANGUAGE FlexibleInstances, ScopedTypeVariables, TupleSections #-}+module Sketch where++import Control.Monad+import Control.Selective+import Data.Bifunctor+import Data.Void++-- This file contains various examples and proof sketches and we keep it here to+-- make sure it still compiles.++------------------------------- Various examples -------------------------------++bindBool :: Selective f => f Bool -> (Bool -> f a) -> f a+bindBool x f = ifS x (f False) (f True)++branch3 :: Selective f => f (Either a (Either b c)) -> f (a -> d) -> f (b -> d) -> f (c -> d) -> f d+branch3 x a b c = (fmap (fmap Left)     <$> x)+              <*? (fmap (Right . Right) <$> a)+              <*? (fmap Right           <$> b)+              <*? c++bindOrdering :: Selective f => f Ordering -> (Ordering -> f a) -> f a+bindOrdering x f = branch3 (toEither <$> x) (const <$> f LT) (const <$> f EQ) (const <$> f GT)+  where+    toEither LT = Left ()+    toEither EQ = Right (Left ())+    toEither GT = Right (Right ())++-------------------------------- Proof sketches --------------------------------+-- A convenient primitive which checks that the types of two given values+-- coincide and returns the first value.+(===) :: a -> a -> a+x === y = if True then x else y++infixl 0 ===++-- First, we typecheck the laws++-- F1 (Free): f <$> select x y = select (fmap f <$> x) (fmap f <$> y)+f1 :: Selective f => (b -> c) -> f (Either a b) -> f (a -> b) -> f c+f1 f x y = f <$> select x y === select (fmap f <$> x) (fmap f <$> y)++-- F2 (Free): select (first f <$> x) y = select x ((. f) <$> y)+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 :: 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)++-- P1 (Generalised identity): select x (pure y) == either y id <$> x+p1 :: Selective f => f (Either a b) -> (a -> b) -> f b+p1 x y = select x (pure y) === either y id <$> x++-- A more basic form of P1, from which P1 itself follows as a free theorem.+-- Intuitively, both 'p1' and 'p1id' make the following Const instance illegal:+--+-- @+-- instance Monoid m => Selective (Const m) where+--    select (Const x) (Const _) = Const (x <> x)+-- @+-- P1id (Identity): select x (pure id) == either id id <$> x+p1id  :: Selective f => f (Either a a) -> f a+p1id x = select x (pure id) === either id id <$> x++-- P2 (does not generally hold): select (pure (Left x)) y = ($x) <$> y+p2 :: Selective f => a -> f (a -> b) -> f b+p2 x y = select (pure (Left  x)) y === y <*> pure x++-- P3 (does not generally hold): select (pure (Right x)) y = pure x+p3 :: Selective f => b -> f (a -> b) -> f b+p3 x y = select (pure (Right x)) y === pure x++-- A1 (Associativity):+--     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+a1 :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b+a1 x y z = 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++-- Intuitively, 'i1' makes the following Const instance illegal, by insisting+-- that effects on the left hand side must be executed.+--+-- @+-- instance Monoid m => Selective (Const m) where+--    select _ _ = Const mempty+-- @+--+-- If we decompose an effect @x :: f a@ into the effect itself @void x@ and the+-- resulting pure value @a@, i.e. @void x *> pure a@, then it becomes clear that+-- 'i1unit' means that all effects must be executed and the remainig pure value+-- will be used to select whether to execute or skip the right hand side.+-- i1unit (Interchange): (x *> y) <*? z = x *> (y <*? z)+i1unit :: Selective f => f c -> f (Either a b) -> f (a -> b) -> f b+i1unit x y z =+    (x *> y) <*? z+    ===+    x *> (y <*? z)++-- i1: x <*> (y <*? z) = (f <$> x <*> y) <*? (g <$> z)+--     where+--       f = (\ab -> bimap (, ab) ab)+--       g = (\ca (c, ab) -> ab (ca c))+i1 :: Selective f => f (a -> b) -> f (Either c a) -> f (c -> a) -> f b+i1 x y z =+    x <*> (y <*? z)+    ===+    (f <$> x <*> y) <*? (g <$> z)+  where+    f ab = bimap (\c ca -> ab (ca c)) ab+    g ca = ($ca)++-- D1 (distributivity): pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z)+d1 :: Selective f => Either a b -> f (a -> b) -> f (a -> b) -> f b+d1 x y z =+    pure x <*? (y *> z)+    ===+    (pure x <*? y) *> (pure x <*? z)++-- TODO: Can we prove the following from D1?+-- ifS (pure x) a1 b1 *> ifS (pure x) a2 b2 = ifS (pure x) (a1 *> a2) (b1 *> b2)++-- Now let's typecheck some theorems++-- This assumes P2, which does not always hold+-- Identity: pure id <*> v = v+t1 :: Selective f => f a -> f a+t1 v =+    -- Express the lefthand side using 'apS'+    apS (pure id) v+    === -- Definition of 'apS'+    select (Left <$> pure id) (flip ($) <$> v)+    === -- Push 'Left' inside 'pure'+    select (pure (Left id)) (flip ($) <$> v)+    === -- Apply P2+    ($id) <$> (flip ($) <$> v)+    === -- Simplify+    id <$> v+    === -- Functor identity: -- Functor identity: fmap id = id+    v++-- Homomorphism: pure f <*> pure x = pure (f x)+t2 :: Selective f => (a -> b) -> a -> f b+t2 f x =+    -- Express the lefthand side using 'apS'+    apS (pure f) (pure x)+    === -- Definition of 'apS'+    select (Left <$> pure f) (flip ($) <$> pure x)+    === -- Push 'Left' inside 'pure'+    select (pure (Left f)) (flip ($) <$> pure x)+    === -- Applicative's fmap-pure law+    select (pure (Left f)) (pure (flip ($) x))+    === -- Apply P1+    either ((flip ($) x)) id <$> pure (Left f)+    === -- Applicative's fmap-pure law+    pure ((flip ($) x) f)+    === -- Simplify+    pure (f x)++-- This assumes P2, which does not always hold+-- Interchange: u <*> pure y = pure ($y) <*> u+t3 :: Selective f => f (a -> b) -> a -> f b+t3 u y =+    -- Express the lefthand side using 'apS'+    apS u (pure y)+    === -- Definition of 'apS'+    select (Left <$> u) (flip ($) <$> pure y)+    === -- Rewrite to have a pure second argument+    select (Left <$> u) (pure ($y))+    === -- Apply P1+    either ($y) id <$> (Left <$> u)+    === -- Simplify, obtaining (#)+    ($y) <$> u++    === -- Express right-hand side of the theorem using 'apS'+    apS (pure ($y)) u+    === -- Definition of 'apS'+    select (Left <$> pure ($y)) (flip ($) <$> u)+    === -- Push 'Left' inside 'pure'+    select (pure (Left ($y))) (flip ($) <$> u)+    === -- Apply P2+    ($($y)) <$> (flip ($) <$> u)+    === -- Simplify, obtaining (#)+    ($y) <$> u++-- Composition: (.) <$> u <*> v <*> w = u <*> (v <*> w)+t4 :: Selective f => f (b -> c) -> f (a -> b) -> f a -> f c+t4 u v w =+    -- Express the lefthand side using 'apS'+    apS (apS ((.) <$> u) v) w+    === -- Definition of 'apS'+    select (Left <$> select (Left <$> (.) <$> u) (flip ($) <$> v)) (flip ($) <$> w)+    === -- Apply F1 to push the leftmost 'Left' inside 'select'+    select (select (second Left <$> Left <$> (.) <$> u) ((Left .) <$> flip ($) <$> v)) (flip ($) <$> w)+    === -- Simplify+    select (select (Left <$> (.) <$> u) ((Left .) <$> flip ($) <$> v)) (flip ($) <$> w)+    === -- Pull (.) outside 'Left'+    select (select (first (.) <$> Left <$> u) ((Left .) <$> flip ($) <$> v)) (flip ($) <$> w)+    === -- Apply F2 to push @(.)@ to the function+    select (select (Left <$> u) ((. (.)) <$> (Left .) <$> flip ($) <$> v)) (flip ($) <$> w)+    === -- Simplify, obtaining (#)+    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) (flip ($) <$> 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))+    === -- Apply A1 to reassociate to the left+    select (select (Left <$> u) ((\y a -> bimap (,a) ($a) y) <$> Left <$> v)) (uncurry . (flip ($) .) <$> flip ($) <$> 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)+    === -- Simplify+    select (first (\(f, g) -> g . f) <$> select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) (flip ($) <$> 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)+    === -- Simplify, obtaining (#)+    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) (flip ($) <$> w)++--------------------------------- End of proofs --------------------------------++-- Various other sketches below++-- Associate to the left+-- f (a + b + c) -> f (a -> (b + c)) -> f (b -> c) -> f c+l :: Selective f => f (Either a (Either b c)) -> f (a -> Either b c) -> f (b -> c) -> f c+l x y z = x <*? y <*? z++-- Associate to the right+-- f (a + b) -> f (c + (a -> b)) -> f (c -> a -> b) -> f b+r :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b+r x y z = x <*? (y <*? z)++-- Normalise: go from right to left association+normalise :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b+normalise x y z = (f <$> x) <*? (g <$> y) <*? (h <$> z)+  where+    f x = Right <$> x+    g y = \a -> bimap (,a) ($a) y+    h z = uncurry z++-- Alternative normalisation which uses Scott encoding of pairs+normalise2 :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b+normalise2 x y z = (f <$> x) <*? (g <$> y) <*? (h <$> z)+  where+    f x = Right <$> x+    g y = \a -> bimap (\c f -> f c a) ($a) y+    h z = ($z) -- h = flip ($)++-- Alternative type classes for selective functors. They all come with an+-- additional requirement that we run effects 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)++-- Composition of Starry and Either monad+-- See: https://duplode.github.io/posts/applicative-archery.html+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+    (|**|) :: f (Either e a) -> f (Either e b) -> f (Either e (a, b))++biselect :: Selective f => f (Either a b) -> f (Either a c) -> f (Either a (b, c))+biselect x y = select ((fmap Left . swapEither) <$> x) ((\e a -> fmap (a,) e) <$> y)++(?*?) :: Selective f => f (Either a b) -> f (Either a c) -> f (Either a (b, c))+(?*?) = biselect++a1M :: Selective f => f (Either a b) -> f (Either a c) -> f (Either a d)+                   -> f (Either a (b, (c, d)))+a1M x y z =+    x ?*? (y ?*? z)+    ===+    second assoc <$> ((x ?*? y) ?*? z)+  where+    assoc ((a, b), c) = (a, (b, c))++apM :: SelectiveM f => f (a -> b) -> f a -> f b+apM f x = fmap (either absurd (uncurry ($))) (fmap Right f |**| fmap Right x)++fromM :: SelectiveM f => f (Either a b) -> f (a -> b) -> f b+fromM x f = either id (\(a, f) -> f a) <$> (fmap swapEither x |**| fmap Right f)++toM :: Selective f => f (Either e a) -> f (Either e b) -> f (Either e (a, b))+toM a b = select ((fmap Left . swapEither) <$> a) ((\e a -> fmap (a,) e) <$> b)++-- | Swap @Left@ and @Right@.+swapEither :: Either a b -> Either b a+swapEither = either Right Left++-- Proof that if select = selectM, and <*> = ap, then <*> = apS.+apSEqualsApply :: (Selective f, Monad f) => f (a -> b) -> f a -> f b+apSEqualsApply fab fa =+    fab <*> fa+    === -- Law: <*> = ap+    ap fab fa+    === -- Free theorem (?)+    selectM (Left <$> fab) (flip ($) <$> fa)+    === -- Law: selectM = select+    select (Left <$> fab) (flip ($) <$> fa)+    === -- Definition of apS+    apS fab fa++-- | Selective function composition, where the first effect is always evaluated,+-- but the second one can be skipped if the first value is @Nothing@.+-- Thanks to the laws of 'Selective', this operator is associative, and has+-- identity @pure (Just id)@.+(.?) :: Selective f => f (Maybe (b -> c)) -> f (Maybe (a -> b)) -> f (Maybe (a -> c))+x .? y = select (maybe (Right Nothing) Left <$> x) ((\ab bc -> (bc .) <$> ab) <$> y)++infixl 4 .?++-- This assumes P2, which does not always hold+-- Proof of left identity: pure (Just id) .? x = x+t5 :: Selective f => f (Maybe (a -> b)) -> f (Maybe (a -> b))+t5 x =+    --- Lefthand side+    pure (Just id) .? x+    === -- Express the lefthand side by expanding the definition of '.?'+    select (maybe (Right Nothing) Left <$> pure (Just id))+        ((\ab bc -> (bc .) <$> ab) <$> x)+    === -- Simplify+    select (pure $ Left id) ((\ab bc -> (bc .) <$> ab) <$> x)+    === -- Apply P2+    ($id) <$> ((\ab bc -> (bc .) <$> ab) <$> x)+    === -- Simplify+    (($id) <$> (\ab bc -> (bc .) <$> ab) <$> x)+    === -- Functor identity: fmap id = id+    id <$> x+    ===+    x++-- Proof of right identity: x .? pure (Just id) = x+t6 :: Selective f => f (Maybe (a -> b)) -> f (Maybe (a -> b))+t6 x =+    --- Lefthand side+    x .? pure (Just id)+    === -- Express the lefthand side by expanding the definition of '.?'+    select (maybe (Right Nothing) Left <$> x)+        ((\ab bc -> (bc .) <$> ab) <$> pure (Just id))+    === -- Simplify+    select (maybe (Right Nothing) Left <$> x) (pure Just)+    === -- Apply P1+    either Just id <$> (maybe (Right Nothing) Left <$> x)+    === -- Functor identity: fmap id = id+    id <$> x+    ===+    x++-- Proof of associativity: (x .? y) .? z = x .? (y .? z)+t7 :: Selective f => f (Maybe (c -> d)) -> f (Maybe (b -> c)) -> f (Maybe (a -> b)) -> f (Maybe (a -> d))+t7 x y z =+    -- Lefthand side+    (x .? y) .? z+    === -- Express the lefthand side by expanding the definition of '.?'+    select (maybe (Right Nothing) Left <$> (select (maybe (Right Nothing) Left <$> x)+        ((\ab bc -> (bc .) <$> ab) <$> y)))+        ((\ab bc -> (bc .) <$> ab) <$> z)+    === -- 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)+    === -- Simplify+    select (maybe (Right Nothing) (\bc -> Left $ fmap $ (bc .)) <$> (select (maybe (Right Nothing) Left <$> x)+        ((\ab bc -> (bc .) <$> ab) <$> y)))+        (flip ($) <$> 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)+    === -- Simplify, obtaining (#)+    select (select (maybe (Right (Right Nothing)) Left <$> x)+        ((\mbc cd -> maybe (Right Nothing) (\bc -> Left $ fmap ((cd . bc) .)) mbc) <$> y))+        (flip ($) <$> z)++    === -- Righthand side+    x .? (y .? z)+    === -- Express the righthand side by expanding the definition of '.?'+    select (maybe (Right Nothing) Left <$> x)+        ((\ab bc -> (bc .) <$> ab) <$> (select (maybe (Right Nothing) Left <$> y)+        ((\ab bc -> (bc .) <$> ab) <$> z)))+    === -- Apply F1 to move the pure function into the inner 'select'+    select (maybe (Right Nothing) Left <$> x)+        (select (second ((\ab bc -> (bc .) <$> ab)) <$> maybe (Right Nothing) Left <$> y)+        ((((\ab bc -> (bc .) <$> ab)).) <$> (\ab bc -> (bc .) <$> ab) <$> z))+    === -- Apply A1 to reassociate to the left+    select (select (fmap Right <$> maybe (Right Nothing) Left <$> x)+        ((\y a -> bimap (,a) ($a) y) <$> second ((\ab bc -> (bc .) <$> ab)) <$> maybe (Right Nothing) Left <$> y))+        (uncurry <$> (((\ab bc -> (bc .) <$> ab)).) <$> (\ab bc -> (bc .) <$> ab) <$> z)+    === -- Simplify+    select (select (maybe (Right (Right Nothing)) Left <$> x)+        ((\m a -> maybe (Right Nothing) (Left . (,a)) m) <$> y))+        ((\ab (bc, cd) -> ((cd . bc) .) <$> ab) <$> z)+    === -- 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)+    === -- 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)