From 982d98c866ec915b677672dff956de2bcae9181e Mon Sep 17 00:00:00 2001 From: Andrey Mokhov Date: Thu, 7 Mar 2019 02:20:30 +0000 Subject: [PATCH] Prepare first Hackage release --- examples/Build.hs | 111 ++++++ {src/Control/Selective => examples}/Parser.hs | 5 +- examples/Processor.hs | 237 +++++++++++++ examples/Teletype.hs | 72 ++++ examples/Validation.hs | 40 +++ selective.cabal | 64 ++-- src/Control/Selective.hs | 58 ++- src/Control/Selective/Example.hs | 198 ----------- src/Control/Selective/Example/ISA.hs | 281 --------------- .../Selective/Example/ISA/Instruction.hs | 333 ------------------ src/Control/Selective/Example/ISA/Programs.hs | 100 ------ src/Control/Selective/Example/ISA/Simulate.hs | 109 ------ src/Control/Selective/Example/ISA/Types.hs | 91 ----- src/Control/Selective/Example/Teletype.hs | 49 --- src/Control/Selective/Free/Rigid.hs | 71 ++-- .../Selective/Free/Rigid/Generalised.hs | 99 ------ test/Main.hs | 222 ++++++++---- {src/Control/Selective => test}/Sketch.hs | 7 +- 18 files changed, 707 insertions(+), 1440 deletions(-) create mode 100644 examples/Build.hs rename {src/Control/Selective => examples}/Parser.hs (91%) create mode 100644 examples/Processor.hs create mode 100644 examples/Teletype.hs create mode 100644 examples/Validation.hs delete mode 100644 src/Control/Selective/Example.hs delete mode 100644 src/Control/Selective/Example/ISA.hs delete mode 100644 src/Control/Selective/Example/ISA/Instruction.hs delete mode 100644 src/Control/Selective/Example/ISA/Programs.hs delete mode 100644 src/Control/Selective/Example/ISA/Simulate.hs delete mode 100644 src/Control/Selective/Example/ISA/Types.hs delete mode 100644 src/Control/Selective/Example/Teletype.hs delete mode 100644 src/Control/Selective/Free/Rigid/Generalised.hs rename {src/Control/Selective => test}/Sketch.hs (99%) diff --git a/examples/Build.hs b/examples/Build.hs new file mode 100644 index 0000000..b54f978 --- /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/src/Control/Selective/Parser.hs b/examples/Parser.hs similarity index 91% rename from src/Control/Selective/Parser.hs rename to examples/Parser.hs index a7cbe2e..ad89eab 100644 --- a/src/Control/Selective/Parser.hs +++ b/examples/Parser.hs @@ -1,10 +1,13 @@ {-# LANGUAGE ConstraintKinds, DeriveFunctor, GADTs, RankNTypes #-} -module Control.Selective.Parser where +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 diff --git a/examples/Processor.hs b/examples/Processor.hs new file mode 100644 index 0000000..a3f4a67 --- /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 index 0000000..7694b17 --- /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 index 0000000..2c885de --- /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 index 433a43c..187789a 100644 --- a/selective.cabal +++ b/selective.cabal @@ -1,17 +1,23 @@ name: selective -version: 0.0.1 +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 +copyright: Andrey Mokhov, 2018-2019 homepage: https://github.com/snowleopard/selective category: Control build-type: Simple -cabal-version: >=1.18 +cabal-version: 1.18 stability: experimental -description: Selective applicative functors +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 @@ -23,24 +29,11 @@ source-repository head library hs-source-dirs: src exposed-modules: Control.Selective, - Control.Selective.Example, - Control.Selective.Example.ISA, - Control.Selective.Example.ISA.Types, - Control.Selective.Example.ISA.Instruction, - Control.Selective.Example.ISA.Programs, - Control.Selective.Example.ISA.Simulate, - Control.Selective.Example.Teletype, - Control.Selective.Free.Rigid.Generalised, - Control.Selective.Free.Rigid, - Control.Selective.Parser, - Control.Selective.Sketch - build-depends: algebraic-graphs >= 0.1.1, - base >= 4.7 && < 5, - binary >= 0.8.5.1, - build >= 1.1, - containers >= 0.5.7.1, - mtl >= 2.2.1 && < 2.3, - transformers >= 0.5.2.0 + 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 @@ -50,19 +43,26 @@ library -Wredundant-constraints test-suite test - hs-source-dirs: test - other-modules: Laws, ArrowLaws + 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: selective, - base >= 4.7 && < 5, - containers >= 0.5.7.1, - mtl >= 2.2.1 && < 2.3, - QuickCheck >= 2.12.6.1, - tasty >= 1.2, - tasty-quickcheck >= 0.10, + 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, - checkers + tasty-quickcheck >= 0.10 default-language: Haskell2010 GHC-options: -Wall -fno-warn-name-shadowing diff --git a/src/Control/Selective.hs b/src/Control/Selective.hs index 761790e..5bed543 100644 --- a/src/Control/Selective.hs +++ b/src/Control/Selective.hs @@ -160,34 +160,26 @@ branch x l r = fmap (fmap Left) x <*? fmap (fmap Right) l <*? r 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) --- @ --- +{-| 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) @@ -247,7 +239,7 @@ whenS x y = select (bool (Right ()) (Left ()) <$> x) (const <$> y) -- selector = bool (Right ()) (Left ()) <$> x -- NB: maps True to Left () -- effect = const <$> y --- | A lifted version of 'fromMaybe'. +-- | 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) @@ -274,12 +266,12 @@ 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 :: forall a b f. (Monoid a, Selective f) => f (Either a b) -> f (a, b) +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 :: f (Either a (a, b)) y = fmap (mempty,) <$> x - h :: f (a -> (a, b)) + -- h :: f (a -> (a, b)) h = (\(as, b) a -> (mappend a as, b)) <$> untilRight x -- | A lifted version of lazy Boolean OR. @@ -320,6 +312,8 @@ 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) diff --git a/src/Control/Selective/Example.hs b/src/Control/Selective/Example.hs deleted file mode 100644 index 35886d1..0000000 --- a/src/Control/Selective/Example.hs +++ /dev/null @@ -1,198 +0,0 @@ -{-# LANGUAGE ConstraintKinds, DeriveFunctor, GADTs, RankNTypes #-} -module Control.Selective.Example where - -import Algebra.Graph -import Algebra.Graph.Export.Dot -import Control.Monad -import Control.Selective.Free.Rigid - -import qualified Build.Task as B -import qualified Data.Set as Set - -------------------------------- Ping-pong example ------------------------------ -pingPongM :: IO () -pingPongM = getLine - >>= - \s -> if s == "ping" then putStrLn "pong" else pure () - -pingPongA :: IO () -pingPongA = fmap (\_ -> id) getLine - <*> - putStrLn "pong" - -pingPongS :: IO () -pingPongS = - (\s -> if s == "ping" then Left () else Right ()) <$> getLine - <*? - (putStrLn "pong" *> pure id) - -pingPongDoM :: IO () -pingPongDoM = do - s <- getLine - when (s == "ping") (putStrLn "pong") - -pingPongWhenS :: IO () -pingPongWhenS = whenS (fmap (=="ping") getLine) (putStrLn "pong") - --- Doesn't make much sense, there are still opaque binds, furthermore getLine --- might happen twice. -pingPongMP :: IO () -pingPongMP = mplus x y - where - x = do - x <- getLine - guard (x == "ping") - putStrLn "pong" - y = do - x <- getLine - guard (x /= "ping") - -------------------------------- Task dependencies ------------------------------ - --- dependencies task "B1" = ["A2","B2","C1"] --- dependencies task "B2" = ["A1","B1","C1"] --- dependencies task "A1" = [] -task :: B.Tasks Selective String Integer -task "B1" = Just $ B.Task $ \fetch -> ifS ((1==) <$> fetch "C1") (fetch "B2") (fetch "A2") -task "B2" = Just $ B.Task $ \fetch -> ifS ((1==) <$> fetch "C1") (fetch "A1") (fetch "B1") -task _ = Nothing - --- dependencies task2 "B1" == ["A1","A2","C5","C6","D5","D6"] -task2 :: B.Tasks Selective String Integer -task2 "B1" = Just $ B.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) -task2 _ = Nothing - -data Key = A Int | B Int | C Int Int deriving (Eq, Show) - -editDistance :: B.Tasks Selective Key Int -editDistance (C i 0) = Just $ B.Task $ const $ pure i -editDistance (C 0 j) = Just $ B.Task $ const $ pure j -editDistance (C i j) = Just $ B.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 - -sprsh1 :: B.Tasks Applicative String Int -sprsh1 "B1" = Just $ B.Task $ \fetch -> ((+) <$> fetch "A1" <*> fetch "A2") -sprsh1 "B2" = Just $ B.Task $ \fetch -> ((*2) <$> fetch "B1") -sprsh1 "C8" = Just $ B.Task $ \_ -> pure 8 -sprsh1 _ = Nothing - --- Code from the paper: - -newtype Task k v = Task { run :: forall f. Selective f => (k -> f v) -> f v } - -type Script k v = k -> Maybe (Task k v) - -tar :: Applicative f => [f String] -> f String -tar xs = concat <$> sequenceA xs - -parse :: Functor f => f String -> f Bool -parse = fmap null - -compile :: Applicative f => [f String] -> f String -compile xs = concat <$> sequenceA xs - -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 - -dependenciesOver :: Task k v -> [k] -dependenciesOver task = getOver $ run task (\k -> Over [k]) - -dependenciesUnder :: Task k v -> [k] -dependenciesUnder task = getUnder $ run task (\k -> Under [k]) - ---------------------------------- Free example --------------------------------- - -data F k v a = Fetch k (v -> a) - deriving Functor - -instance Show k => Show (F k v a) where - show (Fetch k _) = "(Fetch " ++ show k ++ ")" - -fetch :: k -> Select (F k v) v -fetch key = liftSelect $ Fetch key id - -data GP k v a = Get k (v -> a) - | Put k v a - deriving Functor - -instance (Show k, Show v) => Show (GP k v a) where - show (Get k _) = "(Get " ++ show k ++ ")" - show (Put k v _) = "(Put " ++ show k ++ " " ++ show v ++ ")" - -get :: k -> Select (GP k v) v -get key = liftSelect $ Get key id - -put :: k -> v -> Select (GP k v) () -put key value = liftSelect $ Put key value () - -graph :: Ord k => (k -> [k]) -> k -> Graph k -graph deps key = transpose $ overlays [ star k (deps k) | k <- keys Set.empty [key] ] - where - keys seen [] = Set.toList seen - keys seen (x:xs) - | x `Set.member` seen = keys seen xs - | otherwise = keys (Set.insert x seen) (deps x ++ xs) - --- | Extract dependencies from a selective task. -dependencies :: B.Task Selective k v -> [k] -dependencies task = getOver $ B.run task (Over . pure) - -draw :: B.Tasks Selective String v -> String -> String -draw tasks = exportAsIs . graph deps - where - deps k = maybe [] dependencies $ tasks k - -fetchIO :: Read a => String -> IO a -fetchIO prompt = do putStr (prompt ++ ": "); read <$> getLine - ----------------------------------- Validation ---------------------------------- - -type Radius = Word -type Width = Word -type Height = Word - -data Shape = Circle Radius | Rectangle Width Height deriving 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/src/Control/Selective/Example/ISA.hs b/src/Control/Selective/Example/ISA.hs deleted file mode 100644 index 5d42177..0000000 --- a/src/Control/Selective/Example/ISA.hs +++ /dev/null @@ -1,281 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE StandaloneDeriving #-} - -module Control.Selective.Example.ISA where - -import Prelude hiding (read) -import Data.Word (Word8) -import Data.Int (Int16) -import Data.Functor (void) -import qualified Control.Monad.State as S -import Control.Selective -import Control.Selective.Free.Rigid -import qualified Data.Map.Strict as Map - --- | Hijack mtl's MonadState constraint to include Selective -type MonadState s m = (Selective m, S.MonadState s m) - -fromBool :: Num a => Bool -> a -fromBool True = 1 -fromBool False = 0 - --------------------------------------------------------------------------------- --------- Types ----------------------------------------------------------------- --------------------------------------------------------------------------------- - --- | The ISA operates signed 16-bit words -type Value = Int16 - --- | The ISA has 4 registers -data Reg = R1 | R2 | R3 | R4 - deriving (Show, Eq, Ord) - -r0, r1, r2, r3 :: Key -r0 = Register R1 -r1 = Register R2 -r2 = Register R3 -r3 = Register R4 - -type RegisterBank = Map.Map Reg Value - --- | The address space is indexed by one byte -type Address = Word8 - --- | We model memory as a map from bytes to signed 16-bit words -type Memory = Map.Map Address Value - --- | The ISA has two flags -data F = Zero -- ^ tracks if the result of the last arithmetical operation was zero - | Overflow -- ^ tracks integer overflow - deriving (Show, Eq, Ord) - -type Flags = Map.Map F Value - --- | Address in the program memory -type InstructionAddress = Value - --- data Key v where --- Register :: Reg -> Key Value -- ^ Refer to a register --- Memory :: Address -> Key Value -- ^ Refer to a memory location --- Flag :: F -> Key Bool -- ^ Refer to a flag --- PC :: Key InstructionAddress -- ^ Refer to the program counter - -data Key = - Register Reg - | Memory Address - | Flag F - | PC - -instance Show Key where - show (Register r ) = show r - show (Memory addr) = show addr - show (Flag f) = show f - show PC = "PC" - -deriving instance Eq Key - -data ISAState = ISAState { registers :: RegisterBank - , memory :: Memory - , pc :: InstructionAddress - , flags :: Flags - } - -data RW a = R Key (Value -> a) - | W Key (ISA Value) (Value -> a) - deriving Functor - -type ISA 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 - -- show (W k (Select f v) _) = "Write " ++ show k ++ " unknown" - -- show (W k (Select (Pure (Left x)) f) _) = "Write " ++ show k ++ " " -- ++ show x - --- | Interpret the internal ISA effect in 'MonadState' -toState :: MonadState ISAState m => RW a -> m a -toState (R k t) = t <$> case k of - Register r -> (Map.! r ) <$> S.gets registers - Memory 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 - Register r -> do v <- runSelect toState p - let regs' s = Map.insert r v (registers s) - S.state (\s -> (t v, s {registers = regs' s})) - Memory 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' in the state monad -runProgramState :: ISA a -> ISAState -> (a, ISAState) -runProgramState f = S.runState (runSelect toState f) - -read :: Key -> ISA Value -read k = liftSelect (R k id) - -write :: Key -> ISA Value -> ISA Value -write k fv = fv *> liftSelect (W k fv id) - --- -------------------------------------------------------------------------------- --- -------- Instructions ---------------------------------------------------------- --- -------------------------------------------------------------------------------- - -runProgram :: ISA a -> ISAState -> (a, ISAState) -runProgram prog memory = runProgramState prog memory - ------------- --- Add ----- ------------- - --- | Read the values of the variables "x" and "y" and write the sum into the variable "z". --- If the sum is zero, write 1 into the variable "zero", otherwise put 0 there. --- --- This implementation looks intuitive, but it is wrong, since the two write operations --- can be considered independent and the effects required for computing the sum, i.e. --- 'read "x" <*> read "y"' will be executed twice. Consequently: --- * the value written into the "z" variable is not guaranteed to be the same as the one which was --- compared to zero, --- * the static analysis of the computations reports more dependencies then one might have --- naively expected --- --- > analyse addNaive --- ([],Left (W "z" :| [R "y",R "x",W "zero",R "y",R "x"])) --- --- Here, the two instances of 'sum' cause the duplication of 'R "x"' and R '"y"' effects. -addNaive :: Key -> Key -> Key -> ISA Value -addNaive reg1 reg2 reg3 = - let sum = (+) <$> read reg1 <*> read reg2 - isZero = (==) <$> sum <*> pure 0 - in write (Flag Zero) (ifS isZero (pure 1) (pure 0)) - *> write reg3 sum - --- | This implementations of 'add' executes the effects associated with the 'sum' value only once and --- then wires the pure value into the computations which require it without triggering the effects again. --- --- > analyse add --- ([],Left (W "zero" :| [W "z",R "y",R "x"])) --- -add :: Key -> Key -> Key -> ISA Value -add reg1 reg2 reg3 = - let x = read reg1 - y = read reg2 - sum = (+) <$> x <*> y - isZero = (==1) <$> write reg3 sum - in write (Flag Zero) (fromBool <$> isZero) - --- -- | This is a fully inlined version of 'add' --- addNormalForm :: ISA Value --- addNormalForm = --- write "zero" (ifS ((==) <$> pure 0 <*> write "z" ((+) <$> read "x" <*> read "y")) (pure 1) (pure 0)) - --- addState :: Memory --- addState = --- Map.fromList [ ("x", 255) --- , ("y", 1) --- , ("zero", 0) --- , ("overflow", 0) --- , ("ic", 0) --- ] - ------------------ --- jumpZero ----- ------------------ -jumpZero :: Value -> ISA () -jumpZero offset = - let pc = read PC - zeroSet = (==1) <$> read (Flag Zero) - -- modifyPC = void $ write PC (pure offset) -- (fmap (+ offset) pc) - modifyPC = void $ write PC ((+offset) <$> pc) - in whenS zeroSet modifyPC - --- jumpZeroMemory :: Map.Map Key Value --- jumpZeroMemory = --- Map.fromList [ ("ic", 0) --- , ("zero", 0) --- ] - ------------------------------------ --- Add with overflow tracking ----- ------------------------------------ - -{- The following example will demonstrate how important it is to be aware of your effects. - - Problem: implement the semantics of add instruction which would calculate the sum and write it - to the specified destination, update the 'zero' flag if the sum was zero, and also detect if - integer overflow happened and update 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. --- --- > analyse (addOverflow "x" "y" "z") --- ([],Left (W "overflow" :| [R "y",R "x",W "zero",W "z",R "y",R "x"])) --- --- Thus, 'willOverflowPure' might be though as a atomic microcommand in some sense. -addOverflow :: Key -> Key -> Key -> ISA Value -addOverflow var1 var2 dest = - let arg1 = read var1 - arg2 = read var2 - result = (+) <$> arg1 <*> arg2 - isZero = (==) <$> pure 0 <*> write dest result - overflow = willOverflowPure <$> arg1 <*> arg2 - in write (Flag Zero) (fromBool <$> isZero) *> - write (Flag Overflow) (fromBool <$> overflow) - -willOverflowPure :: Value -> Value -> Bool -willOverflowPure arg1 arg2 = - let o1 = (>) arg2 0 - o2 = (>) arg1((-) maxBound arg2) - o3 = (<) arg2 0 - o4 = (<) arg1((-) minBound arg2) - 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 (var1 3x times and var2 5x times) --- --- > analyse (addOverflowNaive "x" "y" "z") --- ([],Left (W "overflow" :| [R "y",R "x",R "y",R "y",R "x",R "y",W "zero",W "z",R "y",R "x"])) --- --- It is not clear at the moment what to do with that. Should we avoid this style? Or could it be --- sometimes useful? -addOverflowNaive :: Key -> Key -> Key -> ISA Value -addOverflowNaive var1 var2 dest = - let arg1 = read var1 - arg2 = read var2 - result = (+) <$> arg1 <*> arg2 - isZero = (==) <$> pure 0 <*> write dest result - overflow = willOverflow arg1 arg2 - in write (Flag Zero) (fromBool <$> isZero) *> - write (Flag Overflow) (fromBool <$> overflow) - -willOverflow :: ISA Value -> ISA Value -> ISA 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/src/Control/Selective/Example/ISA/Instruction.hs b/src/Control/Selective/Example/ISA/Instruction.hs deleted file mode 100644 index fae104f..0000000 --- a/src/Control/Selective/Example/ISA/Instruction.hs +++ /dev/null @@ -1,333 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE LambdaCase #-} - -module Control.Selective.Example.ISA.Instruction where - -import Prelude hiding (div, mod, read) -import qualified Prelude (div, mod) -import qualified Data.List.NonEmpty as NonEmpty -import Data.List.NonEmpty (NonEmpty (..)) -import Data.Functor (void) --- import qualified Data.Map as Map -import qualified Data.Set as Set -import Data.Maybe (fromJust) -import Control.Selective -import Algebra.Graph -import Algebra.Graph.Export.Dot -import Control.Selective.Example.ISA.Types - --------------------------------------------------------------------------------- --------- Instructions ---------------------------------------------------------- --------------------------------------------------------------------------------- - -data Instruction where - Halt :: Instruction - Load :: Register -> Address -> Instruction - Set :: Register -> Value -> Instruction - Store :: Register -> Address -> Instruction - Add :: Register -> Address -> Instruction - Sub :: Register -> Address -> Instruction - Mul :: Register -> Address -> Instruction - Div :: Register -> Address -> Instruction - Mod :: Register -> Address -> Instruction - Abs :: Register -> Instruction - Jump :: Value -> Instruction - JumpZero :: Value -> Instruction - LoadMI :: Register -> Address -> Instruction - -deriving instance Show Instruction - -type Program = NonEmpty (InstructionAddress, Instruction) - -semantics :: Instruction -> ISA Value -semantics i = case i of - Halt -> halt - Load reg addr -> load reg addr - LoadMI _ _ -> undefined -- loadMI reg addr - Set reg val -> set reg val - Store reg addr -> store reg addr - Add reg1 addr -> addOverflow reg1 addr - Sub reg1 addr -> sub reg1 addr - Mul reg addr -> mul reg addr - Div reg addr -> div reg addr - Mod reg addr -> mod reg addr - Abs _ -> undefined -- abs (Register reg) - Jump simm8 -> jump simm8 - JumpZero simm8 -> jumpZero simm8 - -blockSemantics :: NonEmpty Instruction -> ISA Value -blockSemantics is = - let meanings = fmap semantics is - in foldl (*>) (NonEmpty.head meanings) (NonEmpty.tail meanings) - -------------- --- Halt ----- -------------- - -halt :: ISA Value -halt = write (Flag Halted) (pure 1) - ------------- --- Set ----- ------------- - -set :: Register -> Value -> ISA Value -set reg = write (Reg reg) . pure - -------------- --- Load ----- -------------- - -load :: Register -> Address -> ISA Value -load reg addr = write (Reg reg) (read (Cell addr)) - --------------- --- Store ----- --------------- - -store :: Register -> Address -> ISA Value -store reg addr = write (Cell addr) (read (Reg reg)) - ------------- --- Add ----- ------------- - --- | Read the values of the variables "x" and "y" and write the sum into the variable "z". --- If the sum is zero, write 1 into the variable "zero", otherwise put 0 there. --- --- This implementation looks intuitive, but it is wrong, since the two write operations --- can be considered independent and the effects required for computing the sum, i.e. --- 'read "x" <*> read "y"' will be executed twice. Consequently: --- * the value written into the "z" variable is not guaranteed to be the same as the one which was --- compared to zero, --- * the static analysis of the computations reports more dependencies then one might have --- naively expected --- --- > getEffects addNaive --- [Read R0,Read 0,Write Zero,Read R0,Read 0,Write R0] --- --- Here, the two instances of 'sum' cause the duplication of 'Read R0' and 'Read 0' effects. -addNaive :: Register -> Address -> ISA Value -addNaive reg addr = - let sum = (+) <$> read (Reg reg) <*> read (Cell addr) - isZero = (==) <$> sum <*> pure 0 - in write (Flag Zero) (ifS isZero (pure 1) (pure 0)) - *> write (Reg reg) sum - --- | This implementations of 'add' executes the effects associated with the 'sum' value only once and --- then wires the pure value into the computations which require it without triggering the effects again. --- --- > analyse add --- ([],Left (W "zero" :| [W "z",R "y",R "x"])) --- -add :: Register -> Address -> ISA Value -add reg addr = - let x = read (Reg reg) - y = read (Cell addr) - sum = (+) <$> x <*> y - isZero = (==) <$> pure 0 <*> write (Reg reg) sum - in write (Flag Zero) (fromBool <$> isZero) - --- -- | This is a fully inlined version of 'add' --- addNormalForm :: ISA Value --- addNormalForm = --- write "zero" (ifS ((==) <$> pure 0 <*> write "z" ((+) <$> read "x" <*> read "y")) (pure 1) (pure 0)) - --- addState :: Memory --- addState = --- Map.fromList [ ("x", 255) --- , ("y", 1) --- , ("zero", 0) --- , ("overflow", 0) --- , ("ic", 0) --- ] - ------------------ --- jumpZero ----- ------------------ -jumpZero :: Value -> ISA Value -jumpZero offset = - let zeroSet = (/=) <$> pure 0 <*> read (Flag Zero) - -- modifyPC = void $ write PC (pure offset) -- (fmap (+ offset) pc) - modifyPC = void $ write PC ((+offset) <$> read PC) - in whenS zeroSet modifyPC *> pure offset - --- | Unconditional jump. -jump :: Value -> ISA Value -jump simm = - write PC (fmap ((+) $ simm) (read PC)) - --- jumpZeroMemory :: Map.Map Key Value --- jumpZeroMemory = --- Map.fromList [ ("ic", 0) --- , ("zero", 0) --- ] - ------------------------------------ --- Add with overflow tracking ----- ------------------------------------ - -{- The following example will demonstrate how important it is to be aware of your effects. - - Problem: implement the semantics of add instruction which would calculate the sum and write it - to the specified destination, update the 'zero' flag if the sum was zero, and also detect if - integer overflow happened and update 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. --- --- > getEffects (addOverflow R0 1) --- [Read R0,Read 1,Write R0,Write Zero,Read R0,Read 1,Write Overflow] --- --- Thus, 'willOverflowPure' might be though as a atomic microcommand in some sense. -addOverflow :: Register -> Address -> ISA Value -addOverflow reg addr = - let arg1 = read (Reg reg) - arg2 = read (Cell addr) - result = (+) <$> arg1 <*> arg2 - isZero = (==) <$> pure 0 <*> write (Reg reg) result - overflow = willOverflowPure <$> arg1 <*> arg2 - in write (Flag Zero) (fromBool <$> isZero) *> - write (Flag Overflow) (fromBool <$> overflow) - -willOverflowPure :: Value -> Value -> Bool -willOverflowPure arg1 arg2 = - let o1 = (>) arg2 0 - o2 = (>) arg1((-) maxBound arg2) - o3 = (<) arg2 0 - o4 = (<) arg1((-) minBound arg2) - 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 (var1 3x times and addr 5x times) --- --- > analyse (addOverflowNaive "x" "y" "z") --- ([],Left (W "overflow" :| [R "y",R "x",R "y",R "y",R "x",R "y",W "zero",W "z",R "y",R "x"])) --- --- It is not clear at the moment what to do with that. Should we avoid this style? Or could it be --- sometimes useful? -addOverflowNaive :: Register -> Address -> ISA Value -addOverflowNaive reg addr = - let arg1 = read (Reg reg) - arg2 = read (Cell addr) - result = (+) <$> arg1 <*> arg2 - isZero = (==) <$> pure 0 <*> write (Reg reg) result - overflow = willOverflow arg1 arg2 - in write (Flag Zero) (fromBool <$> isZero) *> - write (Flag Overflow) (fromBool <$> overflow) - --- add0 :: ISA (Value, Value, Bool, Bool, Value) --- add0 = (\x y -> (x, y, True, True, 0)) <$> read (Reg R0) <*> read (Mem 1) - --- add1 :: ISA (Value, Value, Bool, Bool, Value) --- add1 = (\(x, y, zero, overflow, sum) -> (x, y, x + y == 0, willOverflowPure x y, x + y)) <$> add0 - --- add2 :: ISA Value --- add2 = write (Reg R1) ((\(x, y, z, o, s) -> s) <$> add1) *> --- write (F Zero) ((\(x, y, z, o, s) -> fromBool z) <$> add1) - - -willOverflow :: ISA Value -> ISA Value -> ISA 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) - ----------------------------------------------------------------------------------------------------- - --- | Subtraction --- NOTE: currently always sets the 'Overflow' flag to zero -sub :: Register -> Address -> ISA Value -sub reg addr = - let arg1 = read (Reg reg) - arg2 = read (Cell addr) - result = (-) <$> arg1 <*> arg2 - isZero = (==) <$> pure 0 <*> write (Reg reg) result - in write (Flag Zero) (fromBool <$> isZero) *> - write (Flag Overflow) (pure 0) - --- | Multiply a value from memory location to one in a register. --- Applicative. -mul :: Register -> Address -> ISA Value -mul reg addr = - let result = (*) <$> read (Reg reg) <*> read (Cell addr) - in write (Flag Zero) (fromBool . (== 0) <$> write (Reg reg) result) - -div :: Register -> Address -> ISA Value -div reg addr = - let result = Prelude.div <$> read (Reg reg) <*> read (Cell addr) - in write (Flag Zero) (fromBool . (== 0) <$> write (Reg reg) result) - -mod :: Register -> Address -> ISA Value -mod reg addr = - let result = Prelude.mod <$> read (Reg reg) <*> read (Cell addr) - in write (Flag Zero) (fromBool . (== 0) <$> write (Reg reg) result) - -toAddress :: Value -> Address -toAddress = fromIntegral - -loadMI :: Register -> Address -> ISA Value -loadMI reg addr = - read (Cell addr) `bindS` \x -> - write (Reg reg) (read (Cell . toAddress $ x)) - --- -------------------------------------------------------------------------------- - -partition :: [RW a] -> ([Key], [Key]) -partition = foldl go ([], []) - where go (accR, accW) = \case (Read k _) -> (k : accR, accW) - (Write k _ _) -> (accR, k : accW) - --- | Compute static data flow graph of an instruction. -instructionGraph :: (InstructionAddress, Instruction) - -> Graph (Either Key (InstructionAddress, Instruction)) -instructionGraph instrInfo@(_, instr) = - let (ins, outs) = partition $ getEffectsISA (semantics instr) - in overlay (star (Right instrInfo) (map Left outs)) - (transpose $ star (Right instrInfo) (map Left ins)) - --- | Compute static data flow graph of a program. -programGraph :: [(InstructionAddress, Instruction)] - -> Graph (Either Key (InstructionAddress, Instruction)) -programGraph p = foldl go empty (map instructionGraph p) - where go acc g = overlay acc g --------------------------------------------------------------------------------- - --- | Serialise data flow graph as a .dot string --- drawGraph :: Graph (Either String (InstructionAddress, Instruction)) -> String -drawGraph :: Graph (Either Key (InstructionAddress, Instruction)) -> String -drawGraph g = - let g' = stringifyVertex <$> g - names = vertexSet g' - style = defaultStyleViaShow - { vertexName = \v -> "v" ++ show (fromJust $ Set.lookupIndex v names) - , vertexAttributes = \x -> case x of - Left k -> [ "shape" := "circle" - , "label" := k ] - Right i -> [ "shape" := "record" - , "label" := i ] } - in export style g' - where - stringifyVertex :: Either Key (InstructionAddress, Instruction) -> - Either String String - stringifyVertex (Left k) = Left (show k) - stringifyVertex (Right (a, i)) = Right $ show a <> "|" <> show i \ No newline at end of file diff --git a/src/Control/Selective/Example/ISA/Programs.hs b/src/Control/Selective/Example/ISA/Programs.hs deleted file mode 100644 index b9dd4fd..0000000 --- a/src/Control/Selective/Example/ISA/Programs.hs +++ /dev/null @@ -1,100 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE StandaloneDeriving #-} - - - -module Control.Selective.Example.ISA.Programs where - -import Prelude hiding (mod, read) -import Data.List.NonEmpty (fromList, toList) -import Control.Selective.Example.ISA.Types -import Control.Selective.Example.ISA.Instruction -import Control.Selective.Example.ISA.Simulate - -addProgram :: Program -addProgram = fromList $ zip [0..] - [Add R0 1] - -addGraph :: IO () -addGraph = writeFile "add.dot" $ - drawGraph (programGraph (toList addProgram)) - -jumpZeroProgram :: Program -jumpZeroProgram = fromList $ zip [0..] - [JumpZero 42] - -jumpZeroGraph :: IO () -jumpZeroGraph = writeFile "jumpZero.dot" $ - drawGraph (programGraph (toList jumpZeroProgram)) - -addAndJump :: Program -addAndJump = fromList $ zip [0..] - [ Add R0 1 - , JumpZero 2 - ] - -addAndJumpSemantics :: ISA Value -addAndJumpSemantics = - addOverflow R0 1 *> - jumpZero 2 - -addAndJumpGraph :: IO () -addAndJumpGraph = writeFile "addAndJump.dot" $ - drawGraph (programGraph (toList addAndJump)) - -notEqual :: Program -notEqual = fromList $ zip [0..] - [ Load R0 0 - , Sub R0 1 - , JumpZero 1 - , Set R1 1 - , Halt - ] - -notEqualGraph :: IO () -notEqualGraph = writeFile "notEqual.dot" $ - drawGraph (programGraph (toList notEqual)) - -notEqualSemantics :: ISA Value -notEqualSemantics = - load R0 0 *> - sub R0 1 *> - jumpZero 1 *> - set R1 1 *> - halt - -notEqualState :: Value -> Value -> ISAState -notEqualState x y = boot notEqual (initialiseMemory [(0, x), (1, y), (2, 42)]) - -gcdProgram :: Program -gcdProgram = fromList $ zip [0..] - -- # Find the greatest common divisor of values in memory locations 0 and 1, - -- # put result to the register R1 - [ (Set R0 0) - , (Store R0 255) - , (Load R0 1) - -- # Test register R0 for being zero by subtracting zero - , (Sub R0 255) - -- # Halt if register R0 contains zero, loop otherwise - , (JumpZero 6) - , (Load R0 0) - , (Mod R0 1) - , (Load R1 1) - , (Store R0 1) - , (Store R1 0) - , (Jump (-8)) - , Halt - ] - -gcdGraph :: IO () -gcdGraph = writeFile "gcd.dot" $ - drawGraph (programGraph (toList gcdProgram)) - -gcdState :: Value -> Value -> ISAState -gcdState x y = boot gcdProgram (initialiseMemory [(0, x), (1, y)]) \ No newline at end of file diff --git a/src/Control/Selective/Example/ISA/Simulate.hs b/src/Control/Selective/Example/ISA/Simulate.hs deleted file mode 100644 index 08e4c3a..0000000 --- a/src/Control/Selective/Example/ISA/Simulate.hs +++ /dev/null @@ -1,109 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE StandaloneDeriving #-} - -module Control.Selective.Example.ISA.Simulate where - -import Prelude hiding (mod, read, (!!)) -import Data.List.NonEmpty (NonEmpty (..), (!!)) -import qualified Control.Monad.State as S -import qualified Data.Map.Strict as Map -import Control.Selective -import Control.Selective.Free.Rigid -import Control.Selective.Example.ISA.Types -import Control.Selective.Example.ISA.Instruction - --- | Hijack mtl's MonadState constraint to include Selective -type MonadState s m = (Selective m, S.MonadState s m) - -type RegisterBank = Map.Map Register Value - -emptyRegisters :: RegisterBank -emptyRegisters = Map.fromList [(R0, 0), (R1, 0), (R2, 0), (R3, 0)] - --- | We model memory as a map from bytes to signed 16-bit words -type Memory = Map.Map Address Value - -emptyMemory :: Memory -emptyMemory = Map.fromList $ zip [0..maxBound] (repeat 0) - -initialiseMemory :: [(Address, Value)] -> Memory -initialiseMemory m = - let blankMemory = Map.fromList $ zip [0..255] [0, 0..] - in foldr (\(addr, value) acc -> Map.adjust (const value) addr acc) blankMemory m - -type Flags = Map.Map Flag Value - -emptyFlags :: Flags -emptyFlags = Map.fromList [(Zero, 0), (Overflow, 0), (Halted, 0)] - -data ISAState = ISAState { registers :: RegisterBank - , memory :: Memory - -- | Program counter - , pc :: InstructionAddress - -- | Instruction register - , program :: NonEmpty Instruction - , flags :: Flags - } deriving Show - --- | Interpret the internal ISA effect in 'MonadState' -toState :: MonadState ISAState m => RW a -> m a -toState (Read 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 -> S.gets pc -toState (Write k fv t) = case k of - Reg r -> do v <- runSelect toState fv - let step s = Map.insert r v (registers s) - S.state $ \s -> (t v, s { registers = step s }) - Cell addr -> do v <- runSelect toState fv - let step s = Map.insert addr v (memory s) - S.state $ \s -> (t v, s { memory = step s }) - Flag f -> do v <- runSelect toState fv - let step s = Map.insert f v (flags s) - S.state $ \s -> (t v, s { flags = step s }) - PC -> do v <- runSelect toState fv - S.state (\s -> (t v, s { pc = v })) - --- | Interpret a 'Program' in the state monad -runProgram :: ISA a -> ISAState -> (a, ISAState) -runProgram f s = S.runState (runSelect toState f) s - -boot :: Program -> Memory -> ISAState -boot prog mem = ISAState { registers = emptyRegisters - , memory = mem - , pc = 0 - , program = fmap snd prog - , flags = emptyFlags - } - -executeInstruction :: MonadState ISAState m => m Value -executeInstruction = do - s <- S.get - -- fetch instruction - let i = (program s) !! (fromIntegral $ pc s) - (v, s') = S.runState (runSelect toState (semantics $ i)) s - S.put (s' {pc = pc s' + 1}) - pure v - -- -- fetch instruction - -- ic <- read IC - -- write IR (read (Prog ic)) - -- -- increment instruction counter - -- write IC (pure $ ic + 1) - -- -- read instruction register and execute the instruction - -- i <- read IR - -- instructionSemantics' i read write - -simulate :: Int -> ISAState -> ISAState -simulate steps state - | steps <= 0 = state - | otherwise = if halted then state else simulate (steps - 1) nextState - where - halted = (/= 0) $ (Map.!) (flags state) Halted - nextState = snd $ S.runState executeInstruction state \ No newline at end of file diff --git a/src/Control/Selective/Example/ISA/Types.hs b/src/Control/Selective/Example/ISA/Types.hs deleted file mode 100644 index 1ba3a63..0000000 --- a/src/Control/Selective/Example/ISA/Types.hs +++ /dev/null @@ -1,91 +0,0 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE StandaloneDeriving #-} - -module Control.Selective.Example.ISA.Types where - -import Prelude hiding (read) -import Data.Word (Word8) -import Data.Functor (void) -import Data.Int (Int8) -import Control.Selective -import Control.Selective.Free.Rigid - -fromBool :: Num a => Bool -> a -fromBool True = 1 -fromBool False = 0 --- fromBool = bool 0 1 - --------------------------------------------------------------------------------- --------- Types ----------------------------------------------------------------- --------------------------------------------------------------------------------- - --- | The ISA operates signed 16-bit words -type Value = Int8 - --- | The ISA has 4 registers -data Register = R0 | R1 | R2 | R3 - deriving (Show, Eq, Ord) - -r0, r1, r2, r3 :: Register -r0 = R0 -r1 = R1 -r2 = R2 -r3 = R3 - --- | The address space is indexed by one byte -type Address = Word8 - --- | The ISA has two flags -data Flag = Zero -- ^ tracks if the result of the last arithmetical operation was zero - | Overflow -- ^ tracks integer overflow - | Halted - deriving (Show, Eq, Ord) - --- | Address in the program memory -type InstructionAddress = Value - --- | Index the locations of the ISA -data Key = Reg Register - | Cell Address - | Flag Flag - | PC - deriving (Eq) - -instance Show Key where - show (Reg r ) = show r - show (Cell addr) = show addr - show (Flag f) = show f - show PC = "PC" - -data RW a = Read Key (Value -> a) - | Write Key (ISA Value) (Value -> a) - deriving Functor - -instance Show a => Show (RW a) where - show (Read k _) = "Read " ++ show k - show (Write k (Pure v) _) = "Write " ++ show k ++ " " ++ show v - show (Write k _ _) = "Write " ++ show k - -type ISA a = Select RW a - -read :: Key -> ISA Value -read k = liftSelect (Read k id) - -write :: Key -> ISA Value -> ISA Value -write k p = liftSelect (Write k p id) - --- | Interpret 'Read' and 'Write' commands in the 'Over' selective functor -inOver :: RW a -> Over [RW ()] b -inOver (Read k _ ) = Over [void $ Read k (const ())] -inOver (Write k fv _) = void (runSelect inOver fv) *> - Over [Write k fv (const ())] - --- | Get effects of an ISA semantics computation -getEffectsISA :: ISA a -> [RW ()] -getEffectsISA = getOver . runSelect inOver diff --git a/src/Control/Selective/Example/Teletype.hs b/src/Control/Selective/Example/Teletype.hs deleted file mode 100644 index b03f2d5..0000000 --- a/src/Control/Selective/Example/Teletype.hs +++ /dev/null @@ -1,49 +0,0 @@ -{-# LANGUAGE DeriveFunctor, GADTs #-} -module Control.Selective.Example.Teletype where - -import Prelude hiding (getLine, putStrLn) -import qualified Prelude (getLine, putStrLn) -import Control.Selective -import Control.Selective.Free.Rigid - -data TeletypeF a = Read (String -> a) - | Write String a - deriving Functor - -instance Show (TeletypeF a) where - show (Read _) = "Read" - show (Write s _) = "Write " ++ show s - --- | Interpret the 'TeletypeF' commands as IO actions -toIO :: TeletypeF a -> IO a -toIO (Read f) = f <$> Prelude.getLine -toIO (Write s a) = a <$ Prelude.putStrLn s - --- | A Teletype program is a free Selective over the 'TeletypeF' functor -type Teletype a = Select TeletypeF a - -getLine :: Teletype String -getLine = liftSelect (Read id) - -putStrLn :: String -> Teletype () -putStrLn s = liftSelect (Write s ()) - -greeting :: IO () -greeting = Prelude.getLine >>= \name -> Prelude.putStrLn ("Hello, " ++ name) - --- | The example from the paper's intro. Implemented in terms of the free --- selective, can now be statically analysed for effects: --- --- > getEffects pingPongS --- [Read,Write "pong"] --- --- We can also execute the program in IO: --- > runSelect toIO pingPong --- ping --- pong --- --- > runSelect toIO pingPong --- bing --- -pingPongS :: Teletype () -pingPongS = whenS (fmap ("ping"==) getLine) (putStrLn "pong") diff --git a/src/Control/Selective/Free/Rigid.hs b/src/Control/Selective/Free/Rigid.hs index eaf8a3f..406cd74 100644 --- a/src/Control/Selective/Free/Rigid.hs +++ b/src/Control/Selective/Free/Rigid.hs @@ -1,19 +1,32 @@ --- Free selective functors for the simple case when @<*> = apS@. --- See the general construction in "Control.Selective.Free". {-# 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 ( - -- * Re-exports - module Control.Selective, + -- * Free rigid selective functors + Select (..), liftSelect, - -- * Free selective functors - Select (..), analyse, getPure, liftSelect, runSelect, foldSelect, - getEffects, getNecessaryEffect, selectOpt + -- * Static analysis + getPure, getEffects, getNecessaryEffect, runSelect, foldSelect ) where import Control.Monad.Trans.Except import Data.Bifunctor import Data.Functor -import Data.List.NonEmpty import Control.Selective -- Inspired by free applicative functors by Capriotti and Kaposi. @@ -26,34 +39,35 @@ import Control.Selective -- 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 selective functors. + +-- | 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: Verify that this is a lawful 'Functor'. +-- 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: Verify that this is a lawful 'Applicative'. +-- TODO: Prove that this is a lawful 'Applicative'. instance Functor f => Applicative (Select f) where pure = Pure - (<*>) = apS + (<*>) = apS -- Rigid selective functors --- TODO: Verify that this is a lawful 'Selective'. +-- TODO: Prove that this is a lawful 'Selective'. instance Functor f => Selective (Select f) where - -- Law P1 + -- Identity law select x (Pure y) = either y id <$> x - -- Law A1 + -- 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 - -- select = selectOpt +{- 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 @@ -69,19 +83,7 @@ go x (Select y z) k = Select (go (f <$> x) y (g . second k)) ((h . (k.)) <$> z) f x = Right <$> x g y = \a -> bimap (,a) ($a) y h z = uncurry z - --- | Statically analyse a given selective computation and return a pair: --- * The list of effects @fs@ that are statically known as /unnecessary/. --- * Either --- + The non-empty list of remaining effects @gs@, first of which is --- statically guaranteed to be /necessary/; or --- + The resulting value, in which case there are no necessary effects. -analyse :: Functor f => Select f a -> ([f ()], Either (NonEmpty (f ())) a) -analyse (Pure a) = ([], Right a) -analyse (Select x f) = case analyse x of - (fs, Right (Right x)) -> (void f : fs, Right x ) - (fs, Right (Left _)) -> (fs , Left (void f :| [])) - (fs, Left gs ) -> (fs , Left (void f <| gs)) +-} -- | Lift a functor into a free selective computation. liftSelect :: Functor f => f a -> Select f a @@ -94,21 +96,20 @@ 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 a. f a -> m) -> Select f a -> m +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. This is --- equivalent to @eitherToMaybe . snd . analyse@ but has no 'Functor' constraint. +-- | 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) - -getEffects = getOver . runSelect (Over . pure . void) +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. diff --git a/src/Control/Selective/Free/Rigid/Generalised.hs b/src/Control/Selective/Free/Rigid/Generalised.hs deleted file mode 100644 index 039d359..0000000 --- a/src/Control/Selective/Free/Rigid/Generalised.hs +++ /dev/null @@ -1,99 +0,0 @@ --- Free selective functors for the simple case when @<*> = apS@. --- This module uses a generalised approach to constructing free structures. --- See "Control.Selective.Free" for a simpler, non-generalised approach. -{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures, RankNTypes #-} -{-# LANGUAGE TupleSections, TypeOperators #-} -module Control.Selective.Free.Rigid.Generalised ( - -- * Re-exports - module Control.Selective, - - -- * Free functors - FreeA, FreeS, FreeM, analyse, liftS, runS - ) where - -import Data.Bifunctor -import Data.Functor -import Data.List.NonEmpty -import Control.Selective - --- This is a generalised free construction that works for free applicative and --- selective functors, as well as monads. See "Control.Selective.Free" for a --- non-generalised version. - --- Three ways of composing functors, whose definitions mirror the type --- signatures of the Applicative's (<*>), Selective's (<*?>) and Monad's (>>=) --- operators. --- Inspired by these awesome blog posts by Bartosz Milewski and Oleg Grenrus: --- https://bartoszmilewski.com/2018/02/17/free-monoidal-functors/ --- http://oleg.fi/gists/posts/2018-02-21-single-free.html -data (:+:) f g a where - (:+:) :: f x -> g (x -> a) -> (f :+: g) a - -data (:|:) f g a where - (:|:) :: f (x -> a) -> g (Either x a) -> (:|:) f g a - -data (:*:) f g a where - (:*:) :: f x -> (x -> g a) -> (:*:) f g a - -data Free (p :: (* -> *) -> (* -> *) -> (* -> *)) f a - = Done a - | More (p f (Free p f) a) - -type FreeA = Free (:+:) -type FreeS = Free (:|:) -type FreeM = Free (:*:) - -instance Functor g => Functor (f :+: g) where - fmap k (f :+: g) = f :+: fmap (fmap k) g - -instance (Functor f, Functor g) => Functor (f :|: g) where - fmap k (f :|: g) = fmap (fmap k) f :|: fmap (fmap k) g - -instance Functor g => Functor (f :*: g) where - fmap k (f :*: g) = f :*: fmap (fmap k) g - -instance Functor f => Functor (Free (:|:) f) where - fmap k (Done a) = Done (k a) - fmap k (More f) = More (fmap k f) - -instance Functor f => Applicative (Free (:|:) f) where - pure = Done - (<*>) = apS - --- Inspired by free applicative functors by Capriotti and Kaposi. --- TODO: This implementation is slow, but we could optimise it similarly to --- http://hackage.haskell.org/package/free/docs/Control-Applicative-Free-Fast.html -instance Functor f => Selective (FreeS f) where - -- Law P1 - select x (Done f) = either f id <$> x - - -- Law A1 - select x (More (z :|: y)) = More ((h <$> z) :|: select (f <$> x) (g <$> y)) - where - f x = Right <$> x - g y = \a -> bimap (,a) ($a) y - h z = uncurry z - --- | Statically analyse a given selective computation and return a pair (fs, x) --- comprising: --- * The list of effects @fs@ that are statically known as unnecessary. --- * Either --- - The non-empty list of remaining effects @gs@, first of which is --- statically known to be necessary; or --- - The resulting value, in which case there are no necessary effects. -analyse :: Functor f => FreeS f a -> ([f ()], Either (NonEmpty (f ())) a) -analyse (Done a) = ([], Right a) -analyse (More (f :|: x)) = case analyse x of - (fs, Right (Right x)) -> (void f : fs, Right x ) - (fs, Right (Left _)) -> (fs , Left (void f :| [])) - (fs, Left gs ) -> (fs , Left (void f <| gs)) - --- | Lift a functor into a free selective computation. -liftS :: Functor f => f a -> FreeS f a -liftS f = More $ fmap const f :|: Done (Left ()) - --- | Given a natural transformation from @f@ to @g@, this gives a canonical --- natural transformation from @FreeS f@ to @g@. -runS :: Selective g => (forall a. f a -> g a) -> FreeS f a -> g a -runS _ (Done a) = pure a -runS t (More (f :|: x)) = select (runS t x) (t f) diff --git a/test/Main.hs b/test/Main.hs index 0d44744..a5bbe11 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -1,21 +1,63 @@ {-# LANGUAGE TypeApplications #-} -import Prelude hiding (maybe) +import Data.Maybe hiding (maybe) import Data.Functor.Identity +import Prelude hiding (maybe) import Test.Tasty -import Test.Tasty.QuickCheck as QC +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 "Selective instances" - [over, under, validation, arrowMonad, maybe, identity] +main = defaultMain $ testGroup "Tests" + [pingPong, build, over, under, validation, arrowMonad, maybe, identity] --- main :: IO () --- main = do --- putStrLn $ "\n\nCyclic dependency graph:\n\n" ++ draw task "B1" +-------------------------------------------------------------------------------- +------------------------ 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 -------------------------------------------------- @@ -23,35 +65,36 @@ main = defaultMain $ testGroup "Selective instances" over :: TestTree over = testGroup "Over" [overLaws, overTheorems, overProperties] +overLaws :: TestTree overLaws = testGroup "Laws" - [ QC.testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ + [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ \x -> lawIdentity @(Over String) x - , QC.testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ + , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ \x -> lawDistributivity @(Over String) @Int @Int x - , QC.testProperty "Associativity: take a look at tests/Laws.hs" $ + , testProperty "Associativity: take a look at tests/Laws.hs" $ \x -> lawAssociativity @(Over String) @Int @Int x ] overTheorems = testGroup "Theorems" - [ QC.testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $ + [ 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 - , QC.testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $ + , 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 - , QC.testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ + , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ \x -> theorem3 @(Over String) @Int @Int @Int x - , QC.testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ + , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ \x -> theorem4 @(Over String) @Int @Int x - , QC.testProperty "(f <*> g) == (f `apS` g)" $ + , testProperty "(f <*> g) == (f `apS` g)" $ \x -> theorem5 @(Over String) @Int @Int x - , QC.testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ + , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ \x -> theorem6 @(Over String) @Int @Int x ] overProperties = testGroup "Properties" [ expectFail $ - QC.testProperty "pure-right: pure (Right x) <*? y = pure x" $ + testProperty "pure-right: pure (Right x) <*? y = pure x" $ \x -> propertyPureRight @(Over String) @Int @Int x - , QC.testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ + , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ \x -> propertyPureLeft @(Over String) @Int @Int x ] @@ -61,36 +104,39 @@ overProperties = testGroup "Properties" under :: TestTree under = testGroup "Under" [underLaws, underTheorems, underProperties] +underLaws :: TestTree underLaws = testGroup "Laws" - [ QC.testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ + [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ \x -> lawIdentity @(Under String) x - , QC.testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ + , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ \x -> lawDistributivity @(Under String) @Int @Int x - , QC.testProperty "Associativity: take a look at tests/Laws.hs" $ + , testProperty "Associativity: take a look at tests/Laws.hs" $ \x -> lawAssociativity @(Under String) @Int @Int x ] +underTheorems :: TestTree underTheorems = testGroup "Theorems" - [ QC.testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $ + [ 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 - , QC.testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $ + , 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 - , QC.testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ + , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ \x -> theorem3 @(Under String) @Int @Int @Int x - , QC.testProperty "Generalised identity: (x <*? pure y) == (either y id <$> 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" $ - QC.testProperty "(f <*> g) == (f `apS` g)" $ + testProperty "(f <*> g) == (f `apS` g)" $ \x -> theorem5 @(Under String) @Int @Int x - , QC.testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ + , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ \x -> theorem6 @(Under String) @Int @Int x ] +underProperties :: TestTree underProperties = testGroup "Properties" - [ QC.testProperty "pure-right: pure (Right x) <*? y = pure x" $ + [ testProperty "pure-right: pure (Right x) <*? y = pure x" $ \x -> propertyPureRight @(Under String) @Int @Int x , expectFail $ - QC.testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ + testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ \x -> propertyPureLeft @(Under String) @Int @Int x ] -------------------------------------------------------------------------------- @@ -99,40 +145,60 @@ underProperties = testGroup "Properties" -------------------------------------------------------------------------------- validation :: TestTree validation = testGroup "Validation" - [validationLaws, validationTheorems, validationProperties] + [validationLaws, validationTheorems, validationProperties, validationExample] +validationLaws :: TestTree validationLaws = testGroup "Laws" - [ QC.testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ + [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ \x -> lawIdentity @(Validation String) @Int x - , QC.testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ + , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ \x -> lawDistributivity @(Validation String) @Int @Int x - , QC.testProperty "Associativity: take a look at tests/Laws.hs" $ + , testProperty "Associativity: take a look at tests/Laws.hs" $ \x -> lawAssociativity @(Validation String) @Int @Int @Int x ] +validationTheorems :: TestTree validationTheorems = testGroup "Theorems" - [ QC.testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $ + [ 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 - , QC.testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $ + , 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 - , QC.testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ + , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ \x -> theorem3 @(Validation String) @Int @Int @Int x - , QC.testProperty "Generalised identity: (x <*? pure y) == (either y id <$> 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" $ - QC.testProperty "(f <*> g) == (f `apS` g)" $ + testProperty "(f <*> g) == (f `apS` g)" $ \x -> theorem5 @(Validation String) @Int @Int x , expectFailBecause "'Validation' is a non-rigid selective functor" $ - QC.testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ + testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ \x -> theorem6 @(Validation String) @Int @Int @Int x ] +validationProperties :: TestTree validationProperties = testGroup "Properties" - [ QC.testProperty "pure-right: pure (Right x) <*? y = pure x" $ + [ testProperty "pure-right: pure (Right x) <*? y = pure x" $ \x -> propertyPureRight @(Validation String) @Int @Int x - , QC.testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ + , 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 -------------------------------------------- -------------------------------------------------------------------------------- @@ -142,37 +208,37 @@ arrowMonad = testGroup "ArrowMonad (->)" [arrowMonadLaws, arrowMonadTheorems, arrowMonadProperties] arrowMonadLaws = testGroup "Laws" - [ QC.testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ + [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ \x -> lawIdentity @(ArrowMonad (->)) @Int x - , QC.testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ + , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ \x -> lawDistributivity @(ArrowMonad (->)) @Int @Int x - , QC.testProperty "Associativity: take a look at tests/Laws.hs" $ + , testProperty "Associativity: take a look at tests/Laws.hs" $ \x -> lawAssociativity @(ArrowMonad (->)) @Int @Int @Int x - , QC.testProperty "select == selectM" $ + , testProperty "select == selectM" $ \x -> lawMonad @(ArrowMonad (->)) @Int @Int x - , QC.testProperty "select == selectA" $ + , testProperty "select == selectA" $ \x -> selectALaw @(ArrowMonad (->)) @Int @Int x ] arrowMonadTheorems = testGroup "Theorems" - [ QC.testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $ + [ 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 - , QC.testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $ + , 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 - , QC.testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ + , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ \x -> theorem3 @(ArrowMonad (->)) @Int @Int @Int x - , QC.testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ + , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ \x -> theorem4 @(ArrowMonad (->)) @Int @Int x - , QC.testProperty "(f <*> g) == (f `apS` g)" $ + , testProperty "(f <*> g) == (f `apS` g)" $ \x -> theorem5 @(ArrowMonad (->)) @Int @Int x - , QC.testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ + , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ \x -> theorem6 @(ArrowMonad (->)) @Int @Int @Int x ] arrowMonadProperties = testGroup "Properties" - [ QC.testProperty "pure-right: pure (Right x) <*? y = pure x" $ + [ testProperty "pure-right: pure (Right x) <*? y = pure x" $ \x -> propertyPureRight @(ArrowMonad (->)) @Int @Int x - , QC.testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ + , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ \x -> propertyPureLeft @(ArrowMonad (->)) @Int @Int x ] -------------------------------------------------------------------------------- @@ -182,35 +248,35 @@ maybe :: TestTree maybe = testGroup "Maybe" [maybeLaws, maybeTheorems, maybeProperties] maybeLaws = testGroup "Laws" - [ QC.testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ + [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ \x -> lawIdentity @Maybe @Int x - , QC.testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ + , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ \x -> lawDistributivity @Maybe @Int @Int x - , QC.testProperty "Associativity: take a look at tests/Laws.hs" $ + , testProperty "Associativity: take a look at tests/Laws.hs" $ \x -> lawAssociativity @Maybe @Int @Int @Int x - , QC.testProperty "select == selectM" $ + , testProperty "select == selectM" $ \x -> lawMonad @Maybe @Int @Int x ] maybeTheorems = testGroup "Theorems" - [ QC.testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $ + [ 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 - , QC.testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $ + , 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 - , QC.testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ + , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ \x -> theorem3 @Maybe @Int @Int @Int x - , QC.testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ + , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ \x -> theorem4 @Maybe @Int @Int x - , QC.testProperty "(f <*> g) == (f `apS` g)" $ + , testProperty "(f <*> g) == (f `apS` g)" $ \x -> theorem5 @Maybe @Int @Int x - , QC.testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ + , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ \x -> theorem6 @Maybe @Int @Int @Int x ] maybeProperties = testGroup "Properties" - [ QC.testProperty "pure-right: pure (Right x) <*? y = pure x" $ + [ testProperty "pure-right: pure (Right x) <*? y = pure x" $ \x -> propertyPureRight @Maybe @Int @Int x - , QC.testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ + , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ \x -> propertyPureLeft @Maybe @Int @Int x ] -------------------------------------------------------------------------------- @@ -221,34 +287,34 @@ identity = testGroup "Identity" [identityLaws, identityTheorems, identityProperties] identityLaws = testGroup "Laws" - [ QC.testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ + [ testProperty "Identity: (x <*? pure id) == (either id id <$> x)" $ \x -> lawIdentity @Identity @Int x - , QC.testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ + , testProperty "Distributivity: (pure x <*? (y *> z)) == ((pure x <*? y) *> (pure x <*? z))" $ \x -> lawDistributivity @Identity @Int @Int x - , QC.testProperty "Associativity: take a look at tests/Laws.hs" $ + , testProperty "Associativity: take a look at tests/Laws.hs" $ \x -> lawAssociativity @Identity @Int @Int @Int x - , QC.testProperty "select == selectM" $ + , testProperty "select == selectM" $ \x -> lawMonad @Identity @Int @Int x ] identityTheorems = testGroup "Theorems" - [ QC.testProperty "Apply a pure function to the result: (f <$> select x y) == (select (second f <$> x) ((f .) <$> y))" $ + [ 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 - , QC.testProperty "Apply a pure function to the Left case of the first argument: (select (first f <$> x) y) == (select x ((. f) <$> y))" $ + , 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 - , QC.testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ + , testProperty "Apply a pure function to the second argument: (select x (f <$> y)) == (select (first (flip f) <$> x) (flip ($) <$> y))" $ \x -> theorem3 @Identity @Int @Int @Int x - , QC.testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ + , testProperty "Generalised identity: (x <*? pure y) == (either y id <$> x)" $ \x -> theorem4 @Identity @Int @Int x - , QC.testProperty "(f <*> g) == (f `apS` g)" $ + , testProperty "(f <*> g) == (f `apS` g)" $ \x -> theorem5 @Identity @Int @Int x - , QC.testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ + , testProperty "Interchange: (x *> (y <*? z)) == ((x *> y) <*? z)" $ \x -> theorem6 @Identity @Int @Int @Int x ] identityProperties = testGroup "Properties" - [ QC.testProperty "pure-right: pure (Right x) <*? y = pure x" $ + [ testProperty "pure-right: pure (Right x) <*? y = pure x" $ \x -> propertyPureRight @Identity @Int @Int x - , QC.testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ + , testProperty "pure-left: pure (Left x) <*? y = ($x) <$> y" $ \x -> propertyPureLeft @Identity @Int @Int x ] \ No newline at end of file diff --git a/src/Control/Selective/Sketch.hs b/test/Sketch.hs similarity index 99% rename from src/Control/Selective/Sketch.hs rename to test/Sketch.hs index 76ac595..3a12c6b 100644 --- a/src/Control/Selective/Sketch.hs +++ b/test/Sketch.hs @@ -1,11 +1,14 @@ {-# LANGUAGE FlexibleInstances, ScopedTypeVariables, TupleSections #-} -module Control.Selective.Sketch where +module Sketch where import Control.Monad -import Control.Selective.Free.Rigid +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