{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# 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.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.Singletons.Prelude.Base
import Data.Singletons.Prelude.Instances
import Data.Singletons.Single

{-
Note [How to get the right kinds when promoting Functor and friends]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To avoid running afoul of a CUSK validity check (see Note [CUSKification]),
classes with type parameters that lack explicit kind signatures will be
defaulted to be of kind Type. This is not what you want for Functor, however,
since its argument is of kind (Type -> Type), so we must explicitly use this
kind when declaring the Functor class (and other classes in this module).
-}

$(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 :: Type -> Type)  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 :: Type -> Type) 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 :: Type -> Type) 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 :: Type -> Type) 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 :: Type -> Type) 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 = (<|>)
  |])

-- Workaround for #326
infixl 4 <$
infixl 4 <*>, <*, *>, <**>
infixl 1 >>, >>=
infixr 1 =<<
infixl 3 <|>

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