{-# 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 :: forall a (m0 :: * -> *). Either a (m0 a) -> Ideal m0 a
ideal = Either a (m0 a) -> Unite m0 a
forall (f :: * -> *) a. Either a (f a) -> Unite f a
Unite

-- | Deconstructor of @Ideal@, for backward compatibility
runIdeal :: Ideal m0 a -> Either a (m0 a)
runIdeal :: forall (m0 :: * -> *) a. Ideal m0 a -> Either a (m0 a)
runIdeal = Unite m0 a -> Either a (m0 a)
forall (m0 :: * -> *) a. Ideal m0 a -> Either a (m0 a)
runUnite

-- | Alias of 'hoistUnite' for naming consistently
hoistIdeal :: (forall a. m0 a -> n a) -> Ideal m0 b -> Ideal n b
hoistIdeal :: forall (m0 :: * -> *) (n :: * -> *) b.
(forall a. m0 a -> n a) -> Ideal m0 b -> Ideal n b
hoistIdeal = (forall a. m0 a -> n a) -> Unite m0 b -> Unite n b
forall (m0 :: * -> *) (n :: * -> *) b.
(forall a. m0 a -> n a) -> Ideal m0 b -> Ideal n b
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 :: forall (m0 :: * -> *) a. MonadIdeal m0 => m0 (Ideal m0 a) -> m0 a
idealize = (m0 (Ideal m0 a) -> (Ideal m0 a -> Ideal m0 a) -> m0 a
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` Ideal m0 a -> Ideal m0 a
forall a. a -> a
id)

-- | 'MonadIdeal' implies 'Bind'
bindDefault :: MonadIdeal m0 => m0 a -> (a -> m0 b) -> m0 b
bindDefault :: forall (m0 :: * -> *) a b.
MonadIdeal m0 =>
m0 a -> (a -> m0 b) -> m0 b
bindDefault m0 a
ma a -> m0 b
k = m0 a
ma m0 a -> (a -> Ideal m0 b) -> 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 b (m0 b) -> Ideal m0 b
forall a (m0 :: * -> *). Either a (m0 a) -> Ideal m0 a
ideal (Either b (m0 b) -> Ideal m0 b)
-> (a -> Either b (m0 b)) -> a -> Ideal m0 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m0 b -> Either b (m0 b)
forall a b. b -> Either a b
Right (m0 b -> Either b (m0 b)) -> (a -> m0 b) -> a -> Either b (m0 b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m0 b
k

-- | 'MonadIdeal' implies 'Isolated'
impureBindDefault :: MonadIdeal m0 => m0 a -> (a -> Unite m0 b) -> Unite m0 b
impureBindDefault :: forall (m0 :: * -> *) a b.
MonadIdeal m0 =>
m0 a -> (a -> Unite m0 b) -> Unite m0 b
impureBindDefault m0 a
ma a -> Unite m0 b
k = Either b (m0 b) -> Unite m0 b
forall a (m0 :: * -> *). Either a (m0 a) -> Ideal m0 a
ideal (Either b (m0 b) -> Unite m0 b)
-> (m0 b -> Either b (m0 b)) -> m0 b -> Unite m0 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m0 b -> Either b (m0 b)
forall a b. b -> Either a b
Right (m0 b -> Unite m0 b) -> m0 b -> Unite m0 b
forall a b. (a -> b) -> a -> b
$ m0 a
ma m0 a -> (a -> Unite m0 b) -> 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` a -> Unite m0 b
k

-- | @Ideal ((,) s) ~ (,) (Maybe s)@
instance (Semigroup s) => MonadIdeal ((,) s) where
  idealBind :: forall a b. (s, a) -> (a -> Ideal ((,) s) b) -> (s, b)
idealBind (s
s1, a
a) a -> Ideal ((,) s) b
k = case Ideal ((,) s) b -> Either b (s, b)
forall (m0 :: * -> *) a. Ideal m0 a -> Either a (m0 a)
runIdeal (a -> Ideal ((,) s) b
k a
a) of
    Left b
b -> (s
s1, b
b)
    Right (s
s2, b
b) -> (s
s1 s -> s -> s
forall a. Semigroup a => a -> a -> a
<> s
s2, b
b)

-- | Any @Monad m@ can be an ideal of @Ideal m@
instance (Monad m) => MonadIdeal (WrappedMonad m) where
  idealBind :: forall a b.
WrappedMonad m a
-> (a -> Ideal (WrappedMonad m) b) -> WrappedMonad m b
idealBind (WrapMonad m a
ma) a -> Ideal (WrappedMonad m) b
k = m b -> WrappedMonad m b
forall (m :: * -> *) a. m a -> WrappedMonad m a
WrapMonad (m b -> WrappedMonad m b) -> m b -> WrappedMonad m b
forall a b. (a -> b) -> a -> b
$ m a
ma m a -> (a -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (b -> m b)
-> (WrappedMonad m b -> m b) -> Either b (WrappedMonad m b) -> m b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure WrappedMonad m b -> m b
forall (m :: * -> *) a. WrappedMonad m a -> m a
unwrapMonad (Either b (WrappedMonad m b) -> m b)
-> (a -> Either b (WrappedMonad m b)) -> a -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ideal (WrappedMonad m) b -> Either b (WrappedMonad m b)
forall (m0 :: * -> *) a. Ideal m0 a -> Either a (m0 a)
runIdeal (Ideal (WrappedMonad m) b -> Either b (WrappedMonad m b))
-> (a -> Ideal (WrappedMonad m) b)
-> a
-> Either b (WrappedMonad m b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Ideal (WrappedMonad m) b
k

destroyIdeal :: (m0 a -> a) -> Ideal m0 a -> a
destroyIdeal :: forall (m0 :: * -> *) a. (m0 a -> a) -> Ideal m0 a -> a
destroyIdeal m0 a -> a
phi = (a -> a
forall a. a -> a
id (a -> a) -> (m0 a -> a) -> Either a (m0 a) -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| m0 a -> a
phi) (Either a (m0 a) -> a)
-> (Ideal m0 a -> Either a (m0 a)) -> Ideal m0 a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ideal m0 a -> Either a (m0 a)
forall (m0 :: * -> *) a. Ideal m0 a -> Either a (m0 a)
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)
    @

-}