on master help sign in
Merge pull request #2959 from ziman/monad-flatten
3963984Edwin Brady
libs/prelude/Prelude/Monad.idr+11−3
@@ -13,17 +13,25 @@ import IO
13infixl 5 >>=
13infixl 5 >>=
14
14
15interface Applicative m => Monad (m : Type -> Type) where
15interface Applicative m => Monad (m : Type -> Type) where
16+ ||| Also called `bind`.
16 (>>=) : m a -> ((result : a) -> m b) -> m b
17 (>>=) : m a -> ((result : a) -> m b) -> m b
17
18
18−||| Also called `join` or mu
19+ ||| Also called `flatten` or mu
19−flatten : Monad m => m (m a) -> m a
20+ join : m (m a) -> m a
20−flatten a = a >>= id
21+
22+ -- default implementations
23+ (>>=) x f = join (f <$> x)
24+ join x = x >>= id
21
25
22||| For compatibility with Haskell. Note that monads are **not** free to
26||| For compatibility with Haskell. Note that monads are **not** free to
23||| define `return` and `pure` differently!
27||| define `return` and `pure` differently!
24return : Monad m => a -> m a
28return : Monad m => a -> m a
25return = pure
29return = pure
26
30
31+flatten : Monad m => m (m a) -> m a
32+flatten = join
33+%deprecate flatten "Please use `join`, which is the standard name."
34+
27-- Annoyingly, these need to be here, so that we can use them in other
35-- Annoyingly, these need to be here, so that we can use them in other
28-- Prelude modules other than the top level.
36-- Prelude modules other than the top level.
29
37
libs/prelude/Prelude/Providers.idr+1
@@ -1,5 +1,6 @@
1module Prelude.Providers
1module Prelude.Providers
2
2
3+import Prelude.Basics
3import Prelude.Functor
4import Prelude.Functor
4import Prelude.Applicative
5import Prelude.Applicative
5import Prelude.Monad
6import Prelude.Monad