diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. diff --git a/examples/Build.hs b/examples/Build.hs new file mode 100644 --- /dev/null +++ b/examples/Build.hs @@ -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) diff --git a/examples/Parser.hs b/examples/Parser.hs new file mode 100644 --- /dev/null +++ b/examples/Parser.hs @@ -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 diff --git a/examples/Processor.hs b/examples/Processor.hs new file mode 100644 --- /dev/null +++ b/examples/Processor.hs @@ -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) diff --git a/examples/Teletype.hs b/examples/Teletype.hs new file mode 100644 --- /dev/null +++ b/examples/Teletype.hs @@ -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) diff --git a/examples/Validation.hs b/examples/Validation.hs new file mode 100644 --- /dev/null +++ b/examples/Validation.hs @@ -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 diff --git a/selective.cabal b/selective.cabal new file mode 100644 --- /dev/null +++ b/selective.cabal @@ -0,0 +1,74 @@ +name: selective +version: 0.1.0 +synopsis: Selective applicative functors +license: MIT +license-file: LICENSE +author: Andrey Mokhov , github: @snowleopard +maintainer: Andrey Mokhov , 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 + . + +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 diff --git a/src/Control/Selective.hs b/src/Control/Selective.hs new file mode 100644 --- /dev/null +++ b/src/Control/Selective.hs @@ -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 ($)) diff --git a/src/Control/Selective/Free/Rigid.hs b/src/Control/Selective/Free/Rigid.hs new file mode 100644 --- /dev/null +++ b/src/Control/Selective/Free/Rigid.hs @@ -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 diff --git a/test/ArrowLaws.hs b/test/ArrowLaws.hs new file mode 100644 --- /dev/null +++ b/test/ArrowLaws.hs @@ -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))) diff --git a/test/Laws.hs b/test/Laws.hs new file mode 100644 --- /dev/null +++ b/test/Laws.hs @@ -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) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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 + ] diff --git a/test/Sketch.hs b/test/Sketch.hs new file mode 100644 --- /dev/null +++ b/test/Sketch.hs @@ -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)