------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of List⁺
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.List.NonEmpty.Effectful where
 
open import Agda.Builtin.List
import Data.List.Effectful as List
open import Data.List.NonEmpty.Base
open import Data.Product.Base using (uncurry)
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Effect.Comonad
open import Function.Base using (flip; _∘′_; _∘_)
 
------------------------------------------------------------------------
-- List⁺ applicative functor
 
functor : ∀ {f} → RawFunctor {f} List⁺
functor = record
  { _<$>_ = map
  }
 
applicative : ∀ {f} → RawApplicative {f} List⁺
applicative = record
  { rawFunctor = functor
  ; pure = [_]
  ; _<*>_  = ap
  }
 
------------------------------------------------------------------------
-- List⁺ monad
 
monad : ∀ {f} → RawMonad {f} List⁺
monad = record
  { rawApplicative = applicative
  ; _>>=_  = flip concatMap
  }
 
------------------------------------------------------------------------
-- List⁺ comonad
 
comonad : ∀ {f} → RawComonad {f} List⁺
comonad = record
  { extract = head
  ; extend  = λ f → uncurry (extend f) ∘′ uncons
  } where
 
  extend : ∀ {A B} → (List⁺ A → B) → A → List A → List⁺ B
  extend f x xs@[]       = f (x ∷ xs) ∷ []
  extend f x xs@(y ∷ ys) = f (x ∷ xs) ∷⁺ extend f y ys
 
 
------------------------------------------------------------------------
-- Get access to other monadic functions
 
module TraversableA {f g F} (App : RawApplicative {f} {g} F) where
 
  open RawApplicative App
 
  sequenceA : ∀ {A} → List⁺ (F A) → F (List⁺ A)
  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ List.TraversableA.sequenceA App xs
 
  mapA : ∀ {a} {A : Set a} {B} → (A → F B) → List⁺ A → F (List⁺ B)
  mapA f = sequenceA ∘ map f
 
  forA : ∀ {a} {A : Set a} {B} → List⁺ A → (A → F B) → F (List⁺ B)
  forA = flip mapA
 
module TraversableM {m n M} (Mon : RawMonad {m} {n} M) where
 
  open RawMonad Mon
 
  open TraversableA rawApplicative public
    renaming
    ( sequenceA to sequenceM
    ; mapA      to mapM
    ; forA      to forM
    )