{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Singletons.Prelude.Monad.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 Data.Singletons.Prelude.Monad.Internal where

import Control.Applicative
import Control.Monad
import Data.List.NonEmpty (NonEmpty(..))
import Data.Singletons.Prelude.Base
import Data.Singletons.Prelude.Instances
import Data.Singletons.Single

$(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
      (*>)   = (>>)

  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 []
  |])