------------------------------------------------------------------------
-- The Agda standard library
--
-- Typeclass instances for TC
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.TCM.Effectful where
open import Effect.Choice
open import Effect.Empty
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Data.List.Base using ([])
open import Function.Base using (_∘_)
open import Level
open import Reflection.TCM
private
variable
ℓ : Level
functor : RawFunctor {ℓ} TC
functor = record
{ _<$>_ = λ f mx → bindTC mx (pure ∘ f)
}
applicative : RawApplicative {ℓ} TC
applicative = record
{ rawFunctor = functor
; pure = pure
; _<*>_ = λ mf mx → bindTC mf λ f → bindTC mx (pure ∘ f)
}
empty : RawEmpty {ℓ} TC
empty = record { empty = typeError [] }
applicativeZero : RawApplicativeZero {ℓ} TC
applicativeZero = record
{ rawApplicative = applicative
; rawEmpty = empty
}
choice : RawChoice {ℓ} TC
choice = record { _<|>_ = catchTC }
alternative : RawAlternative {ℓ} TC
alternative = record
{ rawApplicativeZero = applicativeZero
; rawChoice = choice
}
monad : RawMonad {ℓ} TC
monad = record
{ rawApplicative = applicative
; _>>=_ = bindTC
}
monadZero : RawMonadZero {ℓ} TC
monadZero = record
{ rawMonad = monad
; rawEmpty = empty
}
monadPlus : RawMonadPlus {ℓ} TC
monadPlus = record
{ rawMonadZero = monadZero
; 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