@@ -13,17 +13,25 @@ import IO
1313infixl 5 >>=
1414
1515interface Applicative m => Monad (m : Type -> Type) where
16+ ||| Also called `bind`.
1617 (>>=) : m a -> ((result : a) -> m b) -> m b
1718
18−||| Also called `join` or mu
19−flatten : Monad m => m (m a) -> m a
20−flatten a = a >>= id
19+ ||| Also called `flatten` or mu
20+ join : m (m a) -> m a
21+
22+ -- default implementations
23+ (>>=) x f = join (f <$> x)
24+ join x = x >>= id
2125
2226||| For compatibility with Haskell. Note that monads are **not** free to
2327||| define `return` and `pure` differently!
2428return : Monad m => a -> m a
2529return = pure
2630
31+flatten : Monad m => m (m a) -> m a
32+flatten = join
33+%deprecate flatten "Please use `join`, which is the standard name."
34+
2735-- Annoyingly, these need to be here, so that we can use them in other
2836-- Prelude modules other than the top level.
2937