{-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# 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 import Data.Singletons.TypeLits.Internal {- 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 -- -| Fail with a message. This operation is not part of the -- mathematical definition of a monad, but is invoked on pattern-match -- failure in a @do@ expression. -- -- As part of the MonadFail proposal (MFP), this function is moved -- to its own class 'MonadFail' (see "Control.Monad.Fail" for more -- details). The definition here will be removed in a future -- release. fail :: Symbol -> m a fail s = error s {- 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 (>>) = (*>) fail _ = 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 fail _ = [] 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 [] |])