{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveTraversable #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Control.Monad.Coproduct
-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Koji Miyazato <viercc@gmail.com>
-- Stability   :  experimental
module Control.Monad.Coproduct(
  -- * Ideal Monad Coproduct
  (:+)(..),
  inject1,
  inject2,
  (||||),
  eitherMonad,

  -- * Mutual recursion for ideal monad coproducts
  Mutual (..),
) where

import Data.Functor.Bind
import Control.Monad.Isolated
import Control.Monad.Ideal
import Control.Functor.Internal.Mutual (Mutual(..), foldMutual)

import Data.Bifunctor (Bifunctor(..))
import Data.Bitraversable (bitraverse)
import Data.Bifoldable (bifoldMap)

-- * Coproduct of Monads

-- | Coproduct of impure parts of two `Monad`s.
-- 
-- === As the coproduct of 'Isolated'
-- 
-- Given @'Isolated' m0@ and @Isolated n0@, the functor @m0 :+ n0@ is @Isolated@ too. In other words,
-- given two @Monad@s @Unite m0@ and @Unite n0@, this type constructs a new @Monad (Unite (m0 :+ n0))@.
--
-- Furthermore, as the name suggests,
-- @Unite (m0 :+ n0)@ is the coproduct of @Unite m0@ and @Unite n0@ as a @Monad@.
--
-- - @'hoistUnite' 'inject1' :: Unite m0 ~> Unite (m0 :+ n0)@ is a monad morphism
-- - @'hoistUnite' 'inject2' :: Unite n0 ~> Unite (m0 :+ n0)@ is a monad morphism
-- - @'eitherMonad' mt nt :: (m0 :+ n0) ~> t@ is an impure monad morphism,
--   given @(mt :: m0 ~> t)@ and @(nt :: n0 ~> t)@ are impure monad morphisms.
-- - Any impure monad morphisms @(m0 :+ n0) ~> t@ can be uniquely rewritten as @(eitherMonad mt nt)@.
--
-- Here, a natural transformation @nat :: f ~> g@ is an /impure monad morphism/ means
-- @f@ is an @Isolated@, @g@ is a @Monad@, and @nat@ becomes a monad morphism when combined with @pure@ as below.
--
-- @
-- either pure nat . runUnite :: Unite f ~> g
-- @
--
-- === As the coproduct of 'MonadIdeal'
-- 
-- Given @'MonadIdeal' m0@ and @MonadIdeal n0@, the functor @m0 :+ n0@ is @MonadIdeal@ too.
-- It is the coproduct of @m0@ and @n0@ as a @MonadIdeal@.
--
-- - @inject1 :: m0 ~> (m0 :+ n0)@ is a @MonadIdeal@ morphism
-- - @inject2 :: n0 ~> (m0 :+ n0)@ is a @MonadIdeal@ morphism
-- - @(mt |||| nt) :: (m0 :+ n0) ~> t0@ is a @MonadIdeal@ morphism, given
--   @mt, nt@ are @MonadIdeal@ morphisms.
-- - Any @MonadIdeal@ morphism @(m0 :+ n0) ~> t0@ can be uniquely rewritten as @(mt |||| nt)@.
--
-- Here, a @MonadIdeal@ morphism is a natural transformation @nat@ between @MonadIdeal@ such that
-- preserves @idealBind@.
-- 
-- @
-- nat (idealBind ma k) = idealBind (nat ma) ('hoistIdeal' nat . k)
-- @
-- 
newtype (:+) m0 n0 a = Coproduct { forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct :: Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a) }

deriving instance
  (
    Eq (m0 (Either a (Mutual Either n0 m0 a))),
    Eq (n0 (Either a (Mutual Either m0 n0 a)))
  ) => Eq ((:+) m0 n0 a)
deriving instance
  (
    Show (m0 (Either a (Mutual Either n0 m0 a))),
    Show (n0 (Either a (Mutual Either m0 n0 a)))
  ) => Show ((:+) m0 n0 a)

instance (Foldable m0, Foldable n0) => Foldable (m0 :+ n0) where
  foldMap :: forall m a. Monoid m => (a -> m) -> (:+) m0 n0 a -> m
foldMap a -> m
f = (Mutual Either m0 n0 a -> m)
-> (Mutual Either n0 m0 a -> m)
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> m
forall m a b. Monoid m => (a -> m) -> (b -> m) -> Either a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ((a -> m) -> Mutual Either m0 n0 a -> m
forall m a. Monoid m => (a -> m) -> Mutual Either m0 n0 a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) ((a -> m) -> Mutual Either n0 m0 a -> m
forall m a. Monoid m => (a -> m) -> Mutual Either n0 m0 a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f) (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a) -> m)
-> ((:+) m0 n0 a
    -> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a))
-> (:+) m0 n0 a
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct

instance (Traversable m0, Traversable n0) => Traversable (m0 :+ n0) where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (:+) m0 n0 a -> f ((:+) m0 n0 b)
traverse a -> f b
f = (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
 -> (:+) m0 n0 b)
-> f (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
-> f ((:+) m0 n0 b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
-> (:+) m0 n0 b
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (f (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
 -> f ((:+) m0 n0 b))
-> ((:+) m0 n0 a
    -> f (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)))
-> (:+) m0 n0 a
-> f ((:+) m0 n0 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Mutual Either m0 n0 a -> f (Mutual Either m0 n0 b))
-> (Mutual Either n0 m0 a -> f (Mutual Either n0 m0 b))
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> f (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse ((a -> f b) -> Mutual Either m0 n0 a -> f (Mutual Either m0 n0 b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Mutual Either m0 n0 a -> f (Mutual Either m0 n0 b)
traverse a -> f b
f) ((a -> f b) -> Mutual Either n0 m0 a -> f (Mutual Either n0 m0 b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Mutual Either n0 m0 a -> f (Mutual Either n0 m0 b)
traverse a -> f b
f) (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
 -> f (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)))
-> ((:+) m0 n0 a
    -> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a))
-> (:+) m0 n0 a
-> f (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct

inject1 :: (Functor m0) => m0 a -> (m0 :+ n0) a
inject1 :: forall (m0 :: * -> *) a (n0 :: * -> *).
Functor m0 =>
m0 a -> (:+) m0 n0 a
inject1 = Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
 -> (:+) m0 n0 a)
-> (m0 a -> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a))
-> m0 a
-> (:+) m0 n0 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutual Either m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall a b. a -> Either a b
Left (Mutual Either m0 n0 a
 -> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a))
-> (m0 a -> Mutual Either m0 n0 a)
-> m0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m0 (Either a (Mutual Either n0 m0 a)) -> Mutual Either m0 n0 a
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual (m0 (Either a (Mutual Either n0 m0 a)) -> Mutual Either m0 n0 a)
-> (m0 a -> m0 (Either a (Mutual Either n0 m0 a)))
-> m0 a
-> Mutual Either m0 n0 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a (Mutual Either n0 m0 a))
-> m0 a -> m0 (Either a (Mutual Either n0 m0 a))
forall a b. (a -> b) -> m0 a -> m0 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a (Mutual Either n0 m0 a)
forall a b. a -> Either a b
Left

inject2 :: (Functor n0) => n0 a -> (m0 :+ n0) a
inject2 :: forall (n0 :: * -> *) a (m0 :: * -> *).
Functor n0 =>
n0 a -> (:+) m0 n0 a
inject2 = Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
 -> (:+) m0 n0 a)
-> (n0 a -> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a))
-> n0 a
-> (:+) m0 n0 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutual Either n0 m0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall a b. b -> Either a b
Right (Mutual Either n0 m0 a
 -> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a))
-> (n0 a -> Mutual Either n0 m0 a)
-> n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n0 (Either a (Mutual Either m0 n0 a)) -> Mutual Either n0 m0 a
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual (n0 (Either a (Mutual Either m0 n0 a)) -> Mutual Either n0 m0 a)
-> (n0 a -> n0 (Either a (Mutual Either m0 n0 a)))
-> n0 a
-> Mutual Either n0 m0 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either a (Mutual Either m0 n0 a))
-> n0 a -> n0 (Either a (Mutual Either m0 n0 a))
forall a b. (a -> b) -> n0 a -> n0 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either a (Mutual Either m0 n0 a)
forall a b. a -> Either a b
Left

instance (Functor m0, Functor n0) => Functor (m0 :+ n0) where
  fmap :: forall a b. (a -> b) -> (:+) m0 n0 a -> (:+) m0 n0 b
fmap a -> b
f = Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
-> (:+) m0 n0 b
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
 -> (:+) m0 n0 b)
-> ((:+) m0 n0 a
    -> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
-> (:+) m0 n0 a
-> (:+) m0 n0 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Mutual Either m0 n0 a -> Mutual Either m0 n0 b)
-> (Mutual Either n0 m0 a -> Mutual Either n0 m0 b)
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((a -> b) -> Mutual Either m0 n0 a -> Mutual Either m0 n0 b
forall a b.
(a -> b) -> Mutual Either m0 n0 a -> Mutual Either m0 n0 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) ((a -> b) -> Mutual Either n0 m0 a -> Mutual Either n0 m0 b
forall a b.
(a -> b) -> Mutual Either n0 m0 a -> Mutual Either n0 m0 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
 -> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
-> ((:+) m0 n0 a
    -> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a))
-> (:+) m0 n0 a
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct

instance (MonadIdeal m0, MonadIdeal n0) => Apply (m0 :+ n0) where
  <.> :: forall a b. (:+) m0 n0 (a -> b) -> (:+) m0 n0 a -> (:+) m0 n0 b
(<.>) = (:+) m0 n0 (a -> b) -> (:+) m0 n0 a -> (:+) m0 n0 b
forall (f :: * -> *) a b. Bind f => f (a -> b) -> f a -> f b
apDefault

instance (MonadIdeal m0, MonadIdeal n0) => Bind (m0 :+ n0) where
  >>- :: forall a b. (:+) m0 n0 a -> (a -> (:+) m0 n0 b) -> (:+) m0 n0 b
(>>-) = (:+) m0 n0 a -> (a -> (:+) m0 n0 b) -> (:+) m0 n0 b
forall (m0 :: * -> *) a b.
MonadIdeal m0 =>
m0 a -> (a -> m0 b) -> m0 b
bindDefault

instance (Isolated m0, Isolated n0) => Isolated (m0 :+ n0) where
  impureBind :: forall a b.
(:+) m0 n0 a -> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
impureBind (:+) m0 n0 a
copro a -> Unite (m0 :+ n0) b
k = case (:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct (:+) m0 n0 a
copro of
    Left Mutual Either m0 n0 a
mn -> Mutual Either m0 n0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(Isolated m0, Isolated n0) =>
Mutual Either m0 n0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
imbindMutual1 Mutual Either m0 n0 a
mn a -> Unite (m0 :+ n0) b
k
    Right Mutual Either n0 m0 a
nm -> Mutual Either n0 m0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(Isolated m0, Isolated n0) =>
Mutual Either n0 m0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
imbindMutual2 Mutual Either n0 m0 a
nm a -> Unite (m0 :+ n0) b
k

instance (MonadIdeal m0, MonadIdeal n0) => MonadIdeal (m0 :+ n0) where
  idealBind :: forall a b.
(:+) m0 n0 a -> (a -> Ideal (m0 :+ n0) b) -> (:+) m0 n0 b
idealBind (:+) m0 n0 a
copro a -> Ideal (m0 :+ n0) b
k = Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
-> (:+) m0 n0 b
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
 -> (:+) m0 n0 b)
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
-> (:+) m0 n0 b
forall a b. (a -> b) -> a -> b
$ case (:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct (:+) m0 n0 a
copro of
    Left Mutual Either m0 n0 a
mn -> Mutual Either m0 n0 b
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall a b. a -> Either a b
Left (Mutual Either m0 n0 b
 -> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
-> Mutual Either m0 n0 b
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall a b. (a -> b) -> a -> b
$ Mutual Either m0 n0 a
-> (a -> Ideal (m0 :+ n0) b) -> Mutual Either m0 n0 b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(MonadIdeal m0, MonadIdeal n0) =>
Mutual Either m0 n0 a
-> (a -> Ideal (m0 :+ n0) b) -> Mutual Either m0 n0 b
bindMutual1 Mutual Either m0 n0 a
mn a -> Ideal (m0 :+ n0) b
k
    Right Mutual Either n0 m0 a
nm -> Mutual Either n0 m0 b
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall a b. b -> Either a b
Right (Mutual Either n0 m0 b
 -> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
-> Mutual Either n0 m0 b
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall a b. (a -> b) -> a -> b
$ Mutual Either n0 m0 a
-> (a -> Ideal (m0 :+ n0) b) -> Mutual Either n0 m0 b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(MonadIdeal m0, MonadIdeal n0) =>
Mutual Either m0 n0 a
-> (a -> Ideal (n0 :+ m0) b) -> Mutual Either m0 n0 b
bindMutual2 Mutual Either n0 m0 a
nm a -> Ideal (m0 :+ n0) b
k

bindMutual1 :: (MonadIdeal m0, MonadIdeal n0) => Mutual Either m0 n0 a -> (a -> Ideal (m0 :+ n0) b) -> Mutual Either m0 n0 b
bindMutual1 :: forall (m0 :: * -> *) (n0 :: * -> *) a b.
(MonadIdeal m0, MonadIdeal n0) =>
Mutual Either m0 n0 a
-> (a -> Ideal (m0 :+ n0) b) -> Mutual Either m0 n0 b
bindMutual1 (Mutual m0 (Either a (Mutual Either n0 m0 a))
mn) a -> Ideal (m0 :+ n0) b
k =
  m0 (Either b (Mutual Either n0 m0 b)) -> Mutual Either m0 n0 b
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual (m0 (Either b (Mutual Either n0 m0 b)) -> Mutual Either m0 n0 b)
-> m0 (Either b (Mutual Either n0 m0 b)) -> Mutual Either m0 n0 b
forall a b. (a -> b) -> a -> b
$
    m0 (Either a (Mutual Either n0 m0 a))
mn m0 (Either a (Mutual Either n0 m0 a))
-> (Either a (Mutual Either n0 m0 a)
    -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> m0 (Either b (Mutual Either n0 m0 b))
forall a b. m0 a -> (a -> Ideal m0 b) -> m0 b
forall (m0 :: * -> *) a b.
MonadIdeal m0 =>
m0 a -> (a -> Ideal m0 b) -> m0 b
`idealBind` \Either a (Mutual Either n0 m0 a)
next ->
      case Either a (Mutual Either n0 m0 a)
next of
        Left a
a -> case Ideal (m0 :+ n0) b -> Either b ((:+) m0 n0 b)
forall (m0 :: * -> *) a. Ideal m0 a -> Either a (m0 a)
runIdeal (a -> Ideal (m0 :+ n0) b
k a
a) of
          Left b
b -> Either b (Mutual Either n0 m0 b)
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a. a -> Unite m0 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> Either b (Mutual Either n0 m0 b)
forall a b. a -> Either a b
Left b
b)
          Right (Coproduct (Left Mutual Either m0 n0 b
mn')) -> Either
  (Either b (Mutual Either n0 m0 b))
  (m0 (Either b (Mutual Either n0 m0 b)))
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a (m0 :: * -> *). Either a (m0 a) -> Ideal m0 a
ideal (Either
   (Either b (Mutual Either n0 m0 b))
   (m0 (Either b (Mutual Either n0 m0 b)))
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> (m0 (Either b (Mutual Either n0 m0 b))
    -> Either
         (Either b (Mutual Either n0 m0 b))
         (m0 (Either b (Mutual Either n0 m0 b))))
-> m0 (Either b (Mutual Either n0 m0 b))
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m0 (Either b (Mutual Either n0 m0 b))
-> Either
     (Either b (Mutual Either n0 m0 b))
     (m0 (Either b (Mutual Either n0 m0 b)))
forall a b. b -> Either a b
Right (m0 (Either b (Mutual Either n0 m0 b))
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> m0 (Either b (Mutual Either n0 m0 b))
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a b. (a -> b) -> a -> b
$ Mutual Either m0 n0 b -> m0 (Either b (Mutual Either n0 m0 b))
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
Mutual p m n a -> m (p a (Mutual p n m a))
runMutual Mutual Either m0 n0 b
mn'
          Right (Coproduct (Right Mutual Either n0 m0 b
nm')) -> Either b (Mutual Either n0 m0 b)
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a. a -> Unite m0 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Mutual Either n0 m0 b -> Either b (Mutual Either n0 m0 b)
forall a b. b -> Either a b
Right Mutual Either n0 m0 b
nm')
        Right Mutual Either n0 m0 a
nm -> Either b (Mutual Either n0 m0 b)
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a. a -> Unite m0 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either b (Mutual Either n0 m0 b)
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> (Mutual Either n0 m0 b -> Either b (Mutual Either n0 m0 b))
-> Mutual Either n0 m0 b
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutual Either n0 m0 b -> Either b (Mutual Either n0 m0 b)
forall a b. b -> Either a b
Right (Mutual Either n0 m0 b
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> Mutual Either n0 m0 b
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a b. (a -> b) -> a -> b
$ Mutual Either n0 m0 a
-> (a -> Ideal (m0 :+ n0) b) -> Mutual Either n0 m0 b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(MonadIdeal m0, MonadIdeal n0) =>
Mutual Either m0 n0 a
-> (a -> Ideal (n0 :+ m0) b) -> Mutual Either m0 n0 b
bindMutual2 Mutual Either n0 m0 a
nm a -> Ideal (m0 :+ n0) b
k

bindMutual2 :: (MonadIdeal m0, MonadIdeal n0) => Mutual Either m0 n0 a -> (a -> Ideal (n0 :+ m0) b) -> Mutual Either m0 n0 b
bindMutual2 :: forall (m0 :: * -> *) (n0 :: * -> *) a b.
(MonadIdeal m0, MonadIdeal n0) =>
Mutual Either m0 n0 a
-> (a -> Ideal (n0 :+ m0) b) -> Mutual Either m0 n0 b
bindMutual2 (Mutual m0 (Either a (Mutual Either n0 m0 a))
mn) a -> Ideal (n0 :+ m0) b
k =
  m0 (Either b (Mutual Either n0 m0 b)) -> Mutual Either m0 n0 b
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual (m0 (Either b (Mutual Either n0 m0 b)) -> Mutual Either m0 n0 b)
-> m0 (Either b (Mutual Either n0 m0 b)) -> Mutual Either m0 n0 b
forall a b. (a -> b) -> a -> b
$
    m0 (Either a (Mutual Either n0 m0 a))
mn m0 (Either a (Mutual Either n0 m0 a))
-> (Either a (Mutual Either n0 m0 a)
    -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> m0 (Either b (Mutual Either n0 m0 b))
forall a b. m0 a -> (a -> Ideal m0 b) -> m0 b
forall (m0 :: * -> *) a b.
MonadIdeal m0 =>
m0 a -> (a -> Ideal m0 b) -> m0 b
`idealBind` \Either a (Mutual Either n0 m0 a)
next ->
      case Either a (Mutual Either n0 m0 a)
next of
        Left a
a -> case Ideal (n0 :+ m0) b -> Either b ((:+) n0 m0 b)
forall (m0 :: * -> *) a. Ideal m0 a -> Either a (m0 a)
runIdeal (a -> Ideal (n0 :+ m0) b
k a
a) of
          Left b
b -> Either b (Mutual Either n0 m0 b)
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a. a -> Unite m0 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> Either b (Mutual Either n0 m0 b)
forall a b. a -> Either a b
Left b
b)
          Right (Coproduct (Left Mutual Either n0 m0 b
nm')) -> Either b (Mutual Either n0 m0 b)
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a. a -> Unite m0 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Mutual Either n0 m0 b -> Either b (Mutual Either n0 m0 b)
forall a b. b -> Either a b
Right Mutual Either n0 m0 b
nm')
          Right (Coproduct (Right Mutual Either m0 n0 b
mn')) -> Either
  (Either b (Mutual Either n0 m0 b))
  (m0 (Either b (Mutual Either n0 m0 b)))
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a (m0 :: * -> *). Either a (m0 a) -> Ideal m0 a
ideal (Either
   (Either b (Mutual Either n0 m0 b))
   (m0 (Either b (Mutual Either n0 m0 b)))
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> (m0 (Either b (Mutual Either n0 m0 b))
    -> Either
         (Either b (Mutual Either n0 m0 b))
         (m0 (Either b (Mutual Either n0 m0 b))))
-> m0 (Either b (Mutual Either n0 m0 b))
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m0 (Either b (Mutual Either n0 m0 b))
-> Either
     (Either b (Mutual Either n0 m0 b))
     (m0 (Either b (Mutual Either n0 m0 b)))
forall a b. b -> Either a b
Right (m0 (Either b (Mutual Either n0 m0 b))
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> m0 (Either b (Mutual Either n0 m0 b))
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a b. (a -> b) -> a -> b
$ Mutual Either m0 n0 b -> m0 (Either b (Mutual Either n0 m0 b))
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
Mutual p m n a -> m (p a (Mutual p n m a))
runMutual Mutual Either m0 n0 b
mn'
        Right Mutual Either n0 m0 a
nm -> Either b (Mutual Either n0 m0 b)
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a. a -> Unite m0 a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either b (Mutual Either n0 m0 b)
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> (Mutual Either n0 m0 b -> Either b (Mutual Either n0 m0 b))
-> Mutual Either n0 m0 b
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mutual Either n0 m0 b -> Either b (Mutual Either n0 m0 b)
forall a b. b -> Either a b
Right (Mutual Either n0 m0 b
 -> Ideal m0 (Either b (Mutual Either n0 m0 b)))
-> Mutual Either n0 m0 b
-> Ideal m0 (Either b (Mutual Either n0 m0 b))
forall a b. (a -> b) -> a -> b
$ Mutual Either n0 m0 a
-> (a -> Ideal (n0 :+ m0) b) -> Mutual Either n0 m0 b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(MonadIdeal m0, MonadIdeal n0) =>
Mutual Either m0 n0 a
-> (a -> Ideal (m0 :+ n0) b) -> Mutual Either m0 n0 b
bindMutual1 Mutual Either n0 m0 a
nm a -> Ideal (n0 :+ m0) b
k

(||||) :: (MonadIdeal t) => (forall a. m0 a -> t a) -> (forall a. n0 a -> t a) -> (m0 :+ n0) b -> t b
forall a. m0 a -> t a
mt |||| :: forall (t :: * -> *) (m0 :: * -> *) (n0 :: * -> *) b.
MonadIdeal t =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> (:+) m0 n0 b -> t b
|||| forall a. n0 a -> t a
nt = (Mutual Either m0 n0 b -> t b)
-> (Mutual Either n0 m0 b -> t b)
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
-> t b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
forall (t :: * -> *) (m0 :: * -> *) (n0 :: * -> *) b.
MonadIdeal t =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
foldMutual' m0 a -> t a
forall a. m0 a -> t a
mt n0 a -> t a
forall a. n0 a -> t a
nt) ((forall a. n0 a -> t a)
-> (forall a. m0 a -> t a) -> Mutual Either n0 m0 b -> t b
forall (t :: * -> *) (m0 :: * -> *) (n0 :: * -> *) b.
MonadIdeal t =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
foldMutual' n0 a -> t a
forall a. n0 a -> t a
nt m0 a -> t a
forall a. m0 a -> t a
mt) (Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b) -> t b)
-> ((:+) m0 n0 b
    -> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b))
-> (:+) m0 n0 b
-> t b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (:+) m0 n0 b
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct

foldMutual' :: (MonadIdeal t) => (forall a. m0 a -> t a) -> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
foldMutual' :: forall (t :: * -> *) (m0 :: * -> *) (n0 :: * -> *) b.
MonadIdeal t =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
foldMutual' = (forall a b. t a -> (a -> Either b (t b)) -> t b)
-> (forall a. m0 a -> t a)
-> (forall a. n0 a -> t a)
-> Mutual Either m0 n0 b
-> t b
forall (p :: * -> * -> *) (t :: * -> *) (m :: * -> *) (n :: * -> *)
       c.
Bifunctor p =>
(forall a b. t a -> (a -> p b (t b)) -> t b)
-> (forall a. m a -> t a)
-> (forall a. n a -> t a)
-> Mutual p m n c
-> t c
foldMutual (\t a
ta a -> Either b (t b)
k -> t a
ta t a -> (a -> Ideal t b) -> t b
forall a b. t a -> (a -> Ideal t b) -> t b
forall (m0 :: * -> *) a b.
MonadIdeal m0 =>
m0 a -> (a -> Ideal m0 b) -> m0 b
`idealBind` Either b (t b) -> Ideal t b
forall a (m0 :: * -> *). Either a (m0 a) -> Ideal m0 a
ideal (Either b (t b) -> Ideal t b)
-> (a -> Either b (t b)) -> a -> Ideal t b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b (t b)
k)



{- |

> MonadCoproduct m0 n0 a
>   ~ a + Mutual f g a + Mutual g f a
>   ~ a + f (a + Mutual g f a) + Mutual g f a
>   ~ (a + Mutual g f a) + f (a + Mutual g f a)
>   ~ m0 (a + Mutual g f a)

-}

imbindMutual1 :: (Isolated m0, Isolated n0)
  => Mutual Either m0 n0 a
  -> (a -> Unite (m0 :+ n0) b)
  -> Unite (m0 :+ n0) b
imbindMutual1 :: forall (m0 :: * -> *) (n0 :: * -> *) a b.
(Isolated m0, Isolated n0) =>
Mutual Either m0 n0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
imbindMutual1 (Mutual m0 (Either a (Mutual Either n0 m0 a))
mna) a -> Unite (m0 :+ n0) b
k =
  Unite m0 (Either b (Mutual Either n0 m0 b)) -> Unite (m0 :+ n0) b
forall (m0 :: * -> *) a (n0 :: * -> *).
Unite m0 (Either a (Mutual Either n0 m0 a)) -> Unite (m0 :+ n0) a
review1 (Unite m0 (Either b (Mutual Either n0 m0 b)) -> Unite (m0 :+ n0) b)
-> Unite m0 (Either b (Mutual Either n0 m0 b))
-> Unite (m0 :+ n0) b
forall a b. (a -> b) -> a -> b
$ m0 (Either a (Mutual Either n0 m0 a))
-> (Either a (Mutual Either n0 m0 a)
    -> Unite m0 (Either b (Mutual Either n0 m0 b)))
-> Unite m0 (Either b (Mutual Either n0 m0 b))
forall a b. m0 a -> (a -> Unite m0 b) -> Unite m0 b
forall (m0 :: * -> *) a b.
Isolated m0 =>
m0 a -> (a -> Unite m0 b) -> Unite m0 b
impureBind m0 (Either a (Mutual Either n0 m0 a))
mna ((Either a (Mutual Either n0 m0 a)
  -> Unite m0 (Either b (Mutual Either n0 m0 b)))
 -> Unite m0 (Either b (Mutual Either n0 m0 b)))
-> (Either a (Mutual Either n0 m0 a)
    -> Unite m0 (Either b (Mutual Either n0 m0 b)))
-> Unite m0 (Either b (Mutual Either n0 m0 b))
forall a b. (a -> b) -> a -> b
$ \Either a (Mutual Either n0 m0 a)
na -> case Either a (Mutual Either n0 m0 a)
na of
    Left a
a -> Unite (m0 :+ n0) b -> Unite m0 (Either b (Mutual Either n0 m0 b))
forall (m0 :: * -> *) (n0 :: * -> *) a.
Unite (m0 :+ n0) a -> Unite m0 (Either a (Mutual Either n0 m0 a))
view1 (a -> Unite (m0 :+ n0) b
k a
a)
    Right Mutual Either n0 m0 a
na' -> Unite (m0 :+ n0) b -> Unite m0 (Either b (Mutual Either n0 m0 b))
forall (m0 :: * -> *) (n0 :: * -> *) a.
Unite (m0 :+ n0) a -> Unite m0 (Either a (Mutual Either n0 m0 a))
view1 (Mutual Either n0 m0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(Isolated m0, Isolated n0) =>
Mutual Either n0 m0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
imbindMutual2 Mutual Either n0 m0 a
na' a -> Unite (m0 :+ n0) b
k)

imbindMutual2 :: (Isolated m0, Isolated n0)
  => Mutual Either n0 m0 a
  -> (a -> Unite (m0 :+ n0) b)
  -> Unite (m0 :+ n0) b
imbindMutual2 :: forall (m0 :: * -> *) (n0 :: * -> *) a b.
(Isolated m0, Isolated n0) =>
Mutual Either n0 m0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
imbindMutual2 (Mutual n0 (Either a (Mutual Either m0 n0 a))
nma) a -> Unite (m0 :+ n0) b
k =
  Unite n0 (Either b (Mutual Either m0 n0 b)) -> Unite (m0 :+ n0) b
forall (n0 :: * -> *) a (m0 :: * -> *).
Unite n0 (Either a (Mutual Either m0 n0 a)) -> Unite (m0 :+ n0) a
review2 (Unite n0 (Either b (Mutual Either m0 n0 b)) -> Unite (m0 :+ n0) b)
-> Unite n0 (Either b (Mutual Either m0 n0 b))
-> Unite (m0 :+ n0) b
forall a b. (a -> b) -> a -> b
$ n0 (Either a (Mutual Either m0 n0 a))
-> (Either a (Mutual Either m0 n0 a)
    -> Unite n0 (Either b (Mutual Either m0 n0 b)))
-> Unite n0 (Either b (Mutual Either m0 n0 b))
forall a b. n0 a -> (a -> Unite n0 b) -> Unite n0 b
forall (m0 :: * -> *) a b.
Isolated m0 =>
m0 a -> (a -> Unite m0 b) -> Unite m0 b
impureBind n0 (Either a (Mutual Either m0 n0 a))
nma ((Either a (Mutual Either m0 n0 a)
  -> Unite n0 (Either b (Mutual Either m0 n0 b)))
 -> Unite n0 (Either b (Mutual Either m0 n0 b)))
-> (Either a (Mutual Either m0 n0 a)
    -> Unite n0 (Either b (Mutual Either m0 n0 b)))
-> Unite n0 (Either b (Mutual Either m0 n0 b))
forall a b. (a -> b) -> a -> b
$ \Either a (Mutual Either m0 n0 a)
ma -> case Either a (Mutual Either m0 n0 a)
ma of
    Left a
a -> Unite (m0 :+ n0) b -> Unite n0 (Either b (Mutual Either m0 n0 b))
forall (m0 :: * -> *) (n0 :: * -> *) a.
Unite (m0 :+ n0) a -> Unite n0 (Either a (Mutual Either m0 n0 a))
view2 (a -> Unite (m0 :+ n0) b
k a
a)
    Right Mutual Either m0 n0 a
ma' -> Unite (m0 :+ n0) b -> Unite n0 (Either b (Mutual Either m0 n0 b))
forall (m0 :: * -> *) (n0 :: * -> *) a.
Unite (m0 :+ n0) a -> Unite n0 (Either a (Mutual Either m0 n0 a))
view2 (Mutual Either m0 n0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
forall (m0 :: * -> *) (n0 :: * -> *) a b.
(Isolated m0, Isolated n0) =>
Mutual Either m0 n0 a
-> (a -> Unite (m0 :+ n0) b) -> Unite (m0 :+ n0) b
imbindMutual1 Mutual Either m0 n0 a
ma' a -> Unite (m0 :+ n0) b
k)

view1 :: Unite (m0 :+ n0) a -> Unite m0 (Either a (Mutual Either n0 m0 a))
view1 :: forall (m0 :: * -> *) (n0 :: * -> *) a.
Unite (m0 :+ n0) a -> Unite m0 (Either a (Mutual Either n0 m0 a))
view1 (Unite (Left a
a)) = Either
  (Either a (Mutual Either n0 m0 a))
  (m0 (Either a (Mutual Either n0 m0 a)))
-> Unite m0 (Either a (Mutual Either n0 m0 a))
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (Either a (Mutual Either n0 m0 a)
-> Either
     (Either a (Mutual Either n0 m0 a))
     (m0 (Either a (Mutual Either n0 m0 a)))
forall a b. a -> Either a b
Left (a -> Either a (Mutual Either n0 m0 a)
forall a b. a -> Either a b
Left a
a))
view1 (Unite (Right (:+) m0 n0 a
copro)) = case (:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct (:+) m0 n0 a
copro of
  Left Mutual Either m0 n0 a
mn -> Either
  (Either a (Mutual Either n0 m0 a))
  (m0 (Either a (Mutual Either n0 m0 a)))
-> Unite m0 (Either a (Mutual Either n0 m0 a))
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (m0 (Either a (Mutual Either n0 m0 a))
-> Either
     (Either a (Mutual Either n0 m0 a))
     (m0 (Either a (Mutual Either n0 m0 a)))
forall a b. b -> Either a b
Right (Mutual Either m0 n0 a -> m0 (Either a (Mutual Either n0 m0 a))
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
Mutual p m n a -> m (p a (Mutual p n m a))
runMutual Mutual Either m0 n0 a
mn))
  Right Mutual Either n0 m0 a
nm -> Either
  (Either a (Mutual Either n0 m0 a))
  (m0 (Either a (Mutual Either n0 m0 a)))
-> Unite m0 (Either a (Mutual Either n0 m0 a))
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (Either a (Mutual Either n0 m0 a)
-> Either
     (Either a (Mutual Either n0 m0 a))
     (m0 (Either a (Mutual Either n0 m0 a)))
forall a b. a -> Either a b
Left (Mutual Either n0 m0 a -> Either a (Mutual Either n0 m0 a)
forall a b. b -> Either a b
Right Mutual Either n0 m0 a
nm))

review1 :: Unite m0 (Either a (Mutual Either n0 m0 a)) -> Unite (m0 :+ n0) a 
review1 :: forall (m0 :: * -> *) a (n0 :: * -> *).
Unite m0 (Either a (Mutual Either n0 m0 a)) -> Unite (m0 :+ n0) a
review1 (Unite (Left (Left a
a))) = Either a ((:+) m0 n0 a) -> Unite (m0 :+ n0) a
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (a -> Either a ((:+) m0 n0 a)
forall a b. a -> Either a b
Left a
a)
review1 (Unite (Left (Right Mutual Either n0 m0 a
nm))) = Either a ((:+) m0 n0 a) -> Unite (m0 :+ n0) a
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite ((:+) m0 n0 a -> Either a ((:+) m0 n0 a)
forall a b. b -> Either a b
Right (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Mutual Either n0 m0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall a b. b -> Either a b
Right Mutual Either n0 m0 a
nm)))
review1 (Unite (Right m0 (Either a (Mutual Either n0 m0 a))
mn)) = Either a ((:+) m0 n0 a) -> Unite (m0 :+ n0) a
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite ((:+) m0 n0 a -> Either a ((:+) m0 n0 a)
forall a b. b -> Either a b
Right (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Mutual Either m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall a b. a -> Either a b
Left (m0 (Either a (Mutual Either n0 m0 a)) -> Mutual Either m0 n0 a
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual m0 (Either a (Mutual Either n0 m0 a))
mn))))

view2 :: Unite (m0 :+ n0) a -> Unite n0 (Either a (Mutual Either m0 n0 a))
view2 :: forall (m0 :: * -> *) (n0 :: * -> *) a.
Unite (m0 :+ n0) a -> Unite n0 (Either a (Mutual Either m0 n0 a))
view2 (Unite (Left a
a)) = Either
  (Either a (Mutual Either m0 n0 a))
  (n0 (Either a (Mutual Either m0 n0 a)))
-> Unite n0 (Either a (Mutual Either m0 n0 a))
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (Either a (Mutual Either m0 n0 a)
-> Either
     (Either a (Mutual Either m0 n0 a))
     (n0 (Either a (Mutual Either m0 n0 a)))
forall a b. a -> Either a b
Left (a -> Either a (Mutual Either m0 n0 a)
forall a b. a -> Either a b
Left a
a))
view2 (Unite (Right (:+) m0 n0 a
copro)) = case (:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct (:+) m0 n0 a
copro of
  Left Mutual Either m0 n0 a
mn -> Either
  (Either a (Mutual Either m0 n0 a))
  (n0 (Either a (Mutual Either m0 n0 a)))
-> Unite n0 (Either a (Mutual Either m0 n0 a))
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (Either a (Mutual Either m0 n0 a)
-> Either
     (Either a (Mutual Either m0 n0 a))
     (n0 (Either a (Mutual Either m0 n0 a)))
forall a b. a -> Either a b
Left (Mutual Either m0 n0 a -> Either a (Mutual Either m0 n0 a)
forall a b. b -> Either a b
Right Mutual Either m0 n0 a
mn))
  Right Mutual Either n0 m0 a
nm -> Either
  (Either a (Mutual Either m0 n0 a))
  (n0 (Either a (Mutual Either m0 n0 a)))
-> Unite n0 (Either a (Mutual Either m0 n0 a))
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (n0 (Either a (Mutual Either m0 n0 a))
-> Either
     (Either a (Mutual Either m0 n0 a))
     (n0 (Either a (Mutual Either m0 n0 a)))
forall a b. b -> Either a b
Right (Mutual Either n0 m0 a -> n0 (Either a (Mutual Either m0 n0 a))
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
Mutual p m n a -> m (p a (Mutual p n m a))
runMutual Mutual Either n0 m0 a
nm))

review2 :: Unite n0 (Either a (Mutual Either m0 n0 a)) -> Unite (m0 :+ n0) a 
review2 :: forall (n0 :: * -> *) a (m0 :: * -> *).
Unite n0 (Either a (Mutual Either m0 n0 a)) -> Unite (m0 :+ n0) a
review2 (Unite (Left (Left a
a))) = Either a ((:+) m0 n0 a) -> Unite (m0 :+ n0) a
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite (a -> Either a ((:+) m0 n0 a)
forall a b. a -> Either a b
Left a
a)
review2 (Unite (Left (Right Mutual Either m0 n0 a
mn))) = Either a ((:+) m0 n0 a) -> Unite (m0 :+ n0) a
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite ((:+) m0 n0 a -> Either a ((:+) m0 n0 a)
forall a b. b -> Either a b
Right (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Mutual Either m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall a b. a -> Either a b
Left Mutual Either m0 n0 a
mn)))
review2 (Unite (Right n0 (Either a (Mutual Either m0 n0 a))
nm)) = Either a ((:+) m0 n0 a) -> Unite (m0 :+ n0) a
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite ((:+) m0 n0 a -> Either a ((:+) m0 n0 a)
forall a b. b -> Either a b
Right (Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
forall (m0 :: * -> *) (n0 :: * -> *) a.
Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
-> (:+) m0 n0 a
Coproduct (Mutual Either n0 m0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
forall a b. b -> Either a b
Right (n0 (Either a (Mutual Either m0 n0 a)) -> Mutual Either n0 m0 a
forall (p :: * -> * -> *) (m :: * -> *) (n :: * -> *) a.
m (p a (Mutual p n m a)) -> Mutual p m n a
Mutual n0 (Either a (Mutual Either m0 n0 a))
nm))))

eitherMonad :: (Isolated m0, Isolated n0, Monad t)
  => (forall a. m0 a -> t a)
  -> (forall a. n0 a -> t a)
  -> (m0 :+ n0) b -> t b
eitherMonad :: forall (m0 :: * -> *) (n0 :: * -> *) (t :: * -> *) b.
(Isolated m0, Isolated n0, Monad t) =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> (:+) m0 n0 b -> t b
eitherMonad forall a. m0 a -> t a
mt forall a. n0 a -> t a
nt (:+) m0 n0 b
copro = case (:+) m0 n0 b
-> Either (Mutual Either m0 n0 b) (Mutual Either n0 m0 b)
forall (m0 :: * -> *) (n0 :: * -> *) a.
(:+) m0 n0 a
-> Either (Mutual Either m0 n0 a) (Mutual Either n0 m0 a)
runCoproduct (:+) m0 n0 b
copro of
  Left Mutual Either m0 n0 b
fg -> (forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
forall (t :: * -> *) (m0 :: * -> *) (n0 :: * -> *) b.
Monad t =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
foldMutual'' m0 a -> t a
forall a. m0 a -> t a
mt n0 a -> t a
forall a. n0 a -> t a
nt Mutual Either m0 n0 b
fg
  Right Mutual Either n0 m0 b
gf -> (forall a. n0 a -> t a)
-> (forall a. m0 a -> t a) -> Mutual Either n0 m0 b -> t b
forall (t :: * -> *) (m0 :: * -> *) (n0 :: * -> *) b.
Monad t =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
foldMutual'' n0 a -> t a
forall a. n0 a -> t a
nt m0 a -> t a
forall a. m0 a -> t a
mt Mutual Either n0 m0 b
gf

foldMutual'' :: (Monad t)
  => (forall a. m0 a -> t a)
  -> (forall a. n0 a -> t a)
  -> Mutual Either m0 n0 b -> t b
foldMutual'' :: forall (t :: * -> *) (m0 :: * -> *) (n0 :: * -> *) b.
Monad t =>
(forall a. m0 a -> t a)
-> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b
foldMutual'' = (forall a b. t a -> (a -> Either b (t b)) -> t b)
-> (forall a. m0 a -> t a)
-> (forall a. n0 a -> t a)
-> Mutual Either m0 n0 b
-> t b
forall (p :: * -> * -> *) (t :: * -> *) (m :: * -> *) (n :: * -> *)
       c.
Bifunctor p =>
(forall a b. t a -> (a -> p b (t b)) -> t b)
-> (forall a. m a -> t a)
-> (forall a. n a -> t a)
-> Mutual p m n c
-> t c
foldMutual (\t a
ta a -> Either b (t b)
k -> t a
ta t a -> (a -> t b) -> t b
forall a b. t a -> (a -> t b) -> t b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (b -> t b) -> (t b -> t b) -> Either b (t b) -> t b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> t b
forall a. a -> t a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t b -> t b
forall a. a -> a
id (Either b (t b) -> t b) -> (a -> Either b (t b)) -> a -> t b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b (t b)
k)