------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of Vec
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Effectful where
open import Data.Nat.Base using (ℕ)
open import Data.Fin.Base using (Fin)
open import Data.Vec.Base as Vec hiding (_⊛_)
open import Data.Vec.Properties
open import Effect.Applicative as App using (RawApplicative)
open import Effect.Functor as Fun using (RawFunctor)
open import Effect.Monad using (RawMonad; module Join; RawMonadT; mkRawMonad)
import Function.Identity.Effectful as Id
open import Function.Base using (flip; _∘_)
open import Level using (Level)
private
variable
a : Level
A : Set a
n : ℕ
------------------------------------------------------------------------
-- Functor and applicative
functor : RawFunctor (λ (A : Set a) → Vec A n)
functor = record
{ _<$>_ = map
}
applicative : RawApplicative (λ (A : Set a) → Vec A n)
applicative {n = n} = record
{ rawFunctor = functor
; pure = replicate n
; _<*>_ = Vec._⊛_
}
monad : RawMonad (λ (A : Set a) → Vec A n)
monad = record
{ rawApplicative = applicative
; _>>=_ = DiagonalBind._>>=_
}
join : Vec (Vec A n) n → Vec A n
join = Join.join monad
------------------------------------------------------------------------
-- Get access to other monadic functions
module TraversableA {f g F} (App : RawApplicative {f} {g} F) where
open RawApplicative App
sequenceA : ∀ {A n} → Vec (F A) n → F (Vec A n)
sequenceA [] = pure []
sequenceA (x ∷ xs) = _∷_ <$> x ⊛ sequenceA xs
mapA : ∀ {a} {A : Set a} {B n} → (A → F B) → Vec A n → F (Vec B n)
mapA f = sequenceA ∘ map f
forA : ∀ {a} {A : Set a} {B n} → Vec A n → (A → F B) → F (Vec B n)
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
)
------------------------------------------------------------------------
-- Other
-- lookup is a functor morphism from Vec to Identity.
lookup-functor-morphism : (i : Fin n) → Fun.Morphism (functor {a}) Id.functor
lookup-functor-morphism i = record
{ op = flip lookup i
; op-<$> = lookup-map i
}
-- lookup is an applicative functor morphism.
lookup-morphism : (i : Fin n) → App.Morphism (applicative {a}) Id.applicative
lookup-morphism i = record
{ functorMorphism = lookup-functor-morphism i
; op-pure = lookup-replicate i
; op-<*> = lookup-⊛ i
}
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