A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://agda.github.io/agda-stdlib/master/Effect.Monad.Continuation.html below:

Effect.Monad.Continuation

Effect.Monad.Continuation
------------------------------------------------------------------------
-- The Agda standard library
--
-- A delimited continuation monad
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Effect.Monad.Continuation where

open import Effect.Applicative.Indexed using (IFun)
open import Effect.Monad using (RawMonad)
open import Function.Identity.Effectful as Id using (Identity)
open import Effect.Monad.Indexed using (RawIMonad)
open import Function.Base using (flip)
open import Level using (Level; _⊔_; suc)

private
  variable
    i f : Level
    I : Set i

------------------------------------------------------------------------
-- Delimited continuation monads

DContT : (I  Set f)  (Set f  Set f)  IFun I f
DContT K M r₂ r₁ a = (a  M (K r₁))  M (K r₂)

DCont : (I  Set f)  IFun I f
DCont K = DContT K Identity

DContTIMonad :  (K : I  Set f) {M}  RawMonad M  RawIMonad (DContT K M)
DContTIMonad K Mon = record
  { return = λ a k  k a
  ; _>>=_  = λ c f k  c (flip f k)
  }
  where open RawMonad Mon

DContIMonad : (K : I  Set f)  RawIMonad (DCont K)
DContIMonad K = DContTIMonad K Id.monad

------------------------------------------------------------------------
-- Delimited continuation operations

record RawIMonadDCont {I : Set i} (K : I  Set f)
                      (M : IFun I f) : Set (i  suc f) where
  field
    monad : RawIMonad M
    reset :  {r₁ r₂ r₃}  M r₁ r₂ (K r₂)  M r₃ r₃ (K r₁)
    shift :  {a r₁ r₂ r₃ r₄} 
            ((a  M r₁ r₁ (K r₂))  M r₃ r₄ (K r₄))  M r₃ r₂ a

  open RawIMonad monad public

DContTIMonadDCont :  (K : I  Set f) {M} 
                    RawMonad M  RawIMonadDCont K (DContT K M)
DContTIMonadDCont K Mon = record
  { monad = DContTIMonad K Mon
  ; reset = λ e k  e pure >>= k
  ; shift = λ e k  e  a k′  (k a) >>= k′) pure
  }
  where
  open RawMonad Mon

DContIMonadDCont : (K : I  Set f)  RawIMonadDCont K (DCont K)
DContIMonadDCont K = DContTIMonadDCont K Id.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