on master help sign in
Add flatten to Monad.
3851f59Matus Tejiscak
libs/prelude/Prelude/Monad.idr+7−3
@@ -13,11 +13,15 @@ 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 `join` or mu
19−flatten : Monad m => m (m a) -> m a
20+ flatten : m (m a) -> m a
21+
22+ -- default implementations
20−flatten a = a >>= id
23+ (>>=) x f = flatten (f <$> x)
24+ flatten x = x >>= (\y => y)
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!