------------------------------------------------------------------------
-- 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
    }