{-# LANGUAGE DeriveFunctor, EmptyCase, FlexibleInstances, GADTs, RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses, ScopedTypeVariables, TupleSections #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
module Sketch where

import Control.Arrow hiding (first, second)
import Control.Category (Category)
import Control.Monad
import Control.Selective
import Data.Bifunctor
import Data.Bool
import Data.Function
import Data.Semigroup (Semigroup (..))
import Data.Void

import qualified Control.Arrow    as A
import qualified Control.Category as C

-- This file contains various examples and proof sketches and we keep it here to
-- make sure it still compiles. We ignore HLINT suggestions because they often
-- get in the way of readable "proofs" that use equational reasoning.

{-# ANN module "HLint: ignore" #-}

------------------------------- Various examples -------------------------------

bindBool :: Selective f => f Bool -> (Bool -> f a) -> f a
bindBool x f = ifS x (f False) (f True)

branch3 :: Selective f => f (Either a (Either b c)) -> f (a -> d) -> f (b -> d) -> f (c -> d) -> f d
branch3 x a b c = (fmap (fmap Left)     <$> x)
              <*? (fmap (Right . Right) <$> a)
              <*? (fmap Right           <$> b)
              <*? c

bindOrdering :: Selective f => f Ordering -> (Ordering -> f a) -> f a
bindOrdering x f = branch3 (toEither <$> x) (const <$> f LT) (const <$> f EQ) (const <$> f GT)
  where
    toEither LT = Left ()
    toEither EQ = Right (Left ())
    toEither GT = Right (Right ())

-------------------------------- Proof sketches --------------------------------
-- A convenient primitive which checks that the types of two given values
-- coincide and returns the first value.
(===) :: a -> a -> a
x === y = if True then x else y

infixl 0 ===

-- First, we typecheck the laws

-- F1 (Free): f <$> select x y = select (fmap f <$> x) (fmap f <$> y)
f1 :: Selective f => (b -> c) -> f (Either a b) -> f (a -> b) -> f c
f1 f x y = f <$> select x y === select (fmap f <$> x) (fmap f <$> y)

-- F2 (Free): select (first f <$> x) y = select x ((. f) <$> y)
f2 :: Selective f => (a -> c) -> f (Either a b) -> f (c -> b) -> f b
f2 f x y = select (first f <$> x) y === select x ((. f) <$> y)

-- F3 (Free): select x (f <$> y) = select (first (flip f) <$> x) ((&) <$> y)
f3 :: Selective f => (c -> a -> b) -> f (Either a b) -> f c -> f b
f3 f x y = select x (f <$> y) === select (first (flip f) <$> x) ((&) <$> y)

-- P1 (Generalised identity): select x (pure y) == either y id <$> x
p1 :: Selective f => f (Either a b) -> (a -> b) -> f b
p1 x y = select x (pure y) === either y id <$> x

-- A more basic form of P1, from which P1 itself follows as a free theorem.
-- Intuitively, both 'p1' and 'p1id' make the following Const instance illegal:
--
-- @
-- instance Monoid m => Selective (Const m) where
--    select (Const x) (Const _) = Const (x <> x)
-- @
-- P1id (Identity): select x (pure id) == either id id <$> x
p1id  :: Selective f => f (Either a a) -> f a
p1id x = select x (pure id) === either id id <$> x

-- P2 (does not generally hold): select (pure (Left x)) y = ($x) <$> y
p2 :: Selective f => a -> f (a -> b) -> f b
p2 x y = select (pure (Left  x)) y === y <*> pure x

-- P3 (does not generally hold): select (pure (Right x)) y = pure x
p3 :: Selective f => b -> f (a -> b) -> f b
p3 x y = select (pure (Right x)) y === pure x

-- A1 (Associativity):
--     select x (select y z) = select (select (f <$> x) (g <$> y)) (h <$> z)
--       where f x = Right <$> x
--             g y = \a -> bimap (,a) ($a) y
--             h z = uncurry z
a1 :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b
a1 x y z = select x (select y z) === select (select (f <$> x) (g <$> y)) (h <$> z)
  where
    f x = Right <$> x
    g y = \a -> bimap (,a) ($a) y
    h z = uncurry z

-- Intuitively, 'i1' makes the following Const instance illegal, by insisting
-- that effects on the left hand side must be executed.
--
-- @
-- instance Monoid m => Selective (Const m) where
--    select _ _ = Const mempty
-- @
--
-- If we decompose an effect @x :: f a@ into the effect itself @void x@ and the
-- resulting pure value @a@, i.e. @void x *> pure a@, then it becomes clear that
-- 'i1unit' means that all effects must be executed and the remainig pure value
-- will be used to select whether to execute or skip the right hand side.
-- i1unit (Interchange): (x *> y) <*? z = x *> (y <*? z)
i1unit :: Selective f => f c -> f (Either a b) -> f (a -> b) -> f b
i1unit x y z =
    (x *> y) <*? z
    ===
    x *> (y <*? z)

-- i1: x <*> (y <*? z) = (f <$> x <*> y) <*? (g <$> z)
--     where
--       f = (\ab -> bimap (, ab) ab)
--       g = (\ca (c, ab) -> ab (ca c))
i1 :: Selective f => f (a -> b) -> f (Either c a) -> f (c -> a) -> f b
i1 x y z =
    x <*> (y <*? z)
    ===
    (f <$> x <*> y) <*? (g <$> z)
  where
    f ab = bimap (\c ca -> ab (ca c)) ab
    g ca = ($ca)

-- D1 (distributivity): pure x <*? (y *> z) = (pure x <*? y) *> (pure x <*? z)
d1 :: Selective f => Either a b -> f (a -> b) -> f (a -> b) -> f b
d1 x y z =
    pure x <*? (y *> z)
    ===
    (pure x <*? y) *> (pure x <*? z)

-- TODO: Can we prove the following from D1?
-- ifS (pure x) a1 b1 *> ifS (pure x) a2 b2 = ifS (pure x) (a1 *> a2) (b1 *> b2)

-- Now let's typecheck some theorems

-- This assumes P2, which does not always hold
-- Identity: pure id <*> v = v
t1 :: Selective f => f a -> f a
t1 v =
    -- Express the lefthand side using 'apS'
    apS (pure id) v
    === -- Definition of 'apS'
    select (Left <$> pure id) ((&) <$> v)
    === -- Push 'Left' inside 'pure'
    select (pure (Left id)) ((&) <$> v)
    === -- Apply P2
    ($id) <$> ((&) <$> v)
    === -- Simplify
    id <$> v
    === -- Functor identity: -- Functor identity: fmap id = id
    v

-- Homomorphism: pure f <*> pure x = pure (f x)
t2 :: Selective f => (a -> b) -> a -> f b
t2 f x =
    -- Express the lefthand side using 'apS'
    apS (pure f) (pure x)
    === -- Definition of 'apS'
    select (Left <$> pure f) ((&) <$> pure x)
    === -- Push 'Left' inside 'pure'
    select (pure (Left f)) ((&) <$> pure x)
    === -- Applicative's fmap-pure law
    select (pure (Left f)) (pure ((&) x))
    === -- Apply P1
    either (((&) x)) id <$> pure (Left f)
    === -- Applicative's fmap-pure law
    pure (((&) x) f)
    === -- Simplify
    pure (f x)

-- This assumes P2, which does not always hold
-- Interchange: u <*> pure y = pure ($y) <*> u
t3 :: Selective f => f (a -> b) -> a -> f b
t3 u y =
    -- Express the lefthand side using 'apS'
    apS u (pure y)
    === -- Definition of 'apS'
    select (Left <$> u) ((&) <$> pure y)
    === -- Rewrite to have a pure second argument
    select (Left <$> u) (pure ($y))
    === -- Apply P1
    either ($y) id <$> (Left <$> u)
    === -- Simplify, obtaining (#)
    ($y) <$> u

    === -- Express right-hand side of the theorem using 'apS'
    apS (pure ($y)) u
    === -- Definition of 'apS'
    select (Left <$> pure ($y)) ((&) <$> u)
    === -- Push 'Left' inside 'pure'
    select (pure (Left ($y))) ((&) <$> u)
    === -- Apply P2
    ($($y)) <$> ((&) <$> u)
    === -- Simplify, obtaining (#)
    ($y) <$> u

-- Composition: (.) <$> u <*> v <*> w = u <*> (v <*> w)
t4 :: Selective f => f (b -> c) -> f (a -> b) -> f a -> f c
t4 u v w =
    -- Express the lefthand side using 'apS'
    apS (apS ((.) <$> u) v) w
    === -- Definition of 'apS'
    select (Left <$> select (Left <$> (.) <$> u) ((&) <$> v)) ((&) <$> w)
    === -- Apply F1 to push the leftmost 'Left' inside 'select'
    select (select (second Left <$> Left <$> (.) <$> u) ((Left .) <$> (&) <$> v)) ((&) <$> w)
    === -- Simplify
    select (select (Left <$> (.) <$> u) ((Left .) <$> (&) <$> v)) ((&) <$> w)
    === -- Pull (.) outside 'Left'
    select (select (first (.) <$> Left <$> u) ((Left .) <$> (&) <$> v)) ((&) <$> w)
    === -- Apply F2 to push @(.)@ to the function
    select (select (Left <$> u) ((. (.)) <$> (Left .) <$> (&) <$> v)) ((&) <$> w)
    === -- Simplify, obtaining (#)
    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) ((&) <$> w)

    === -- Express the righthand side using 'apS'
    apS u (apS v w)
    === -- Definition of 'apS'
    select (Left <$> u) ((&) <$> select (Left <$> v) ((&) <$> w))
    === -- Apply F1 to push @(&)@ inside 'select'
    select (Left <$> u) (select (Left <$> v) (((&) .) <$> (&) <$> w))
    === -- Apply A1 to reassociate to the left
    select (select (Left <$> u) ((\y a -> bimap (,a) ($a) y) <$> Left <$> v)) (uncurry . ((&) .) <$> (&) <$> w)
    === -- Simplify
    select (select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) ((\x (f, g) -> g (f x)) <$> w)
    === -- Apply F3 to pull the rightmost pure function inside 'select'
    select (first (flip ((\x (f, g) -> g (f x)))) <$> select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) ((&) <$> w)
    === -- Simplify
    select (first (\(f, g) -> g . f) <$> select (Left <$> u) ((\y a -> Left (y, a)) <$> v)) ((&) <$> w)
    === -- Apply F1 to push the leftmost pure function inside 'select'
    select (select (Left <$> u) (((first (\(f, g) -> g . f)).) <$> (\y a -> Left (y, a)) <$> v)) ((&) <$> w)
    === -- Simplify, obtaining (#)
    select (select (Left <$> u) ((Left .) <$> flip (.) <$> v)) ((&) <$> w)

--------------------------------- End of proofs --------------------------------

-- Various other sketches below

-- Associate to the left
-- f (a + b + c) -> f (a -> (b + c)) -> f (b -> c) -> f c
l :: Selective f => f (Either a (Either b c)) -> f (a -> Either b c) -> f (b -> c) -> f c
l x y z = x <*? y <*? z

-- Associate to the right
-- f (a + b) -> f (c + (a -> b)) -> f (c -> a -> b) -> f b
r :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b
r x y z = x <*? (y <*? z)

-- Normalise: go from right to left association
normalise :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b
normalise x y z = (f <$> x) <*? (g <$> y) <*? (h <$> z)
  where
    f x = Right <$> x
    g y = \a -> bimap (,a) ($a) y
    h z = uncurry z

-- Alternative normalisation which uses Scott encoding of pairs
normalise2 :: Selective f => f (Either a b) -> f (Either c (a -> b)) -> f (c -> a -> b) -> f b
normalise2 x y z = (f <$> x) <*? (g <$> y) <*? (h <$> z)
  where
    f x = Right <$> x
    g y = \a -> bimap (\c f -> f c a) ($a) y
    h z = ($z) -- h = (&)

-- Alternative formulations of selective functors.

-- Factoring out the selection logic into a pure argument
class Applicative f => SelectiveBy f where
    selectBy :: (a -> Either (b -> c) c) -> f a -> f b -> f c

fromSelectBy :: SelectiveBy f => f (Either a b) -> f (a -> b) -> f b
fromSelectBy = selectBy (first ((&)))

toSelectBy :: Selective f => (a -> Either (b -> c) c) -> f a -> f b -> f c
toSelectBy f x y = select (f <$> x) ((&) <$> y)

whenBy :: SelectiveBy f => f Bool -> f () -> f ()
whenBy = selectBy (bool (Right ()) (Left id))

-- A first-order version of selective functors.
class Applicative f => SelectiveF f where
    selectF :: f (Either a b) -> f c -> f (Either a (b, c))

toF :: Selective f => f (Either a b) -> f c -> f (Either a (b, c))
toF x y = branch x (pure Left) ((\c b -> Right (b, c)) <$> y)

fromF :: SelectiveF f => f (Either a b) -> f (a -> b) -> f b
fromF x y = either id (uncurry ((&))) <$> selectF (swapEither <$> x) y

-- A few variants that have a sum type in both arguments. They are not
-- equivalent to 'Selective' of 'SelectiveF' unless we require that effects are
-- executed from left to right.

-- Composition of Applicative and Either monad
class Applicative f => SelectiveA f where
    (|*|) :: f (Either e (a -> b)) -> f (Either e a) -> f (Either e b)

-- Composition of Starry and Either monad
-- See: https://duplode.github.io/posts/applicative-archery.html
class Applicative f => SelectiveS f where
    (|.|) :: f (Either e (b -> c)) -> f (Either e (a -> b)) -> f (Either e (a -> c))

-- Composition of Monoidal and Either monad
-- See: http://blog.ezyang.com/2012/08/applicative-functors/
class Applicative f => SelectiveM f where
    (|**|) :: f (Either e a) -> f (Either e b) -> f (Either e (a, b))

biselect :: Selective f => f (Either a b) -> f (Either a c) -> f (Either a (b, c))
biselect x y = select ((fmap Left . swapEither) <$> x) ((\e a -> fmap (a,) e) <$> y)

(?*?) :: Selective f => f (Either a b) -> f (Either a c) -> f (Either a (b, c))
(?*?) = biselect

a1M :: Selective f => f (Either a b) -> f (Either a c) -> f (Either a d)
                   -> f (Either a (b, (c, d)))
a1M x y z =
    x ?*? (y ?*? z)
    ===
    fmap assoc <$> ((x ?*? y) ?*? z)
  where
    assoc ((a, b), c) = (a, (b, c))

apM :: SelectiveM f => f (a -> b) -> f a -> f b
apM f x = fmap (either absurd (uncurry ($))) (fmap Right f |**| fmap Right x)

fromM :: SelectiveM f => f (Either a b) -> f (a -> b) -> f b
fromM x f = either id (\(a, f) -> f a) <$> (fmap swapEither x |**| fmap Right f)

toM :: Selective f => f (Either e a) -> f (Either e b) -> f (Either e (a, b))
toM = biselect

-- Proof that if select = selectM, and <*> = ap, then <*> = apS.
apSEqualsApply :: (Selective f, Monad f) => f (a -> b) -> f a -> f b
apSEqualsApply fab fa =
    fab <*> fa
    === -- Law: <*> = ap
    ap fab fa
    === -- Free theorem (?)
    selectM (Left <$> fab) ((&) <$> fa)
    === -- Law: selectM = select
    select (Left <$> fab) ((&) <$> fa)
    === -- Definition of apS
    apS fab fa

-- | Selective function composition, where the first effect is always evaluated,
-- but the second one can be skipped if the first value is @Nothing@.
-- Thanks to the laws of 'Selective', this operator is associative, and has
-- identity @pure (Just id)@.
(.?) :: Selective f => f (Maybe (b -> c)) -> f (Maybe (a -> b)) -> f (Maybe (a -> c))
x .? y = select (maybe (Right Nothing) Left <$> x) ((\ab bc -> (bc .) <$> ab) <$> y)

infixl 4 .?

-- This assumes P2, which does not always hold
-- Proof of left identity: pure (Just id) .? x = x
t5 :: Selective f => f (Maybe (a -> b)) -> f (Maybe (a -> b))
t5 x =
    --- Lefthand side
    pure (Just id) .? x
    === -- Express the lefthand side by expanding the definition of '.?'
    select (maybe (Right Nothing) Left <$> pure (Just id))
        ((\ab bc -> (bc .) <$> ab) <$> x)
    === -- Simplify
    select (pure $ Left id) ((\ab bc -> (bc .) <$> ab) <$> x)
    === -- Apply P2
    ($id) <$> ((\ab bc -> (bc .) <$> ab) <$> x)
    === -- Simplify
    (($id) <$> (\ab bc -> (bc .) <$> ab) <$> x)
    === -- Functor identity: fmap id = id
    id <$> x
    ===
    x

-- Proof of right identity: x .? pure (Just id) = x
t6 :: Selective f => f (Maybe (a -> b)) -> f (Maybe (a -> b))
t6 x =
    --- Lefthand side
    x .? pure (Just id)
    === -- Express the lefthand side by expanding the definition of '.?'
    select (maybe (Right Nothing) Left <$> x)
        ((\ab bc -> (bc .) <$> ab) <$> pure (Just id))
    === -- Simplify
    select (maybe (Right Nothing) Left <$> x) (pure Just)
    === -- Apply P1
    either Just id <$> (maybe (Right Nothing) Left <$> x)
    === -- Functor identity: fmap id = id
    id <$> x
    ===
    x

-- Proof of associativity: (x .? y) .? z = x .? (y .? z)
t7 :: Selective f => f (Maybe (c -> d)) -> f (Maybe (b -> c)) -> f (Maybe (a -> b)) -> f (Maybe (a -> d))
t7 x y z =
    -- Lefthand side
    (x .? y) .? z
    === -- Express the lefthand side by expanding the definition of '.?'
    select (maybe (Right Nothing) Left <$> (select (maybe (Right Nothing) Left <$> x)
        ((\ab bc -> (bc .) <$> ab) <$> y)))
        ((\ab bc -> (bc .) <$> ab) <$> z)
    === -- Apply F3 to move the rightmost pure function into the outer 'select'
    select (first (flip $ (\ab bc -> (bc .) <$> ab)) <$> maybe (Right Nothing) Left <$> (select (maybe (Right Nothing) Left <$> x)
        ((\ab bc -> (bc .) <$> ab) <$> y)))
        ((&) <$> z)
    === -- Simplify
    select (maybe (Right Nothing) (\bc -> Left $ fmap $ (bc .)) <$> (select (maybe (Right Nothing) Left <$> x)
        ((\ab bc -> (bc .) <$> ab) <$> y)))
        ((&) <$> z)
    === -- Apply F1 to move the pure function into the inner 'select'
    select (select (second (maybe (Right Nothing) (\bc -> Left $ fmap $ (bc .))) <$> maybe (Right Nothing) Left <$> x)
        (((maybe (Right Nothing) (\bc -> Left $ fmap $ (bc .))).) <$> (\ab bc -> (bc .) <$> ab) <$> y))
        ((&) <$> z)
    === -- Simplify, obtaining (#)
    select (select (maybe (Right (Right Nothing)) Left <$> x)
        ((\mbc cd -> maybe (Right Nothing) (\bc -> Left $ fmap ((cd . bc) .)) mbc) <$> y))
        ((&) <$> z)

    === -- Righthand side
    x .? (y .? z)
    === -- Express the righthand side by expanding the definition of '.?'
    select (maybe (Right Nothing) Left <$> x)
        ((\ab bc -> (bc .) <$> ab) <$> (select (maybe (Right Nothing) Left <$> y)
        ((\ab bc -> (bc .) <$> ab) <$> z)))
    === -- Apply F1 to move the pure function into the inner 'select'
    select (maybe (Right Nothing) Left <$> x)
        (select (second ((\ab bc -> (bc .) <$> ab)) <$> maybe (Right Nothing) Left <$> y)
        ((((\ab bc -> (bc .) <$> ab)).) <$> (\ab bc -> (bc .) <$> ab) <$> z))
    === -- Apply A1 to reassociate to the left
    select (select (fmap Right <$> maybe (Right Nothing) Left <$> x)
        ((\y a -> bimap (,a) ($a) y) <$> second ((\ab bc -> (bc .) <$> ab)) <$> maybe (Right Nothing) Left <$> y))
        (uncurry <$> (((\ab bc -> (bc .) <$> ab)).) <$> (\ab bc -> (bc .) <$> ab) <$> z)
    === -- Simplify
    select (select (maybe (Right (Right Nothing)) Left <$> x)
        ((\m a -> maybe (Right Nothing) (Left . (,a)) m) <$> y))
        ((\ab (bc, cd) -> ((cd . bc) .) <$> ab) <$> z)
    === -- Apply F3 to move the rightmost pure function into the outer 'select'
    select (first (flip $ \ab (bc, cd) -> ((cd . bc) .) <$> ab) <$> select (maybe (Right (Right Nothing)) Left <$> x)
        ((\m a -> maybe (Right Nothing) (Left . (,a)) m) <$> y))
        ((&) <$> z)
    === -- Apply F1 to move the pure function into the inner 'select', obtaining (#)
    select (select (maybe (Right (Right Nothing)) Left <$> x)
        ((\mbc cd -> maybe (Right Nothing) (\bc -> Left $ fmap ((cd . bc) .)) mbc) <$> y))
        ((&) <$> z)

------------------------ McCarthy's Conditional combinator -------------------------
-- See: http://www4.di.uminho.pt/~jno/ps/pdbc.pdf
-- And also: https://themattchan.com/docs/algprog.pdf

-- Guard function used in McCarthy's conditional
-- | It provides information about the outcome of testing @p@ on some input @a@,
-- encoded in terms of the coproduct injections without losing the input
-- @a@ itself.
grdS :: Applicative f => f (a -> Bool) -> f a -> f (Either a a)
grdS f a = selector <$> applyF f (dup <$> a)
  where
    dup x = (x, x)
    applyF fab faa = bimap <$> fab <*> pure id <*> faa
    selector (b, x) = bool (Right x) (Left x) b

-- | McCarthy's conditional, denoted p -> f,g is a well-known functional
-- combinator, which suggests that, to reason about conditionals, one may
-- seek help in the algebra of coproducts.
--
-- This combinator is very similar to the very nature of the 'select'
-- operator and benefits from a series of properties and laws.
condS :: Selective f => f (b -> Bool) -> f (b -> c) -> f (b -> c) -> f b -> f c
condS p f g = (\r -> branch r f g) . grdS p

------------------------ Carter Schonwald's copatterns -------------------------
-- See: https://github.com/cartazio/symmetric-monoidal/blob/15b209953b7d4a47651f615b02dbb0171de8af40/src/Control/Monoidal.hs#L93
-- And also: https://twitter.com/andreymokhov/status/1102648479841701888

data Choose a b c where
    CLeft  :: Choose a b a
    CRight :: Choose a b b

newtype Choice a b = Choice (forall r . Choose a b r -> r)

class SelectiveC f where
    choose :: f (Either a b) -> Choice (f (a -> c)) (f (b -> c)) -> f c

-- Recover selective 'branch' from 'choose'.
branchC :: SelectiveC f => f (Either a b) -> f (a -> c) -> f (b -> c) -> f c
branchC x l r = choose x $ Choice $ \c -> case c of { CLeft -> l; CRight -> r }

-- Recover 'choose' from selective 'branch'.
chooseS :: Selective f => f (Either a b) -> Choice (f (a -> c)) (f (b -> c)) -> f c
chooseS x (Choice c) = branch x (c CLeft) (c CRight)

------------------------------- ApplicativeError -------------------------------
-- See https://twitter.com/LukaJacobowitz/status/1148756733243940864.

class Applicative f => ApplicativeEither f e where
    raise  :: e -> f a
    handle :: f a -> f (e -> a) -> f a -- Note that the handler may fail too

-- If the first computation succeeds with an @a@, this function just returns it.
-- Otherwise, it attempts to handle the error @e@ by running the second
-- computation. If the latter fails too, we return the very first error @e@,
-- otherwise we handle the error with the obtained function @e -> a@ and return
-- the resulting value @a@.
handleS :: Selective f => f (Either e a) -> f (Either e (e -> a)) -> f (Either e a)
handleS x y = select (second Right <$> x) (handlePure <$> y)
  where
    handlePure :: Either e (e -> a) -> e -> Either e a
    handlePure (Left  _) e = Left e
    handlePure (Right f) e = Right (f e)

instance Selective f => ApplicativeEither (ComposeEither f e) e where
    raise                                      = ComposeEither . pure . Left
    handle (ComposeEither x) (ComposeEither y) = ComposeEither (handleS x y)
------------------------------- Free ArrowChoice -------------------------------

-- A free 'ArrowChoice' built on top of base components @f i o@.
newtype FreeArrowChoice f a b = FreeArrowChoice {
    runFreeArrowChoice :: forall arr. ArrowChoice arr =>
        (forall i o. f i o -> arr i o) -> arr a b }

instance Category (FreeArrowChoice f) where
    id = FreeArrowChoice (\_ -> C.id)
    FreeArrowChoice x . FreeArrowChoice y = FreeArrowChoice (\t -> x t C.. y t)

instance Arrow (FreeArrowChoice f) where
    arr x = FreeArrowChoice (\_ -> A.arr x)
    first (FreeArrowChoice x) = FreeArrowChoice (\t -> A.first (x t))

instance ArrowChoice (FreeArrowChoice f) where
    left (FreeArrowChoice x) = FreeArrowChoice (\t -> A.left (x t))

-- A constant arrow, similar to the 'Const' applicative functor.
newtype ConstArrow m a b = ConstArrow { getConstArrow :: m }

instance Monoid m => Category (ConstArrow m) where
    id = ConstArrow mempty
    ConstArrow x . ConstArrow y = ConstArrow (mappend x y)

instance Monoid m => Arrow (ConstArrow m) where
    arr _ = ConstArrow mempty
    first (ConstArrow x) = ConstArrow x

instance Monoid m => ArrowChoice (ConstArrow m) where
    left (ConstArrow x) = ConstArrow x

-- Collect all base arrows in a 'FreeArrowChoice'.
foldArrowChoice :: Monoid m => (forall i o. f i o -> m) -> FreeArrowChoice f a b -> m
foldArrowChoice f arr = getConstArrow $ runFreeArrowChoice arr (ConstArrow . f)

-- Execute a 'FreeArrowChoice' in an arbitrary monad.
runArrowChoice :: Monad m => (forall i o. f i o -> (i -> m o)) -> FreeArrowChoice f a b -> (a -> m b)
runArrowChoice f arr = runKleisli $ runFreeArrowChoice arr (Kleisli . f)

-------------------------------- Simplified Haxl -------------------------------

data BlockedRequests
instance Semigroup BlockedRequests where (<>) x _ = case x of {}

-- A Haxl computation is either completed (Done) or Blocked on pending data requests
data Result a = Done a | Blocked BlockedRequests (Haxl a) deriving Functor
newtype Haxl a = Haxl { runHaxl :: IO (Result a) } deriving Functor

instance Applicative Haxl where
    pure = Haxl . return . Done

    Haxl iof <*> Haxl iox = Haxl $ do
        rf <- iof
        rx <- iox
        return $ case (rf, rx) of
            (Done f      , _           ) -> f    <$> rx
            (_           , Done x      ) -> ($x) <$> rf
            (Blocked bf f, Blocked bx x) -> Blocked (bf <> bx) (f <*> x) -- parallelism

instance Selective Haxl where
    select (Haxl iox) (Haxl iof) = Haxl $ do
        rx <- iox
        rf <- iof
        return $ case (rx, rf) of
            (Done (Right b), _           ) -> Done b -- abandon the second computation
            (Done (Left  a), _           ) -> ($a) <$> rf
            (_             , Done       f) -> either f id <$> rx
            (Blocked bx x  , Blocked bf f) -> Blocked (bx <> bf) (select x f) -- speculative
                                                                              -- execution
instance Monad Haxl where
    return = pure

    Haxl iox >>= f = Haxl $ do
        rx <- iox
        case rx of Done       x -> runHaxl (f x) -- dynamic dependency on runtime value 'x'
                   Blocked bx x -> return (Blocked bx (x >>= f))