------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of Vec
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Vec.Effectful.Transformer where
open import Data.Nat.Base using (ℕ)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; RawMonadT)
open import Function.Base using (_∘′_; _$_ )
open import Level using (Level)
import Data.Vec.Effectful as Vec
private
variable
f g : Level
n : ℕ
M : Set f → Set g
------------------------------------------------------------------------
-- Vec monad transformer
record VecT (n : ℕ) (M : Set f → Set g) (A : Set f) : Set g where
constructor mkVecT
field runVecT : M (Vec A n)
open VecT public
functor : RawFunctor M → RawFunctor {f} (VecT n M)
functor M = record
{ _<$>_ = λ f → mkVecT ∘′ (Vec.map f <$>_) ∘′ runVecT
} where open RawFunctor M
applicative : RawApplicative M → RawApplicative {f} (VecT n M)
applicative M = record
{ rawFunctor = functor rawFunctor
; pure = mkVecT ∘′ pure ∘′ Vec.replicate _
; _<*>_ = λ mf ma → mkVecT (Vec.zipWith _$_ <$> runVecT mf <*> runVecT ma)
} where open RawApplicative M
monad : {M : Set f → Set g} → RawMonad M → RawMonad (VecT n M)
monad {f} {g} M = record
{ rawApplicative = applicative rawApplicative
; _>>=_ = λ ma k → mkVecT $ do
a ← runVecT ma
bs ← mapM {a = f} (runVecT ∘′ k) a
pure (Vec.diagonal bs)
} where open RawMonad M; open Vec.TraversableM {m = f} {n = g} M
monadT : RawMonadT {f} {g} (VecT n)
monadT M = record
{ lift = mkVecT ∘′ (Vec.replicate _ <$>_)
; rawMonad = monad M
} where open RawMonad M
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