{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE NoNamedWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------

-- |

-- Module      :  Control.Monad.Singletons.Internal

-- Copyright   :  (C) 2018 Ryan Scott

-- License     :  BSD-style (see LICENSE)

-- Maintainer  :  Ryan Scott

-- Stability   :  experimental

-- Portability :  non-portable

--

-- Defines the promoted and singled versions of:

--

-- * 'Functor'

-- * 'Applicative'

-- * 'Alternative'

-- * 'Monad'

-- * 'MonadPlus'

--

-- As well as auxiliary definitions.

--

-- This module exists to break up import cycles.

--

----------------------------------------------------------------------------


module Control.Monad.Singletons.Internal where

import Control.Applicative
import Control.Monad
import Data.List.NonEmpty (NonEmpty(..))
import Data.Singletons.Base.Instances
import Data.Singletons.TH
import GHC.Base.Singletons

$(singletonsOnly [d|
  infixl 4  <$

  {- -| The 'Functor' class is used for types that can be mapped over.
  Instances of 'Functor' should satisfy the following laws:

  > fmap id  ==  id
  > fmap (f . g)  ==  fmap f . fmap g

  The instances of 'Functor' for lists, 'Data.Maybe.Maybe' and 'System.IO.IO'
  satisfy these laws.
  -}

  class  Functor f  where
      fmap        :: (a -> b) -> f a -> f b

      -- -| Replace all locations in the input with the same value.

      -- The default definition is @'fmap' . 'const'@, but this may be

      -- overridden with a more efficient version.

      (<$)        :: a -> f b -> f a
      (<$)        =  fmap . const

  infixl 4 <*>, <*, *>, <**>

  -- -| A functor with application, providing operations to

  --

  -- -* embed pure expressions ('pure'), and

  --

  -- -* sequence computations and combine their results ('<*>' and 'liftA2').

  --

  -- A minimal complete definition must include implementations of 'pure'

  -- and of either '<*>' or 'liftA2'. If it defines both, then they must behave

  -- the same as their default definitions:

  --

  --      @('<*>') = 'liftA2' 'id'@

  --

  --      @'liftA2' f x y = f '<$>' x '<*>' y@

  --

  -- Further, any definition must satisfy the following:

  --

  -- [/identity/]

  --

  --      @'pure' 'id' '<*>' v = v@

  --

  -- [/composition/]

  --

  --      @'pure' (.) '<*>' u '<*>' v '<*>' w = u '<*>' (v '<*>' w)@

  --

  -- [/homomorphism/]

  --

  --      @'pure' f '<*>' 'pure' x = 'pure' (f x)@

  --

  -- [/interchange/]

  --

  --      @u '<*>' 'pure' y = 'pure' ('$' y) '<*>' u@

  --

  --

  -- The other methods have the following default definitions, which may

  -- be overridden with equivalent specialized implementations:

  --

  --   * @u '*>' v = ('id' '<$' u) '<*>' v@

  --

  --   * @u '<*' v = 'liftA2' 'const' u v@

  --

  -- As a consequence of these laws, the 'Functor' instance for @f@ will satisfy

  --

  --   * @'fmap' f x = 'pure' f '<*>' x@

  --

  --

  -- It may be useful to note that supposing

  --

  --      @forall x y. p (q x y) = f x . g y@

  --

  -- it follows from the above that

  --

  --      @'liftA2' p ('liftA2' q u v) = 'liftA2' f u . 'liftA2' g v@

  --

  --

  -- If @f@ is also a 'Monad', it should satisfy

  --

  --   * @'pure' = 'return'@

  --

  --   * @('<*>') = 'ap'@

  --

  --   * @('*>') = ('>>')@

  --

  -- (which implies that 'pure' and '<*>' satisfy the applicative functor laws).


  class Functor f => Applicative f where
      -- {-# MINIMAL pure, ((<*>) | liftA2) #-}

      -- -| Lift a value.

      pure :: a -> f a

      -- -| Sequential application.

      --

      -- A few functors support an implementation of '<*>' that is more

      -- efficient than the default one.

      (<*>) :: f (a -> b) -> f a -> f b
      (<*>) = liftA2 id

      -- -| Lift a binary function to actions.

      --

      -- Some functors support an implementation of 'liftA2' that is more

      -- efficient than the default one. In particular, if 'fmap' is an

      -- expensive operation, it is likely better to use 'liftA2' than to

      -- 'fmap' over the structure and then use '<*>'.

      liftA2 :: (a -> b -> c) -> f a -> f b -> f c
      liftA2 f x = (<*>) (fmap f x)

      -- -| Sequence actions, discarding the value of the first argument.

      (*>) :: f a -> f b -> f b
      a1 *> a2 = (id <$ a1) <*> a2
      -- This is essentially the same as liftA2 (flip const), but if the

      -- Functor instance has an optimized (<$), it may be better to use

      -- that instead. Before liftA2 became a method, this definition

      -- was strictly better, but now it depends on the functor. For a

      -- functor supporting a sharing-enhancing (<$), this definition

      -- may reduce allocation by preventing a1 from ever being fully

      -- realized. In an implementation with a boring (<$) but an optimizing

      -- liftA2, it would likely be better to define (*>) using liftA2.


      -- -| Sequence actions, discarding the value of the second argument.

      (<*) :: f a -> f b -> f a
      (<*) = liftA2 const

  -- -| A variant of '<*>' with the arguments reversed.

  (<**>) :: Applicative f => f a -> f (a -> b) -> f b
  (<**>) = liftA2 (\a f -> f a)
  -- Don't use $ here, see the note at the top of the page


  -- -| Lift a function to actions.

  -- This function may be used as a value for `fmap` in a `Functor` instance.

  liftA :: Applicative f => (a -> b) -> f a -> f b
  liftA f a = pure f <*> a
  -- Caution: since this may be used for `fmap`, we can't use the obvious

  -- definition of liftA = fmap.


  -- -| Lift a ternary function to actions.

  liftA3 :: Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
  liftA3 f a b c = liftA2 f a b <*> c

  infixl 1  >>, >>=
  infixr 1  =<<

  -- -| The 'join' function is the conventional monad join operator. It

  -- is used to remove one level of monadic structure, projecting its

  -- bound argument into the outer level.

  --

  -- ==== __Examples__

  --

  -- A common use of 'join' is to run an 'IO' computation returned from

  -- an 'GHC.Conc.STM' transaction, since 'GHC.Conc.STM' transactions

  -- can't perform 'IO' directly. Recall that

  --

  -- @

  -- 'GHC.Conc.atomically' :: STM a -> IO a

  -- @

  --

  -- is used to run 'GHC.Conc.STM' transactions atomically. So, by

  -- specializing the types of 'GHC.Conc.atomically' and 'join' to

  --

  -- @

  -- 'GHC.Conc.atomically' :: STM (IO b) -> IO (IO b)

  -- 'join'       :: IO (IO b)  -> IO b

  -- @

  --

  -- we can compose them as

  --

  -- @

  -- 'join' . 'GHC.Conc.atomically' :: STM (IO b) -> IO b

  -- @

  --

  -- to run an 'GHC.Conc.STM' transaction and the 'IO' action it

  -- returns.

  join              :: (Monad m) => m (m a) -> m a
  join x            =  x >>= id

  {- -| The 'Monad' class defines the basic operations over a /monad/,
  a concept from a branch of mathematics known as /category theory/.
  From the perspective of a Haskell programmer, however, it is best to
  think of a monad as an /abstract datatype/ of actions.
  Haskell's @do@ expressions provide a convenient syntax for writing
  monadic expressions.

  Instances of 'Monad' should satisfy the following laws:

  * @'return' a '>>=' k  =  k a@
  * @m '>>=' 'return'  =  m@
  * @m '>>=' (\\x -> k x '>>=' h)  =  (m '>>=' k) '>>=' h@

  Furthermore, the 'Monad' and 'Applicative' operations should relate as follows:

  * @'pure' = 'return'@
  * @('<*>') = 'ap'@

  The above laws imply:

  * @'fmap' f xs  =  xs '>>=' 'return' . f@
  * @('>>') = ('*>')@

  and that 'pure' and ('<*>') satisfy the applicative functor laws.

  The instances of 'Monad' for lists, 'Data.Maybe.Maybe' and 'System.IO.IO'
  defined in the "Prelude" satisfy these laws.
  -}
  class Applicative m => Monad m where
      -- -| Sequentially compose two actions, passing any value produced

      -- by the first as an argument to the second.

      (>>=)       :: forall a b. m a -> (a -> m b) -> m b

      -- -| Sequentially compose two actions, discarding any value produced

      -- by the first, like sequencing operators (such as the semicolon)

      -- in imperative languages.

      (>>)        :: forall a b. m a -> m b -> m b
      m >> k = m >>= \_ -> k -- See Note [Recursive bindings for Applicative/Monad]


      -- -| Inject a value into the monadic type.

      return      :: a -> m a
      return      = pure

  {- Note [Recursive bindings for Applicative/Monad]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  The original Applicative/Monad proposal stated that after
  implementation, the designated implementation of (>>) would become

    (>>) :: forall a b. m a -> m b -> m b
    (>>) = (*>)

  by default. You might be inclined to change this to reflect the stated
  proposal, but you really shouldn't! Why? Because people tend to define
  such instances the /other/ way around: in particular, it is perfectly
  legitimate to define an instance of Applicative (*>) in terms of (>>),
  which would lead to an infinite loop for the default implementation of
  Monad! And people do this in the wild.

  This turned into a nasty bug that was tricky to track down, and rather
  than eliminate it everywhere upstream, it's easier to just retain the
  original default.

  -}

  -- -| Same as '>>=', but with the arguments interchanged.

  (=<<)           :: Monad m => (a -> m b) -> m a -> m b
  f =<< x         = x >>= f

  -- -| Conditional execution of 'Applicative' expressions. For example,

  --

  -- > when debug (putStrLn "Debugging")

  --

  -- will output the string @Debugging@ if the Boolean value @debug@

  -- is 'True', and otherwise do nothing.

  when      :: (Applicative f) => Bool -> f () -> f ()
  when p s  = if p then s else pure ()

  -- -| Promote a function to a monad.

  liftM   :: (Monad m) => (a1 -> r) -> m a1 -> m r
  liftM f m1              = do { x1 <- m1; return (f x1) }

  -- -| Promote a function to a monad, scanning the monadic arguments from

  -- left to right.  For example,

  --

  -- > liftM2 (+) [0,1] [0,2] = [0,2,1,3]

  -- > liftM2 (+) (Just 1) Nothing = Nothing

  --

  liftM2  :: (Monad m) => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
  liftM2 f m1 m2          = do { x1 <- m1; x2 <- m2; return (f x1 x2) }
  -- Caution: since this may be used for `liftA2`, we can't use the obvious

  -- definition of liftM2 = liftA2.


  -- -| Promote a function to a monad, scanning the monadic arguments from

  -- left to right (cf. 'liftM2').

  liftM3  :: (Monad m) => (a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
  liftM3 f m1 m2 m3       = do { x1 <- m1; x2 <- m2; x3 <- m3; return (f x1 x2 x3) }

  -- -| Promote a function to a monad, scanning the monadic arguments from

  -- left to right (cf. 'liftM2').

  liftM4  :: (Monad m) => (a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
  liftM4 f m1 m2 m3 m4    = do { x1 <- m1; x2 <- m2; x3 <- m3; x4 <- m4; return (f x1 x2 x3 x4) }

  -- -| Promote a function to a monad, scanning the monadic arguments from

  -- left to right (cf. 'liftM2').

  liftM5  :: (Monad m) => (a1 -> a2 -> a3 -> a4 -> a5 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m a5 -> m r
  liftM5 f m1 m2 m3 m4 m5 = do { x1 <- m1; x2 <- m2; x3 <- m3; x4 <- m4; x5 <- m5; return (f x1 x2 x3 x4 x5) }

  {- -| In many situations, the 'liftM' operations can be replaced by uses of
  'ap', which promotes function application.

  > return f `ap` x1 `ap` ... `ap` xn

  is equivalent to

  > liftMn f x1 x2 ... xn

  -}

  ap                :: (Monad m) => m (a -> b) -> m a -> m b
  ap m1 m2          = do { x1 <- m1; x2 <- m2; return (x1 x2) }
  -- Since many Applicative instances define (<*>) = ap, we

  -- cannot define ap = (<*>)


  -- -----------------------------------------------------------------------------

  -- The Alternative class definition


  infixl 3 <|>

  -- -| A monoid on applicative functors.

  --

  -- If defined, 'some' and 'many' should be the least solutions

  -- of the equations:

  --

  -- -* @'some' v = (:) '<$>' v '<*>' 'many' v@

  --

  -- -* @'many' v = 'some' v '<|>' 'pure' []@

  class Applicative f => Alternative f where
      -- -| The identity of '<|>'

      empty :: f a
      -- -| An associative binary operation

      (<|>) :: f a -> f a -> f a

      {-
      some and many rely on infinite lists

      -- -| One or more.
      some :: f a -> f [a]
      some v = some_v
        where
          many_v = some_v <|> pure []
          some_v = liftA2 (:) v many_v

      -- -| Zero or more.
      many :: f a -> f [a]
      many v = many_v
        where
          many_v = some_v <|> pure []
          some_v = liftA2 (:) v many_v
      -}

  -- -| @'guard' b@ is @'pure' ()@ if @b@ is 'True',

  -- and 'empty' if @b@ is 'False'.

  guard           :: (Alternative f) => Bool -> f ()
  guard True      =  pure ()
  guard False     =  empty

  -- -----------------------------------------------------------------------------

  -- The MonadPlus class definition


  -- -| Monads that also support choice and failure.

  class (Alternative m, Monad m) => MonadPlus m where
     -- -| The identity of 'mplus'.  It should also satisfy the equations

     --

     -- > mzero >>= f  =  mzero

     -- > v >> mzero   =  mzero

     --

     -- The default definition is

     --

     -- @

     -- mzero = 'empty'

     -- @

     mzero :: m a
     mzero = empty

     -- -| An associative operation. The default definition is

     --

     -- @

     -- mplus = ('<|>')

     -- @

     mplus :: m a -> m a -> m a
     mplus = (<|>)
  |])

$(singletonsOnly [d|
  -------------------------------------------------------------------------------

  -- Instances


  deriving instance Functor Maybe
  deriving instance Functor NonEmpty
  deriving instance Functor []
  deriving instance Functor (Either a)

  instance Applicative Maybe where
      pure = Just

      Just f  <*> m       = fmap f m
      Nothing <*> _m      = Nothing

      liftA2 f (Just x) (Just y) = Just (f x y)
      liftA2 _ Just{}   Nothing  = Nothing
      liftA2 _ Nothing  Just{}   = Nothing
      liftA2 _ Nothing  Nothing  = Nothing

      Just _m1 *> m2      = m2
      Nothing  *> _m2     = Nothing

  instance Applicative NonEmpty where
    pure a = a :| []
    (<*>) = ap
    liftA2 = liftM2

  instance Applicative [] where
      pure x = [x]
      (<*>)  = ap
      liftA2 = liftM2
      m *> k = m >>= \_ -> k

  instance Applicative (Either e) where
      pure          = Right
      Left  e <*> _ = Left e
      Right f <*> r = fmap f r

  instance  Monad Maybe  where
      (Just x) >>= k      = k x
      Nothing  >>= _      = Nothing

      (>>) = (*>)

  instance Monad NonEmpty where
    (a :| as) >>= f = b :| (bs ++ bs')
      where b :| bs = f a
            bs' = as >>= toList . f
            toList (c :| cs) = c : cs

  instance Monad []  where
      xs >>= f = foldr ((++) . f) [] xs

  instance Monad (Either e) where
      Left  l >>= _ = Left l
      Right r >>= k = k r

  instance Alternative Maybe where
      empty = Nothing
      Nothing    <|> r = r
      l@(Just{}) <|> _ = l

  instance Alternative [] where
      empty = []
      (<|>) = (++)

  instance MonadPlus Maybe
  instance MonadPlus []
  |])