proofs.hs

type Item u e a = Either (Either u e) a

-- | 'Eggshell' is an eggshell-thin wrapper around 'Turtle.Shell' which makes it
--   easier to redirect @stdout@ and @stderr@. 'Eggshell' carries lines of
--   @stdout@ and @stderr@ (the white stuff) /implicitly/ alongside the
--   values we actually care about (the yolk), so that we can capture stdout
--   and stderr without them interfering with the comprehensions we actually
--   want to write.  It contains a @Shell (Either (Either Line Line) a)@.
data Eggshell a = Eggshell
    { runEggshell :: Shell (Item Line Line a) -- ^ Crack the Eggshell, and void your warranty.
    }

-- STATUS:  NOT PROVEN   FIXME
instance Functor Eggshell where
    fmap f (Eggshell xs) = Eggshell (fmap (fmap f) xs)

-- STATUS: Follows from proof of Monad
instance Applicative Eggshell where
    pure = Eggshell . pure . Right
    (<*>) = ap

-- STATUS:  PROVEN (?)
--          But not verified...
--          Would you trust it?
--
--
--
--
--          (correct answer: yeah prolly lol)

-- These proofs use the following abbreviations:
--     run = runEggshell
--     Mk  = MkEggshell

-- 1. LEFT IDENTITY:   pure v >>= f = f v
--   - pure v >>= f                                               :: given
--   - Mk $ run (pure v) >>= either (pure . Left) (run . f)       :: defn of (>>=)
--   - Mk $ run (Mk . pure . Right $ v)                           :: defn of pure
--             >>= either (pure . Left) (run . f)
--   - Mk $ (run . Mk . pure . Right $ v)                         :: defn of (.)
--             >>= either (pure . Left) (run . f)
--   - Mk $ (pure . Right $ v) >>= either (pure . Left) (run . f) :: run . Mk = id
--   - Mk $ pure (Right v) >>= either (pure . Left) (run . f)     :: defn of (.)
--   - Mk $ either (pure . Left) (run . f) (Right v)              :: Left Identity for Shell (a known Monad)
--   - Mk $ (run . f) v                                           :: case matching on 'either'
--   - (Mk . run . f) v                                           :: defn of (.)
--   - f v                                                        :: run . Mk = id

-- 2. RIGHT IDENTITY:   v >>= pure = v

--   - v >>= pure                                          :: given
--   - Mk $ run v >>= either (pure . Left) (run . pure)    :: defn of (>>=)
--   - Mk $ run v >>= either (pure . Left)                 :: defn of pure
--                           (run . Mk . pure . Right)
--   - Mk $ run v >>= either (pure . Left) (pure . Right)  :: run . Mk = id
--   - Mk $ run v >>= pure . either Left Right             :: factorize case match
--   - Mk $ run v >>= pure                                 :: either Left Right = id
--   - Mk $ run v                                          :: Right Identity for Shell (a known Monad)
--   - v                                                   :: Mk . run = id

-- 3. ASSOCIATIVITY:   (v >>= f) >>= g = v >>= (\x -> f x >>= g)
--
--   - v >>= (\x -> f x >>= g)                             :: RHS
--   - Mk $ run v >>= either (pure . Left)                 :: defn of (>>=)
--                           (run . \x -> f x >>= g)
--   - Mk $ run v >>= K (run . \x -> f x >>= g)                        :: let K :: forall a b.
--                                                                                 (a -> Shell (Item b))
--                                                                              -> (Item a)
--                                                                              -> Shell (Item b)
--                                                                            K = either (pure . Left)
--   - Mk $ run v >>= K (run . \x -> Mk $ run (f x) >>= K (run . g))   :: another (>>=)
--   - Mk $ run v >>= K (run . \x -> Mk $ run (f x) >>= K (run . g))   :: another (>>=)
--   - Mk $ run v >>= K (run . \x -> Mk $ (run . f) x >>= K (run . g)) :: aw geez man
--   - Mk $ v' >>= K (run . \x -> Mk $ f' x >>= K g')                  :: let f' = run . f  :: A -> Shell (Item B)
--                                                                            g' = run . g  :: B -> Shell (Item C)
--                                                                            v' = run v    :: Shell (Item A)
--   - Mk $ v' >>= K (run . \x -> Mk $ (\x -> f' x >>= K g') x)        :: eta expand
--   - Mk $ v' >>= K (run . \x -> Mk . (\x -> f' x >>= K g') $ x)      :: more (.) tricks
--   - Mk $ v' >>= K (run . Mk . (\x -> f' x >>= K g'))                :: un-eta expand
--   - Mk $ v' >>= K (\x -> f' x >>= K g')                             :: run . Mk

--   - (v >>= f) >>= g                                       :: LHS
--   - (Mk $ run v >>= K (run . f)) >>= g                    :: here we go again
--   - Mk $ run (Mk $ run v >>= K (run . f)) >>= K (run . g) :: ok that's not too bad
--   - Mk $ run (Mk $ v' >>= K f') >>= K g'                  :: v', f' and g' from above
--   - Mk $ (v' >>= K f') >>= K g'                           :: another (run . Mk) cancellation

--
--   Goal is to prove these two equal
--   - LHS:  Mk $ (v' >>= K f') >>= K g'
--   - RHS:  Mk $ v' >>= K (\x -> f' x >>= K g')
--
--   Hence we can factor out the leading Mk.
--   - LHS:  (v' >>= K f') >>= K g'
--   - RHS:  v' >>= K (\x -> f' x >>= K g')
--
--   Let f'' = K f' :: Item A -> Shell (Item B)
--       g'' = K g' :: Item B -> Shell (Item C)
--   - LHS:  (v' >>= f'') >>= g''
--   - RHS:  v' >>= K (\x -> f' x >>= g'')
--
--   Apply the monad Associativity Law on Shells to the LHS
--   - LHS:  v' >>= (\x -> f'' x >>= g'')
--   - RHS:  v' >>= K (\x -> f' x >>= g'')
--
--   Factor
--   - LHS:  (\x -> f'' x >>= g'')
--   - RHS:  K (\x -> f' x >>= g'')
--
--   Functional extensionality (i.e. apply x to both sides)
--   - LHS:  f'' x >>= g''
--   - RHS:  K (\x -> f' x >>= g'') x
--
--   - RHS:  either (pure . Left) (\x -> f' x >>= g'') x
--   - RHS:  case x of Left  x -> pure (Left x)
--                     Right x -> f' x >>= g''
--
--   - LHS:  K f' x >>= g''
--   - LHS:  either (pure . Left) f' x >>= g''
--   - LHS:  (case x of Left  x -> pure (Left x)
--                      Right x -> f' x) >>= g''
--   - LHS:  case x of Left  x -> pure (Left x) >>= g''
--                     Right x -> f' x >>= g''
--
--   New goal:  pure (Left x) >>= g''   ==   pure (Left x)
--
--   - pure (Left x) >>= g''
--   - g'' (Left x)
--   - K g' (Left x)
--   - either (pure . Left) g' (Left x)
--   - (pure . Left) x
--   - pure (Left x)                           QED.

instance Monad Eggshell where
    xs >>= f = Eggshell $
        runEggshell xs >>= either
            (pure . Left)      -- forward stdout/stderr
            (runEggshell . f)  -- normal Shell behavior on values

-- STATUS:  NOT PROVEN   FIXME
instance Alternative Eggshell where
    empty = Eggshell empty
    a <|> b = Eggshell $ (runEggshell a) <|> (runEggshell b)

-- STATUS:  NOT PROVEN   FIXME
instance MonadIO Eggshell where
    liftIO = Eggshell . liftIO . fmap pure

-- STATUS:  NOT PROVEN   FIXME
instance MonadManaged Eggshell where
    using = Eggshell . using . fmap pure

-- STATUS:  NOT PROVEN   FIXME
instance MonadPlus Eggshell where

-- NOTE: Tragedy of tragedies, Eggshell cannot implement MonadZip, thanks to this law:
--
--  INFORMATION PRESERVATION:
--    if:   fmap (const ()) ma = fmap (const ()) mb
--    then: ma = fmap fst (mzip ma mb)
--          mb = fmap snd (mzip ma mb)
--
--  Eggshell fails an even simpler law:  'fmap fst (mzip ma ma) /= ma', as the content
--  of stdout/stderr would get duplicated in the LHS.