------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of the identity function
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Effect.Monad.Identity where
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad; module Join)
open import Effect.Comonad using (RawComonad)
open import Function.Base using (id; _∘′_; _|>′_; _$′_; flip)
open import Level using (Level)
private
variable
a : Level
A : Set a
record Identity (A : Set a) : Set a where
constructor mkIdentity
field runIdentity : A
open Identity public
functor : RawFunctor {a} Identity
functor = record
{ _<$>_ = λ f a → mkIdentity (f (runIdentity a))
}
applicative : RawApplicative {a} Identity
applicative = record
{ rawFunctor = functor
; pure = mkIdentity
; _<*>_ = λ f a → mkIdentity (runIdentity f $′ runIdentity a)
}
monad : RawMonad {a} Identity
monad = record
{ rawApplicative = applicative
; _>>=_ = _|>′_ ∘′ runIdentity
}
comonad : RawComonad {a} Identity
comonad = record
{ extract = runIdentity
; extend = λ f a → mkIdentity (f a)
}
join : Identity (Identity A) → Identity A
join = Join.join monad
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