------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of List⁺
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.NonEmpty.Effectful where
open import Data.List.Base using (List; []; _∷_)
import Data.List.Effectful as List
open import Data.List.NonEmpty.Base
open import Data.Product.Base using (uncurry)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad)
open import Effect.Comonad using (RawComonad)
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
)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4