------------------------------------------------------------------------
-- The Agda standard library
--
-- An effectful view of Delay
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --sized-types #-}
module Codata.Sized.Delay.Effectful where
open import Codata.Sized.Delay
using (Delay; now; never; later; map; bind; zipWith; alignWith)
open import Function.Base using (id)
open import Effect.Choice using (RawChoice)
open import Effect.Empty using (RawEmpty)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative
using (RawApplicative; RawApplicativeZero; RawAlternative)
open import Effect.Monad using (RawMonad; RawMonadZero)
open import Data.These using (leftMost)
functor : ∀ {i ℓ} → RawFunctor {ℓ} (λ A → Delay A i)
functor = record { _<$>_ = λ f → map f }
module Sequential where
applicative : ∀ {i ℓ} → RawApplicative {ℓ} (λ A → Delay A i)
applicative = record
{ rawFunctor = functor
; pure = now
; _<*>_ = λ df da → bind df (λ f → map f da)
}
empty : ∀ {i ℓ} → RawEmpty {ℓ} (λ A → Delay A i)
empty = record { empty = never }
applicativeZero : ∀ {i ℓ} → RawApplicativeZero {ℓ} (λ A → Delay A i)
applicativeZero = record
{ rawApplicative = applicative
; rawEmpty = empty
}
monad : ∀ {i ℓ} → RawMonad {ℓ} (λ A → Delay A i)
monad = record
{ rawApplicative = applicative
; _>>=_ = bind
}
monadZero : ∀ {i ℓ} → RawMonadZero {ℓ} (λ A → Delay A i)
monadZero = record
{ rawMonad = monad
; rawEmpty = empty
}
module Zippy where
applicative : ∀ {i ℓ} → RawApplicative {ℓ} (λ A → Delay A i)
applicative = record
{ rawFunctor = functor
; pure = now
; _<*>_ = zipWith id
}
empty : ∀ {i ℓ} → RawEmpty {ℓ} (λ A → Delay A i)
empty = record { empty = never }
applicativeZero : ∀ {i ℓ} → RawApplicativeZero {ℓ} (λ A → Delay A i)
applicativeZero = record
{ rawApplicative = applicative
; rawEmpty = empty
}
choice : ∀ {i ℓ} → RawChoice {ℓ} (λ A → Delay A i)
choice = record { _<|>_ = alignWith leftMost }
alternative : ∀ {i ℓ} → RawAlternative {ℓ} (λ A → Delay A i)
alternative = record
{ rawApplicativeZero = applicativeZero
; rawChoice = choice
}
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