------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of vectors defined by recursion
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Recursive.Effectful where
open import Agda.Builtin.Nat using (suc; zero)
open import Data.Product.Base hiding (map)
open import Data.Vec.Recursive
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Function.Base using (_∘_; flip)
------------------------------------------------------------------------
-- Functor and applicative
functor : ∀ {ℓ} n → RawFunctor {ℓ} (_^ n)
functor n = record { _<$>_ = λ f → map f n }
applicative : ∀ {ℓ} n → RawApplicative {ℓ} (_^ n)
applicative n = record
{ rawFunctor = functor n
; pure = replicate n
; _<*>_ = ap n
}
------------------------------------------------------------------------
-- Get access to other monadic functions
module _ {f g F} (App : RawApplicative {f} {g} F) where
open RawApplicative App
sequenceA : ∀ {n A} → F A ^ n → F (A ^ n)
sequenceA {0} _ = pure _
sequenceA {1} fa = fa
sequenceA {suc (suc _)} (fa , fas) = _,_ <$> fa ⊛ sequenceA fas
mapA : ∀ {n a} {A : Set a} {B} → (A → F B) → A ^ n → F (B ^ n)
mapA f = sequenceA ∘ map f _
forA : ∀ {n a} {A : Set a} {B} → A ^ n → (A → F B) → F (B ^ n)
forA = flip mapA
module _ {m n M} (Mon : RawMonad {m} {n} M) where
private App = RawMonad.rawApplicative Mon
sequenceM : ∀ {n A} → M A ^ n → M (A ^ n)
sequenceM = sequenceA App
mapM : ∀ {n a} {A : Set a} {B} → (A → M B) → A ^ n → M (B ^ n)
mapM = mapA App
forM : ∀ {n a} {A : Set a} {B} → A ^ n → (A → M B) → M (B ^ n)
forM = forA App
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