packages feed

monad-ideals (empty) → 0.1.0.0

raw patch · 14 files changed

+1313/−0 lines, 14 filesdep +basedep +bifunctor-classes-compatdep +comonad

Dependencies added: base, bifunctor-classes-compat, comonad, monad-ideals, semigroupoids

Files

+ CHANGELOG.md view
@@ -0,0 +1,9 @@+# Revision history for monad-ideals++## 0.1.0.0 -- 2024-04-23++* Created based on [category-extras-0.53.5](https://hackage.haskell.org/package/category-extras-0.53.5)+  with updates++  - Changes needed to work with current ecosystem+  - Implement coproduct of ideal monads (product of coideal comonads)
+ LICENSE view
@@ -0,0 +1,33 @@+Copyright 2008 Edward Kmett+Copyright 2007 Iavor Diatchki+Copyright 2004-2008 Dave Menendez+Copyright 2024 Koji Miyazato++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Koji Miyazato nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,137 @@+# monad-ideals: Ideal Monads and coproduct of Monads++Revives `Control.Monad.Ideal` from old versions of [category-extras](https://hackage.haskell.org/package/category-extras-0.53.25).++## Ideal Monads++Ideal monads[^1] are certain kind of monads. Informally, an ideal monad `M`+is a `Monad` which can be written as a disjoint union of "pure" values and "impure" values,+and its `join` operation on "impure" values never produces "pure" values.++[^1]: N. Ghani and T. Uustalu, [“Coproducts of ideal monads,”](http://www.numdam.org/article/ITA_2004__38_4_321_0.pdf) Theoret. Inform. and Appl., vol. 38, pp. 321–342, 2004.++```haskell+data M a = Pure a | Impure (...)++pure :: a -> M a+pure = Pure++join :: M (M a) -> M a+join (Pure ma) = ma+join (Impure ...) = Impure (...)+  -- Impure values of @M a@ never becomes pure again +```++Formally, an ideal monad `m` is a `Monad` equipped with ++- `Functor m₀`, called the ideal part of `m`+- Natural isomorphism `iso :: ∀a. Either a (m₀ a) -> m a` (and its inverse `iso⁻¹ :: ∀a. m a -> Either a (m₀ a)`)+- Natural transformation `idealize :: ∀a. m₀ (m a) -> m₀ a`++satisfying these two properties.++- `iso . Left === pure :: ∀a. a -> m a`+- `either id (iso . Right . idealize) . iso⁻¹ === join :: m (m a) -> m a`++This package provides `MonadIdeal`, a type class to represent ideal monads in terms of+its ideal part `m₀` (instead of a subclass of `Monad` to represent ideal monad itself.)++```haskell+class (Isolated m0, Bind m0) => MonadIdeal m0 where+  idealBind :: m0 a -> (a -> Ideal m0 b) -> m0 b++type Ideal m0 a++-- | Constructor of @Ideal@+ideal :: Either a (m0 a) -> Ideal m0 a++-- | Deconstructor of @Ideal@+runIdeal :: Ideal m0 a -> Either a (m0 a)+```++Here, `Ideal m0` corresponds to the ideal monad which would have `m0` as its ideal part.++## `Isolated` class++There is a generalization to ideal monads, which are almost ideal monads,+but lack a condition that says "an impure value does not become a pure value by the `join` operation".++A monad `m` in this class has natural isomorphism `Either a (m₀ a) -> m a` with some functor `m₀`, and+`pure` is the part of `m` which is not `m₀`. Formally, the defining data of this class are:++- `Functor m₀`, called the impure part of `m`+- Natural isomorphism `iso :: ∀a. Either a (m₀ a) -> m a` (and its inverse `iso⁻¹ :: ∀a. m a -> Either a (m₀ a)`)+- `iso . Left === pure :: ∀a. a -> m a`++Combined with the monad laws of `m`, `join :: ∀a. m (m a) -> m a` must be equal to the following natural transformation+with some `impureJoin`.++```haskell+join :: ∀a. m (m a) -> m a+join mma = case iso⁻¹ mma of+  Left ma -> ma+  Right m₀ma -> impureJoin m₀ma+  where+    impureJoin :: ∀a. m₀ (m a) -> m a+```++The `Isolated` class is a type class for a functor which can be thought of as an+impure part of some monad.++```haskell+newtype Unite f a = Unite { runUnite :: Either a (f a) }++class Functor m0 => Isolated m0 where+  impureBind :: m0 a -> (a -> Unite m0 b) -> Unite m0 b+```++## Coproduct of monads++Coproduct `m ⊕ n` of two monads[^2] `m, n` is the coproduct (category-theoretic sum) in the category of monad+and [monad morphisms](https://hackage.haskell.org/package/mmorph-1.2.0/docs/Control-Monad-Morph.html). [^3]++In basic terms, `m ⊕ n` is a monad with the following functions and properties.++- Monad morphism `inject1 :: ∀a. m a -> (m ⊕ n) a`+- Monad morphism `inject2 :: ∀a. n a -> (m ⊕ n) a`+- Function `eitherMonad` which takes two monad morphisms and return a monad morphism.++  ```+  eitherMonad :: (∀a. m a -> t a) -> (∀a. n a -> t a) -> (∀a. (m ⊕ n) a -> t a)+  ```++- Given arbitrary monads `m, n, t`,++  - For all monad morphisms `f1` and `f2`,++    - `eitherMonad f1 f2 . inject1 = f1`+    - `eitherMonad f1 f2 . inject2 = f2`++  - For any monad morphism `f :: ∀a. (m ⊕ n) a -> t a`, `f` equals to `eitherMonad f1 f2` for some unique `f1, f2`.+    Or, equvalently, `f = eitherMonad (f . inject1) (f . inject2)`.++Coproduct of two monads does not always exist, but for ideal monads or monads with `Isolated` impure parts,+their coproducts exist. This package provides a type constructor `(:+)` below.++```haskell+-- Control.Monad.Coproduct+data (:+) (m :: Type -> Type) (n :: Type -> Type) (a :: Type)+```++Using this type constructor, coproduct of monad can be constructed in two ways.++- If `m0, n0` are `Isolated` i.e. the impure part of monads `Unite m0, Unite n0` respectively,+  `m0 :+ n0` is also `Isolated` and `Unite (m0 :+ n0)` is the coproduct of monads `Unite m0 ⊕ Unite n0`.++- If `m0, n0` are `MonadIdeal` i.e. the ideal part of ideal monads `Ideal m0, Ideal n0` respectively,+  `m0 :+ n0` is also `MonadIdeal` and `Ideal (m0 :+ n0)` is the coproduct of monads `Ideal m0 ⊕ Ideal n0`.++[^2]: Jiří Adámek, Nathan Bowler, Paul B. Levy and Stefan Milius, ["Coproducts of Monads on Set."](https://arxiv.org/abs/1409.3804) (https://doi.org/10.48550/arXiv.1409.3804)++[^3]: To name the same concept to monad morphism, the term "monad transformation" is used in `transformers` package ([Control.Monad.Trans.Class](https://hackage.haskell.org/package/transformers-0.6.0.3/docs/Control-Monad-Trans-Class.html#t:MonadTrans).)++## Duals++This package also provides the duals of ideal monads and coproducts of them: _Coideal comonads_ and _products_ of them.++--------
+ monad-ideals.cabal view
@@ -0,0 +1,69 @@+cabal-version:      3.0+name:               monad-ideals+version:            0.1.0.0++synopsis:           Ideal Monads and coproduct of them+description:+  Type class to represent ideal monads in terms of the+  "ideal part" of ideal monads. See README for more.++license:            BSD-3-Clause+license-file:       LICENSE+author:             Koji Miyazato+maintainer:         viercc@gmail.com+homepage:           https://github.com/viercc/monad-ideals+copyright: Copyright (C) 2008 Edward A. Kmett, +           Copyright (C) 2004--2008 Dave Menendez, +           Copyright (C) 2007 Iavor Diatchki,+           Copyright (C) 2024 Koji Miyazato++category:           Control+build-type:         Simple++extra-doc-files:    CHANGELOG.md, README.md+tested-with: GHC ==8.10.7, GHC ==9.0.2, GHC ==9.2.8, GHC ==9.4.8, GHC ==9.6.5, GHC ==9.8.2++source-repository head+  type:     git+  location: https://github.com/viercc/monad-ideals.git+  branch:   main++common warnings+    ghc-options: -Wall -Wcompat++library+    import:           warnings++    exposed-modules:+        Control.Functor.Internal.Mutual,+        Control.Monad.Ideal,+        Control.Monad.Isolated,+        Control.Monad.Coproduct,+        Control.Comonad.Coideal,++        Data.List.TwoOrMore,+        Data.List.NotOne,+        Data.Functor.KeepLeft,++    build-depends:+      base >=4.14 && < 4.21,+      bifunctor-classes-compat >= 0.1 && < 1,+      comonad >= 5.0.8 && < 5.1,+      semigroupoids >= 6.0.0 && < 6.1,++    hs-source-dirs:   src+    default-language: Haskell2010++test-suite monad-ideals-test+    import:           warnings+    default-language: Haskell2010+    type:             exitcode-stdio-1.0++    hs-source-dirs:   test+    main-is:        Main.hs+    other-modules:+        CoidealExample+    build-depends:+        base,+        comonad,+        monad-ideals
+ src/Control/Comonad/Coideal.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Control.Comonad.Coideal+-- 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.Comonad.Coideal+  ( -- * Coideal Comonads+    ComonadCoideal (..),+    Coideal(..),+    buildCoideal,++    -- * Mutual recursion for (co)ideal (co)monad (co)products+    Mutual (..),++    -- * Coideal Comonad Product+    (:*)(..),+    project1, project2,+    (&&&&)+  )+where++import Control.Arrow ((&&&))+import Control.Comonad++import Control.Functor.Internal.Mutual++newtype Coideal f a = Coideal { runCoideal :: (a, f a) }+  deriving (Functor, Foldable, Traversable)++class (Functor w) => ComonadCoideal w where+  coidealExtend :: (Coideal w a -> b) -> w a -> w b++coidealize :: (ComonadCoideal w) => w a -> w (Coideal w a)+coidealize = coidealExtend id++instance (ComonadCoideal w) => Comonad (Coideal w) where+  extract = fst . runCoideal+  extend f = fmap f . Coideal . (id &&& coidealize . snd . runCoideal)++buildCoideal :: (a -> w a) -> a -> Coideal w a+buildCoideal phi = Coideal . (id &&& phi)++-- * (Co)ideal (Co)products++newtype (:*) w v a = CoidealProduct { runCoidealProduct :: (Mutual (,) w v a, Mutual (,) v w a) }+  deriving Functor++deriving instance+  (+    Eq (m0 ((,) a (Mutual (,) n0 m0 a))),+    Eq (n0 ((,) a (Mutual (,) m0 n0 a)))+  ) => Eq ((:*) m0 n0 a)+deriving instance+  (+    Show (m0 ((,) a (Mutual (,) n0 m0 a))),+    Show (n0 ((,) a (Mutual (,) m0 n0 a)))+  ) => Show ((:*) m0 n0 a)++project1 :: (Functor w) => (w :* v) a -> w a+project1 = fmap fst . runMutual . fst . runCoidealProduct++project2 :: (Functor v) => (w :* v) a -> v a+project2 = fmap fst . runMutual . snd . runCoidealProduct++instance (ComonadCoideal w, ComonadCoideal v) => ComonadCoideal (w :* v) where+  coidealExtend k (CoidealProduct (wv, vw)) = CoidealProduct (extendMutual1 k wv, extendMutual2 k vw)++extendMutual1 ::+  (ComonadCoideal w, ComonadCoideal v) =>+  (Coideal (w :* v) a -> b) ->+  Mutual (,) w v a ->+  Mutual (,) w v b+extendMutual1 k (Mutual wv) =+  Mutual $ coidealExtend (\(Coideal ((a, vw), w')) -> (k (Coideal (a, CoidealProduct (Mutual w', vw))), extendMutual2 k vw)) wv++extendMutual2 ::+  (ComonadCoideal w, ComonadCoideal v) =>+  (Coideal (v :* w) a -> b) ->+  Mutual (,) w v a ->+  Mutual (,) w v b+extendMutual2 k (Mutual wv) =+  Mutual $ coidealExtend (\(Coideal ((a, vw), w')) -> (k (Coideal (a, CoidealProduct (vw, Mutual w'))), extendMutual1 k vw)) wv++(&&&&) :: (ComonadCoideal s) => (forall a. s a -> w a) -> (forall a. s a -> v a) -> s b -> (w :* v) b+tw &&&& tv = CoidealProduct . (unfoldMutual' tw tv &&& unfoldMutual' tv tw)++unfoldMutual' :: (ComonadCoideal s) => (forall a. s a -> w a) -> (forall a. s a -> v a) -> s b -> Mutual (,) w v b+unfoldMutual' = unfoldMutual (\k sa -> coidealExtend (k . runCoideal) sa)
+ src/Control/Functor/Internal/Mutual.hs view
@@ -0,0 +1,39 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Control.Functor.Internal.Mutual+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+module Control.Functor.Internal.Mutual where++import Data.Bifunctor++newtype Mutual p m n a = Mutual {runMutual :: m (p a (Mutual p n m a))}++deriving instance (Eq (m (p a (Mutual p n m a))), Eq (n (p a (Mutual p m n a)))) => Eq (Mutual p n m a)+deriving instance (Show (m (p a (Mutual p n m a))), Show (n (p a (Mutual p m n a)))) => Show (Mutual p n m a)++instance (Bifunctor p, Functor m, Functor n) => Functor (Mutual p m n) where+  fmap f = Mutual . fmap (bimap f (fmap f)) . runMutual++foldMutual+  :: 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 bind mt nt = (`bind` second (foldMutual bind nt mt)) . mt . runMutual++unfoldMutual+  :: Bifunctor p+  => (forall a b. (p a (s a) -> b) -> s a -> s b)+  -> (forall a. s a -> w a)+  -> (forall a. s a -> v a)+  -> s c -> Mutual p w v c+unfoldMutual ext sw sv = Mutual . sw . ext (second (unfoldMutual ext sv sw))
+ src/Control/Monad/Coproduct.hs view
@@ -0,0 +1,205 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-}+-----------------------------------------------------------------------------+-- |+-- 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(..))++-- * 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 { 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)++inject1 :: (Functor m0) => m0 a -> (m0 :+ n0) a+inject1 = Coproduct . Left . Mutual . fmap Left++inject2 :: (Functor n0) => n0 a -> (m0 :+ n0) a+inject2 = Coproduct . Right . Mutual . fmap Left++instance (Functor m0, Functor n0) => Functor (m0 :+ n0) where+  fmap f = Coproduct . bimap (fmap f) (fmap f) . runCoproduct++instance (MonadIdeal m0, MonadIdeal n0) => Apply (m0 :+ n0) where+  (<.>) = apDefault++instance (MonadIdeal m0, MonadIdeal n0) => Bind (m0 :+ n0) where+  (>>-) = bindDefault++instance (Isolated m0, Isolated n0) => Isolated (m0 :+ n0) where+  impureBind copro k = case runCoproduct copro of+    Left mn -> imbindMutual1 mn k+    Right nm -> imbindMutual2 nm k++instance (MonadIdeal m0, MonadIdeal n0) => MonadIdeal (m0 :+ n0) where+  idealBind copro k = Coproduct $ case runCoproduct copro of+    Left mn -> Left $ bindMutual1 mn k+    Right nm -> Right $ bindMutual2 nm k++bindMutual1 :: (MonadIdeal m0, MonadIdeal n0) => Mutual Either m0 n0 a -> (a -> Ideal (m0 :+ n0) b) -> Mutual Either m0 n0 b+bindMutual1 (Mutual mn) k =+  Mutual $+    mn `idealBind` \next ->+      case next of+        Left a -> case runIdeal (k a) of+          Left b -> pure (Left b)+          Right (Coproduct (Left mn')) -> ideal . Right $ runMutual mn'+          Right (Coproduct (Right nm')) -> pure (Right nm')+        Right nm -> pure . Right $ bindMutual2 nm k++bindMutual2 :: (MonadIdeal m0, MonadIdeal n0) => Mutual Either m0 n0 a -> (a -> Ideal (n0 :+ m0) b) -> Mutual Either m0 n0 b+bindMutual2 (Mutual mn) k =+  Mutual $+    mn `idealBind` \next ->+      case next of+        Left a -> case runIdeal (k a) of+          Left b -> pure (Left b)+          Right (Coproduct (Left nm')) -> pure (Right nm')+          Right (Coproduct (Right mn')) -> ideal . Right $ runMutual mn'+        Right nm -> pure . Right $ bindMutual1 nm k++(||||) :: (MonadIdeal t) => (forall a. m0 a -> t a) -> (forall a. n0 a -> t a) -> (m0 :+ n0) b -> t b+mt |||| nt = either (foldMutual' mt nt) (foldMutual' nt mt) . runCoproduct++foldMutual' :: (MonadIdeal t) => (forall a. m0 a -> t a) -> (forall a. n0 a -> t a) -> Mutual Either m0 n0 b -> t b+foldMutual' = foldMutual (\ta k -> ta `idealBind` ideal . 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 (Mutual mna) k =+  review1 $ impureBind mna $ \na -> case na of+    Left a -> view1 (k a)+    Right na' -> view1 (imbindMutual2 na' k)++imbindMutual2 :: (Isolated m0, Isolated n0)+  => Mutual Either n0 m0 a+  -> (a -> Unite (m0 :+ n0) b)+  -> Unite (m0 :+ n0) b+imbindMutual2 (Mutual nma) k =+  review2 $ impureBind nma $ \ma -> case ma of+    Left a -> view2 (k a)+    Right ma' -> view2 (imbindMutual1 ma' k)++view1 :: Unite (m0 :+ n0) a -> Unite m0 (Either a (Mutual Either n0 m0 a))+view1 (Unite (Left a)) = Unite (Left (Left a))+view1 (Unite (Right copro)) = case runCoproduct copro of+  Left mn -> Unite (Right (runMutual mn))+  Right nm -> Unite (Left (Right nm))++review1 :: Unite m0 (Either a (Mutual Either n0 m0 a)) -> Unite (m0 :+ n0) a +review1 (Unite (Left (Left a))) = Unite (Left a)+review1 (Unite (Left (Right nm))) = Unite (Right (Coproduct (Right nm)))+review1 (Unite (Right mn)) = Unite (Right (Coproduct (Left (Mutual mn))))++view2 :: Unite (m0 :+ n0) a -> Unite n0 (Either a (Mutual Either m0 n0 a))+view2 (Unite (Left a)) = Unite (Left (Left a))+view2 (Unite (Right copro)) = case runCoproduct copro of+  Left mn -> Unite (Left (Right mn))+  Right nm -> Unite (Right (runMutual nm))++review2 :: Unite n0 (Either a (Mutual Either m0 n0 a)) -> Unite (m0 :+ n0) a +review2 (Unite (Left (Left a))) = Unite (Left a)+review2 (Unite (Left (Right mn))) = Unite (Right (Coproduct (Left mn)))+review2 (Unite (Right nm)) = Unite (Right (Coproduct (Right (Mutual 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 mt nt copro = case runCoproduct copro of+  Left fg -> foldMutual'' mt nt fg+  Right gf -> foldMutual'' nt mt gf++foldMutual'' :: (Monad t)+  => (forall a. m0 a -> t a)+  -> (forall a. n0 a -> t a)+  -> Mutual Either m0 n0 b -> t b+foldMutual'' = foldMutual (\ta k -> ta >>= either pure id . k)
+ src/Control/Monad/Ideal.hs view
@@ -0,0 +1,122 @@++{-# LANGUAGE RankNTypes #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Control.Monad.Ideal+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+module Control.Monad.Ideal+  ( -- * Ideal Monads+    MonadIdeal (..), idealize,++    Ideal, ideal, runIdeal, hoistIdeal,++    destroyIdeal,++    bindDefault,+    impureBindDefault,+    +    -- * Relation between @MonadIdeal@, @Bind@, and @Isolated@+    -- +    -- $relation_to_bind_and_isolate+  )+where++import Prelude+import Control.Arrow ((|||))++import Data.Functor.Bind (Bind (..))+import Control.Applicative (WrappedMonad (..))++import Control.Monad.Isolated++-- | Ideal monad is a special case of @Unite m0@+type Ideal = Unite++-- | Constructor of @Ideal@, for backward compatibility+ideal :: Either a (m0 a) -> Ideal m0 a+ideal = Unite++-- | Deconstructor of @Ideal@, for backward compatibility+runIdeal :: Ideal m0 a -> Either a (m0 a)+runIdeal = runUnite++-- | Alias of 'hoistUnite' for naming consistently+hoistIdeal :: (forall a. m0 a -> n a) -> Ideal m0 b -> Ideal n b+hoistIdeal = hoistUnite++-- | @m0@ is the "ideal part" of an ideal monad.+--+-- ==== Laws+--+-- Methods inherited from superclasses must be equivalent to the+-- canocical ones.+--+-- - @'(>>-)' === 'bindDefault'@+-- - @'impureBind' === 'impureBindDefault'@+class (Bind m0, Isolated m0) => MonadIdeal m0 where+  idealBind :: m0 a -> (a -> Ideal m0 b) -> m0 b++infixl 1 `idealBind`++idealize :: (MonadIdeal m0) => m0 (Ideal m0 a) -> m0 a+idealize = (`idealBind` id)++-- | 'MonadIdeal' implies 'Bind'+bindDefault :: MonadIdeal m0 => m0 a -> (a -> m0 b) -> m0 b+bindDefault ma k = ma `idealBind` ideal . Right . k++-- | 'MonadIdeal' implies 'Isolated'+impureBindDefault :: MonadIdeal m0 => m0 a -> (a -> Unite m0 b) -> Unite m0 b+impureBindDefault ma k = ideal . Right $ ma `idealBind` k++-- | @Ideal ((,) s) ~ (,) (Maybe s)@+instance (Semigroup s) => MonadIdeal ((,) s) where+  idealBind (s1, a) k = case runIdeal (k a) of+    Left b -> (s1, b)+    Right (s2, b) -> (s1 <> s2, b)++-- | Any @Monad m@ can be an ideal of @Ideal m@+instance (Monad m) => MonadIdeal (WrappedMonad m) where+  idealBind (WrapMonad ma) k = WrapMonad $ ma >>= either pure unwrapMonad . runIdeal . k++destroyIdeal :: (m0 a -> a) -> Ideal m0 a -> a+destroyIdeal phi = (id ||| phi) . runIdeal++{- $relation_to_bind_and_isolate++@MonadIdeal@ is a requirement stronger than both of 'Bind' and 'Isolated'.+In fact, these subset relations hold.++- Every @MonadIdeal@ is @Bind@+- Every @MonadIdeal@ is @Isolated@++These are /strict/ subset relation and neither of three classes can be dropped.++- 'Data.List.NotOne.NotOne' is both @Bind@ and @Isolated@, but not @MonadIdeal@.++- @NullBind c@ is @Bind@ but can't be @Isolated@, because @Unite (NullBind c)@ can't be a @Monad@ in a compatible way.++    @+    newtype NullBind c a = NullBind (Maybe c)+    instance Bind (NullBind c a) where+      _ >>- _ = NullBind Nothing+    @++- @Toggle@ shown below is @Isolated@, but can't be a @Bind@ in a compatible way.++    @+    newtype Toggle a = Toggle a+      deriving Functor++    instance Isolated Toggle where+      impureBind (Toggle a) k = case k a of+        Unite (Left b)           -> Unite (Right (Toggle b))+        Unite (Right (Toggle b)) -> Unite (Left b)+    @++-}
+ src/Control/Monad/Isolated.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE RankNTypes #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Control.Monad.Isolated+-- Copyright   :  (C) 2008 Edward Kmett, (C) 2024 Koji Miyazato+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>+-- Stability   :  experimental+-- Portability :  portable+module Control.Monad.Isolated(+  -- * Impure part isolated from a Monad+  Isolated(..),++  -- * (Re)Unite a Monad from pure and impure parts+  Unite(..),+  hoistUnite,+) where++import Data.Functor.Bind+import Data.Semigroup.Traversable+import Data.Semigroup.Foldable+import Data.Bifunctor (Bifunctor(..))+import Data.Proxy+import Control.Applicative (WrappedMonad(..))++newtype Unite f a = Unite { runUnite :: Either a (f a) }+  deriving (Show, Read, Eq, Ord)++hoistUnite :: (forall a. f a -> g a) -> Unite f b -> Unite g b+hoistUnite fg = Unite . fmap fg . runUnite++instance (Functor g) => Functor (Unite g) where+  fmap f = Unite . bimap f (fmap f) . runUnite++instance (Foldable g) => Foldable (Unite g) where+  foldMap f = either f (foldMap f) . runUnite++instance (Foldable1 g) => Foldable1 (Unite g) where+  foldMap1 f = either f (foldMap1 f) . runUnite++instance (Traversable g) => Traversable (Unite g) where+  traverse f = fmap Unite . either (fmap Left . f) (fmap Right . traverse f) . runUnite++instance (Traversable1 g) => Traversable1 (Unite g) where+  traverse1 f = fmap Unite . either (fmap Left . f) (fmap Right . traverse1 f) . runUnite++-- | @Isolated m0@ is a @Functor@ which can be thought of as an impure part of a @Monad@.+-- +-- ==== Examples+-- +-- - 'Proxy' is @Isolated@ by being same to the 'Nothing' part of the 'Maybe' monad.+--+-- - 'Data.List.NotOne.NotOne' is @Isolated@ by being the list monad ('[]') minus singleton lists,+--   the 'pure' part of the list monad.+--+-- ==== Non-example+--+-- Not every @Monad@ can be isolated its pure and impure parts as the sum of functors.+-- For example, the reader monad cannot be written as a sum of two functors.+--+-- ==== Laws+-- +-- 'impureBind' must be implemented so that the @Monad (Unite m0)@ instance derived from+-- it is lawful.+-- +-- @+-- return a = Unite (Left a)+-- +-- Unite (Left a) >>= k = k a+-- Unite (Right ma) >>= k = ma \`impureBind\` k+-- @+-- +-- Translating the @Monad@ laws on @Unite m0@ in terms of @impureBind@,+-- the following equations are the @Isolated@ laws on its own.+--+-- - (Right identity)+--+--     @+--     ma \`impureBind\` Unite . Left === Unite (Right ma)+--     @+--+-- - (Associativity)+--+--     @+--     (ma \`impureBind\` f) \`impureBind\` g === ma `impureBind` \a -> either g (\`impureBind\` g) (runUnite fa)+--     @+class Functor m0 => Isolated m0 where+  impureBind :: m0 a -> (a -> Unite m0 b) -> Unite m0 b++infixl 1 `impureBind`++instance Isolated m0 => Apply (Unite m0) where+  (<.>) = apDefault++instance Isolated m0 => Applicative (Unite m0) where+  pure = Unite . Left+  (<*>) = (<.>)++instance Isolated m0 => Bind (Unite m0) where+  Unite (Left a) >>- k = k a+  Unite (Right ma) >>- k = ma `impureBind` k++instance Isolated m0 => Monad (Unite m0) where+  (>>=) = (>>-)++instance Isolated Proxy where+  _ `impureBind` _ = Unite (Right Proxy)++instance Semigroup s => Isolated ((,) s) where+  (s, a) `impureBind` k = case runUnite (k a) of+    Left b -> Unite (Right (s, b))+    Right (s', b) -> Unite (Right (s <> s', b))++instance Monad m => Isolated (WrappedMonad m) where+  WrapMonad ma `impureBind` k = Unite . Right . WrapMonad $ ma >>= \a ->+    case runUnite (k a) of+      Left b -> pure b+      Right (WrapMonad mb) -> mb
+ src/Data/Functor/KeepLeft.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE DeriveTraversable #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Functor.KeepLeft+-- Copyright   :  (C) 2024 Koji Miyazato+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>+-- Stability   :  experimental+module Data.Functor.KeepLeft where++import Data.Functor.Const (Const(..))+import Data.Semigroup (First(..))+import Data.Bitraversable (Bitraversable (..))+import Data.Bifoldable (Bifoldable)+import Data.Bifunctor (Bifunctor)++import Data.Functor.Classes ( Eq1, Ord1, Eq2, Ord2 )+import Data.Functor.Bind.Class ( Apply(..), Bind(..) )+import Control.Monad.Isolated ( Isolated(..) )+import Control.Monad.Ideal ( MonadIdeal(..), impureBindDefault )++import Data.Semigroup.Bifoldable (Bifoldable1)+import Data.Semigroup.Bitraversable (Bitraversable1)+import Data.Semigroup.Traversable.Class (Bitraversable1(..))++-- | Another choices of instances for 'Const'. @'KeepLeft' c@ have 'Apply' instance isomorphic to+--   @Const ('First' c)@, which can also (exceptionally) have 'Bind' instance.+--+-- The most used constant functor 'Const' lacks the instance of 'Bind', due to incompatibility+-- between 'Bind' and 'Apply'.+-- +-- @+-- instance (Semigroup c) => 'Apply' ('Const' c)+-- @+-- +-- While any @Semigroup c@ instance yields a lawful @Apply (Const c)@ instance, large number of+-- them do not have @Bind (Const c)@ instance compatible to @Apply@. One of few exceptional @Semigroup@+-- instance is the one defined as below, which is isomorphic to @'First' c@ semigroup.+--+-- @+-- (<>) :: c -> c -> c+-- x <> _ = x+-- @+newtype KeepLeft c a = KeepLeft { getKeepLeft :: c }+  deriving stock (Show, Read, Eq, Ord, Functor, Foldable, Traversable)+  deriving (Semigroup) via (First c)+  deriving (Eq1, Ord1, Apply) via (Const (First c))+  deriving (Eq2, Ord2, Bifunctor, Bifoldable, Bifoldable1) via Const++instance Bitraversable KeepLeft where+  bitraverse f _ (KeepLeft c) = KeepLeft <$> f c++instance Bitraversable1 KeepLeft where+  bitraverse1 f _ (KeepLeft c) = KeepLeft <$> f c++instance Bind (KeepLeft c) where+  KeepLeft c >>- _ = KeepLeft c++instance Isolated (KeepLeft c) where+  impureBind = impureBindDefault++-- | @Ideal (KeepLeft c) a ~ Either c a@+instance MonadIdeal (KeepLeft c) where+  idealBind (KeepLeft c) _ = KeepLeft c
+ src/Data/List/NotOne.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE DeriveTraversable #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.List.NotOne+-- Copyright   :  (C) 2024 Koji Miyazato+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>+-- Stability   :  experimental+module Data.List.NotOne where++import Data.Maybe (mapMaybe)+import Data.Foldable (toList)++import Data.Functor.Bind+import Data.Functor.Plus (Alt(..), Plus(..))+import Control.Monad.Isolated++import Data.List.TwoOrMore++-- | List sans singleton+data NotOne a = Zero | Multiple (TwoOrMore a)+  deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable)++notOne :: [a] -> Either a (NotOne a)+notOne [] = Right Zero+notOne [a] = Left a+notOne (a1 : a2 : as) = Right . Multiple $ TwoOrMore a1 a2 as++getMultiple :: NotOne a -> Maybe (TwoOrMore a)+getMultiple Zero = Nothing+getMultiple (Multiple as) = Just as++instance Semigroup (NotOne a) where+  Zero <> bs = bs+  Multiple (TwoOrMore a1 a2 as) <> bs = Multiple $ TwoOrMore a1 a2 (as ++ toList bs)++instance Monoid (NotOne a) where+  mempty = Zero++instance Apply NotOne where+  Zero <.> _ = Zero+  Multiple _ <.> Zero = Zero+  Multiple as <.> Multiple bs = Multiple (as <.> bs)++instance Alt NotOne where+  (<!>) = (<>)++instance Plus NotOne where+  zero = mempty++-- | @(>>-) = flip foldMap@+instance Bind NotOne where+  Zero >>- _ = Zero+  Multiple as >>- k = case mapMaybe (getMultiple . k) (toList as) of+    [] -> Zero+    [bs] -> Multiple bs+    bs1 : bs2 : bss -> Multiple $ join (TwoOrMore bs1 bs2 bss)++instance Isolated NotOne where+  impureBind as k = Unite . notOne $ toList as >>= toList . k
+ src/Data/List/TwoOrMore.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE DeriveTraversable #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.List.TwoOrMore+-- Copyright   :  (C) 2024 Koji Miyazato+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Koji Miyazato <viercc@gmail.com>+-- Stability   :  experimental+module Data.List.TwoOrMore(TwoOrMore(..), twoOrMore, toNonEmpty) where++import Data.Foldable (toList)+import Data.List.NonEmpty (NonEmpty((:|)))+import Data.Semigroup.Foldable (Foldable1(..))++import Data.Functor.Bind+import Data.Functor.Alt (Alt(..))+import Control.Monad.Isolated+import Control.Monad.Ideal (MonadIdeal(..), impureBindDefault, Ideal, runIdeal)+++-- | List of two or more elements+data TwoOrMore a = TwoOrMore a a [a]+  deriving (Show, Read, Eq, Ord, Functor, Foldable, Traversable)++instance Foldable1 TwoOrMore where+  foldMap1 f (TwoOrMore a1 a2 as) = f a1 <> foldMap1 f (a2 :| as)+  toNonEmpty (TwoOrMore a1 a2 as) = a1 :| (a2 : as)++twoOrMore :: NonEmpty a -> Either a (TwoOrMore a)+twoOrMore (a1 :| as) = case as of+  [] -> Left a1+  a2 : as' -> Right (TwoOrMore a1 a2 as')++instance Semigroup (TwoOrMore a) where+  TwoOrMore a1 a2 as <> bs = TwoOrMore a1 a2 (as ++ toList bs)++instance Apply TwoOrMore where+  TwoOrMore x1 x2 xs <.> TwoOrMore y1 y2 ys = TwoOrMore (x1 y1) (x1 y2) (fmap x1 ys ++ (x2 : xs <*> y1 : y2 : ys))++instance Alt TwoOrMore where+  (<!>) = (<>)++-- | @(>>-) = flip foldMap1@+instance Bind TwoOrMore where+  TwoOrMore a1 a2 as >>- k = case k a1 of+    TwoOrMore b1 b2 bs -> TwoOrMore b1 b2 $ bs ++ ((a2 : as) >>= toList . k)++instance Isolated TwoOrMore where+  impureBind = impureBindDefault++-- | @Ideal TwoOrMore ~ NonEmpty@+instance MonadIdeal TwoOrMore where+  idealBind as k = bindNonEmpty as (idealToNonEmpty . k)++idealToNonEmpty :: Ideal TwoOrMore a -> NonEmpty a+idealToNonEmpty = either pure toNonEmpty . runIdeal++bindNonEmpty :: TwoOrMore a -> (a -> NonEmpty b) -> TwoOrMore b+bindNonEmpty (TwoOrMore a1 a2 as) k = case (k a1, k a2) of+  (b1 :| [], b2 :| []) -> TwoOrMore b1 b2 $ as >>= toList . k+  (b1 :| [], b2 :| bs) -> TwoOrMore b1 b2 $ bs ++ (as >>= toList . k)+  (b1 :| b2 : bs, bs') -> TwoOrMore b1 b2 $ bs ++ toList bs' ++ (as >>= toList . k)
+ test/CoidealExample.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE RankNTypes #-}+module CoidealExample where++import Control.Comonad+import Control.Comonad.Coideal+import Numeric.Natural (Natural)++-- * The example coideal++-- | Example coideal comonad+data A x = Src x x | Tgt x+  deriving (Show, Eq, Functor)++instance Comonad A where+  extract (Src x _) = x+  extract (Tgt x) = x++  duplicate ax@(Src _ x1) = Src ax (Tgt x1)+  duplicate ax@(Tgt _) = Tgt ax++-- | the only one nontrivial cokleisli arrow+advance :: A x -> x+advance ax = case ax of+  Src _ x' -> x'+  Tgt x -> x++-- Accumulating store+data Accum x = Accum Natural (Natural -> x)+  deriving Functor++instance Comonad Accum where+  extract (Accum _ f) = f 0+  duplicate (Accum n f) = Accum n $ \m1 -> Accum (n + m1) (\m2 -> f (m1 + m2))++data Accum' x = Accum' Natural (Natural -> x)+  deriving Functor++fromAccum' :: Coideal Accum' x -> Accum x+fromAccum' wx' = case runCoideal wx' of+  (x, Accum' n f) -> Accum n (\m -> if m == 0 then x else f (m - 1))++toAccum' :: Accum x -> Coideal Accum' x+toAccum' (Accum n f) = Coideal (f 0, Accum' n (\m -> f (m + 1)))++instance ComonadCoideal Accum' where+  coidealExtend k (Accum' n f) = Accum' n $ \m1 -> k (toAccum' $ Accum (n + 1 + m1) (\m2 -> f (m1 + m2)))++-- | Comonad morphism to A.+nextMultipleOf :: Natural -> Accum x -> A x+nextMultipleOf d (Accum n f) = case n `mod` d of+  0 -> Tgt (f 0)+  r -> Src (f 0) (f (d - r))++-- | ComonadIdeal morphism to A'+nextMultipleOf' :: Natural -> Accum' x -> A' x+nextMultipleOf' d (Accum' n f) = case n `mod` d of+  0 -> Tgt'+  r -> Src' (f (d - r - 1))++-- | The coideal part of A+data A' x = Src' x | Tgt'+  deriving (Show, Eq, Functor)++instance ComonadCoideal A' where+  coidealExtend f (Src' x) = Src' (f $ Coideal (x, Tgt'))+  coidealExtend _ Tgt' = Tgt'++fromA' :: Coideal A' x -> A x+fromA' ax' = case runCoideal ax' of+  (x, Src' x') -> Src x x'+  (x, Tgt') -> Tgt x++toA' :: A x -> Coideal A' x+toA' (Src x x') = Coideal (x, Src' x')+toA' (Tgt x) = Coideal (x, Tgt')
+ test/Main.hs view
@@ -0,0 +1,218 @@+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ExtendedDefaultRules #-}+{-# OPTIONS_GHC -Wno-type-defaults #-}+{-# LANGUAGE TypeOperators #-}+module Main (main) where++import System.IO (stderr, hPutStrLn)+import System.Exit (exitFailure)++import Data.Char (toUpper)+import Data.Foldable (toList)+import Data.Proxy+import Data.Semigroup (Min(..))+import Numeric.Natural (Natural)++import Data.List.NonEmpty (NonEmpty(..))+import Control.Monad.Isolated+import Control.Monad.Ideal+import Data.Functor.KeepLeft+import Data.List.TwoOrMore+import Data.List.NotOne+import Control.Monad.Coproduct++import Control.Comonad.Coideal+import CoidealExample++putErr :: String -> IO ()+putErr = hPutStrLn stderr++(===) :: (Show a, Eq a) => a -> a -> String -> IO ()+(===) x y name = if x == y then pure () else putErr errMsg >> exitFailure+  where+    sx = show x+    sy = show y+    errMsg = "failure: " ++ name ++ "\n\t" ++ sx ++ " =/= " ++ sy++infix 1 ===++item :: String -> (String -> IO ()) -> IO ()+item = flip ($)++main :: IO ()+main = do+  testsIsolated+  testsIdeal+  testsKeepLeft+  testsTwoOrMore+  testsNotOne+  testsCoproduct+  testsCoideal++testsIsolated :: IO ()+testsIsolated = do+  -- Unite+  item "fmapUnite" $ fmap @(Unite []) succ (Unite (Left 1)) === Unite (Left 2)+  item "fmapUnite" $ fmap @(Unite []) succ (Unite (Right [1,1])) === Unite (Right [2,2])+  item "toListUnite" $ toList (Unite (Left 'a')) === ['a']+  item "hoistUnite" $ hoistUnite toList (Unite (Left 'a')) === Unite (Left 'a')+  item "hoistUnite" $ hoistUnite toList (Unite (Right Nothing)) === Unite (Right [])++  item "Isolated Proxy" $+    (Proxy `impureBind` pure) === Unite (Right Proxy)+  item "Isolated ((,) s)" $+    ((Min 1, 2) `impureBind` \x -> Unite (Right (Min x, x + 1)))+      ===+    Unite (Right (Min 1, 3))++testsIdeal :: IO ()+testsIdeal = do+  item "MonadIdeal ((,) s)" $+    ((Min 1, 2) `idealBind` pure) === (Min 1, 2)+  item "MonadIdeal ((,) s)" $+    ((Min 1, 2) `idealBind` \x -> (ideal . Right) (Min 0, x + 1))+      ===+    (Min 0, 3)++testsKeepLeft :: IO ()+testsKeepLeft = do+  item "Semigroup (KeepLeft c)" $ KeepLeft 1 <> KeepLeft 5 === KeepLeft 1+  item "Semigroup (KeepLeft c)" $ KeepLeft 1 <> KeepLeft 6 === KeepLeft 1+  item "Semigroup (KeepLeft c)" $ KeepLeft 2 <> KeepLeft 5 === KeepLeft 2+  item "Semigroup (KeepLeft c)" $ KeepLeft 2 <> KeepLeft 6 === KeepLeft 2+  +  item "MonadIdeal (KeepLeft c)" $+    (KeepLeft 1 `idealBind` pure) === KeepLeft 1+  item "MonadIdeal (KeepLeft c)" $+    (KeepLeft 1 `idealBind` \a -> ideal . Right $ KeepLeft (10 + a)) === KeepLeft 1++testsTwoOrMore :: IO ()+testsTwoOrMore = do+  item "twoOrMore" $ twoOrMore ("a" :| []) === Left "a"+  item "twoOrMore" $ twoOrMore ("a" :| ["b", "c"]) === Right (TwoOrMore "a" "b" ["c"])++  let abc = TwoOrMore 'a' 'b' ['c']++  item "MonadIdeal TwoOrMore" $+    (abc `idealBind` \x -> pure (toUpper x)) === TwoOrMore 'A' 'B' ['C']+  item "MonadIdeal TwoOrMore" $+    (abc `idealBind` \x -> ideal . Right $ TwoOrMore x x [x, x]) === TwoOrMore 'a' 'a' "aabbbbcccc"+  +testsNotOne :: IO ()+testsNotOne = do+  item "notOne" $ notOne "" === Right Zero+  item "notOne" $ notOne "a" === Left 'a'+  item "notOne" $ notOne "abcd" === Right (Multiple $ TwoOrMore 'a' 'b' "cd")++  let abc = Multiple $ TwoOrMore 'a' 'b' ['c']+      empty' = Zero+      quadruple x = Multiple $ TwoOrMore x x [x, x]++  item "Isolated NotOne" $+    (abc `impureBind` \x -> pure (toUpper x)) === Unite (Right (fmap toUpper abc))+  item "Isolated NotOne" $+    (abc `impureBind` \x -> if x == 'a' then pure 'M' else Unite (Right empty')) === pure 'M'+  item "Isolated NotOne" $+    (abc `impureBind` \x -> Unite . Right $ quadruple x)+      ===+    (Unite . Right . Multiple $ TwoOrMore 'a' 'a' "aabbbbcccc")++impure :: f a -> Unite f a+impure = Unite . Right++injectMonad1 :: Functor m0 => Unite m0 a -> Unite (m0 :+ n0) a+injectMonad1 = hoistUnite inject1++injectMonad2 :: Functor n0 => Unite n0 a -> Unite (m0 :+ n0) a+injectMonad2 = hoistUnite inject2++testsCoproduct :: IO ()+testsCoproduct = do+  let abc = Multiple $ TwoOrMore 'a' 'b' ['c']+      double x = Multiple $ TwoOrMore x x [] +      quadruple x = Multiple $ TwoOrMore x x [x, x]+      abc' = TwoOrMore 'a' 'b' ['c']+  item "Coproduct-inject1-inject1" $+    let m1 :: Unite (NotOne :+ NotOne) Char+        m1 = do+          x <- injectMonad1 $ impure abc+          injectMonad1 $ impure (quadruple x)+        m2 = injectMonad1 $ impure abc >>= impure . quadruple+    in m1 === m2+  item "Coproduct-inject2-inject2" $+    let m1 :: Unite (NotOne :+ NotOne) Char+        m1 = do+          x <- injectMonad2 $ impure abc+          injectMonad2 $ impure (quadruple x)+        m2 = injectMonad2 $ impure abc >>= impure . quadruple+    in m1 === m2+  +  item "Coproduct-collapse" $+    let m1 :: Unite (NotOne :+ NotOne) Char+        m1 = do+          x <- injectMonad1 $ impure abc+          y <- injectMonad2 $ impure abc+          injectMonad2 $ if x == y then pure () else impure Zero+          pure y+        m2 = injectMonad1 $ impure abc+    in m1 === m2+  +  item "Coproduct-eitherMonad" $+    let m1 :: [Char]+        m1 = either pure (eitherMonad toList toList) . runUnite $ do+          x <- injectMonad1 $ impure abc+          y <- if x == 'a' then injectMonad2 (impure abc) else injectMonad1 (impure abc)+          if y == 'b' then injectMonad2 (impure (double y)) else pure y+        m2 = "abbcabbcabbc"+    in m1 === m2+  +  let f :: Char -> Ideal (TwoOrMore :+ TwoOrMore) Char+      f 'a' = ideal . Right $ inject1 (TwoOrMore 'A' 'A' [])+      f 'b' = ideal . Right $ inject2 (TwoOrMore 'B' 'B' [])+      f c   = ideal . Left $ c+  +  item "Coproduct-idealBind" $+    let m1 :: (TwoOrMore :+ TwoOrMore) Char+        m1 = inject1 abc' `idealBind` f+        +        m2 :: (TwoOrMore :+ TwoOrMore) Char+        m2 = Coproduct $ Left $ Mutual $+          TwoOrMore+            (Left 'A')+            (Left 'A')+            [+              Right (Mutual $ TwoOrMore (Left 'B') (Left 'B') [])+            , Left 'c'+            ]+    in m1 === m2+  +  item "Coproduct-||||" $+    let m1 = id |||| id $ inject1 abc' `idealBind` f+        m2 = TwoOrMore 'A' 'A' ['B', 'B', 'c']+    in m1 === m2++accumToProd :: Accum' x -> (A' :* A') x+accumToProd = nextMultipleOf' 3 &&&& nextMultipleOf' 5++s1 :: Accum' Natural+(_, s1) = runCoideal $ toAccum' (Accum 1 id)++testsCoideal :: IO ()+testsCoideal = do+  let +      w1, w2 :: (A' :* A') Natural+      w1 = accumToProd s1+      w2 = CoidealProduct (cons 2 path, path)+        where+          cons :: a -> Mutual (,) A' A' a -> Mutual (,) A' A' a+          cons a as = Mutual $ Src' (a, as)+          +          nil :: Mutual (,) A' A' a+          nil = Mutual Tgt'++          infixr 4 `cons`++          path :: Mutual (,) A' A' Natural+          path = 4 `cons` 5 `cons` 9 `cons` 11 `cons` 14 `cons` nil+  item "Coideal-&&&&" $ w1 === w2