
   0 | module Control.Monad.List
   1 | 
   2 | import Control.HigherOrder
   3 | 
   4 | import Control.Monad.Trans
   5 | 
   6 | 
   7 | public export
   8 | data ListM : (Type -> Type) -> (Type -> Type) where
   9 |   Nil : ListM m a
  10 |   (::) : a -> m (ListM m a) -> ListM m a
  11 | 
  12 | public export
  13 | 0
  14 | ListT : (Type -> Type) -> (Type -> Type)
  15 | ListT m a = m (ListM m a)
  16 | 
  17 | namespace Semigroup
  18 | 
  19 |   export
  20 |   [ListT] Monad m => Semigroup (ListT m a) where
  21 |     xs <+> ys =
  22 |       case !xs of
  23 |         [] => ys -- No idea it can't find the instance automatically.
  24 |         (x :: xs) => pure $ x :: ((<+>) @{ListT} xs ys)
  25 | 
  26 |   export
  27 |   [ListM] Monad m => Semigroup (ListM m a) where
  28 |     [] <+> ys = ys
  29 |     (x :: xs) <+> ys = x :: (<+>) @{ListT} xs (pure ys)
  30 | 
  31 |   %hint export
  32 |   ListTSemigroup : Monad m => Semigroup (ListT m a)
  33 |   ListTSemigroup = Semigroup.ListT
  34 | 
  35 | namespace Monoid
  36 |   %hint
  37 |   export
  38 |   ListT : Monad m => Monoid (ListT m a)
  39 |   ListT = MkMonoid @{Semigroup.ListT} (pure [])
  40 | 
  41 |   %hint
  42 |   export
  43 |   ListM : Monad m => Monoid (ListM m a)
  44 |   ListM = MkMonoid @{Semigroup.ListM} []
  45 | 
  46 | namespace Functor
  47 |   mutual
  48 |     export
  49 |     [ListM] Functor m => Functor (ListM m) where
  50 |       map f [] = []
  51 |       map f (x :: xs) = f x :: map @{ListT} f xs
  52 | 
  53 |     export
  54 |     [ListT] Functor m => Functor (ListT m) where
  55 |       map f x = map (map @{ListM} f) x
  56 | 
  57 | namespace Applicative
  58 |   %hint export
  59 |   ListT : Monad m => Applicative (ListT m)
  60 |   ListT = MkApplicative @{Functor.ListT}
  61 |     (pure . (:: pure Nil))
  62 |     $
  63 |     \fs, ys =>
  64 |       case !fs of
  65 |         [] => pure []
  66 |         f :: fs => (<+>) @{Semigroup.ListT}
  67 |           (map @{Functor.ListT} f ys)
  68 |           ((<*>) @{Applicative.ListT} fs ys)
  69 | 
  70 | namespace Monad
  71 | 
  72 |   bind : Monad m => ListT m a -> (a -> ListT m b) -> ListT m b
  73 |   bind xs f = do
  74 |     case !xs of
  75 |       [] => pure []
  76 |       x :: xs => (<+>) @{ListT} (f x) (bind xs f)
  77 | 
  78 |   %hint export
  79 |   ListT : Monad m => Monad (ListT m)
  80 |   ListT = MkMonad @{Applicative.ListT}
  81 |     (bind {m})
  82 |     (flip (bind {m}) id)
  83 | 
  84 | namespace Alternative
  85 |   %hint public export
  86 |   ListT : Monad m => Alternative (ListT m)
  87 |   ListT = MkAlternative @{Applicative.ListT} (pure []) (\x, y => (<+>) @{ListT} x y)
  88 | 
  89 | export
  90 | MonadTrans ListT where
  91 |   lift = (>>= pure @{ListT})
  92 | 
  93 | export
  94 | runListT' : Monad m => ListT m a -> m (Maybe a)
  95 | runListT' x = do
  96 |   case !x of
  97 |     [] => pure Nothing
  98 |     x :: xs => pure (Just x)
  99 | 
 100 | export
 101 | runListT : Monad m => ListT m a -> m (List a)
 102 | runListT x = do
 103 |   case !x of
 104 |     [] => pure []
 105 |     x :: xs => map (x ::) (runListT xs)
 106 | 
 107 | export
 108 | liftList : Applicative m => List a -> ListT m a
 109 | liftList [] = pure []
 110 | liftList (x :: xs) = pure (x :: liftList xs)
 111 |